:: Free Magmas
:: by Marco Riccardi
::
:: Received October 20, 2009
:: Copyright (c) 2009-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, FUNCT_1, ORDINAL1, RELAT_1, XBOOLE_0, TARSKI, AFINSQ_1,
SUBSET_1, YELLOW_6, ZFMISC_1, CLASSES1, PARTFUN1, ALGSTR_0, BINOP_1,
EQREL_1, MSUALG_6, STRUCT_0, GROUP_6, MSSUBFAM, FUNCT_2, SETFAM_1,
REALSET1, CIRCUIT2, CARD_1, XXREAL_0, FINSEQ_1, ARYTM_1, CARD_3, ARYTM_3,
NAT_1, XCMPLX_0, MCART_1, NAT_LAT, ALGSTR_4, REWRITE1, GROUP_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, CARD_1, XCMPLX_0,
XFAMILY, RELAT_1, FUNCT_1, ORDINAL1, NUMBERS, SETFAM_1, FUNCT_6, FUNCT_2,
XXREAL_0, NAT_1, CLASSES1, FINSEQ_1, CARD_3, AFINSQ_1, NAT_D, YELLOW_6,
BINOP_1, STRUCT_0, ALGSTR_0, RELSET_1, GROUP_1, GROUP_6, MCART_1,
NAT_LAT, PARTFUN1, REALSET1, EQREL_1, ALG_1, GROUP_2, REWRITE1;
constructors NAT_1, CLASSES1, AFINSQ_1, NAT_D, YELLOW_6, BINOP_1, RELSET_1,
FACIRC_1, GROUP_6, NAT_LAT, REALSET1, EQREL_1, XTUPLE_0, XFAMILY,
REWRITE1;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FINSET_1,
XXREAL_0, XREAL_0, NAT_1, CARD_1, FUNCT_2, INT_1, STRUCT_0, RELSET_1,
NAT_LAT, REALSET1, EQREL_1, GROUP_1, GROUP_2, XTUPLE_0, ALGSTR_0,
ZFMISC_1, PARTFUN1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI;
equalities TARSKI, ALGSTR_0, ORDINAL1;
expansions TARSKI;
theorems TARSKI, XBOOLE_1, ORDINAL1, RELAT_1, FUNCT_1, FUNCT_2, AFINSQ_1,
FINSEQ_1, XREAL_1, NAT_1, XXREAL_0, XREAL_0, ZFMISC_1, CLASSES1, CARD_3,
YELLOW_6, BINOP_1, RELSET_1, MCART_1, INT_1, SUBSET_1, XBOOLE_0, NAT_LAT,
FUNCT_5, GROUP_6, PARTFUN1, REALSET1, SETFAM_1, EQREL_1, OSALG_4,
GROUP_1, GROUP_2, FUNCT_6, XTUPLE_0;
schemes ORDINAL1, NAT_1, CLASSES1, FINSEQ_1, BINOP_1, FUNCT_2, EQREL_1,
RELAT_1, XFAMILY;
begin :: Preliminaries
registration
let X be set;
let f be sequence of X;
let n be Nat;
cluster f|n -> Sequence-like;
correctness
proof
per cases;
suppose A1: X <> {};
n c= NAT; then
n c= dom f by A1,FUNCT_2:def 1; then
dom(f|n) is ordinal by RELAT_1:62;
hence thesis by ORDINAL1:def 7;
end;
suppose X = {}; then
f = {};
hence thesis;
end;
end;
end;
definition
let X,x be set;
func IFXFinSequence(x,X) -> XFinSequence of X equals :Def1:
x if x is XFinSequence of X
otherwise <%>X;
correctness;
end;
definition
let X be non empty set;
let f be Function of X^omega, X;
let c be XFinSequence of X;
redefine func f.c -> Element of X; :: redefines . (FUNCT_1, definition)
correctness
proof
c in X^omega by AFINSQ_1:def 7;
hence thesis by FUNCT_2:5;
end;
end;
theorem Th1:
for X,Y,Z being set st Y c= the_universe_of X & Z c= the_universe_of X
holds [:Y,Z:] c= the_universe_of X
proof
let X,Y,Z be set;
assume Y c= the_universe_of X; then
A1: Y c= Tarski-Class the_transitive-closure_of X by YELLOW_6:def 1;
assume Z c= the_universe_of X; then
Z c= Tarski-Class the_transitive-closure_of X by YELLOW_6:def 1;
then
[:Y,Z:] c= Tarski-Class the_transitive-closure_of X by A1,CLASSES1:28;
hence [:Y,Z:] c= the_universe_of X by YELLOW_6:def 1;
end;
scheme FuncRecursiveUniq { F(set) -> set, F1,F2() -> Function }:
F1() = F2()
provided
A1: dom F1() = NAT & for n being Nat holds F1().n = F(F1()|n) and
A2: dom F2() = NAT & for n being Nat holds F2().n = F(F2()|n)
proof
reconsider L1=F1() as Sequence by A1,ORDINAL1:def 7;
reconsider L2=F2() as Sequence by A2,ORDINAL1:def 7;
A3: dom L1 = NAT &
for B being Ordinal,T1 being Sequence st B in NAT & T1 = L1|B
holds L1.B = F(T1) by A1;
A4: dom L2 = NAT &
for B being Ordinal,T2 being Sequence st B in NAT & T2 = L2|B
holds L2.B = F(T2) by A2;
L1 = L2 from ORDINAL1:sch 3(A3,A4);
hence thesis;
end;
scheme FuncRecursiveExist { F(set) -> set }:
ex f being Function st dom f = NAT &
for n being Nat holds f.n = F(f|n)
proof
consider L being Sequence such that
A1: dom L = NAT and
A2: for B being Ordinal,L1 being Sequence st B in NAT & L1 = L|B
holds L.B = F(L1) from ORDINAL1:sch 4;
take L;
thus dom L = NAT by A1;
let n be Nat;
reconsider B=n as Ordinal;
B in NAT by ORDINAL1:def 12; then
L.B = F(L|B) by A2;
hence thesis;
end;
scheme FuncRecursiveUniqu2
{ X() -> non empty set, F(XFinSequence of X()) -> Element of X(),
F1,F2() -> sequence of X()}:
F1() = F2()
provided
A1: for n being Nat holds F1().n = F(F1()|n) and
A2: for n being Nat holds F2().n = F(F2()|n)
proof
deffunc FX(set) = F(IFXFinSequence($1,X()));
reconsider f1=F1() as Function;
reconsider f2=F2() as Function;
A3: dom f1 = NAT & for n being Nat holds f1.n = FX(f1|n)
proof
thus dom f1 = NAT by FUNCT_2:def 1;
let n be Nat;
thus f1.n = F(F1()|n) by A1 .= FX(f1|n) by Def1;
end;
A4: dom f2 = NAT & for n being Nat holds f2.n = FX(f2|n)
proof
thus dom f2 = NAT by FUNCT_2:def 1;
let n be Nat;
thus f2.n = F(F2()|n) by A2 .= FX(f2|n) by Def1;
end;
f1 = f2 from FuncRecursiveUniq(A3,A4);
hence thesis;
end;
scheme FuncRecursiveExist2
{ X() -> non empty set, F(XFinSequence of X()) -> Element of X() }:
ex f being sequence of X() st
for n being Nat holds f.n = F(f|n)
proof
deffunc FX(set) = F(IFXFinSequence($1,X()));
consider f be Function such that
A1: dom f = NAT and
A2: for n being Nat holds f.n = FX(f|n) from FuncRecursiveExist;
for y being object st y in rng f holds y in X()
proof
let y be object;
assume y in rng f; then
consider x be object such that
A3: x in dom f & y = f.x by FUNCT_1:def 3;
reconsider x as Nat by A1,A3;
y = F(IFXFinSequence(f|x,X())) by A3,A2;
hence y in X();
end; then
rng f c= X(); then
reconsider f9=f as sequence of X() by A1,FUNCT_2:2;
take f9;
let n be Nat;
f.n = F(IFXFinSequence(f9|n,X())) by A2
.= F(f9|n) by Def1;
hence thesis;
end;
definition
let f,g be Function;
pred f extends g means
dom g c= dom f & f tolerates g;
end;
registration
cluster empty for multMagma;
existence
proof
take multMagma(# {}, the BinOp of {} #);
thus thesis;
end;
end;
begin :: Equivalence Relations and Relators
:: Ch I ?1.6 Def.11 Algebra I Bourbaki
definition
let M be multMagma;
let R be Equivalence_Relation of M;
attr R is compatible means :Def3:
for v,v9,w,w9 being Element of M st v in Class(R,v9) & w in Class(R,w9)
holds v*w in Class(R,v9*w9);
end;
registration
let M be multMagma;
cluster nabla the carrier of M -> compatible;
correctness
proof
set R = nabla the carrier of M;
let v,v9,w,w9 be Element of M;
assume v in Class(R,v9) & w in Class(R,w9);
then
A1: M is non empty;
then Class(R,v9*w9) = the carrier of M by EQREL_1:26;
hence thesis by A1,SUBSET_1:def 1;
end;
end;
registration
let M be multMagma;
cluster compatible for Equivalence_Relation of M;
correctness
proof
take nabla the carrier of M;
thus thesis;
end;
end;
:: added by SK, 25.04.2025
registration
let M be non empty trivial multMagma;
cluster -> compatible for Equivalence_Relation of M;
coherence
proof
let R be Equivalence_Relation of M;
consider x being object such that
A1: the carrier of M = {x} by ZFMISC_1:131;
reconsider x as Element of M by A1, TARSKI:def 1;
now
let v,v9,w,w9 be Element of M;
assume v in Class(R,v9) & w in Class(R,w9);
A2: v*w = x & v9*w9 = x by A1, TARSKI:def 1;
v9*w9 in Class(R,v9*w9) by EQREL_1:20;
hence v*w in Class(R,v9*w9) by A2;
end;
hence thesis;
end;
end;
theorem Th2:
for M being multMagma, R being Equivalence_Relation of M holds
R is compatible iff for v,v9,w,w9 being Element of M
st Class(R,v) = Class(R,v9) & Class(R,w) = Class(R,w9)
holds Class(R,v*w) = Class(R,v9*w9)
proof
let M be multMagma;
let R be Equivalence_Relation of M;
hereby
assume A1: R is compatible;
let v,v9,w,w9 be Element of M;
assume A2: Class(R,v) = Class(R,v9) & Class(R,w) = Class(R,w9);
per cases;
suppose A3: M is empty;
hence Class(R,v*w) = {} .= Class(R,v9*w9) by A3;
end;
suppose M is not empty; then
v in Class(R,v9) & w in Class(R,w9) by A2,EQREL_1:23; then
v*w in Class(R,v9*w9) by A1;
hence Class(R,v*w) = Class(R,v9*w9) by EQREL_1:23;
end;
end;
assume A4: for v,v9,w,w9 being Element of M
st Class(R,v) = Class(R,v9) & Class(R,w) = Class(R,w9)
holds Class(R,v*w) = Class(R,v9*w9);
for v,v9,w,w9 being Element of M st v in Class(R,v9) & w in Class(R,w9)
holds v*w in Class(R,v9*w9)
proof
let v,v9,w,w9 be Element of M;
assume A5: v in Class(R,v9) & w in Class(R,w9);
per cases;
suppose M is empty; hence thesis by A5; end;
suppose A6: M is not empty;
Class(R,v9) = Class(R,v) &
Class(R,w9) = Class(R,w) by A5,EQREL_1:23; then
Class(R,v*w) = Class(R,v9*w9) by A4;
hence v*w in Class(R,v9*w9) by A6,EQREL_1:23;
end;
end;
hence R is compatible;
end;
definition
let M be multMagma;
let R be compatible Equivalence_Relation of M;
func ClassOp R -> BinOp of Class R means :Def4:
for x,y being Element of Class R, v,w being Element of M
st x = Class(R,v) & y = Class(R,w) holds it.(x,y) = Class(R,v*w)
if M is non empty otherwise it = {};
correctness
proof
A1: M is not empty implies ex b being BinOp of Class R st
for x, y being Element of Class R, v,w being Element of M st
x = Class(R,v) & y = Class(R,w) holds b.(x,y) = Class(R,v*w)
proof
assume A2: M is not empty; then
reconsider X = Class R as non empty set;
defpred P[set,set,set] means for x,y being Element of Class R,
v,w being Element of M st x=$1 & y=$2 & x = Class(R,v) & y = Class(R,w)
holds $3 = Class(R,v*w);
A3: for x,y being Element of X ex z being Element of X st P[x,y,z]
proof
let x,y be Element of X;
x in Class R; then
consider v be object such that
A4: v in the carrier of M & x = Class(R,v) by EQREL_1:def 3;
reconsider v as Element of M by A4;
y in Class R; then
consider w be object such that
A5: w in the carrier of M & y = Class(R,w) by EQREL_1:def 3;
reconsider w as Element of M by A5;
reconsider z = Class(R,v*w) as Element of X by A2,EQREL_1:def 3;
take z;
thus thesis by A4,A5,Th2;
end;
consider b be Function of [:X,X:],X such that
A6: for x,y being Element of X holds P[x,y,b.(x,y)]
from BINOP_1:sch 3(A3);
reconsider b as BinOp of Class R;
take b;
thus thesis by A6;
end;
A7: M is empty implies ex b being BinOp of Class R st b = {}
proof
assume M is empty; then
the carrier of M is empty; then
A8: Class R is empty;
set b = the BinOp of Class R;
take b;
thus b = {} by A8;
end;
for b1, b2 being BinOp of Class R holds M is not empty &
(for x,y being Element of Class R, v,w being Element of M
st x = Class(R,v) & y = Class(R,w) holds b1.(x,y) = Class(R,v*w)) &
(for x,y being Element of Class R, v,w being Element of M
st x = Class(R,v) & y = Class(R,w) holds b2.(x,y) = Class(R,v*w))
implies b1 = b2
proof
let b1,b2 be BinOp of Class R;
assume M is not empty;
assume A9: for x,y being Element of Class R, v,w being Element of M
st x = Class(R,v) & y = Class(R,w) holds b1.(x,y) = Class(R,v*w);
assume A10: for x,y being Element of Class R, v,w being Element of M
st x = Class(R,v) & y = Class(R,w) holds b2.(x,y) = Class(R,v*w);
for x,y being set st x in Class R & y in Class R
holds b1.(x,y) = b2.(x,y)
proof
let x,y be set;
assume A11: x in Class R; then
reconsider x9=x as Element of Class R;
assume A12: y in Class R; then
reconsider y9=y as Element of Class R;
consider v be object such that
A13: v in the carrier of M & x9 = Class(R,v) by A11,EQREL_1:def 3;
consider w be object such that
A14:w in the carrier of M & y9 = Class(R,w) by A12,EQREL_1:def 3;
reconsider v,w as Element of M by A13,A14;
b1.(x9,y9) = Class(R,v*w) by A13,A14,A9;
hence b1.(x,y) = b2.(x,y) by A13,A14,A10;
end;
hence thesis by BINOP_1:1;
end;
hence thesis by A1,A7;
end;
end;
:: Ch I ?1.6 Def.11 Algebra I Bourbaki
definition
let M be multMagma;
let R be compatible Equivalence_Relation of M;
func M ./. R -> multMagma equals
multMagma(# Class R, ClassOp R #);
correctness;
end;
registration
let M be multMagma;
let R be compatible Equivalence_Relation of M;
cluster M ./. R -> strict;
correctness;
end;
registration
let M be non empty multMagma;
let R be compatible Equivalence_Relation of M;
cluster M ./. R -> non empty;
correctness;
end;
definition
let M be non empty multMagma;
let R be compatible Equivalence_Relation of M;
func nat_hom R -> Function of M, M ./. R means :Def6:
for v being Element of M holds it.v = Class(R,v);
existence
proof
defpred P[object,object] means
ex v being Element of M st $1=v & $2=Class(R,v);
A1: for x being object st x in the carrier of M ex y being object st P[x,y]
proof
let x be object;
assume x in the carrier of M;
then reconsider v = x as Element of M;
reconsider y = Class(R,v) as set;
take y,v;
thus thesis;
end;
consider f being Function such that
A2: dom f = the carrier of M and
A3: for x being object st x in the carrier of M
holds P[x,f.x] from CLASSES1:sch 1(A1);
rng f c= the carrier of M ./. R
proof
let x be object;
assume x in rng f;
then consider y be object such that
A4: y in dom f and
A5: f.y = x by FUNCT_1:def 3;
consider v be Element of M such that
A6: y = v & f.y = Class(R,v) by A2,A3,A4;
thus thesis by A5,A6,EQREL_1:def 3;
end;
then reconsider f as Function of M, M ./. R
by A2,FUNCT_2:def 1,RELSET_1:4;
take f;
let v be Element of M;
ex w being Element of M st v = w & f.v = Class(R,w) by A3;
hence thesis;
end;
uniqueness
proof
let f1,f2 be Function of M, M ./. R such that
A7: for v being Element of M holds f1.v = Class(R,v) and
A8: for v being Element of M holds f2.v = Class(R,v);
now
let v being Element of M;
f1.v = Class(R,v) & f2.v = Class(R,v) by A7,A8;
hence f1.v = f2.v;
end;
hence thesis by FUNCT_2:63;
end;
end;
registration
let M be non empty multMagma;
let R be compatible Equivalence_Relation of M;
cluster nat_hom R -> multiplicative;
correctness
proof
for v,w being Element of M
holds (nat_hom R).(v*w) = (nat_hom R).v * (nat_hom R).w
proof
let v,w be Element of M;
(nat_hom R).v = Class(R,v) & (nat_hom R).w = Class(R,w) by Def6; then
(ClassOp R).((nat_hom R).v,(nat_hom R).w) = Class(R,v*w) by Def4;
hence (nat_hom R).(v*w) = (nat_hom R).v * (nat_hom R).w by Def6;
end;
hence thesis by GROUP_6:def 6;
end;
end;
registration
let M be non empty multMagma;
let R be compatible Equivalence_Relation of M;
cluster nat_hom R -> onto;
correctness
proof
for y being object st y in the carrier of (M ./. R)
holds y in rng nat_hom R
proof
let y be object;
assume y in the carrier of (M ./. R); then
consider x be object such that
A1: x in the carrier of M & y = Class(R,x) by EQREL_1:def 3;
reconsider x as Element of M by A1;
the carrier of M = dom(nat_hom R) by FUNCT_2:def 1; then
x in dom(nat_hom R) & (nat_hom R).x = Class(R,x) by Def6;
hence y in rng nat_hom R by A1,FUNCT_1:def 3;
end; then
the carrier of (M ./. R) c= rng nat_hom R; then
rng nat_hom R = the carrier of (M ./. R) by XBOOLE_0:def 10;
hence thesis by FUNCT_2:def 3;
end;
end;
definition
let M be multMagma;
mode Relators of M is [:the carrier of M,the carrier of M:]-valued Function;
end;
:: Ch I ?1.6 Algebra I Bourbaki
definition
let M be multMagma;
let r be Relators of M;
func equ_rel r -> Equivalence_Relation of M equals
meet {R where R is compatible Equivalence_Relation of M:
for i being set, v,w being Element of M st i in dom r & r.i = [v,w]
holds v in Class(R,w)};
correctness
proof
set X = {R where R is compatible Equivalence_Relation of M :
for i being set, v,w being Element of M st i in dom r & r.i = [v,w]
holds v in Class(R,w)};
per cases;
suppose M is empty; then
A1: the carrier of M = {};
for x being object st x in X holds x in {{}}
proof
let x be object;
assume x in X; then
consider R be compatible Equivalence_Relation of M such that
A2: x=R &
for i being set, v,w being Element of M st i in dom r & r.i = [v,w]
holds v in Class(R,w);
x is Subset of {} by A2,A1;
hence x in {{}} by TARSKI:def 1;
end; then
X c= {{}}; then
X = {} or X = {{}} by ZFMISC_1:33;
hence thesis by A1,OSALG_4:9,SETFAM_1:10,def 1;
end;
suppose A3: M is not empty;
for i being set, v,w being Element of M st i in dom r & r.i = [v,w]
holds v in Class(nabla the carrier of M,w)
proof
let i be set;
let v,w be Element of M;
assume i in dom r & r.i = [v,w];
Class(nabla the carrier of M,w) = the carrier of M by A3,EQREL_1:26;
hence v in Class(nabla the carrier of M,w) by A3,SUBSET_1:def 1;
end; then
A4: nabla the carrier of M in X;
for x being object st x in X
holds x in bool [:the carrier of M,the carrier of M:]
proof
let x be object;
assume x in X; then
consider R be compatible Equivalence_Relation of M such that
A5: x=R &
for i being set, x,y being Element of M st i in dom r & r.i = [x,y]
holds x in Class(R,y);
thus thesis by A5;
end; then
reconsider X as Subset-Family of [:the carrier of M,the carrier of M:]
by TARSKI:def 3;
for Y being set st Y in X holds Y is Equivalence_Relation of M
proof
let Y be set;
assume Y in X; then
consider R be compatible Equivalence_Relation of M such that
A6: Y=R &
for i being set, v,w being Element of M st i in dom r & r.i = [v,w]
holds v in Class(R,w);
thus Y is Equivalence_Relation of M by A6;
end;
hence thesis by A4,EQREL_1:11;
end;
end;
end;
theorem Th3:
for M being multMagma, r being Relators of M,
R being compatible Equivalence_Relation of M
st (for i being set, v,w being Element of M st i in dom r & r.i = [v,w]
holds v in Class(R,w))
holds equ_rel r c= R
proof
let M be multMagma;
let r be Relators of M;
let R be compatible Equivalence_Relation of M;
assume A1: for i being set, v,w being Element of M
st i in dom r & r.i = [v,w] holds v in Class(R,w);
let X be object;
R in {R9 where R9 is compatible Equivalence_Relation of M:
for i being set, v,w being Element of M st i in dom r & r.i = [v,w]
holds v in Class(R9,w)} by A1;
hence thesis by SETFAM_1:def 1;
end;
registration
let M be multMagma;
let r be Relators of M;
cluster equ_rel r -> compatible;
coherence
proof
set X = {R where R is compatible Equivalence_Relation of M :
for i being set, v,w being Element of M st i in dom r & r.i = [v,w]
holds v in Class(R,w)};
for v,v9,w,w9 being Element of M
st v in Class(equ_rel r,v9) & w in Class(equ_rel r,w9)
holds v*w in Class(equ_rel r,v9*w9)
proof
let v,v9,w,w9 be Element of M;
assume v in Class(equ_rel r,v9); then
A1: [v9,v] in equ_rel r by EQREL_1:18;
assume w in Class(equ_rel r,w9); then
A2: [w9,w] in equ_rel r by EQREL_1:18;
per cases;
suppose X = {}; hence thesis by A1,SETFAM_1:def 1; end;
suppose A3: X <> {};
for Y being set st Y in X holds [v9*w9,v*w] in Y
proof
let Y be set;
assume A4: Y in X; then
consider R be compatible Equivalence_Relation of M such that
A5: Y = R &
for i being set, v,w being Element of M st i in dom r & r.i = [v,w]
holds v in Class(R,w);
[v9,v] in Y by A1,A4,SETFAM_1:def 1; then
A6: v in Class(R,v9) by A5,EQREL_1:18;
[w9,w] in Y by A2,A4,SETFAM_1:def 1; then
w in Class(R,w9) by A5,EQREL_1:18;
then v*w in Class(R,v9*w9) by A6,Def3;
hence [v9*w9,v*w] in Y by A5,EQREL_1:18;
end; then
[v9*w9,v*w] in meet X by A3,SETFAM_1:def 1;
hence v*w in Class(equ_rel r,v9*w9) by EQREL_1:18;
end;
end;
hence thesis;
end;
end;
definition
let X,Y be set;
let f be Function of X,Y;
func equ_kernel f -> Equivalence_Relation of X means :Def8:
for x,y being object holds [x,y] in it iff x in X & y in X & f.x = f.y;
existence
proof
defpred P[object,object] means f.$1 = f.$2;
A1: for x being object st x in X holds P[x,x];
A2: for x,y being object st P[x,y] holds P[y,x];
A3: for x,y,z being object st P[x,y] & P[y,z] holds P[x,z];
ex EqR being Equivalence_Relation of X st
for x,y being object holds [x,y] in EqR iff x in X & y in X & P[x,y]
from EQREL_1:sch 1(A1,A2,A3);
hence thesis;
end;
uniqueness
proof
let R1, R2 be Equivalence_Relation of X;
defpred P[object,object] means $1 in X & $2 in X & f.$1 = f.$2;
assume for x,y being object holds [x,y] in R1
iff x in X & y in X & f.x = f.y; then
A4: for x,y being object holds [x,y] in R1 iff P[x,y];
assume for x,y being object holds [x,y] in R2
iff x in X & y in X & f.x = f.y; then
A5: for x,y being object holds [x,y] in R2 iff P[x,y];
thus R1 = R2 from RELAT_1:sch 2(A4,A5);
end;
end;
reserve M,N for non empty multMagma,
f for Function of M, N;
theorem Th4:
f is multiplicative implies equ_kernel f is compatible
proof
assume A1: f is multiplicative;
set R = equ_kernel f;
for v,v9,w,w9 being Element of M st v in Class(R,v9) & w in Class(R,w9) holds
v*w in Class(R,v9*w9)
proof
let v,v9,w,w9 be Element of M;
assume v in Class(R,v9); then
A2: [v9,v] in R by EQREL_1:18;
assume w in Class(R,w9); then
[w9,w] in R by EQREL_1:18; then
A3: f.w9 = f.w by Def8;
f.(v9*w9) = f.v9 * f.w9 by A1,GROUP_6:def 6
.= f.v * f.w by A2,A3,Def8
.= f.(v*w) by A1,GROUP_6:def 6; then
[v9*w9,v*w] in R by Def8;
hence v*w in Class(R,v9*w9) by EQREL_1:18;
end;
hence equ_kernel f is compatible;
end;
theorem Th5:
f is multiplicative implies
ex r being Relators of M st equ_kernel f = equ_rel r
proof
assume A1: f is multiplicative;
set I = {[v,w] where v,w is Element of M: f.v = f.w};
set r = id I;
for y being object st y in rng r
holds y in [: the carrier of M, the carrier of M:]
proof
let y be object;
assume y in rng r; then
consider x be object such that
A2: x in dom r & y = r.x by FUNCT_1:def 3;
y = x by A2,FUNCT_1:17; then
y in I by A2; then
consider v9,w9 be Element of M such that
A3: y = [v9,w9] & f.v9 = f.w9;
thus thesis by A3,ZFMISC_1:def 2;
end; then
rng r c= [: the carrier of M, the carrier of M:]; then
reconsider r as Relators of M by FUNCT_2:2;
take r;
reconsider R=equ_kernel f as compatible Equivalence_Relation of M by A1,Th4;
A4: for i being set, v,w being Element of M
st i in dom r & r.i = [v,w] holds v in Class(R,w)
proof
let i be set;
let v,w be Element of M;
assume A5: i in dom r & r.i = [v,w]; then
A6: r.i = i by FUNCT_1:17;
consider v9,w9 be Element of M such that
A7: i=[v9,w9] & f.v9 = f.w9 by A5;
[v,w] in equ_kernel f by A7,Def8,A5,A6;
hence v in Class(R,w) by EQREL_1:19;
end; then
A8: equ_rel r c= R by Th3;
for z being object st z in R holds z in equ_rel r
proof
let z be object;
assume A9: z in R;
then consider x,y be object such that
A10: x in the carrier of M & y in the carrier of M &
z = [x,y] by ZFMISC_1:def 2;
A11: f.x = f.y by A9,A10,Def8;
reconsider x,y as Element of M by A10;
set X9 = {R9 where R9 is compatible Equivalence_Relation of M:
for i being set, v,w being Element of M st i in dom r & r.i = [v,w]
holds v in Class(R9,w)};
A12: R in X9 by A4;
for Y being set st Y in X9 holds z in Y
proof
let Y be set;
assume Y in X9; then
consider R9 be compatible Equivalence_Relation of M such that
A13: R9=Y & for i being set, v,w being Element of M
st i in dom r & r.i = [v,w] holds v in Class(R9,w);
set i = [x,y];
A14: i in I by A11; then
r.i = [x,y] by FUNCT_1:17; then
x in Class(R9,y) by A14,A13;
hence z in Y by A10,A13,EQREL_1:19;
end;
hence thesis by A12,SETFAM_1:def 1;
end; then
R c= equ_rel r;
hence thesis by A8,XBOOLE_0:def 10;
end;
begin :: Submagmas and Stable Subsets
definition
let M be multMagma;
mode multSubmagma of M -> multMagma means :Def9:
the carrier of it c= the carrier of M &
the multF of it = (the multF of M)||the carrier of it;
existence
proof
set S = the empty multMagma;
reconsider A = the carrier of S as set;
reconsider X = [: A, A :] as set;
the multF of S = (the multF of M) | X
.= (the multF of M)||the carrier of S by REALSET1:def 2;
hence thesis by XBOOLE_1:2;
end;
end;
registration
let M be multMagma;
cluster strict for multSubmagma of M;
existence
proof
set N = multMagma(# the carrier of M, the multF of M #);
the multF of N
= (the multF of N)|[:the carrier of N,the carrier of N:]
.= (the multF of M)||the carrier of N by REALSET1:def 2; then
reconsider N as multSubmagma of M by Def9;
take N;
thus thesis;
end;
end;
registration
let M be non empty multMagma;
cluster non empty for multSubmagma of M;
existence
proof
set N = multMagma(# the carrier of M, the multF of M #);
the multF of N
= (the multF of N)|[:the carrier of N,the carrier of N:]
.= (the multF of M)||the carrier of N by REALSET1:def 2; then
reconsider N as multSubmagma of M by Def9;
take N;
thus thesis;
end;
end;
reserve M for multMagma;
reserve N,K for multSubmagma of M;
:: like GROUP_2:64
theorem Th6:
N is multSubmagma of K & K is multSubmagma of N
implies the multMagma of N = the multMagma of K
proof
assume that
A1: N is multSubmagma of K and
A2: K is multSubmagma of N;
set A = the carrier of N;
set B = the carrier of K;
set f = the multF of N;
set g = the multF of K;
A3: A c= B & B c= A by A1,A2,Def9;
f = g||A by A1,Def9
.= (f||B)||A by A2,Def9
.= (f|[:B,B:])||A by REALSET1:def 2
.= (f|[:B,B:])|[:A,A:] by REALSET1:def 2
.= f||B by REALSET1:def 2
.= g by A2,Def9;
hence thesis by A3,XBOOLE_0:def 10;
end;
theorem Th7:
the carrier of N = the carrier of M
implies the multMagma of N = the multMagma of M
proof
assume A1: the carrier of N = the carrier of M;
per cases;
suppose the carrier of M = {};
hence thesis by A1;
end;
suppose the carrier of M <> {};
A2: the multF of M
= (the multF of M)|[:the carrier of M,the carrier of M:]
.= (the multF of M)||(the carrier of M) by REALSET1:def 2; then
reconsider M9=M as multSubmagma of M by Def9;
the multF of M9 = (the multF of N)||the carrier of M9 by A1,A2,Def9; then
M9 is multSubmagma of N by A1,Def9;
hence thesis by Th6;
end;
end;
:: Ch I ?1.4 Def.6 Algebra I Bourbaki
definition
let M be multMagma;
let A be Subset of M;
attr A is stable means :Def10:
for v,w being Element of M st v in A & w in A holds v*w in A;
end;
registration
let M be multMagma;
cluster stable for Subset of M;
correctness
proof
reconsider A = the carrier of M as Subset of M by ZFMISC_1:def 1;
take A;
thus thesis;
end;
end;
theorem Th8:
the carrier of N is stable Subset of M
proof
for v,w being Element of M st v in the carrier of N & w in the carrier of N
holds v*w in the carrier of N
proof
let v,w be Element of M;
assume A1: v in the carrier of N & w in the carrier of N; then
reconsider v9=v, w9=w as Element of N;
A2: [v,w] in [:the carrier of N,the carrier of N:] by A1,ZFMISC_1:def 2;
v9*w9 = (the multF of N).[v9,w9] by BINOP_1:def 1
.= ((the multF of M)||the carrier of N).[v9,w9] by Def9
.= ((the multF of M)|[:the carrier of N,the carrier of N:]).[v,w]
by REALSET1:def 2
.= (the multF of M).[v,w] by A2,FUNCT_1:49
.= v*w by BINOP_1:def 1;
hence v*w in the carrier of N by A1;
end;
hence the carrier of N is stable Subset of M by Def9,Def10;
end;
registration
let M be multMagma;
let N be multSubmagma of M;
cluster the carrier of N -> stable for Subset of M;
correctness by Th8;
end;
theorem Th9:
for F being Function st
(for i being set st i in dom F holds F.i is stable Subset of M) holds
meet F is stable Subset of M
proof
let F be Function;
assume A1: for i being set st i in dom F holds F.i is stable Subset of M;
A2: for x being object st x in meet F holds x in the carrier of M
proof
let x be object;
assume x in meet F; then
A3: x in meet rng F by FUNCT_6:def 4;
per cases;
suppose dom F is empty; then
F = {};
hence thesis by A3,SETFAM_1:1;
end;
suppose dom F is not empty; then
consider i be object such that
A4: i in dom F by XBOOLE_0:def 1;
meet rng F c= F.i by A4,FUNCT_1:3,SETFAM_1:3; then
A5: x in F.i by A3;
F.i is stable Subset of M by A1,A4;
hence x in the carrier of M by A5;
end;
end;
for v,w being Element of M st v in meet F & w in meet F holds v*w in meet F
proof
let v,w be Element of M;
assume A6: v in meet F & w in meet F;
per cases;
suppose F = {}; then
meet rng F = {} by SETFAM_1:1;
hence thesis by A6,FUNCT_6:def 4;
end;
suppose A7: F <> {};
A8: v in meet rng F & w in meet rng F by A6,FUNCT_6:def 4;
for Y being set holds Y in rng F implies v*w in Y
proof
let Y be set;
assume A9: Y in rng F; then
A10: v in Y & w in Y by A8,SETFAM_1:def 1;
consider i be object such that
A11: i in dom F & Y = F.i by A9,FUNCT_1:def 3;
Y is stable Subset of M by A1,A11;
hence v*w in Y by A10,Def10;
end; then
v*w in meet rng F by A7,SETFAM_1:def 1;
hence v*w in meet F by FUNCT_6:def 4;
end;
end;
hence thesis by A2,Def10,TARSKI:def 3;
end;
reserve M,N for non empty multMagma,
A for Subset of M,
f,g for Function of M,N,
X for stable Subset of M,
Y for stable Subset of N;
theorem
A is stable iff A * A c= A
proof
hereby
assume A1: A is stable;
for x being object st x in A * A holds x in A
proof
let x be object;
assume x in A * A; then
consider v,w be Element of M such that
A2: x = v * w & v in A & w in A by GROUP_2:8;
thus x in A by A1,A2;
end;
hence A * A c= A;
end;
assume A3: A * A c= A;
for v,w being Element of M st v in A & w in A holds v*w in A
proof
let v,w be Element of M;
assume v in A & w in A; then
v*w in A * A by GROUP_2:8;
hence v*w in A by A3;
end;
hence A is stable;
end;
:: Ch I ?1.4 Pro.1 Algebra I Bourbaki
theorem Th11:
f is multiplicative implies f.:X is stable Subset of N
proof
assume A1: f is multiplicative;
for v,w being Element of N st v in f.:X & w in f.:X holds v*w in f.:X
proof
let v,w be Element of N;
assume v in f.:X; then
consider v9 be object such that
A2: v9 in dom f & v9 in X & v = f.v9 by FUNCT_1:def 6;
assume w in f.:X; then
consider w9 be object such that
A3: w9 in dom f & w9 in X & w = f.w9 by FUNCT_1:def 6;
reconsider v9,w9 as Element of M by A2,A3;
v9*w9 in the carrier of M; then
A4: v9*w9 in dom f by FUNCT_2:def 1;
v9*w9 in X by A2,A3,Def10; then
f.(v9*w9) in f.:X by A4,FUNCT_1:def 6;
hence v*w in f.:X by A2,A3,A1,GROUP_6:def 6;
end;
hence f .: X is stable Subset of N by Def10;
end;
:: Ch I ?1.4 Pro.1 Algebra I Bourbaki
theorem Th12:
f is multiplicative implies f"Y is stable Subset of M
proof
assume A1: f is multiplicative;
for v,w being Element of M st v in f"Y & w in f"Y holds v*w in f"Y
proof
let v,w be Element of M;
assume v in f"Y; then
A2: v in dom f & f.v in Y by FUNCT_1:def 7;
assume w in f"Y; then
A3: w in dom f & f.w in Y by FUNCT_1:def 7;
v*w in the carrier of M; then
A4: v*w in dom f by FUNCT_2:def 1;
f.v*f.w in Y by A2,A3,Def10; then
f.(v*w) in Y by A1,GROUP_6:def 6;
hence v*w in f"Y by A4,FUNCT_1:def 7;
end;
hence f"Y is stable Subset of M by Def10;
end;
:: Ch I ?1.4 Pro.1 Algebra I Bourbaki
theorem
f is multiplicative & g is multiplicative
implies {v where v is Element of M: f.v=g.v} is stable Subset of M
proof
assume A1: f is multiplicative;
assume A2: g is multiplicative;
set X = {v where v is Element of M: f.v=g.v};
for x being object st x in X holds x in the carrier of M
proof
let x be object;
assume x in X; then
consider v be Element of M such that
A3: x=v & f.v=g.v;
thus x in the carrier of M by A3;
end; then
reconsider X as Subset of M by TARSKI:def 3;
for v,w being Element of M st v in X & w in X holds v*w in X
proof
let v,w be Element of M;
assume v in X; then
consider v9 be Element of M such that
A4: v=v9 & f.v9=g.v9;
assume w in X; then
consider w9 be Element of M such that
A5: w=w9 & f.w9=g.w9;
f.(v*w) = g.v*g.w by A4,A5,A1,GROUP_6:def 6
.= g.(v*w) by A2,GROUP_6:def 6;
hence v*w in X;
end;
hence thesis by Def10;
end;
:: Ch I ?1.4 Def.6 Algebra I Bourbaki
definition
let M be multMagma;
let A be stable Subset of M;
func the_mult_induced_by A -> BinOp of A equals
(the multF of M) || A;
correctness
proof
for x being set holds x in [:A,A:] implies (the multF of M).x in A
proof
let x be set;
assume x in [:A,A:]; then
consider v,w be object such that
A1: v in A & w in A & x = [v,w] by ZFMISC_1:def 2;
reconsider v,w as Element of M by A1;
v*w in A by A1,Def10;
hence (the multF of M).x in A by A1,BINOP_1:def 1;
end; then
A is Preserv of (the multF of M) by REALSET1:def 1;
hence thesis by REALSET1:2;
end;
end;
:: like GROUP_4:def 5
definition
let M be multMagma;
let A be Subset of M;
func the_submagma_generated_by A -> strict multSubmagma of M means :Def12:
A c= the carrier of it & for N being strict multSubmagma of M
st A c= the carrier of N holds it is multSubmagma of N;
existence
proof
defpred P[set] means ex H being strict multSubmagma of M st
$1 = the carrier of H & A c= $1;
consider X be set such that
A1: for Y being set holds Y in X iff Y in bool the carrier of M & P[Y]
from XFAMILY:sch 1;
set F = id X;
set A1 = meet id X;
for x being set st x in dom F holds F.x is stable Subset of M
proof
let x be set;
assume A2: x in dom F; then
x in bool the carrier of M & P[x] by A1;
hence thesis by A2,FUNCT_1:18;
end; then
reconsider A1 as stable Subset of M by Th9;
set N1 = multMagma(# A1, the_mult_induced_by A1 #);
take N1;
per cases;
suppose A3: X = {};
A4: the carrier of M in bool the carrier of M by ZFMISC_1:def 1;
ex H being strict multSubmagma of M st
the carrier of M= the carrier of H & A c= the carrier of M
proof
the multF of M = (the multF of M)|[:the carrier of M,the carrier of M:]
; then
the multF of M = (the multF of M)||the carrier of M
by REALSET1:def 2; then
reconsider H = the multMagma of M as strict multSubmagma of M by Def9;
take H;
thus the carrier of M = the carrier of H;
thus A c= the carrier of M;
end;
hence thesis by A3,A4,A1;
end;
suppose A5: X <> {};
A6: for x being object st x in A holds x in A1
proof
let x be object;
assume A7: x in A;
for Y being set st Y in X holds x in Y
proof
let Y be set;
assume Y in X; then
consider H be strict multSubmagma of M such that
A8: Y = the carrier of H & A c= Y by A1;
thus x in Y by A8,A7;
end; then
x in meet X by A5,SETFAM_1:def 1; then
x in meet rng id X;
hence thesis by FUNCT_6:def 4;
end;
for N being strict multSubmagma of M
st A c= the carrier of N holds N1 is multSubmagma of N
proof
let N be strict multSubmagma of M;
assume A9: A c= the carrier of N;
for x being object
st x in the carrier of N1 holds x in the carrier of N
proof
let x be object;
assume x in the carrier of N1; then
x in meet rng id X by FUNCT_6:def 4; then
A10: x in meet X;
the carrier of N c= the carrier of M by Def9;
then the carrier of N in X by A1,A9;
hence x in the carrier of N by A10,SETFAM_1:def 1;
end; then
A11: the carrier of N1 c= the carrier of N;
A12: (the multF of M)|[:the carrier of N,the carrier of N:]
= (the multF of M)||the carrier of N by REALSET1:def 2
.= the multF of N by Def9;
the multF of N1
= (the multF of M)|[:the carrier of N1,the carrier of N1:]
by REALSET1:def 2
.= ((the multF of M)|[:the carrier of N,the carrier of N:])
|[:the carrier of N1,the carrier of N1:]
by A11,RELAT_1:74,ZFMISC_1:96
.= (the multF of N)||the carrier of N1 by A12,REALSET1:def 2;
hence N1 is multSubmagma of N by A11,Def9;
end;
hence thesis by A6,Def9;
end;
end;
uniqueness
proof
let H1,H2 be strict multSubmagma of M;
assume A c= the carrier of H1 & (for N being strict multSubmagma of M
st A c= the carrier of N holds H1 is multSubmagma of N) &
A c= the carrier of H2 & (for N being strict multSubmagma of M
st A c= the carrier of N holds H2 is multSubmagma of N);
then H1 is multSubmagma of H2 & H2 is multSubmagma of H1;
hence thesis by Th6;
end;
end;
theorem Th14:
for M being multMagma, A being Subset of M
holds A is empty iff the_submagma_generated_by A is empty
proof
let M be multMagma;
let A be Subset of M;
hereby
assume A1: A is empty;
then
for v,w being Element of M st v in A & w in A holds v*w in A; then
reconsider A9=A as stable Subset of M by Def10;
reconsider N=multMagma(# A9, the_mult_induced_by A9 #)
as strict multSubmagma of M by Def9;
the_submagma_generated_by A is multSubmagma of N by Def12; then
the carrier of the_submagma_generated_by A c= the carrier of N by Def9;
hence the_submagma_generated_by A is empty by A1;
end;
assume the_submagma_generated_by A is empty; then
the carrier of the_submagma_generated_by A = {}; then
A c= {} by Def12;
hence A is empty;
end;
registration
let M be multMagma;
let A be empty Subset of M;
cluster the_submagma_generated_by A -> empty;
correctness by Th14;
end;
:: Ch I ?1.4 Pro.1 Algebra I Bourbaki
theorem Th15:
for M,N being non empty multMagma, f being Function of M,N,
X being Subset of M st f is multiplicative holds
f.:the carrier of the_submagma_generated_by X =
the carrier of the_submagma_generated_by f.:X
proof
let M,N be non empty multMagma;
let f be Function of M,N;
let X be Subset of M;
assume A1: f is multiplicative;
set X9 = the_submagma_generated_by X;
set A = f.:the carrier of X9;
the carrier of X9 is stable Subset of M by Th8; then
reconsider A as stable Subset of N by A1,Th11;
set Y9 = the_submagma_generated_by f.:X;
set B = f"the carrier of Y9;
the carrier of Y9 is stable Subset of N by Th8; then
reconsider B as stable Subset of M by A1,Th12;
A2: f.:X c= the carrier of Y9 & for N1 being strict multSubmagma of N
st f.:X c= the carrier of N1
holds Y9 is multSubmagma of N1 by Def12;
reconsider N1 = multMagma(# A, the_mult_induced_by A #) as
strict multSubmagma of N by Def9;
X c= the carrier of X9 by Def12; then
Y9 is multSubmagma of N1 by A2,RELAT_1:123; then
A3: the carrier of Y9 c= A by Def9;
A4: X c= the carrier of X9 & for M1 being strict multSubmagma of M
st X c= the carrier of M1
holds X9 is multSubmagma of M1 by Def12;
reconsider M1 = multMagma(# B, the_mult_induced_by B #) as
strict multSubmagma of M by Def9;
A5: f.:(f"the carrier of Y9) c= the carrier of Y9 by FUNCT_1:75;
f.:X c= the carrier of the_submagma_generated_by f.:X by Def12; then
A6: f"(f.:X) c= f"the carrier of the_submagma_generated_by f.:X
by RELAT_1:143;
X c= the carrier of M; then
X c= dom f by FUNCT_2:def 1; then
X c= f"(f.:X) by FUNCT_1:76; then
X9 is multSubmagma of M1 by A4,A6,XBOOLE_1:1; then
the carrier of X9 c= B by Def9; then
A c= f.:(f"the carrier of Y9) by RELAT_1:123; then
A c= the carrier of Y9 by A5;
hence thesis by A3,XBOOLE_0:def 10;
end;
begin :: Free Magmas
:: Ch I ?7.1 Algebra I Bourbaki
definition
let X be set;
defpred P[object,object] means
for fs being XFinSequence of bool the_universe_of(X \/ NAT)
st $1=fs holds
(dom fs = 0 implies $2 = {}) &
(dom fs = 1 implies $2 = X) &
for n being Nat st n>=2 & dom fs = n holds
ex fs1 being FinSequence st len fs1 = n-1 &
(for p being Nat st p>=1 & p<=n-1 holds
fs1.p = [: fs.p, fs.(n-p) :] ) & $2 = Union disjoin fs1;
A1: for e being object st e in (bool the_universe_of(X \/ NAT))^omega
ex u being object st P[e,u]
proof
let e be object;
assume e in (bool the_universe_of(X \/ NAT))^omega; then
reconsider fs = e as
XFinSequence of bool the_universe_of(X \/ NAT) by AFINSQ_1:def 7;
dom fs = 0 or dom fs + 1 > 0+1 by XREAL_1:6; then
dom fs = 0 or dom fs >= 1 by NAT_1:13; then
dom fs = 0 or dom fs = 1 or dom fs > 1 by XXREAL_0:1; then
A2: dom fs = 0 or dom fs = 1 or dom fs + 1 > 1+1 by XREAL_1:6;
per cases by A2,NAT_1:13;
suppose A3: dom fs = 0; set u = {};
take u; thus P[e,u] by A3; end;
suppose A4: dom fs = 1; set u = X;
take u; thus P[e,u] by A4; end;
suppose A5: dom fs >= 2;
reconsider n = dom fs as Nat;
reconsider n9= n -' 1 as Nat;
n-1 >= 2-1 by A5,XREAL_1:9; then
A6: n9 = n-1 by XREAL_0:def 2;
defpred P2[set,object] means for p being Nat
st p>=1 & p<=n-1 & $1=p holds $2 = [: fs.p, fs.(n-p) :];
A7: for k being Nat st k in Seg n9 ex x being object st P2[k,x]
proof
let k be Nat;
assume k in Seg n9;
set x = [: fs.k, fs.(n-k) :];
take x;
thus thesis;
end;
consider fs1 be FinSequence such that
A8: dom fs1 = Seg n9 & for k being Nat st k in Seg n9 holds P2[k,fs1.k]
from FINSEQ_1:sch 1(A7);
set u = Union disjoin fs1;
take u;
A9: len fs1 = n-1 by A6,A8,FINSEQ_1:def 3;
for p being Nat st p>=1 & p<=n-1 holds
fs1.p = [: fs.p, fs.(n-p) :] by A8,A6,FINSEQ_1:1;
hence P[e,u] by A5,A9;
end;
end;
consider F be Function such that
A10: dom F = (bool the_universe_of(X \/ NAT))^omega &
for e being object st e in (bool the_universe_of(X \/ NAT))^omega
holds P[e,F.e] from CLASSES1:sch 1(A1);
A11: for e being object st e in (bool the_universe_of(X \/ NAT))^omega
holds F.e in bool the_universe_of(X \/ NAT)
proof
let e be object;
assume A12: e in (bool the_universe_of(X \/ NAT))^omega;
then reconsider fs=e as XFinSequence of bool the_universe_of(X \/ NAT)
by AFINSQ_1:def 7;
A13: (dom fs = 0 implies F.e = {}) & (dom fs = 1 implies F.e = X) &
for n being Nat st n>=2 & dom fs = n holds
ex fs1 being FinSequence st len fs1 = n-1 &
(for p being Nat st p>=1 & p<=n-1 holds
fs1.p = [: fs.p, fs.(n-p) :] ) & F.e = Union disjoin fs1 by A12,A10;
dom fs = 0 or dom fs + 1 > 0+1 by XREAL_1:6; then
dom fs = 0 or dom fs >= 1 by NAT_1:13; then
dom fs = 0 or dom fs = 1 or dom fs > 1 by XXREAL_0:1; then
A14: dom fs = 0 or dom fs = 1 or dom fs + 1 > 1+1 by XREAL_1:6;
per cases by A14,NAT_1:13;
suppose A15: dom fs = 0;
{} c= the_universe_of(X \/ NAT);
hence F.e in bool the_universe_of(X \/ NAT) by A15,A13;
end;
suppose dom fs = 1; then
A16: F.e = X by A12,A10;
for x being object st x in X holds
x in Tarski-Class the_transitive-closure_of(X \/ NAT)
proof
let x be object;
reconsider xx=x as set by TARSKI:1;
assume x in X; then
xx c= (union X) \/ union NAT by XBOOLE_1:10,ZFMISC_1:74; then
A17: xx c= union(X \/ NAT) by ZFMISC_1:78;
A18: the_transitive-closure_of(X \/ NAT) in
Tarski-Class the_transitive-closure_of(X \/ NAT) by CLASSES1:2;
A19: union(X \/ NAT) c= union the_transitive-closure_of(X \/ NAT)
by CLASSES1:52,ZFMISC_1:77;
union the_transitive-closure_of(X \/ NAT)
c= the_transitive-closure_of(X \/ NAT)
by CLASSES1:48,51; then
union(X \/ NAT) c= the_transitive-closure_of(X \/ NAT)
by A19;
hence thesis by A18,A17,CLASSES1:3,XBOOLE_1:1;
end; then
X c= Tarski-Class the_transitive-closure_of(X \/ NAT); then
X c= the_universe_of(X \/ NAT) by YELLOW_6:def 1;
hence F.e in bool the_universe_of(X \/ NAT) by A16;
end;
suppose A20: dom fs >= 2;
set n=dom fs;
consider fs1 be FinSequence such that
A21: len fs1 = n-1 & (for p being Nat st p>=1 & p<=n-1 holds
fs1.p = [: fs.p, fs.(n-p) :]) &
F.e = Union disjoin fs1 by A20,A12,A10;
reconsider n9= n -' 1 as Nat;
n-1 >= 2-1 by A20,XREAL_1:9; then
A22: n9 = n-1 by XREAL_0:def 2;
A23: for p being Nat st p>=1 & p<=n-1 holds
fs1.p c= the_universe_of(X \/ NAT)
proof
let p be Nat;
assume A24: p>=1 & p<=n-1; then
A25: fs1.p = [: fs.p, fs.(n-p) :] by A21;
A26: p in Seg n9 by A22,A24,FINSEQ_1:1;
-p <= -1 & -p >= -(n-1) by A24,XREAL_1:24; then
A27: -p +n <= -1+n & -p+n >= -(n-1)+n by XREAL_1:6; then
A28: n-p <= n-'1 & n-p >= 1 by XREAL_0:def 2;
A29: n-p = n-'p by A27,XREAL_0:def 2; then
A30: n-'p in Seg n9 by A28,FINSEQ_1:1;
A31: Seg n9 c= Segm(n9+1) by AFINSQ_1:3; then
A32: fs.p in rng fs by A26,A22,FUNCT_1:3;
fs.(n-p) in rng fs by A29,A31,A22,A30,FUNCT_1:3;
hence fs1.p c= the_universe_of(X \/ NAT) by A25,A32,Th1;
end;
for x being set st x in rng disjoin fs1
holds x c= the_universe_of(X \/ NAT)
proof
let x be set;
assume x in rng disjoin fs1; then
consider p be object such that
A33: p in dom disjoin fs1 & x = (disjoin fs1).p by FUNCT_1:def 3;
A34: p in dom fs1 by A33,CARD_3:def 3;
then A35: x = [:fs1.p,{p}:] by A33,CARD_3:def 3;
A36: p in Seg n9 by A21,A22,A34,FINSEQ_1:def 3;
reconsider p as Nat by A34;
p>=1 & p<=n-1 by A22,A36,FINSEQ_1:1; then
A37: fs1.p c= the_universe_of(X \/ NAT) by A23;
A38: for y being set st y in {p} holds y in NAT
proof
let y be set;
assume y in {p}; then
y = p by TARSKI:def 1;
hence y in NAT by ORDINAL1:def 12;
end;
for x being object st x in {p} holds
x in Tarski-Class the_transitive-closure_of(X \/ NAT)
proof
let x be object;
reconsider xx=x as set by TARSKI:1;
assume x in {p}; then
x in NAT by A38; then
xx c= (union X) \/ union NAT by XBOOLE_1:10,ZFMISC_1:74; then
A39: xx c= union(X \/ NAT) by ZFMISC_1:78;
A40: the_transitive-closure_of(X \/ NAT) in
Tarski-Class the_transitive-closure_of(X \/ NAT) by CLASSES1:2;
A41: union(X \/ NAT) c= union the_transitive-closure_of(X \/ NAT)
by CLASSES1:52,ZFMISC_1:77;
union the_transitive-closure_of(X \/ NAT)
c= the_transitive-closure_of(X \/ NAT)
by CLASSES1:48,51; then
union(X \/ NAT) c= the_transitive-closure_of(X \/ NAT)
by A41;
hence thesis by A40,A39,CLASSES1:3,XBOOLE_1:1;
end; then
{p} c= Tarski-Class the_transitive-closure_of(X \/ NAT); then
{p} c= the_universe_of(X \/ NAT) by YELLOW_6:def 1;
hence thesis by A35,A37,Th1;
end; then
union (rng disjoin fs1) c= the_universe_of(X \/ NAT)
by ZFMISC_1:76; then
union (rng disjoin fs1) in bool the_universe_of(X \/ NAT);
hence thesis by A21,CARD_3:def 4;
end;
end;
func free_magma_seq X ->
sequence of bool the_universe_of(X \/ NAT) means :Def13:
it.0 = {} & it.1 = X & for n being Nat st n>=2 holds
ex fs being FinSequence st len fs = n-1 &
(for p being Nat st p>=1 & p<=n-1 holds
fs.p = [: it.p, it.(n-p) :] ) & it.n = Union disjoin fs;
existence
proof
reconsider F as Function of (bool the_universe_of(X \/ NAT))^omega,
bool the_universe_of(X \/ NAT) by A11,A10,FUNCT_2:3;
deffunc FX(XFinSequence of bool the_universe_of(X \/ NAT)) = F.$1;
consider f be sequence of bool the_universe_of(X \/ NAT) such that
A42: for n being Nat holds f.n = FX(f|n)
from FuncRecursiveExist2;
take f;
A43: {} in (bool the_universe_of(X \/ NAT))^omega by AFINSQ_1:43;
A44: dom {} = {};
thus f.0 = F.(f|{}) by A42 .= {} by A43,A44,A10;
1 c= NAT; then
1 c= dom f by FUNCT_2:def 1; then
A45: dom(f|1) = 1 by RELAT_1:62;
A46: f|1 in (bool the_universe_of(X \/ NAT))^omega by AFINSQ_1:42;
thus f.1 = F.(f|1) by A42 .= X by A45,A46,A10;
let n be Nat;
assume A47: n >= 2;
n c= NAT; then
n c= dom f by FUNCT_2:def 1; then
A48: dom(f|n) = n by RELAT_1:62;
f|n in (bool the_universe_of(X \/ NAT))^omega by AFINSQ_1:42;
then consider fs1 be FinSequence such that
A49: len fs1 = n-1 & (for p being Nat st p>=1 & p<=n-1 holds
fs1.p = [: (f|n).p, (f|n).(n-p) :] ) &
F.(f|n) = Union disjoin fs1 by A47,A48,A10;
take fs1;
thus len fs1 = n-1 by A49;
thus for p being Nat st p>=1 & p<=n-1
holds fs1.p = [: f.p, f.(n - p):]
proof
let p be Nat;
assume A50: p >= 1 & p <= n - 1;
set n9 = n-'1;
n-1 >= 2-1 by A47,XREAL_1:9; then
A51: n9 = n-1 by XREAL_0:def 2; then
A52: p in Seg n9 by A50,FINSEQ_1:1;
Seg n9 c= Segm(n9+1) by AFINSQ_1:3; then
A53: (f|n).p = f.p by A51,A52,FUNCT_1:49;
-p <= -1 & -p >= -(n-1) by A50,XREAL_1:24; then
A54: -p +n <= -1+n & -p+n >= -(n-1)+n by XREAL_1:6; then
A55: n-p <= n-'1 & n-p >= 1 by XREAL_0:def 2;
A56: n-p = n-'p by A54,XREAL_0:def 2; then
A57: n-'p in Seg n9 by A55,FINSEQ_1:1;
A58: Seg n9 c= Segm(n9+1) by AFINSQ_1:3;
thus fs1.p = [: (f|n).p, (f|n).(n-p) :] by A50,A49
.= [: f.p, f.(n-p):] by A53,A58,A56,A51,A57,FUNCT_1:49;
end;
thus f.n = Union disjoin fs1 by A49,A42;
end;
uniqueness
proof
let f1, f2 be sequence of bool the_universe_of(X \/ NAT);
assume A59: f1.0 = {};
assume A60: f1.1 = X;
assume A61: for n being Nat st n >= 2 holds
ex fs being FinSequence st len fs = n - 1 &
(for p being Nat st p >= 1 & p <= n - 1 holds
fs.p = [: f1.p, f1.(n-p) :] ) & f1.n = Union disjoin fs;
assume A62: f2.0 = {};
assume A63: f2.1 = X;
assume A64: for n being Nat st n >= 2 holds
ex fs being FinSequence st len fs = n - 1 &
(for p being Nat st p >= 1 & p <= n - 1 holds
fs.p = [: f2.p, f2.(n-p):] ) & f2.n = Union disjoin fs;
{} in (bool the_universe_of(X \/ NAT))^omega by AFINSQ_1:43; then
A65: P[{},F.{}] & {} is XFinSequence of bool the_universe_of(X \/ NAT)
by A10,AFINSQ_1:42;
A66: dom {} = {};
reconsider F as Function of (bool the_universe_of(X \/ NAT))^omega,
bool the_universe_of(X \/ NAT) by A11,A10,FUNCT_2:3;
deffunc FX(XFinSequence of bool the_universe_of(X \/ NAT)) = F.$1;
A67: for n being Nat holds f1.n = FX(f1|n)
proof
let n be Nat;
n = 0 or n + 1 > 0+1 by XREAL_1:6; then
n = 0 or n >= 1 by NAT_1:13; then
n = 0 or n = 1 or n > 1 by XXREAL_0:1; then
A68: n = 0 or n = 1 or n + 1 > 1+1 by XREAL_1:6;
per cases by A68,NAT_1:13;
suppose A69: n=0;
hence f1.n = F.{} by A65,A66,A59
.= FX(f1|n) by A69;
end;
suppose A70: n=1;
1 c= NAT; then
1 c= dom f1 by FUNCT_2:def 1; then
A71: dom(f1|1) = 1 by RELAT_1:62;
f1|1 in (bool the_universe_of(X \/ NAT))^omega by AFINSQ_1:42;
hence f1.n = FX(f1|n) by A70,A71,A10,A60;
end;
suppose A72: n>=2;
n c= NAT; then
n c= dom f1 by FUNCT_2:def 1; then
A73: dom(f1|n) = n by RELAT_1:62;
f1|n in (bool the_universe_of(X \/ NAT))^omega by AFINSQ_1:42; then
consider fs1 be FinSequence such that
A74: len fs1 = n-1 & (for p being Nat st p>=1 & p<=n-1 holds
fs1.p = [: (f1|n).p, (f1|n).(n-p) :] ) &
F.(f1|n) = Union disjoin fs1 by A72,A73,A10;
consider fs2 be FinSequence such that
A75: len fs2 = n - 1 &
(for p being Nat st p >= 1 & p <= n - 1 holds
fs2.p = [: f1.p, f1.(n - p) :] ) &
f1.n = Union disjoin fs2 by A72,A61;
for p being Nat st 1 <= p & p <= len fs1 holds fs1.p = fs2.p
proof
let p be Nat;
assume A76: 1 <= p & p <= len fs1;
then A77: fs1.p = [: (f1|n).p, (f1|n).(n-p) :] by A74;
A78: fs2.p = [: f1.p, f1.(n-p):] by A76,A74,A75;
set n9 = n-'1;
n-1 >= 2-1 by A72,XREAL_1:9; then
A79: n9 = n-1 by XREAL_0:def 2; then
A80: p in Seg n9 by A76,A74,FINSEQ_1:1;
A81: Seg n9 c= Segm(n9+1) by AFINSQ_1:3;
-p <= -1 & -p >= -(n-1) by A76,A74,XREAL_1:24; then
A82: -p +n <= -1+n & -p+n >= -(n-1)+n by XREAL_1:6; then
A83: n-p <= n-'1 & n-p >= 1 by XREAL_0:def 2;
A84: n-p = n-'p by A82,XREAL_0:def 2; then
A85: n-'p in Seg n9 by A83,FINSEQ_1:1;
Seg n9 c= Segm(n9+1) by AFINSQ_1:3; then
(f1|n).(n-p) = f1.(n-p) by A84,A79,A85,FUNCT_1:49;
hence fs1.p = fs2.p by A81,A77,A78,A79,A80,FUNCT_1:49;
end;
hence f1.n = FX(f1|n) by A74,A75,FINSEQ_1:14;
end;
end;
A86: for n being Nat holds f2.n = FX(f2|n)
proof
let n be Nat;
n = 0 or n + 1 > 0+1 by XREAL_1:6; then
n = 0 or n >= 1 by NAT_1:13; then
n = 0 or n = 1 or n > 1 by XXREAL_0:1; then
A87: n = 0 or n = 1 or n + 1 > 1+1 by XREAL_1:6;
per cases by A87,NAT_1:13;
suppose A88: n=0; hence f2.n = F.{} by A65,A66,A62 .= FX(f2|n) by A88;
end;
suppose A89: n=1;
1 c= NAT; then
1 c= dom f2 by FUNCT_2:def 1; then
A90: dom(f2|1) = 1 by RELAT_1:62;
f2|1 in (bool the_universe_of(X \/ NAT))^omega by AFINSQ_1:42;
hence f2.n = FX(f2|n) by A90,A10,A89,A63;
end;
suppose A91: n>=2;
n c= NAT; then
n c= dom f2 by FUNCT_2:def 1; then
A92: dom(f2|n) = n by RELAT_1:62;
f2|n in (bool the_universe_of(X \/ NAT))^omega by AFINSQ_1:42; then
consider fs1 be FinSequence such that
A93: len fs1 = n-1 & (for p being Nat st p>=1 & p<=n-1 holds
fs1.p = [: (f2|n).p, (f2|n).(n-p) :] ) &
F.(f2|n) = Union disjoin fs1 by A91,A92,A10;
consider fs2 be FinSequence such that
A94: len fs2 = n - 1 &
(for p being Nat st p >= 1 & p <= n - 1 holds
fs2.p = [: f2.p, f2.(n-p):] ) & f2.n = Union disjoin fs2 by A91,A64;
for p being Nat st 1 <= p & p <= len fs1 holds fs1.p = fs2.p
proof
let p be Nat;
assume A95: 1 <= p & p <= len fs1; then
A96: fs1.p = [: (f2|n).p, (f2|n).(n-p) :] by A93;
A97: fs2.p = [: f2.p, f2.(n-p):] by A95,A93,A94;
set n9 = n-'1;
n-1 >= 2-1 by A91,XREAL_1:9; then
A98: n9 = n-1 by XREAL_0:def 2; then
A99: p in Seg n9 by A95,A93,FINSEQ_1:1;
A100: Seg n9 c= Segm(n9+1) by AFINSQ_1:3;
-p <= -1 & -p >= -(n-1) by A95,A93,XREAL_1:24; then
A101: -p +n <= -1+n & -p+n >= -(n-1)+n by XREAL_1:6; then
A102: n-p <= n-'1 & n-p >= 1 by XREAL_0:def 2;
A103: n-p = n-'p by A101,XREAL_0:def 2; then
A104: n-'p in Seg n9 by A102,FINSEQ_1:1;
Seg n9 c= Segm(n9+1) by AFINSQ_1:3; then
(f2|n).(n-p) = f2.(n-p) by A104,A103,A98,FUNCT_1:49;
hence fs1.p = fs2.p by A100,A96,A97,A98,A99,FUNCT_1:49;
end;
hence f2.n = FX(f2|n) by A94,A93,FINSEQ_1:14;
end;
end;
f1=f2 from FuncRecursiveUniqu2(A67,A86);
hence thesis;
end;
end;
definition
let X be set;
let n be Nat;
func free_magma(X,n) -> set equals (free_magma_seq X).n;
correctness;
end;
registration
let X be non empty set;
let n be non zero Nat;
cluster free_magma(X,n) -> non empty;
correctness
proof
defpred P[Nat] means $1 = 0 or (free_magma_seq X).$1 <> {};
A1: for k being Nat st for n being Nat st n < k holds P[n] holds P[k]
proof
let k be Nat;
assume A2: for n being Nat st n < k holds P[n];
k = 0 or k + 1 > 0+1 by XREAL_1:6; then
k = 0 or k >= 1 by NAT_1:13; then
k = 0 or k = 1 or k > 1 by XXREAL_0:1; then
A3: k = 0 or k = 1 or k + 1 > 1+1 by XREAL_1:6;
per cases by A3,NAT_1:13;
suppose k=0; hence P[k]; end;
suppose k=1; hence P[k] by Def13; end;
suppose A4: k>=2; then
consider fs be FinSequence such that
A5: len fs = k-1 & (for p being Nat st p>=1 & p<=k-1 holds
fs.p = [: (free_magma_seq X).p, (free_magma_seq X).(k-p) :] ) &
(free_magma_seq X).k = Union disjoin fs by Def13;
A6: 2-1<=k-1 by A4,XREAL_1:9; then
1 in Seg len fs by A5,FINSEQ_1:1; then
A7: 1 in dom fs by FINSEQ_1:def 3; then
A8: 1 in dom disjoin fs by CARD_3:def 3;
A9: (disjoin fs).1 = [:fs.1,{1}:] by A7,CARD_3:def 3;
A10: fs.1=[:(free_magma_seq X).1,(free_magma_seq X).(k-1) :] by A5,A6;
1+1 <= k-1+1 by A4; then
1 < k by NAT_1:13; then
A11: (free_magma_seq X).1 <> {} by A2;
A12: -1+k < 0+k by XREAL_1:8;
k-1 in NAT by A6,INT_1:3; then
reconsider k9=k-1 as Nat;
(free_magma_seq X).k9 <> {} by A12,A6,A2;
then consider x be object such that
A13: x in [:fs.1,{1}:] by A11,A10,XBOOLE_0:def 1;
[:fs.1,{1}:] c= union rng disjoin fs by A9,A8,FUNCT_1:3,ZFMISC_1:74;
hence P[k] by A13,A5,CARD_3:def 4;
end;
end;
for n being Nat holds P[n] from NAT_1:sch 4(A1);
hence thesis;
end;
end;
reserve X for set;
theorem
free_magma(X,0) = {} by Def13;
theorem
free_magma(X,1) = X by Def13;
theorem Th18:
free_magma(X,2) = [:[:X,X:],{1}:]
proof
consider fs be FinSequence such that
A1: len fs = 2-1 & (for p being Nat st p>=1 & p<=2-1 holds
fs.p = [: (free_magma_seq X).p, (free_magma_seq X).(2-p) :] ) &
(free_magma_seq X).2 = Union disjoin fs by Def13;
A2: fs.1 = [: (free_magma_seq X).1, (free_magma_seq X).(2-1) :] by A1
.= [: free_magma(X,1), X :] by Def13 .= [: X, X :] by Def13; then
A3: fs = <* [:X,X:] *> by A1,FINSEQ_1:40;
A4: for y being object
holds y in union rng disjoin fs iff y in [:[:X,X:],{1}:]
proof
let y be object;
hereby
assume y in union rng disjoin fs; then
consider Y be set such that
A5: y in Y & Y in rng disjoin fs by TARSKI:def 4;
consider x be object such that
A6: x in dom disjoin fs & Y = (disjoin fs).x by A5,FUNCT_1:def 3;
A7: x in dom fs by A6,CARD_3:def 3; then
x in Seg 1 by A3,FINSEQ_1:38; then
x = 1 by FINSEQ_1:2,TARSKI:def 1;
hence y in [:[:X,X:],{1}:] by A5,A2,A6,A7,CARD_3:def 3;
end;
assume A8: y in [:[:X,X:],{1}:];
1 in Seg 1 by FINSEQ_1:1; then
A9: 1 in dom fs by A3,FINSEQ_1:38; then
A10: 1 in dom disjoin fs by CARD_3:def 3;
[:[:X,X:],{1}:] = (disjoin fs).1 by A2,A9,CARD_3:def 3; then
[:[:X,X:],{1}:] in rng disjoin fs by A10,FUNCT_1:def 3;
hence y in union rng disjoin fs by A8,TARSKI:def 4;
end;
thus free_magma(X,2) = union rng disjoin fs by A1,CARD_3:def 4
.= [:[:X,X:],{1}:] by A4,TARSKI:2;
end;
theorem
free_magma(X,3) = [:[:X,[:[:X,X:],{1}:]:],{1}:] \/
[:[:[:[:X,X:],{1}:],X:],{2}:]
proof
set X1 = [:[:X,[:[:X,X:],{1}:]:],{1}:];
set X2 = [:[:[:[:X,X:],{1}:],X:],{2}:];
consider fs be FinSequence such that
A1: len fs = 3-1 & (for p being Nat st p>=1 & p<=3-1 holds
fs.p = [: (free_magma_seq X).p, (free_magma_seq X).(3-p) :] ) &
(free_magma_seq X).3 = Union disjoin fs by Def13;
A2: fs.1 = [: free_magma(X,1), free_magma(X,2) :] by A1
.= [: free_magma(X,1), [:[:X,X:],{1}:] :] by Th18
.= [:X,[:[:X,X:],{1}:]:] by Def13;
A3: fs.2 = [: (free_magma_seq X).2, (free_magma_seq X).(3-2) :] by A1
.= [: free_magma(X,2), X :] by Def13 .= [:[:[:X,X:],{1}:],X:] by Th18;
A4: for y being object
holds y in union rng disjoin fs iff y in X1 or y in X2
proof
let y be object;
hereby
assume y in union rng disjoin fs; then
consider Y be set such that
A5: y in Y & Y in rng disjoin fs by TARSKI:def 4;
consider x be object such that
A6: x in dom disjoin fs & Y = (disjoin fs).x by A5,FUNCT_1:def 3;
A7: x in dom fs by A6,CARD_3:def 3; then
x in {1,2} by A1,FINSEQ_1:2,def 3; then
x = 1 or x = 2 by TARSKI:def 2;
hence y in X1 or y in X2 by A2,A3,A5,A6,A7,CARD_3:def 3;
end;
assume A8: y in X1 or y in X2;
1 in Seg 2 & 2 in Seg 2 by FINSEQ_1:1; then
A9: 1 in dom fs & 2 in dom fs by A1,FINSEQ_1:def 3; then
A10: 1 in dom disjoin fs & 2 in dom disjoin fs by CARD_3:def 3;
X1 = (disjoin fs).1 & X2 = (disjoin fs).2 by A2,A3,A9,CARD_3:def 3; then
X1 in rng disjoin fs & X2 in rng disjoin fs by A10,FUNCT_1:def 3;
hence y in union rng disjoin fs by A8,TARSKI:def 4;
end;
thus free_magma(X,3) = union rng disjoin fs by A1,CARD_3:def 4
.= [:[:X,[:[:X,X:],{1}:]:],{1}:] \/ [:[:[:[:X,X:],{1}:],X:],{2}:]
by A4,XBOOLE_0:def 3;
end;
reserve x,y,Y for set;
reserve n,m,p for Nat;
theorem Th20:
n >= 2 implies ex fs being FinSequence st len fs = n-1 &
(for p st p>=1 & p<=n-1 holds
fs.p = [: free_magma(X,p), free_magma(X,n-'p) :] ) &
free_magma(X,n) = Union disjoin fs
proof
assume n >= 2; then
consider fs be FinSequence such that
A1: len fs = n-1 & (for p st p>=1 & p<=n-1 holds
fs.p = [: (free_magma_seq X).p, (free_magma_seq X).(n-p) :] ) &
(free_magma_seq X).n = Union disjoin fs by Def13;
take fs;
thus len fs = n-1 by A1;
thus for p st p>=1 & p<=n-1
holds fs.p = [: free_magma(X,p), free_magma(X,n-'p) :]
proof
let p;
assume A2: p>=1 & p<=n-1; then
-p <= -1 & -p >= -(n-1) by XREAL_1:24; then
-p +n <= -1+n & -p+n >= -(n-1)+n by XREAL_1:6;
then n-p=n-'p by XREAL_0:def 2;
hence thesis by A2,A1;
end;
thus free_magma(X,n) = Union disjoin fs by A1;
end;
theorem Th21:
n >= 2 & x in free_magma(X,n) implies ex p,m st x`2 = p & 1<=p & p<=n-1 &
x`1`1 in free_magma(X,p) & x`1`2 in free_magma(X,m) & n = p + m &
x in [:[:free_magma(X,p),free_magma(X,m):],{p}:]
proof
assume A1: n>=2;
assume A2: x in free_magma(X,n);
consider fs be FinSequence such that
A3: len fs = n-1 and
A4: (for p st p>=1 & p<=n-1 holds
fs.p = [:(free_magma_seq X).p,(free_magma_seq X).(n-p) :] ) and
A5: (free_magma_seq X).n = Union disjoin fs by A1,Def13;
x in union rng disjoin fs by A2,A5,CARD_3:def 4; then
consider Y be set such that
A6: x in Y & Y in rng disjoin fs by TARSKI:def 4;
consider p be object such that
A7: p in dom disjoin fs & Y = (disjoin fs).p by A6,FUNCT_1:def 3;
A8: p in dom fs by A7,CARD_3:def 3; then
reconsider p as Nat;
A9: p in Seg len fs by A8,FINSEQ_1:def 3; then
A10: 1 <= p & p <= len fs by FINSEQ_1:1; then
A11: fs.p = [:(free_magma_seq X).p,(free_magma_seq X).(n-p):] by A3,A4;
then x in [:[:(free_magma_seq X).p,(free_magma_seq X).(n-p):],{p}:]
by A6,A7,A8,CARD_3:def 3; then
A12: x`1 in [:(free_magma_seq X).p,(free_magma_seq X).(n-p):] &
x`2 in {p} by MCART_1:10;
-p >= -(n-1) by A10,A3,XREAL_1:24; then
-p+n >= -(n-1)+n by XREAL_1:7; then
n-p in NAT by INT_1:3; then
reconsider m = n-p as Nat;
take p,m;
thus thesis by A3,A9,A6,A11,A7,A8,A12,CARD_3:def 3,FINSEQ_1:1,MCART_1:10
,TARSKI:def 1;
end;
theorem Th22:
x in free_magma(X,n) & y in free_magma(X,m) implies
[[x,y],n] in free_magma(X,n+m)
proof
assume A1: x in free_magma(X,n);
assume A2: y in free_magma(X,m);
per cases;
suppose n=0 or m=0; hence thesis by Def13,A1,A2; end;
suppose n<>0 & m<>0; then
A3: n>=0+1 & m>=0+1 by NAT_1:13; then
n+m>=1+1 by XREAL_1:7; then
consider fs be FinSequence such that
A4: len fs = (n+m)-1 & (for p st p>=1 & p<=(n+m)-1 holds
fs.p = [: (free_magma_seq X).p,(free_magma_seq X).((n+m)-p) :] )
& (free_magma_seq X).(n+m) = Union disjoin fs by Def13;
1-1 <= m-1 by A3,XREAL_1:9; then
A5: 0+n <= (m-1)+n by XREAL_1:7;
then fs.n = [: (free_magma_seq X).n,(free_magma_seq X).((n+m)-n) :]
by A4,A3
.= [: (free_magma_seq X).n, (free_magma_seq X).m :];
then A6: [x,y] in fs.n by A1,A2,ZFMISC_1:def 2;
n in {n} by TARSKI:def 1; then
A7: [[x,y],n] in [:fs.n, {n}:] by A6,ZFMISC_1:def 2;
n in Seg len fs by A4,A3,A5,FINSEQ_1:1; then
A8: n in dom fs by FINSEQ_1:def 3; then
A9: (disjoin fs).n = [:fs.n,{n}:] by CARD_3:def 3;
n in dom disjoin fs by A8,CARD_3:def 3; then
[:fs.n,{n}:] in rng disjoin fs by A9,FUNCT_1:3; then
[[x,y],n] in union rng disjoin fs by A7,TARSKI:def 4;
hence [[x,y],n] in free_magma(X,n+m) by A4,CARD_3:def 4;
end;
end;
theorem Th23:
X c= Y implies free_magma(X,n) c= free_magma(Y,n)
proof
defpred P[Nat] means X c= Y implies free_magma(X,$1) c= free_magma(Y,$1);
A1: for k being Nat st for n being Nat st n < k holds P[n] holds P[k]
proof
let k be Nat;
assume A2: for n being Nat st n < k holds P[n];
thus X c= Y implies free_magma(X,k) c= free_magma(Y,k)
proof
assume A3: X c= Y;
k = 0 or k + 1 > 0+1 by XREAL_1:6; then
k = 0 or k >= 1 by NAT_1:13; then
k = 0 or k = 1 or k > 1 by XXREAL_0:1; then
A4: k = 0 or k = 1 or k + 1 > 1+1 by XREAL_1:6;
per cases by A4,NAT_1:13;
suppose k=0; then free_magma(X,k) = {} & free_magma(Y,k) = {} by Def13;
hence free_magma(X,k) c= free_magma(Y,k);
end;
suppose k=1; then free_magma(X,k) = X & free_magma(Y,k) = Y by Def13;
hence free_magma(X,k) c= free_magma(Y,k) by A3;
end;
suppose A5: k>=2;
for x being object st x in free_magma(X,k) holds x in free_magma(Y,k)
proof
let x be object;
assume x in free_magma(X,k); then
consider p,m be Nat such that
A6: x`2 = p & 1<=p & p<=k-1 &
x`1`1 in free_magma(X,p) & x`1`2 in free_magma(X,m) & k = p + m &
x in [:[:free_magma(X,p),free_magma(X,m):],{p}:] by A5,Th21;
consider fs be FinSequence such that
A7: len fs = k-1 & (for p being Nat st p>=1 & p<=k-1 holds
fs.p = [: free_magma(Y,p), free_magma(Y,k-'p) :]) &
free_magma(Y,k) = Union disjoin fs by A5,Th20;
A8: fs.p = [: free_magma(Y,p), free_magma(Y,k-'p) :] by A6,A7;
A9: x`1 in [:free_magma(X,p),free_magma(X,m):] & x`2 in {p}
by A6,MCART_1:10;
A10: x = [x`1,x`2] by A6,MCART_1:21;
A11: x`1 = [x`1`1,x`1`2] by A9,MCART_1:21;
p+1 <= k-1+1 by A6,XREAL_1:7; then
A12: p<k by NAT_1:13; then
A13: free_magma(X,p) c= free_magma(Y,p) by A2,A3;
p-p<k-p by A12,XREAL_1:14; then
A14: k-'p = m by A6,XREAL_0:def 2;
p+m>0+m by A6,XREAL_1:8; then
free_magma(X,m) c= free_magma(Y,k-'p) by A6,A2,A3,A14; then
x`1 in [:free_magma(Y,p),free_magma(Y,k-'p):]
by A6,A11,A13,ZFMISC_1:def 2; then
A15: x in [:fs.p,{p}:] by A8,A10,A9,ZFMISC_1:def 2;
p in Seg len fs by A6,A7,FINSEQ_1:1; then
A16: p in dom fs by FINSEQ_1:def 3; then
A17: (disjoin fs).p = [:fs.p,{p}:] by CARD_3:def 3;
p in dom disjoin fs by A16,CARD_3:def 3; then
[:fs.p,{p}:] in rng disjoin fs by A17,FUNCT_1:3; then
x in union rng disjoin fs by A15,TARSKI:def 4;
hence x in free_magma(Y,k) by A7,CARD_3:def 4;
end;
hence free_magma(X,k) c= free_magma(Y,k);
end;
end;
end;
for k being Nat holds P[k] from NAT_1:sch 4(A1);
hence thesis;
end;
definition
let X be set;
func free_magma_carrier X -> set
equals Union disjoin((free_magma_seq X)|NATPLUS);
correctness;
end;
Lm1: n>0 implies [:free_magma(X,n),{n}:] c= free_magma_carrier X
proof
assume A1: n > 0;
let x be object;
assume A2: x in [:free_magma(X,n),{n}:];
n in NAT by ORDINAL1:def 12; then
A3: n in dom free_magma_seq X by FUNCT_2:def 1;
n in NATPLUS by A1,NAT_LAT:def 6; then
A4: n in dom ((free_magma_seq X)|NATPLUS) by A3,RELAT_1:57; then
A5: (disjoin((free_magma_seq X)|NATPLUS)).n
= [:((free_magma_seq X)|NATPLUS).n,{n}:] by CARD_3:def 3
.= [:(free_magma_seq X).n,{n}:] by A4,FUNCT_1:47;
n in dom disjoin((free_magma_seq X)|NATPLUS) by A4,CARD_3:def 3; then
[:free_magma(X,n),{n}:] in rng disjoin((free_magma_seq X)|NATPLUS)
by A5,FUNCT_1:3;
then
x in union rng disjoin((free_magma_seq X)|NATPLUS) by A2,TARSKI:def 4;
hence x in free_magma_carrier X by CARD_3:def 4;
end;
theorem Th24:
X = {} iff free_magma_carrier X = {}
proof
hereby
assume A1: X = {};
defpred P[Nat] means (free_magma_seq X).$1 = {};
A2: for k being Nat st for n being Nat st n < k holds P[n] holds P[k]
proof
let k be Nat;
assume A3: for n being Nat st n < k holds P[n];
k = 0 or k + 1 > 0+1 by XREAL_1:6; then
k = 0 or k >= 1 by NAT_1:13; then
k = 0 or k = 1 or k > 1 by XXREAL_0:1; then
A4: k = 0 or k = 1 or k + 1 > 1+1 by XREAL_1:6;
per cases by A4,NAT_1:13;
suppose k=0; hence P[k] by Def13; end;
suppose k=1; hence P[k] by A1,Def13; end;
suppose k>=2; then
consider fs be FinSequence such that
A5: len fs = k-1 & (for p being Nat st p>=1 & p<=k-1 holds
fs.p = [: (free_magma_seq X).p, (free_magma_seq X).(k-p) :] ) &
(free_magma_seq X).k = Union disjoin fs by Def13;
for y being set st y in rng disjoin fs holds y c= {}
proof
let y be set;
assume y in rng disjoin fs; then
consider p be object such that
A6: p in dom disjoin fs & y = (disjoin fs).p by FUNCT_1:def 3;
A7: p in dom fs by A6,CARD_3:def 3; then
A8: p in Seg len fs by FINSEQ_1:def 3;
reconsider p as Nat by A7;
A9: p >= 1 & p <= k-1 by A5,A8,FINSEQ_1:1; then
p+1 <= k-1+1 by XREAL_1:7; then
p < k by NAT_1:13; then
A10: (free_magma_seq X).p = {} by A3;
A11: fs.p = [:(free_magma_seq X).p,(free_magma_seq X).(k-p):]
by A5,A9
.= {} by A10;
(disjoin fs).p = [:fs.p,{p}:] by A7,CARD_3:def 3
.= {} by A11;
hence y c= {} by A6;
end; then
union rng disjoin fs c= {} by ZFMISC_1:76;
hence P[k] by A5,CARD_3:def 4;
end;
end;
A12: for n being Nat holds P[n] from NAT_1:sch 4(A2);
for Y being set st Y in rng disjoin((free_magma_seq X)|NATPLUS)
holds Y c= {}
proof
let Y be set;
assume Y in rng disjoin((free_magma_seq X)|NATPLUS); then
consider n be object such that
A13: n in dom disjoin((free_magma_seq X)|NATPLUS) &
Y = (disjoin((free_magma_seq X)|NATPLUS)).n by FUNCT_1:def 3;
A14: n in dom((free_magma_seq X)|NATPLUS) by A13,CARD_3:def 3; then
reconsider n as Nat;
A15: n in dom ((free_magma_seq X)|NATPLUS) by A13,CARD_3:def 3;
(disjoin((free_magma_seq X)|NATPLUS)).n
= [:((free_magma_seq X)|NATPLUS).n,{n}:] by A14,CARD_3:def 3
.= [:(free_magma_seq X).n,{n}:] by A15,FUNCT_1:47
.= [:{},{n}:] by A12 .= {};
hence Y c= {} by A13;
end; then
union rng disjoin((free_magma_seq X)|NATPLUS) c= {} by ZFMISC_1:76;
hence free_magma_carrier X = {} by CARD_3:def 4;
end;
assume A16: free_magma_carrier X = {};
[:free_magma(X,1),{1}:] c= free_magma_carrier X by Lm1;
hence X = {} by A16;
end;
registration
let X be empty set;
cluster free_magma_carrier X -> empty;
correctness by Th24;
end;
registration
let X be non empty set;
cluster free_magma_carrier X -> non empty;
correctness by Th24;
let w be Element of free_magma_carrier X;
cluster w`2 -> non zero natural for number;
correctness
proof
w in free_magma_carrier X; then
w in union rng disjoin((free_magma_seq X)|NATPLUS) by CARD_3:def 4; then
consider Y be set such that
A1: w in Y & Y in rng disjoin((free_magma_seq X)|NATPLUS) by TARSKI:def 4;
consider n be object such that
A2: n in dom disjoin((free_magma_seq X)|NATPLUS) &
Y = disjoin((free_magma_seq X)|NATPLUS).n by A1,FUNCT_1:def 3;
A3: n in dom((free_magma_seq X)|NATPLUS) by A2,CARD_3:def 3; then
n in NATPLUS by RELAT_1:57; then
reconsider n as non zero Nat;
w in [:((free_magma_seq X)|NATPLUS).n,{n}:] by A2,A1,A3,CARD_3:def 3; then
w`2 in {n} by MCART_1:10;
hence thesis by TARSKI:def 1;
end;
end;
theorem Th25:
for X being non empty set, w being Element of free_magma_carrier X
holds w in [:free_magma(X,w`2),{w`2}:]
proof
let X be non empty set;
let w be Element of free_magma_carrier X;
w in free_magma_carrier X; then
w in union rng disjoin((free_magma_seq X)|NATPLUS) by CARD_3:def 4; then
consider Y be set such that
A1: w in Y & Y in rng disjoin((free_magma_seq X)|NATPLUS) by TARSKI:def 4;
consider n be object such that
A2: n in dom disjoin((free_magma_seq X)|NATPLUS) &
Y = disjoin((free_magma_seq X)|NATPLUS).n by A1,FUNCT_1:def 3;
A3: n in dom((free_magma_seq X)|NATPLUS) by A2,CARD_3:def 3; then
A4: ((free_magma_seq X)|NATPLUS).n = (free_magma_seq X).n by FUNCT_1:47;
reconsider n as Nat by A3;
w in [:((free_magma_seq X)|NATPLUS).n,{n}:] by A2,A1,A3,CARD_3:def 3; then
w`2 in {n} by MCART_1:10; then
w`2 = n by TARSKI:def 1;
hence w in [:free_magma(X,w`2),{w`2}:] by A4,A2,A1,A3,CARD_3:def 3;
end;
theorem Th26:
for X being non empty set, v,w being Element of free_magma_carrier X
holds [[[v`1,w`1],v`2],v`2+w`2] is Element of free_magma_carrier X
proof
let X be non empty set;
let v,w be Element of free_magma_carrier X;
v in [:free_magma(X,v`2),{v`2}:] by Th25; then
A1: v`1 in free_magma(X,v`2) by MCART_1:10;
w in [:free_magma(X,w`2),{w`2}:] by Th25; then
w`1 in free_magma(X,w`2) by MCART_1:10; then
A2: [[v`1,w`1],v`2] in free_magma(X,v`2+w`2) by A1,Th22;
A3: v`2 + w`2 in {v`2 + w`2} by TARSKI:def 1;
set z = [[[v`1,w`1],v`2],v`2+w`2];
A4: z`1 in free_magma(X,v`2+w`2) by A2;
z`2 in {v`2 + w`2} by A3; then
A5: z in [:free_magma(X,v`2+w`2),{v`2+w`2}:] by A4,ZFMISC_1:def 2;
[:free_magma(X,v`2 + w`2),{v`2 + w`2}:] c= free_magma_carrier X by Lm1;
hence thesis by A5;
end;
theorem Th27:
X c= Y implies free_magma_carrier X c= free_magma_carrier Y
proof
assume A1: X c= Y;
per cases;
suppose X = {}; then
free_magma_carrier X = {};
hence free_magma_carrier X c= free_magma_carrier Y;
end;
suppose A2: X <> {};
let x be object;
assume A3: x in free_magma_carrier X;
reconsider X9=X as non empty set by A2;
reconsider w=x as Element of free_magma_carrier X9 by A3;
A4: w in [:free_magma(X9,w`2),{w`2}:] by Th25; then
A5: w`1 in free_magma(X9,w`2) & w`2 in {w`2} by MCART_1:10;
reconsider Y9=Y as non empty set by A2,A1;
A6: free_magma(X9,w`2) c= free_magma(Y9,w`2) by A1,Th23;
w = [w`1,w`2] by A4,MCART_1:21; then
A7: w in [:free_magma(Y9,w`2),{w`2}:] by A6,A5,ZFMISC_1:def 2;
[:free_magma(Y9,w`2),{w`2}:] c= free_magma_carrier Y9 by Lm1;
hence x in free_magma_carrier Y by A7;
end;
end;
theorem
n>0 implies [:free_magma(X,n),{n}:] c= free_magma_carrier X by Lm1;
definition
let X be set;
func free_magma_mult X -> BinOp of free_magma_carrier X means :Def16:
for v,w being Element of free_magma_carrier X, n,m st n = v`2 & m = w`2
holds it.(v,w) = [[[v`1,w`1],v`2],n+m]
if X is non empty otherwise it = {};
correctness
proof
A1: X is non empty implies ex f being BinOp of free_magma_carrier X st
for v,w being Element of free_magma_carrier X, n,m st n = v`2 & m = w`2
holds f.(v,w) = [[[v`1,w`1],v`2],n+m]
proof
assume A2: X is non empty;
defpred P[set,set,set] means for n,m st n=$1`2 & m=$2`2
holds $3 = [[[$1`1,$2`1],$1`2],n+m];
reconsider Y = free_magma_carrier X as non empty set by A2;
A3: for x being Element of Y for y being Element of Y
ex z being Element of Y st P[x,y,z]
proof
let x be Element of Y;
let y be Element of Y;
reconsider X9=X as non empty set by A2;
reconsider v=x as Element of free_magma_carrier X9;
reconsider w=y as Element of free_magma_carrier X9;
reconsider z=[[[v`1,w`1],v`2],v`2+w`2] as Element of Y by Th26;
take z;
thus thesis;
end;
consider f be Function of [:Y,Y:],Y such that
A4: for x being Element of Y for y being Element of Y
holds P[x,y,f.(x,y)] from BINOP_1:sch 3(A3);
reconsider f as BinOp of free_magma_carrier X;
take f;
thus thesis by A4;
end;
A5: X is empty implies ex f being BinOp of free_magma_carrier X st f = {}
proof
assume A6: X is empty; then
A7: free_magma_carrier X = {};
{} c= [:{} qua set,{} qua set:]; then
reconsider f = {} as Relation of [:{} qua set,{} qua set:],{};
([:{} qua set,{} qua set:] = {} implies {}={}) &
dom f = [:{} qua set,{} qua set:]; then
reconsider f = {} as BinOp of {};
for v,w being Element of free_magma_carrier X, n,m st n = v`2 & m = w`2 &
v in free_magma_carrier X & w in free_magma_carrier X holds
f.(v,w) = [[[v`1,w`1],v`2],n+m] by A6;
hence thesis by A7;
end;
now
let f1, f2 be BinOp of free_magma_carrier X;
thus X is non empty & ( for v, w being Element of free_magma_carrier X,
n,m st n = v`2 & m = w`2 holds f1.(v,w) = [[[v`1,w`1],v`2],n+m])
& (for v, w being Element of free_magma_carrier X,
n,m st n = v`2 & m = w`2 holds f2.(v,w) = [[[v`1,w`1],v`2],n+m])
implies f1 = f2
proof
assume A8: X is non empty;
assume A9: for v, w being Element of free_magma_carrier X,
n,m st n = v`2 & m = w`2 holds f1.(v,w) = [[[v`1,w`1],v`2],n+m];
assume A10: for v, w being Element of free_magma_carrier X,
n,m st n = v`2 & m = w`2 holds f2.(v,w) = [[[v`1,w`1],v`2],n+m];
for v,w being Element of free_magma_carrier X holds f1.(v,w) = f2.(v,w)
proof
let v,w be Element of free_magma_carrier X;
set n = v`2, m = w`2;
reconsider n,m as Nat by A8;
thus f1.(v,w) = [[[v`1,w`1],v`2],n+m] by A9 .= f2.(v,w) by A10;
end;
hence f1 = f2 by BINOP_1:2;
end;
assume X is empty & f1 = {} & f2 = {}; hence thesis;
end;
hence thesis by A1,A5;
end;
end;
:: Ch I ?7.1 Algebra I Bourbaki
definition
let X be set;
func free_magma X -> multMagma equals
multMagma(# free_magma_carrier X, free_magma_mult X #);
correctness;
end;
registration
let X be set;
cluster free_magma X -> strict;
correctness;
end;
registration
let X be empty set;
cluster free_magma X -> empty;
correctness;
end;
registration
let X be non empty set;
cluster free_magma X -> non empty;
correctness;
let w be Element of free_magma X;
cluster w`2 -> non zero natural for number;
correctness;
end;
theorem
for X being set, S being Subset of X
holds free_magma S is multSubmagma of free_magma X
proof
let X be set;
let S be Subset of X;
A1: the carrier of free_magma S c= the carrier of free_magma X by Th27;
reconsider A = the carrier of free_magma S as set;
A2: (the multF of free_magma X) | [: A, A :]
= (the multF of free_magma X)||the carrier of free_magma S by REALSET1:def 2;
per cases;
suppose A3: S is empty;
then A4: the carrier of free_magma S = {};
the multF of free_magma S = (the multF of free_magma X) | {} by A3
.= (the multF of free_magma X) | [: A, A :] by A4;
hence thesis by A2,A1,Def9;
end;
suppose A5: S is not empty;
then A6: dom the multF of free_magma S = [:A,A:] by FUNCT_2:def 1;
A7: X is non empty by A5;
[:A,A:] c= [: free_magma_carrier X, free_magma_carrier X:]
by A1,ZFMISC_1:96; then
[:A,A:] c= dom the multF of free_magma X by A7,FUNCT_2:def 1;
then A8: dom the multF of free_magma S
= dom((the multF of free_magma X)||the carrier of free_magma S)
by A6,A2,RELAT_1:62;
for z being object st z in dom the multF of free_magma S holds
(the multF of free_magma S).z
=((the multF of free_magma X)||the carrier of free_magma S).z
proof
let z be object;
assume A9: z in dom the multF of free_magma S;
then consider x,y being object such that
A10: x in A & y in A & z=[x,y] by ZFMISC_1:def 2;
reconsider x,y as Element of free_magma_carrier S by A10;
reconsider n=x`2,m=y`2 as Nat by A5;
reconsider x9=x,y9=y as Element of free_magma_carrier X by A10,A1;
(the multF of free_magma S).z
= (the multF of free_magma S).(x,y) by A10,BINOP_1:def 1
.= [[[x`1,y`1],x`2],n+m] by A5,Def16
.= (free_magma_mult X).(x9,y9) by A7,Def16
.= (the multF of free_magma X).z by A10,BINOP_1:def 1
.= ((the multF of free_magma X)|[:A,A:]).z by A9,FUNCT_1:49;
hence thesis by REALSET1:def 2;
end;
then the multF of free_magma S
= (the multF of free_magma X)||the carrier of free_magma S
by A8,FUNCT_1:2;
hence free_magma S is multSubmagma of free_magma X by A1,Def9;
end;
end;
definition
let X be set;
let w be Element of free_magma X;
func length w -> Nat equals :Def18:
w`2 if X is non empty otherwise 0;
correctness;
end;
theorem Th30:
X = {w`1 where w is Element of free_magma X: length w = 1}
proof
for x being object holds x in X iff
x in {w`1 where w is Element of free_magma X: length w = 1}
proof
let x be object;
hereby
assume A1: x in X; then
A2: x in free_magma(X,1) by Def13;
1 in {1} by TARSKI:def 1; then
A3: [x,1] in [:free_magma(X,1),{1}:] by A2,ZFMISC_1:def 2;
[:free_magma(X,1),{1}:] c= free_magma_carrier X by Lm1; then
reconsider w9 = [x,1] as Element of free_magma X by A3;
1 = [x,1]`2; then
A4: length w9 = 1 by A1,Def18;
x = [x,1]`1;
hence x in {w`1 where w is Element of free_magma X: length w = 1} by A4;
end;
assume x in {w`1 where w is Element of free_magma X: length w = 1}; then
consider w be Element of free_magma X such that
A5: x = w`1 & length w = 1;
A6: w`2 = 1 by A5,Def18;
per cases;
suppose X is non empty; then
w in [:free_magma(X,1),{1}:] by A6,Th25; then
w in [:X,{1}:] by Def13;
hence x in X by A5,MCART_1:10;
end;
suppose X is empty; hence thesis by A5,Def18; end;
end;
hence thesis by TARSKI:2;
end;
reserve v,v1,v2,w,w1,w2 for Element of free_magma X;
theorem Th31:
X is non empty implies v*w = [[[v`1,w`1],v`2],length v + length w]
proof
assume A1: X is non empty; then
length v = v`2 & length w = w`2 by Def18;
hence thesis by A1,Def16;
end;
theorem Th32:
X is non empty implies v = [v`1,v`2] & length v >= 1
proof
assume X is non empty; then
reconsider X9=X as non empty set;
reconsider v9=v as Element of free_magma X9;
v9 in [:free_magma(X,v9`2),{v9`2}:] by Th25; then
ex x,y being object st x in free_magma(X,v9`2) &
y in {v9`2} & v9=[x,y] by ZFMISC_1:def 2;
hence v = [v`1,v`2];
reconsider v99=v9 as Element of free_magma_carrier X9;
v99`2 > 0; then
length v9 > 0 by Def18; then
length v9+1 > 0+1 by XREAL_1:6;
hence thesis by NAT_1:13;
end;
theorem
length(v*w) = length v + length w
proof
set vw = v*w;
per cases;
suppose A1: X is non empty; then
v*w = [[[v`1,w`1],v`2],length v + length w] by Th31;
hence length(v*w) = [[[v`1,w`1],v`2],length v + length w]`2 by A1,Def18
.= length v + length w;
end;
suppose A2: X is empty;
hence length(v*w) = 0 by Def18
.= length v + 0 by A2,Def18
.= length v + length w by A2,Def18;
end;
end;
theorem Th34:
length w >= 2 implies
ex w1,w2 st w = w1*w2 & length w1 < length w & length w2 < length w
proof
assume A1: length w >= 2; then
reconsider X9=X as non empty set by Def18;
reconsider w9=w as Element of free_magma X9;
A2: w9 in [:free_magma(X,w9`2),{w9`2}:] by Th25;
set n = length w;
A3: n = w9`2 by Def18;
consider fs be FinSequence such that
A4: len fs = n-1 and
A5: (for p being Nat st p>=1 & p<=n-1 holds
fs.p = [:(free_magma_seq X).p,(free_magma_seq X).(n-p) :] ) and
A6: (free_magma_seq X).n = Union disjoin fs by A1,Def13;
w9`1 in (free_magma_seq X).n by A3,A2,MCART_1:10; then
w9`1 in union rng disjoin fs by A6,CARD_3:def 4; then
consider Y be set such that
A7: w9`1 in Y & Y in rng disjoin fs by TARSKI:def 4;
consider p be object such that
A8: p in dom disjoin fs & Y = (disjoin fs).p by A7,FUNCT_1:def 3;
A9: p in dom fs by A8,CARD_3:def 3; then
reconsider p as Nat;
A10: p in Seg len fs by A9,FINSEQ_1:def 3; then
A11: 1 <= p & p <= len fs by FINSEQ_1:1; then
fs.p = [:(free_magma_seq X).p,(free_magma_seq X).(n-p):] by A4,A5;
then A12: w9`1 in [:[:(free_magma_seq X).p,(free_magma_seq X).(n-p):],{p}:]
by A7,A8,A9,CARD_3:def 3; then
A13: w9`1`1 in [:(free_magma_seq X).p,(free_magma_seq X).(n-p):] &
w9`1`2 in {p} by MCART_1:10; then
A14: w9`1`1`1 in (free_magma_seq X).p & w9`1`1`2 in (free_magma_seq X).(n-p)
by MCART_1:10;
-p >= -(n-1) by A11,A4,XREAL_1:24; then
A15: -p+n >= -(n-1)+n by XREAL_1:7; then
n-p in NAT by INT_1:3; then
reconsider m = n-p as Nat;
set w19 = [w9`1`1`1,p];
set w29 = [w9`1`1`2,m];
p in {p} by TARSKI:def 1; then
A16: w19 in [: free_magma(X,p),{p}:] by A14,ZFMISC_1:def 2;
m in {m} by TARSKI:def 1; then
A17: w29 in [: free_magma(X,m),{m}:] by A14,ZFMISC_1:def 2;
[: free_magma(X,p),{p}:] c= free_magma_carrier X by A11,Lm1; then
reconsider w19 as Element of free_magma_carrier X by A16;
[: free_magma(X,m),{m}:] c= free_magma_carrier X by A15,Lm1; then
reconsider w29 as Element of free_magma_carrier X by A17;
reconsider w1=w19,w2=w29 as Element of free_magma X;
A18: length w1 = [w9`1`1`1,p]`2 by Def18 .= p;
A19: length w2 = [w9`1`1`2,m]`2 by Def18 .= m;
ex x,y being object
st x in [:(free_magma_seq X).p,(free_magma_seq X).(n-p):] &
y in {p} & w9`1=[x,y] by A12,ZFMISC_1:def 2; then
A20: w9`1 = [w9`1`1,p] by TARSKI:def 1;
A21: ex x,y being object st x in (free_magma_seq X).p &
y in (free_magma_seq X).(n-p) & w9`1`1=[x,y] by A13,ZFMISC_1:def 2;
take w1,w2;
ex x,y being object st x in free_magma(X,w9`2) &
y in {w9`2} & w9=[x,y] by A2,ZFMISC_1:def 2;
hence w = [[w9`1`1,p],n] by A20,Def18
.= [[w9`1`1,w1`2],length w1 + length w2] by A18,A19
.= [[[w9`1`1`1,w9`1`1`2],w1`2],length w1 + length w2] by A21
.= [[[w1`1,w2`1],w1`2],length w1 + length w2]
.= w1*w2 by Th31;
p <= (n-1) by A10,A4,FINSEQ_1:1; then
p+1 <= (n-1)+1 by XREAL_1:7;
hence length w1 < length w by A18,NAT_1:13;
-1 >= -p by A11,XREAL_1:24; then
-1+(n+1) >= -p+(n+1) by XREAL_1:7; then
n >= m+1;
hence length w2 < length w by A19,NAT_1:13;
end;
theorem
v1*v2 = w1*w2 implies v1 = w1 & v2 = w2
proof
assume A1: v1*v2 = w1*w2;
per cases;
suppose A2: X is non empty; then
v1*v2 = [[[v1`1,v2`1],v1`2],length v1 + length v2] &
w1*w2 = [[[w1`1,w2`1],w1`2],length w1 + length w2] by Th31; then
A3: [[v1`1,v2`1],v1`2] = [[w1`1,w2`1],w1`2] &
length v1 + length v2 = length w1 + length w2 by A1,XTUPLE_0:1; then
A4: [v1`1,v2`1] = [w1`1,w2`1] & v1`2 = w1`2 by XTUPLE_0:1;
length v1 = v1`2 by A2,Def18 .= length w1 by A2,A4,Def18; then
v2`2 = length w2 by A2,A3,Def18; then
A5: v2`2 = w2`2 by A2,Def18;
thus v1 = [v1`1,v1`2] by A2,Th32 .= [w1`1,w1`2] by A4,XTUPLE_0:1
.= w1 by A2,Th32;
thus v2 = [v2`1,v2`2] by A2,Th32 .= [w2`1,w2`2] by A5,A4,XTUPLE_0:1
.= w2 by A2,Th32;
end;
suppose X is empty; then
v1 = {} & w1 = {} & v2 = {} & w2 = {} by SUBSET_1:def 1;
hence thesis;
end;
end;
definition
let X be set;
let n be Nat;
func canon_image(X,n) -> Function of free_magma(X,n),free_magma X means
:Def19:
for x st x in dom it holds it.x = [x,n] if n > 0 otherwise it = {};
correctness
proof
A1: n > 0 implies ex f being Function of free_magma(X,n),free_magma X st
for x st x in dom f holds f.x = [x,n]
proof
assume A2: n > 0;
deffunc F(object) = [$1,n];
A3: for x being object st x in free_magma(X,n)
holds F(x) in the carrier of free_magma X
proof
let x be object;
assume A4: x in free_magma(X,n);
n in {n} by TARSKI:def 1; then
A5: F(x) in [:free_magma(X,n),{n}:] by A4,ZFMISC_1:def 2;
[:free_magma(X,n),{n}:] c= free_magma_carrier X by A2,Lm1;
hence F(x) in the carrier of free_magma X by A5;
end;
consider f be Function of free_magma(X,n),the carrier of free_magma X
such that
A6: for x being object st x in free_magma(X,n) holds f.x = F(x)
from FUNCT_2:sch 2(A3);
take f;
let x;
assume x in dom f;
hence f.x = [x,n] by A6;
end;
A7: not n > 0 implies
ex f being Function of free_magma(X,n),free_magma X st f = {}
proof
assume not n > 0; then
n = 0; then
A8: free_magma(X,n) = {} by Def13;
set f = {};
A9: dom f = {};
rng f c= the carrier of free_magma X; then
reconsider f as Function of free_magma(X,n),free_magma X
by A8,A9,FUNCT_2:2;
take f;
thus f = {};
end;
for f1,f2 being Function of free_magma(X,n),free_magma X holds n > 0 &
(for x st x in dom f1 holds f1.x = [x,n] ) &
(for x st x in dom f2 holds f2.x = [x,n] ) implies f1 = f2
proof
let f1,f2 be Function of free_magma(X,n),free_magma X;
assume n > 0;
assume A10: for x st x in dom f1 holds f1.x = [x,n];
assume A11: for x st x in dom f2 holds f2.x = [x,n];
per cases;
suppose X is empty; hence thesis; end;
suppose A12: X is non empty; then
A13: dom f1 = free_magma(X,n) by FUNCT_2:def 1
.= dom f2 by A12,FUNCT_2:def 1;
for x being object st x in dom f1 holds f1.x = f2.x
proof
let x be object;
assume A14: x in dom f1;
hence f1.x = [x,n] by A10 .= f2.x by A11,A13,A14;
end;
hence thesis by A13,FUNCT_1:2;
end;
end;
hence thesis by A1,A7;
end;
end;
Lm2:
canon_image(X,n) is one-to-one
proof
for x1,x2 being object st x1 in dom canon_image(X,n) &
x2 in dom canon_image(X,n) & canon_image(X,n).x1 = canon_image(X,n).x2
holds x1 = x2
proof
let x1,x2 be object;
assume A1: x1 in dom canon_image(X,n) & x2 in dom canon_image(X,n);
assume A2: canon_image(X,n).x1 = canon_image(X,n).x2;
per cases;
suppose n>0; then
canon_image(X,n).x1 = [x1,n] & canon_image(X,n).x2 = [x2,n] by A1,Def19;
hence x1 = x2 by A2,XTUPLE_0:1;
end;
suppose not n>0; then
canon_image(X,n) = {} by Def19;
hence thesis by A1;
end;
end;
hence canon_image(X,n) is one-to-one by FUNCT_1:def 4;
end;
registration
let X be set;
let n be Nat;
cluster canon_image(X,n) -> one-to-one;
correctness by Lm2;
end;
reserve X,Y,Z for non empty set;
Lm3: dom canon_image(X,1) = X &
for x being set st x in X holds canon_image(X,1).x = [x,1]
proof
dom canon_image(X,1) = free_magma(X,1) by FUNCT_2:def 1;
hence dom canon_image(X,1) = X by Def13;
hence
for x being set st x in X holds canon_image(X,1).x = [x,1] by Def19;
end;
theorem Th36:
for A being Subset of free_magma X st A = canon_image(X,1) .: X
holds free_magma X = the_submagma_generated_by A
proof
let A be Subset of free_magma X;
set N = the_submagma_generated_by A;
assume A1: A = canon_image(X,1) .: X;
per cases;
suppose A2: A is empty;
X is empty
proof
assume X is non empty;
consider x being object such that
A3: x in X by XBOOLE_0:def 1;
x in dom canon_image(X,1) by Lm3,A3; then
canon_image(X,1).x in canon_image(X,1) .: X by A3,FUNCT_1:def 6;
hence contradiction by A2,A1;
end;
hence thesis;
end;
suppose A4: A is not empty;
A5: the carrier of N c= the carrier of free_magma X by Def9;
for x being object
st x in the carrier of free_magma X holds x in the carrier of N
proof
let x be object;
assume A6: x in the carrier of free_magma X;
defpred P[Nat] means for v being Element of free_magma X st
length v = $1 holds v in the carrier of N;
A7: for k being Nat st for n being Nat st n < k holds P[n] holds P[k]
proof
let k be Nat;
assume A8: for n being Nat st n < k holds P[n];
k = 0 or k + 1 > 0+1 by XREAL_1:6; then
k = 0 or k >= 1 by NAT_1:13; then
k = 0 or k = 1 or k > 1 by XXREAL_0:1; then
A9: k = 0 or k = 1 or k + 1 > 1+1 by XREAL_1:6;
per cases by A9,NAT_1:13;
suppose k = 0; hence P[k] by Th32; end;
suppose A10: k = 1;
for v being Element of free_magma X st length v = 1
holds v in the carrier of N
proof
let v be Element of free_magma X;
assume A11: length v = 1;
A12: v = [v`1,v`2] by Th32
.= [v`1,1] by A11,Def18;
v`1 in {w`1 where w is Element of free_magma X: length w = 1}
by A11; then
v`1 in X by Th30;
then v`1 in dom canon_image(X,1) & v`1 in X &
v = canon_image(X,1).(v`1) by A12,Lm3; then
A13: v in A by A1,FUNCT_1:def 6;
A c= the carrier of N by Def12;
hence thesis by A13;
end;
hence P[k] by A10;
end;
suppose A14: k >= 2;
for v being Element of free_magma X st length v = k
holds v in the carrier of N
proof
let v be Element of free_magma X;
assume A15: length v = k; then
consider v1,v2 be Element of free_magma X such that
A16: v = v1*v2 & length v1 < length v & length v2 < length v
by A14,Th34;
A17: v1 in the carrier of N by A8,A15,A16;
reconsider v19=v1 as Element of N by A8,A15,A16;
A18: v2 in the carrier of N by A8,A15,A16;
reconsider v29=v2 as Element of N by A8,A15,A16;
N is non empty by A4,Th14; then
A19: the carrier of N <> {};
A20: [v1,v2] in [:the carrier of N,the carrier of N:]
by A17,A18,ZFMISC_1:87;
v19*v29 = (the multF of N).[v19,v29] by BINOP_1:def 1
.= ((the multF of free_magma X)||the carrier of N).[v1,v2] by Def9
.= ((the multF of free_magma X)|
[:the carrier of N,the carrier of N:]).[v1,v2] by REALSET1:def 2
.= (the multF of free_magma X).[v1,v2] by A20,FUNCT_1:49
.= v1*v2 by BINOP_1:def 1;
hence v in the carrier of N by A16,A19;
end;
hence P[k];
end;
end;
A21: for n being Nat holds P[n] from NAT_1:sch 4(A7);
reconsider v = x as Element of free_magma X by A6;
reconsider k = length v as Nat;
P[k] by A21;
hence x in the carrier of N;
end; then
the carrier of free_magma X c= the carrier of N; then
the carrier of free_magma X = the carrier of N by A5,XBOOLE_0:def 10;
hence thesis by Th7;
end;
end;
theorem
for R being compatible Equivalence_Relation of free_magma(X) holds
(free_magma X)./.R =
the_submagma_generated_by (nat_hom R).: (canon_image(X,1) .: X)
proof
let R be compatible Equivalence_Relation of free_magma(X);
set A = canon_image(X,1) .: X;
reconsider A as Subset of free_magma X;
A1: the carrier of the_submagma_generated_by A
= the carrier of free_magma X by Th36;
the carrier of (free_magma X)./.R = rng nat_hom R by FUNCT_2:def 3; then
the carrier of (free_magma X)./.R = (nat_hom R) .: dom(nat_hom R)
by RELAT_1:113; then
the carrier of (free_magma X)./.R =
(nat_hom R).: the carrier of the_submagma_generated_by A
by A1,FUNCT_2:def 1; then
the carrier of (free_magma X)./.R =
the carrier of the_submagma_generated_by (nat_hom R).: A by Th15;
hence thesis by Th7;
end;
theorem Th38:
for f being Function of X,Y
holds canon_image(Y,1)*f is Function of X, free_magma Y
proof
let f be Function of X,Y;
A1: dom f = X by FUNCT_2:def 1;
dom canon_image(Y,1) = Y by Lm3; then
rng f c= dom canon_image(Y,1); then
A2: dom(canon_image(Y,1)*f) = X by A1,RELAT_1:27;
rng(canon_image(Y,1)*f) c= rng canon_image(Y,1) by RELAT_1:26;
hence thesis by A2,FUNCT_2:2;
end;
definition
let X be non empty set;
let M be non empty multMagma;
let n,m be non zero Nat;
let f be Function of free_magma(X,n),M;
let g be Function of free_magma(X,m),M;
func [:f,g:] ->
Function of [:[:free_magma(X,n),free_magma(X,m):],{n}:], M means :Def20:
for x being Element of [:[:free_magma(X,n),free_magma(X,m):],{n}:],
y being Element of free_magma(X,n), z being Element of free_magma(X,m)
st y = x`1`1 & z = x`1`2 holds it.x = f.y * g.z;
existence
proof
set X1 = [:[:free_magma(X,n),free_magma(X,m):],{n}:];
defpred P[object,object] means
for x being Element of X1,
y being Element of free_magma(X,n), z being Element of free_magma(X,m)
st $1=x & y = x`1`1 & z = x`1`2 holds $2 = f.y * g.z;
A1: for x being object st x in X1
ex y being object st y in the carrier of M & P[x,y]
proof
let x be object;
assume x in X1; then
A2: x`1 in [:free_magma(X,n),free_magma(X,m):] by MCART_1:10; then
reconsider x1 = x`1`1 as Element of free_magma(X,n) by MCART_1:10;
reconsider x2 = x`1`2 as Element of free_magma(X,m) by A2,MCART_1:10;
set y = f.x1 * g.x2;
take y;
thus y in the carrier of M;
thus P[x,y];
end;
consider h be Function of X1, the carrier of M such that
A3: for x being object st x in X1 holds P[x,h.x] from FUNCT_2:sch 1(A1);
take h;
thus thesis by A3;
end;
uniqueness
proof
let f1,f2 be Function of [:[:free_magma(X,n),free_magma(X,m):],{n}:], M;
assume A4:
for x being Element of [:[:free_magma(X,n),free_magma(X,m):],{n}:],
y being Element of free_magma(X,n), z being Element of free_magma(X,m) st
y = x`1`1 & z = x`1`2 holds f1.x = f.y * g.z;
assume A5:
for x being Element of [:[:free_magma(X,n),free_magma(X,m):],{n}:],
y being Element of free_magma(X,n), z being Element of free_magma(X,m) st
y = x`1`1 & z = x`1`2 holds f2.x = f.y * g.z;
for x being object st x in [:[:free_magma(X,n),free_magma(X,m):],{n}:]
holds f1.x = f2.x
proof
let x be object;
assume x in [:[:free_magma(X,n),free_magma(X,m):],{n}:]; then
reconsider x9=x as
Element of [:[:free_magma(X,n),free_magma(X,m):],{n}:];
A6: x9`1 in [:free_magma(X,n),free_magma(X,m):] by MCART_1:10; then
reconsider x1 = x9`1`1 as Element of free_magma(X,n) by MCART_1:10;
reconsider x2 = x9`1`2 as Element of free_magma(X,m) by A6,MCART_1:10;
thus f1.x = f.x1 * g.x2 by A4 .= f2.x by A5;
end;
hence thesis by FUNCT_2:12;
end;
end;
reserve M for non empty multMagma;
:: Ch I ?7.1 Pro.1 Algebra I Bourbaki
theorem Th39:
for f being Function of X,M holds
ex h being Function of free_magma X, M st h is multiplicative &
h extends f*(canon_image(X,1)")
proof
let f be Function of X,M;
defpred P1[object,object] means ex n st n=$1 &
$2 = Funcs(free_magma(X,n),the carrier of M);
A1: for x being object st x in NAT ex y being object st P1[x,y]
proof
let x be object;
assume x in NAT; then
reconsider n=x as Nat;
set y = Funcs(free_magma(X,n),the carrier of M);
take y;
thus P1[x,y];
end;
consider F1 be Function such that
A2: dom F1 = NAT &
for x being object st x in NAT holds P1[x,F1.x] from CLASSES1:sch 1(A1);
A3: f in Funcs(X,the carrier of M) by FUNCT_2:8;
P1[1,F1.1] by A2; then
F1.1 = Funcs(X,the carrier of M) by Def13; then
Funcs(X,the carrier of M) in rng F1 by A2,FUNCT_1:3; then
A4: f in union rng F1 by A3,TARSKI:def 4; then
A5: f in Union F1 by CARD_3:def 4;
reconsider X1 = Union F1 as non empty set by A4,CARD_3:def 4;
defpred P2[object,object] means
for fs being XFinSequence of X1
st $1=fs holds
(((for m being non zero Nat st m in dom fs
holds fs.m is Function of free_magma(X,m),M) implies (
(dom fs = 0 implies $2 = {}) &
(dom fs = 1 implies $2 = f) &
for n being Nat st n>=2 & dom fs = n holds
ex fs1 being FinSequence st len fs1 = n-1 &
(for p being Nat st p>=1 & p<=n-1 holds
ex m1,m2 being non zero Nat,
f1 being Function of free_magma(X,m1),M,
f2 being Function of free_magma(X,m2),M
st m1=p & m2 = n-p & f1=fs.m1 & f2=fs.m2
& fs1.p = [: f1, f2 :]) & $2 = Union fs1)) &
(not (for m being non zero Nat st m in dom fs
holds fs.m is Function of free_magma(X,m),M) implies $2 = f));
A6: for e being object st e in X1^omega ex u being object st P2[e,u]
proof
let e be object;
assume e in X1^omega; then
reconsider fs = e as XFinSequence of X1 by AFINSQ_1:def 7;
per cases;
suppose A7: for m being non zero Nat st m in dom fs
holds fs.m is Function of free_magma(X,m),M;
dom fs = 0 or dom fs + 1 > 0+1 by XREAL_1:6; then
dom fs = 0 or dom fs >= 1 by NAT_1:13; then
dom fs = 0 or dom fs = 1 or dom fs > 1 by XXREAL_0:1; then
A8: dom fs = 0 or dom fs = 1 or dom fs + 1 > 1+1 by XREAL_1:6;
per cases by A8,NAT_1:13;
suppose A9: dom fs = 0; set u = {};
take u; thus P2[e,u] by A9; end;
suppose A10: dom fs = 1; set u = f;
take u; thus P2[e,u] by A10; end;
suppose A11: dom fs >= 2;
reconsider n = dom fs as Nat;
reconsider n9= n -' 1 as Nat;
n-1 >= 2-1 by A11,XREAL_1:9; then
A12: n9 = n-1 by XREAL_0:def 2;
A13: Seg n9 c= Segm(n9+1) by AFINSQ_1:3;
defpred P3[set,object] means
for p being Nat st p>=1 & p<=n-1 & $1=p holds
ex m1,m2 being non zero Nat,
f1 being Function of free_magma(X,m1),M,
f2 being Function of free_magma(X,m2),M
st m1=p & m2 = n-p & f1=fs.m1 & f2=fs.m2
& $2 = [: f1, f2 :];
A14: for k being Nat st k in Seg n9 ex x being object st P3[k,x]
proof
let k be Nat;
assume A15: k in Seg n9; then
A16: 1<=k & k<=n9 by FINSEQ_1:1; then
k+1<=n-1+1 by A12,XREAL_1:7; then
A17: k+1-k<=n-k by XREAL_1:9;
then A18: n-'k = n-k by XREAL_0:def 2;
reconsider m1=k as non zero Nat by A15,FINSEQ_1:1;
reconsider m2=n-k as non zero Nat by A17,A18;
reconsider f1=fs.m1 as Function of free_magma(X,m1),M
by A7,A15,A13,A12;
-1>=-k by A16,XREAL_1:24; then
-1+n>=-k+n by XREAL_1:7; then
m2 in Seg n9 by A12,A17,FINSEQ_1:1; then
reconsider f2=fs.m2 as Function of free_magma(X,m2),M by A7,A13,A12;
set x = [: f1, f2 :];
take x;
thus thesis;
end;
consider fs1 be FinSequence such that
A19: dom fs1 = Seg n9 &
for k being Nat st k in Seg n9 holds P3[k,fs1.k]
from FINSEQ_1:sch 1(A14);
set u = Union fs1;
take u;
now
assume for m being non zero Nat st m in dom fs
holds fs.m is Function of free_magma(X,m),M;
thus (dom fs = 0 implies u = {}) & (dom fs = 1 implies u = f) by A11;
thus for n being Nat st n>=2 & dom fs = n holds
ex fs1 being FinSequence st len fs1 = n-1 &
(for p being Nat st p>=1 & p<=n-1 holds
ex m1,m2 being non zero Nat,
f1 being Function of free_magma(X,m1),M,
f2 being Function of free_magma(X,m2),M
st m1=p & m2 = n-p & f1=fs.m1 & f2=fs.m2
& fs1.p = [: f1, f2 :]) & u = Union fs1
proof
let n99 be Nat;
assume n99>=2;
assume A20: dom fs = n99;
take fs1;
thus len fs1 = n99-1 by A12,A20,A19,FINSEQ_1:def 3;
thus for p being Nat st p>=1 & p<=n99-1 holds
ex m1,m2 being non zero Nat,
f1 being Function of free_magma(X,m1),M,
f2 being Function of free_magma(X,m2),M
st m1=p & m2 = n99-p & f1=fs.m1 & f2=fs.m2 & fs1.p = [: f1, f2 :]
by A20,FINSEQ_1:1,A12,A19;
thus u = Union fs1;
end;
end;
hence thesis by A7;
end;
end;
suppose A21: not for m being non zero Nat st m in dom fs
holds fs.m is Function of free_magma(X,m),M;
take f; thus thesis by A21;
end;
end;
consider F2 be Function such that
A22: dom F2 = X1^omega &
for e being object st e in X1^omega holds P2[e,F2.e]
from CLASSES1:sch 1(A6);
A23: for n being Nat, fs being XFinSequence of X1
st n>=2 & dom fs = n & (for m being non zero Nat st m in dom fs
holds fs.m is Function of free_magma(X,m),M) &
(ex fs1 being FinSequence st len fs1 = n-1 &
(for p being Nat st p>=1 & p<=n-1 holds
ex m1,m2 being non zero Nat,
f1 being Function of free_magma(X,m1),M,
f2 being Function of free_magma(X,m2),M
st m1=p & m2 = n-p & f1=fs.m1 & f2=fs.m2 & fs1.p = [: f1, f2 :]) &
F2.fs = Union fs1) holds
F2.fs in Funcs(free_magma(X,n),the carrier of M)
proof
let n be Nat;
let fs be XFinSequence of X1;
assume A24: n>=2;
assume dom fs = n;
assume for m being non zero Nat st m in dom fs
holds fs.m is Function of free_magma(X,m),M;
assume ex fs1 being FinSequence st len fs1 = n-1 &
(for p being Nat st p>=1 & p<=n-1 holds
ex m1,m2 being non zero Nat,
f1 being Function of free_magma(X,m1),M,
f2 being Function of free_magma(X,m2),M
st m1=p & m2 = n-p & f1=fs.m1 & f2=fs.m2 & fs1.p = [: f1, f2 :]) &
F2.fs = Union fs1; then
consider fs1 be FinSequence such that
A25: len fs1 = n-1 and
A26: for p being Nat st p>=1 & p<=n-1 holds
ex m1,m2 being non zero Nat,
f1 being Function of free_magma(X,m1),M,
f2 being Function of free_magma(X,m2),M
st m1=p & m2 = n-p & f1=fs.m1 & f2=fs.m2 & fs1.p = [: f1, f2 :] and
A27: F2.fs = Union fs1;
A28: for x being object st x in F2.fs ex y,z being object st x = [y,z]
proof
let x be object;
assume x in F2.fs; then
x in union rng fs1 by A27,CARD_3:def 4; then
consider Y be set such that
A29: x in Y & Y in rng fs1 by TARSKI:def 4;
consider p be object such that
A30: p in dom fs1 & Y = fs1.p by A29,FUNCT_1:def 3;
reconsider p as Nat by A30;
p in Seg len fs1 by A30,FINSEQ_1:def 3; then
1<=p & p<=n-1 by A25,FINSEQ_1:1; then
consider m1,m2 be non zero Nat,
f1 be Function of free_magma(X,m1),M,
f2 be Function of free_magma(X,m2),M such that
A31: m1=p & m2 = n-p & f1=fs.m1 & f2=fs.m2 & fs1.p = [: f1, f2 :] by A26;
consider y,z be object such that
A32: x = [y,z] by A29,A30,A31,RELAT_1:def 1;
take y,z;
thus x = [y,z] by A32;
end;
for x,y1,y2 being object st [x,y1] in F2.fs & [x,y2] in F2.fs holds y1=y2
proof
let x,y1,y2 be object;
assume [x,y1] in F2.fs; then
[x,y1] in union rng fs1 by A27,CARD_3:def 4; then
consider Y1 be set such that
A33: [x,y1] in Y1 & Y1 in rng fs1 by TARSKI:def 4;
consider p1 be object such that
A34: p1 in dom fs1 & Y1 = fs1.p1 by A33,FUNCT_1:def 3;
reconsider p1 as Nat by A34;
p1 in Seg len fs1 by A34,FINSEQ_1:def 3; then
1<=p1 & p1<=n-1 by A25,FINSEQ_1:1; then
consider m19,m29 be non zero Nat,
f19 be Function of free_magma(X,m19),M,
f29 be Function of free_magma(X,m29),M such that
A35: m19=p1 & m29 = n-p1 & f19=fs.m19 & f29=fs.m29
& fs1.p1 = [: f19, f29 :] by A26;
A36: x in dom [: f19, f29 :] by A33,A34,A35,FUNCT_1:1;
then x`2 in {m19} by MCART_1:10; then
A37: x`2 = m19 by TARSKI:def 1;
assume [x,y2] in F2.fs; then
[x,y2] in union rng fs1 by A27,CARD_3:def 4; then
consider Y2 be set such that
A38: [x,y2] in Y2 & Y2 in rng fs1 by TARSKI:def 4;
consider p2 be object such that
A39: p2 in dom fs1 & Y2 = fs1.p2 by A38,FUNCT_1:def 3;
reconsider p2 as Nat by A39;
p2 in Seg len fs1 by A39,FINSEQ_1:def 3; then
1<=p2 & p2<=n-1 by A25,FINSEQ_1:1; then
consider m199,m299 be non zero Nat,
f199 be Function of free_magma(X,m199),M,
f299 be Function of free_magma(X,m299),M such that
A40: m199=p2 & m299 = n-p2 & f199=fs.m199 & f299=fs.m299
& fs1.p2 = [: f199, f299 :] by A26;
A41: x in dom [: f199, f299 :] by A38,A39,A40,FUNCT_1:1;
then x`2 in {m199} by MCART_1:10;
then A42: f19 = f199 & f29 = f299 by A35,A40,A37,TARSKI:def 1;
A43: x`1 in [:free_magma(X,m19),free_magma(X,m29):] by A36,MCART_1:10;
reconsider x1=x as
Element of [:[:free_magma(X,m19),free_magma(X,m29):],{m19}:] by A36;
reconsider y19=x`1`1 as Element of free_magma(X,m19) by A43,MCART_1:10;
reconsider z1=x`1`2 as Element of free_magma(X,m29) by A43,MCART_1:10;
A44: x`1 in [:free_magma(X,m199),free_magma(X,m299):] by A41,MCART_1:10;
reconsider x2=x as
Element of [:[:free_magma(X,m199),free_magma(X,m299):],{m199}:] by A41;
reconsider y29=x`1`1 as Element of free_magma(X,m199) by A44,MCART_1:10;
reconsider z2=x`1`2 as Element of free_magma(X,m299) by A44,MCART_1:10;
thus y1 = [: f19, f29 :].x1 by A33,A34,A35,FUNCT_1:1
.= f19.y19 * f29.z1 by Def20
.= f199.y29 * f299.z2 by A42
.= [: f199, f299 :].x2 by Def20
.= y2 by A38,A39,A40,FUNCT_1:1;
end; then
reconsider f9=F2.fs as Function by A28,FUNCT_1:def 1,RELAT_1:def 1;
for x being object holds x in free_magma(X,n) iff
ex y being object st [x,y] in f9
proof
let x be object;
hereby
assume x in free_magma(X,n); then
consider p,m be Nat such that
A45: x`2 = p & 1<=p & p<=n-1 &
x`1`1 in free_magma(X,p) & x`1`2 in free_magma(X,m) &
n = p + m &
x in [:[:free_magma(X,p),free_magma(X,m):],{p}:] by A24,Th21;
consider m1,m2 be non zero Nat,
f1 be Function of free_magma(X,m1),M,
f2 be Function of free_magma(X,m2),M such that
A46: m1=p & m2 = n-p & f1=fs.m1 & f2=fs.m2
& fs1.p = [: f1, f2 :] by A26,A45;
reconsider x9 = x as Element of
[:[:free_magma(X,m1),free_magma(X,m2):],{m1}:] by A45,A46;
reconsider y9 = x`1`1 as Element of free_magma(X,m1) by A45,A46;
reconsider z9 = x`1`2 as Element of free_magma(X,m2) by A45,A46;
reconsider y = f1.y9 * f2.z9 as object;
A47: dom [: f1, f2 :] = [:[:free_magma(X,m1),free_magma(X,m2):],{m1}:]
by FUNCT_2:def 1;
A48: [: f1, f2 :].x9 = y by Def20;
take y;
A49: [x,y] in fs1.p by A46,A47,A48,FUNCT_1:1;
p in Seg len fs1 by A45,A25,FINSEQ_1:1; then
p in dom fs1 by FINSEQ_1:def 3; then
fs1.p in rng fs1 by FUNCT_1:3; then
[x,y] in union rng fs1 by A49,TARSKI:def 4;
hence [x,y] in f9 by A27,CARD_3:def 4;
end;
given y being object such that
A50: [x,y] in f9;
[x,y] in union rng fs1 by A27,A50,CARD_3:def 4; then
consider Y be set such that
A51: [x,y] in Y & Y in rng fs1 by TARSKI:def 4;
consider p be object such that
A52: p in dom fs1 & Y = fs1.p by A51,FUNCT_1:def 3;
A53: p in Seg len fs1 by A52,FINSEQ_1:def 3;
reconsider p as Nat by A52;
p >= 1 & p <= n-1 by A53,A25,FINSEQ_1:1; then
consider m1,m2 be non zero Nat,
f1 be Function of free_magma(X,m1),M,
f2 be Function of free_magma(X,m2),M such that
A54: m1=p & m2 = n-p & f1=fs.m1 & f2=fs.m2 & fs1.p = [: f1, f2 :] by A26;
A55: x in dom [: f1, f2 :] by A51,A52,A54,FUNCT_1:1;
then A56: x`1 in [:free_magma(X,m1),free_magma(X,m2):] & x`2 in {m1}
by MCART_1:10; then
A57: x`1`1 in free_magma(X,m1) & x`1`2 in free_magma(X,m2) by MCART_1:10;
x = [x`1,x`2] by A55,MCART_1:21; then
A58: x = [[x`1`1,x`1`2],x`2] by A56,MCART_1:21;
x`2 = m1 by A56,TARSKI:def 1; then
x in free_magma(X,m1+m2) by A58,Th22,A57;
hence x in free_magma(X,n) by A54;
end; then
A59: dom f9 = free_magma(X,n) by XTUPLE_0:def 12;
for y being object st y in rng f9 holds y in the carrier of M
proof
let y be object;
assume y in rng f9; then
consider x being object such that
A60: x in dom f9 & y = f9.x by FUNCT_1:def 3;
[x,y] in Union fs1 by A27,A60,FUNCT_1:1; then
[x,y] in union rng fs1 by CARD_3:def 4; then
consider Y be set such that
A61: [x,y] in Y & Y in rng fs1 by TARSKI:def 4;
consider p be object such that
A62: p in dom fs1 & Y = fs1.p by A61,FUNCT_1:def 3;
A63: p in Seg len fs1 by A62,FINSEQ_1:def 3;
reconsider p as Nat by A62;
p >= 1 & p <= n-1 by A63,A25,FINSEQ_1:1; then
consider m1,m2 be non zero Nat,
f1 be Function of free_magma(X,m1),M,
f2 be Function of free_magma(X,m2),M such that
A64: m1=p & m2 = n-p & f1=fs.m1 & f2=fs.m2 & fs1.p = [: f1, f2 :] by A26;
y in rng [: f1, f2 :] by A61,A62,A64,XTUPLE_0:def 13;
hence y in the carrier of M;
end; then
rng f9 c= the carrier of M;
hence thesis by A59,FUNCT_2:def 2;
end;
for e being object st e in X1^omega holds F2.e in X1
proof
let e be object;
assume A65: e in X1^omega;
then reconsider fs=e as XFinSequence of X1 by AFINSQ_1:def 7;
per cases;
suppose A66: for m being non zero Nat st m in dom fs
holds fs.m is Function of free_magma(X,m),M; then
A67: (dom fs = 0 implies F2.e = {}) & (dom fs = 1 implies F2.e = f) &
for n being Nat st n>=2 & dom fs = n holds
ex fs1 being FinSequence st len fs1 = n-1 &
(for p being Nat st p>=1 & p<=n-1 holds
ex m1,m2 being non zero Nat,
f1 being Function of free_magma(X,m1),M,
f2 being Function of free_magma(X,m2),M
st m1=p & m2 = n-p & f1=fs.m1 & f2=fs.m2
& fs1.p = [: f1, f2 :]) & F2.e = Union fs1 by A65,A22;
dom fs = 0 or dom fs + 1 > 0+1 by XREAL_1:6; then
dom fs = 0 or dom fs >= 1 by NAT_1:13; then
dom fs = 0 or dom fs = 1 or dom fs > 1 by XXREAL_0:1; then
A68: dom fs = 0 or dom fs = 1 or dom fs + 1 > 1+1 by XREAL_1:6;
per cases by A68,NAT_1:13;
suppose A69: dom fs = 0;
Funcs({},the carrier of M) = {{}} by FUNCT_5:57; then
A70: {} in Funcs({},the carrier of M) by TARSKI:def 1;
P1[0,F1.0] by A2; then
F1.0 = Funcs({},the carrier of M) by Def13; then
Funcs({},the carrier of M) in rng F1 by A2,FUNCT_1:3; then
{} in union rng F1 by A70,TARSKI:def 4;
hence F2.e in X1 by A69,A67,CARD_3:def 4;
end;
suppose dom fs = 1;
hence F2.e in X1 by A5,A66,A65,A22;
end;
suppose A71: dom fs >= 2;
set n=dom fs;
ex fs1 being FinSequence st len fs1 = n-1 &
(for p being Nat st p>=1 & p<=n-1 holds
ex m1,m2 being non zero Nat,
f1 being Function of free_magma(X,m1),M,
f2 being Function of free_magma(X,m2),M
st m1=p & m2 = n-p & f1=fs.m1 & f2=fs.m2
& fs1.p = [: f1, f2 :]) & F2.e = Union fs1 by A66,A71,A65,A22; then
A72: F2.e in Funcs(free_magma(X,n),the carrier of M) by A23,A71,A66;
A73: n in dom F1 by A2,ORDINAL1:def 12; then
P1[n,F1.n] by A2; then
Funcs(free_magma(X,n),the carrier of M) in rng F1
by A73,FUNCT_1:3; then
F2.e in union rng F1 by A72,TARSKI:def 4;
hence F2.e in X1 by CARD_3:def 4;
end;
end;
suppose not (for m being non zero Nat st m in dom fs
holds fs.m is Function of free_magma(X,m),M);
hence F2.e in X1 by A5,A65,A22;
end;
end; then
reconsider F2 as Function of X1^omega, X1 by A22,FUNCT_2:3;
deffunc FX(XFinSequence of X1) = F2.$1;
consider F3 be sequence of X1 such that
A74: for n being Nat holds F3.n = FX(F3|n)
from FuncRecursiveExist2;
A75: for n being Nat st n>0
holds F3.n is Function of free_magma(X,n),M
proof
defpred P4[Nat] means for n being Nat st $1 = n & n > 0
holds F3.n is Function of free_magma(X,n),M;
A76: for k being Nat st for n being Nat st n < k holds P4[n] holds P4[k]
proof
let k be Nat;
assume A77: for n being Nat st n < k holds P4[n];
thus P4[k]
proof
let n be Nat;
assume A78: k = n;
assume n > 0;
A79: for m being non zero Nat st m in dom(F3|n)
holds (F3|n).m is Function of free_magma(X,m),M
proof
let m be non zero Nat;
assume A80: m in dom(F3|n);
then A81: (F3|n).m = F3.m by FUNCT_1:47;
m in Segm k by A78,A80; then
m < k by NAT_1:44;
hence (F3|n).m is Function of free_magma(X,m),M by A81,A77;
end;
A82: F3|n in X1^omega by AFINSQ_1:def 7;
reconsider fs=F3|n as XFinSequence of X1;
A83: (dom fs = 0 implies F2.fs = {}) & (dom fs = 1 implies F2.fs = f) &
for n being Nat st n>=2 & dom fs = n holds
ex fs1 being FinSequence st len fs1 = n-1 &
(for p being Nat st p>=1 & p<=n-1 holds
ex m1,m2 being non zero Nat,
f1 being Function of free_magma(X,m1),M,
f2 being Function of free_magma(X,m2),M
st m1=p & m2 = n-p & f1=fs.m1 & f2=fs.m2
& fs1.p = [: f1, f2 :]) & F2.fs = Union fs1 by A79,A82,A22;
A84: n in NAT by ORDINAL1:def 12;
dom F3 = NAT by FUNCT_2:def 1; then
A85: n c= dom F3 by A84,ORDINAL1:def 2;
A86: dom fs = dom F3 /\ n by RELAT_1:61
.= n by A85,XBOOLE_1:28;
F2.fs is Function of free_magma(X,n),M
proof
n = 0 or n + 1 > 0+1 by XREAL_1:6; then
n = 0 or n >= 1 by NAT_1:13; then
n = 0 or n = 1 or n > 1 by XXREAL_0:1; then
A87: n = 0 or n = 1 or n + 1 > 1+1 by XREAL_1:6;
per cases by A87,NAT_1:13;
suppose A88: n = 0;
Funcs({},the carrier of M) = {{}} by FUNCT_5:57; then
F2.fs in Funcs({},the carrier of M) by A88,A83,TARSKI:def 1; then
F2.fs in Funcs(free_magma(X,n),the carrier of M) by A88,Def13; then
ex f being Function st F2.fs = f & dom f = free_magma(X,n)
& rng f c= the carrier of M by FUNCT_2:def 2;
hence thesis by FUNCT_2:2;
end;
suppose A89: n = 1;
free_magma(X,1) = X by Def13;
hence thesis by A79,A82,A22,A89,A86;
end;
suppose A90: n >= 2; then
ex fs1 being FinSequence st len fs1 = n-1 &
(for p being Nat st p>=1 & p<=n-1 holds
ex m1,m2 being non zero Nat,
f1 being Function of free_magma(X,m1),M,
f2 being Function of free_magma(X,m2),M
st m1=p & m2 = n-p & f1=fs.m1 & f2=fs.m2
& fs1.p = [: f1, f2 :]) & F2.fs = Union fs1
by A79,A82,A22,A86; then
F2.fs in Funcs(free_magma(X,n),the carrier of M)
by A23,A90,A86,A79; then
ex f being Function st F2.fs = f & dom f = free_magma(X,n)
& rng f c= the carrier of M by FUNCT_2:def 2;
hence thesis by FUNCT_2:2;
end;
end;
hence F3.n is Function of free_magma(X,n),M by A74;
end;
end;
for k being Nat holds P4[k] from NAT_1:sch 4(A76);
hence thesis;
end;
reconsider X9 = the carrier of free_magma X as set;
defpred P5[object,object] means
for w being Element of free_magma X,
f9 being Function of free_magma(X,w`2),M st w = $1 & f9 = F3.w`2
holds $2 = f9.w`1;
A91: for x being object st x in X9
ex y being object st y in the carrier of M & P5[x,y]
proof
let x be object;
assume x in X9; then
reconsider w=x as Element of free_magma X;
reconsider f9=F3.w`2 as Function of free_magma(X,w`2),M by A75;
set y = f9.w`1;
take y;
w in [:free_magma(X,w`2),{w`2}:] by Th25; then
w`1 in free_magma(X,w`2) by MCART_1:10;
hence y in the carrier of M by FUNCT_2:5;
thus P5[x,y];
end;
consider h be Function of X9,the carrier of M such that
A92: for x being object st x in X9 holds P5[x,h.x] from FUNCT_2:sch 1(A91);
reconsider h as Function of free_magma X, M;
take h;
for a,b being Element of free_magma X holds h.(a * b) = h.a * h.b
proof
let a,b be Element of free_magma X;
reconsider fab=F3.(a*b)`2 as Function of free_magma(X,(a*b)`2),M by A75;
a*b = [[[a`1,b`1],a`2],length a + length b] by Th31; then
A93: (a*b)`1=[[a`1,b`1],a`2] & (a*b)`2 = length a + length b; then
A94: fab = F2.(F3|(length a + length b)) by A74;
A95: F3|(length a + length b) in X1^omega by AFINSQ_1:def 7;
A96: for m being non zero Nat
st m in dom(F3|(length a + length b))
holds (F3|(length a + length b)).m is Function of free_magma(X,m),M
proof
let m be non zero Nat;
assume A97: m in dom(F3|(length a + length b));
F3.m is Function of free_magma(X,m),M by A75;
hence thesis by A97,FUNCT_1:47;
end;
set n = length a + length b;
length a >= 1 & length b >= 1 by Th32; then
A98: length a + length b >= 1+1 by XREAL_1:7;
A99: n in NAT by ORDINAL1:def 12;
dom F3 = NAT by FUNCT_2:def 1; then
A100: n c= dom F3 by A99,ORDINAL1:def 2;
dom(F3|n) = dom F3 /\ n by RELAT_1:61
.= n by A100,XBOOLE_1:28; then
consider fs1 be FinSequence such that
A101: len fs1 = n-1 and
A102: for p being Nat st p>=1 & p<=n-1 holds
ex m1,m2 being non zero Nat,
f1 being Function of free_magma(X,m1),M,
f2 being Function of free_magma(X,m2),M
st m1=p & m2 = n-p & f1=(F3|n).m1 & f2=(F3|n).m2
& fs1.p = [: f1, f2 :] and
A103: fab = Union fs1 by A96,A98,A95,A22,A94;
a*b in [:free_magma(X,(a*b)`2),{(a*b)`2}:] by Th25; then
(a*b)`1 in free_magma(X,(a*b)`2) by MCART_1:10; then
(a*b)`1 in dom fab by FUNCT_2:def 1; then
[(a*b)`1,fab.(a*b)`1] in Union fs1 by A103,FUNCT_1:1; then
[(a*b)`1,fab.(a*b)`1] in union rng fs1 by CARD_3:def 4; then
consider Y be set such that
A104: [(a*b)`1,fab.(a*b)`1] in Y & Y in rng fs1 by TARSKI:def 4;
consider p be object such that
A105: p in dom fs1 & Y = fs1.p by A104,FUNCT_1:def 3;
A106: p in Seg len fs1 by A105,FINSEQ_1:def 3;
reconsider p as Nat by A105;
p >= 1 & p <= n-1 by A106,A101,FINSEQ_1:1; then
consider m1,m2 be non zero Nat,
f1 be Function of free_magma(X,m1),M,
f2 be Function of free_magma(X,m2),M such that
A107: m1=p & m2 = n-p & f1=(F3|n).m1 & f2=(F3|n).m2
& fs1.p = [: f1, f2 :] by A102;
A108: (a*b)`1 in dom [: f1, f2 :] by A107,A104,A105,FUNCT_1:1;
then (a*b)`1`1 in [:free_magma(X,m1),free_magma(X,m2):] & (a*b)`1`2 in {m1}
by MCART_1:10; then
A109: [a`1,b`1] in [:free_magma(X,m1),free_magma(X,m2):] & a`2 in {m1}
by A93; then
m1 = a`2 by TARSKI:def 1; then
A110: m1 = length a by Def18;
length b >= 0+1 by Th32; then
length b + length a > 0 + length a by XREAL_1:6; then
A111: m1 in Segm n by A110,NAT_1:44;
length a >= 0+1 by Th32; then
length a + length b > 0 + length b by XREAL_1:6; then
A112: m2 in Segm n by A110,A107,NAT_1:44;
reconsider x=(a*b)`1
as Element of [:[:free_magma(X,m1),free_magma(X,m2):],{m1}:] by A108;
A113: x`1 in [:free_magma(X,m1),free_magma(X,m2):] by MCART_1:10; then
reconsider y = x`1`1 as Element of free_magma(X,m1) by MCART_1:10;
reconsider z = x`1`2 as Element of free_magma(X,m2) by A113,MCART_1:10;
A114: x`1 = [a`1,b`1] by A93;
A115: [: f1, f2 :].x = f1.y * f2.z by Def20;
A116: h.(a*b) = fab.(a*b)`1 by A92;
A117: fab.(a*b)`1 = [: f1, f2 :].x by A107,A104,A105,FUNCT_1:1;
reconsider fa=F3.a`2 as Function of free_magma(X,a`2),M by A75;
reconsider fb=F3.b`2 as Function of free_magma(X,b`2),M by A75;
f1 = F3.m1 by A107,A111,FUNCT_1:49
.= fa by A109,TARSKI:def 1; then
A118: fa.a`1 = f1.y by A114;
f2 = F3.m2 by A107,A112,FUNCT_1:49
.= fb by Def18,A110,A107; then
A119: fb.b`1 = f2.z by A114;
h.b = fb.b`1 by A92;
hence h.(a * b) = h.a * h.b by A115,A116,A118,A119,A92,A117;
end;
hence h is multiplicative by GROUP_6:def 6;
set fX = canon_image(X,1);
for x being object st x in dom(f*(fX")) holds x in dom h
proof
let x be object;
assume A120: x in dom(f*(fX"));
dom(f*(fX")) c= dom(fX") by RELAT_1:25; then
x in dom(fX") by A120; then
x in rng fX by FUNCT_1:33; then
x in the carrier of free_magma X;
hence x in dom h by FUNCT_2:def 1;
end; then
A121: dom(f*(fX")) c= dom h;
for x being object st x in (dom h) /\ dom(f*(fX")) holds h.x = (f*(fX")).x
proof
let x be object;
assume x in (dom h) /\ dom(f*(fX")); then
A122: x in dom(f*(fX")) by A121,XBOOLE_1:28;
A123: dom(f*(fX")) c= dom(fX") by RELAT_1:25; then
x in dom(fX") by A122;
then x in rng fX by FUNCT_1:33;
then consider x9 be object such that
A124: x9 in dom fX & x = fX.x9 by FUNCT_1:def 3;
A125: 1 in {1} by TARSKI:def 1;
[:free_magma(X,1),{1}:] c= free_magma_carrier X by Lm1; then
A126: [:X,{1}:] c= free_magma_carrier X by Def13;
A127: x9 in X by A124,Lm3;
A128: x = [x9,1] by A124,Def19; then
x in [:X,{1}:] by A125,A127,ZFMISC_1:def 2; then
reconsider w=x as Element of free_magma X by A126;
A129: (fX").x = x9 by A124,FUNCT_1:34;
set f9 = F3.w`2;
reconsider f9 as Function of free_magma(X,w`2),M by A75;
A130: f9 = F3.1 by A128 .= FX(F3|1) by A74;
A131: for m being non zero Nat st m in dom(F3|1)
holds (F3|1).m is Function of free_magma(X,m),M
proof
let m be non zero Nat;
assume m in dom(F3|1);
then (F3|1).m = F3.m by FUNCT_1:47;
hence (F3|1).m is Function of free_magma(X,m),M by A75;
end;
A132: F3|1 in X1^omega by AFINSQ_1:def 7;
reconsider fs=F3|1 as XFinSequence of X1;
dom F3 = NAT by FUNCT_2:def 1; then
A133: 1 c= dom F3 by ORDINAL1:def 2;
A134: dom fs = dom F3 /\ 1 by RELAT_1:61
.= 1 by A133,XBOOLE_1:28;
thus h.x = f9.w`1 by A92 .= f9.x9 by A128
.= f.((fX").x) by A129,A130,A134,A131,A132,A22
.= (f*(fX")).x by A123,A122,FUNCT_1:13;
end; then
h tolerates f*(fX") by PARTFUN1:def 4;
hence h extends f*(canon_image(X,1)") by A121;
end;
theorem Th40:
for f being Function of X,M, h,g being Function of free_magma X, M
st h is multiplicative & h extends f*(canon_image(X,1)") &
g is multiplicative & g extends f*(canon_image(X,1)") holds h = g
proof
let f be Function of X,M;
let h,g be Function of free_magma X, M;
assume A1: h is multiplicative;
assume A2: h extends f*(canon_image(X,1)");
assume A3: g is multiplicative;
assume A4: g extends f*(canon_image(X,1)");
defpred P[Nat] means for w being Element of free_magma X st length w = $1
holds h.w=g.w;
A5: for k being Nat st for n being Nat st n < k holds P[n] holds P[k]
proof
let k be Nat;
assume A6: for n being Nat st n < k holds P[n];
thus for w being Element of free_magma X st length w = k holds h.w=g.w
proof
let w be Element of free_magma X;
assume A7: length w = k;
A8: w = [w`1,w`2] & length w >= 1 by Th32; then
length w = 1 or length w > 1 by XXREAL_0:1; then
A9: length w = 1 or length w +1 > 1+1 by XREAL_1:8;
per cases by A9,NAT_1:13;
suppose A10: length w = 1;
set x = w`1;
x in {w9`1 where w9 is Element of free_magma X: length w9 = 1}
by A10; then
A11: x in X by Th30;
A12: dom(f*(canon_image(X,1)")) c= dom h &
h tolerates f*(canon_image(X,1)") by A2;
A13: dom(f*(canon_image(X,1)")) c= dom g &
g tolerates f*(canon_image(X,1)") by A4;
A14: canon_image(X,1).x = [x,1] by A11,Lm3 .= w by Def18,A8,A10;
x in dom canon_image(X,1) by A11,Lm3; then
w in rng canon_image(X,1) by A14,FUNCT_1:3; then
A15: w in dom(canon_image(X,1)") by FUNCT_1:33;
X c= dom f by FUNCT_2:def 1; then
dom canon_image(X,1) c= dom f by Lm3; then
rng(canon_image(X,1)") c= dom f by FUNCT_1:33; then
w in dom(f*(canon_image(X,1)")) by A15,RELAT_1:27; then
w in dom h /\ dom(f*(canon_image(X,1)")) &
w in dom g /\ dom(f*(canon_image(X,1)")) by A12,A13,XBOOLE_1:28; then
h.w = (f*(canon_image(X,1)")).w & g.w = (f*(canon_image(X,1)")).w
by A12,A13,PARTFUN1:def 4;
hence thesis;
end;
suppose length w >= 2; then
consider w1,w2 be Element of free_magma X such that
A16: w = w1*w2 & length w1 < length w & length w2 < length w by Th34;
h.w1 = g.w1 & h.w2 = g.w2 by A6,A7,A16; then
h.(w1*w2) = g.w1*g.w2 by A1,GROUP_6:def 6;
hence h.w=g.w by A16,A3,GROUP_6:def 6;
end;
end;
end;
A17: for k being Nat holds P[k] from NAT_1:sch 4(A5);
for w being Element of free_magma X holds h.w=g.w
proof
let w be Element of free_magma X;
reconsider k=length w as Nat;
P[k] by A17;
hence h.w=g.w;
end;
then for x being object st x in the carrier of free_magma X holds h.x = g.x;
hence h = g by FUNCT_2:12;
end;
reserve M,N for non empty multMagma,
f for Function of M, N,
H for non empty multSubmagma of N,
R for compatible Equivalence_Relation of M;
theorem Th41:
f is multiplicative & the carrier of H = rng f & R = equ_kernel f implies
ex g being Function of M./.R, H st f = g * nat_hom R &
g is bijective & g is multiplicative
proof
assume A1: f is multiplicative;
assume A2: the carrier of H = rng f;
assume A3: R = equ_kernel f;
set g = ((nat_hom R)~) * f;
for x,y1,y2 being object st [x,y1] in g & [x,y2] in g holds y1 = y2
proof
let x,y1,y2 be object;
assume [x,y1] in g; then
consider z1 be object such that
A4: [x,z1] in (nat_hom R)~ & [z1,y1] in f by RELAT_1:def 8;
assume [x,y2] in g; then
consider z2 be object such that
A5: [x,z2] in (nat_hom R)~ & [z2,y2] in f by RELAT_1:def 8;
A6: [z1,x] in nat_hom R & [z2,x] in nat_hom R by A4,A5,RELAT_1:def 7; then
z1 in dom nat_hom R & z2 in dom nat_hom R by XTUPLE_0:def 12;
then reconsider z1,z2 as Element of M;
A7: x = (nat_hom R).z1 & x = (nat_hom R).z2 by A6,FUNCT_1:1;
A8: f.z1 = y1 & f.z2 = y2 by A4,A5,FUNCT_1:1;
(nat_hom R).z1 = Class(R,z1) & (nat_hom R).z2 = Class(R,z2) by Def6; then
z2 in Class(R,z1) by A7,EQREL_1:23; then
[z1,z2] in equ_kernel f by A3,EQREL_1:18;
hence y1 = y2 by A8,Def8;
end; then
reconsider g as Function by FUNCT_1:def 1;
rng nat_hom R = the carrier of M./.R by FUNCT_2:def 3; then
A9: dom((nat_hom R)~) = the carrier of M./.R by RELAT_1:20;
the carrier of M c= dom f by FUNCT_2:def 1; then
dom nat_hom R c= dom f; then
rng((nat_hom R)~) c= dom f by RELAT_1:20; then
A10: dom g = the carrier of M./.R by A9,RELAT_1:27;
dom f c= the carrier of M; then
dom f c= dom(nat_hom R) by FUNCT_2:def 1; then
dom f c= rng((nat_hom R)~) by RELAT_1:20; then
A11: rng g = the carrier of H by A2,RELAT_1:28;
then reconsider g as Function of M./.R, H by A10,FUNCT_2:1;
take g;
for x1,x2 being object st x1 in dom g & x2 in dom g & g.x1 = g.x2
holds x1 = x2
proof
let x1,x2 be object;
assume A12: x1 in dom g;
assume A13: x2 in dom g;
assume A14: g.x1 = g.x2;
set y=g.x1;
[x1,y] in g by A12,FUNCT_1:1; then
consider z1 be object such that
A15: [x1,z1] in (nat_hom R)~ & [z1,y] in f by RELAT_1:def 8;
[x2,y] in g by A14,A13,FUNCT_1:1; then
consider z2 be object such that
A16: [x2,z2] in (nat_hom R)~ & [z2,y] in f by RELAT_1:def 8;
A17: [z1,x1] in nat_hom R & [z2,x2] in nat_hom R
by A15,A16,RELAT_1:def 7; then
z1 in dom nat_hom R & z2 in dom nat_hom R by XTUPLE_0:def 12;
then reconsider z1,z2 as Element of M;
z1 in dom f & z2 in dom f & f.z1=y & f.z2=y by A15,A16,FUNCT_1:1; then
[z1,z2] in equ_kernel f by Def8; then
A18: z2 in Class(R,z1) by A3,EQREL_1:18;
A19: (nat_hom R).z1 = Class(R,z1) & (nat_hom R).z2 = Class(R,z2) by Def6;
x1 = (nat_hom R).z1 & x2 = (nat_hom R).z2 by A17,FUNCT_1:1;
hence x1 = x2 by A19,A18,EQREL_1:23;
end; then
A20: g is one-to-one by FUNCT_1:def 4;
A21: for x being object
holds x in dom f iff x in dom nat_hom R & (nat_hom R).x in dom g
proof
let x be object;
hereby
assume x in dom f; then
x in the carrier of M;
hence x in dom nat_hom R by FUNCT_2:def 1; then
(nat_hom R).x in rng nat_hom R by FUNCT_1:3; then
(nat_hom R).x in the carrier of M./.R;
hence (nat_hom R).x in dom g by FUNCT_2:def 1;
end;
assume x in dom nat_hom R & (nat_hom R).x in dom g; then
x in the carrier of M;
hence x in dom f by FUNCT_2:def 1;
end;
for x being object st x in dom f holds f.x = g.((nat_hom R).x)
proof
let x be object;
assume A22: x in dom f;
set y = (nat_hom R).x;
y in dom g by A22,A21; then
[y,g.y] in g by FUNCT_1:1; then
consider z be object such that
A23: [y,z] in (nat_hom R)~ & [z,g.y] in f by RELAT_1:def 8;
[z,y] in nat_hom R by A23,RELAT_1:def 7; then
A24: z in dom nat_hom R & y = (nat_hom R).z by FUNCT_1:1;
A25: z in dom f & g.y = f.z by A23,FUNCT_1:1; then
reconsider z9=z,x9=x as Element of M by A22;
(nat_hom R).z9 = Class(R,z9) & (nat_hom R).x9 = Class(R,x9) by Def6; then
z9 in Class (R,x9) by A24,EQREL_1:23; then
[x,z] in R by EQREL_1:18;
hence f.x = g.((nat_hom R).x) by A25,A3,Def8;
end;
hence f = g * nat_hom R by A21,FUNCT_1:10;
g is onto by A11,FUNCT_2:def 3;
hence g is bijective by A20;
for v,w being Element of M./.R holds g.(v*w) = g.v * g.w
proof
let v,w be Element of M./.R;
v*w in the carrier of M./.R; then
v*w in dom g by FUNCT_2:def 1; then
[v*w,g.(v*w)] in g by FUNCT_1:1; then
consider z be object such that
A26: [v*w,z] in (nat_hom R)~ & [z,g.(v*w)] in f by RELAT_1:def 8;
[z,v*w] in nat_hom R by A26,RELAT_1:def 7; then
A27: z in dom nat_hom R & (nat_hom R).z = v*w by FUNCT_1:1;
A28: f.z = g.(v*w) by A26,FUNCT_1:1;
v in the carrier of M./.R; then
v in dom g by FUNCT_2:def 1; then
[v,g.v] in g by FUNCT_1:1; then
consider z1 be object such that
A29: [v,z1] in (nat_hom R)~ & [z1,g.v] in f by RELAT_1:def 8;
[z1,v] in nat_hom R by A29,RELAT_1:def 7; then
A30: z1 in dom nat_hom R & (nat_hom R).z1 = v by FUNCT_1:1;
A31: f.z1 = g.v by A29,FUNCT_1:1;
w in the carrier of M./.R; then
w in dom g by FUNCT_2:def 1; then
[w,g.w] in g by FUNCT_1:1; then
consider z2 be object such that
A32: [w,z2] in (nat_hom R)~ & [z2,g.w] in f by RELAT_1:def 8;
[z2,w] in nat_hom R by A32,RELAT_1:def 7; then
A33: z2 in dom nat_hom R & (nat_hom R).z2 = w by FUNCT_1:1;
A34: f.z2 = g.w by A32,FUNCT_1:1;
reconsider z1,z2,z as Element of M by A30,A33,A27;
A35: (nat_hom R).z = (nat_hom R).(z1*z2) by A30,A33,A27,GROUP_6:def 6;
(nat_hom R).(z1*z2) = Class(R,z1*z2) & (nat_hom R).z = Class(R,z)
by Def6; then
z1*z2 in Class(R,z) by A35,EQREL_1:23; then
[z,z1*z2] in R by EQREL_1:18; then
A36: f.z = f.(z1*z2) by A3,Def8
.= f.z1 * f.z2 by A1,GROUP_6:def 6;
A37: [g.v,g.w] in [:the carrier of H,the carrier of H:] by ZFMISC_1:def 2;
thus g.(v*w) = (the multF of N).[g.v,g.w] by A31,A34,A36,A28,BINOP_1:def 1
.= ((the multF of N)|[:the carrier of H,the carrier of H:]).[g.v,g.w]
by A37,FUNCT_1:49
.= ((the multF of N)|[:the carrier of H,the carrier of H:]).(g.v,g.w)
by BINOP_1:def 1
.= ((the multF of N)||the carrier of H).(g.v,g.w) by REALSET1:def 2
.= g.v * g.w by Def9;
end;
hence g is multiplicative by GROUP_6:def 6;
end;
theorem
for g1,g2 being Function of M./.R, N st g1 * nat_hom R = g2 * nat_hom R
holds g1 = g2
proof
let g1,g2 be Function of M./.R, N;
assume A1: g1 * nat_hom R = g2 * nat_hom R;
set Y = rng nat_hom R;
rng nat_hom R = the carrier of M ./. R by FUNCT_2:def 3; then
dom g1 = Y & dom g2 = Y by FUNCT_2:def 1;
hence g1 = g2 by A1,FUNCT_1:86;
end;
theorem
for M being non empty multMagma holds ex X being non empty set,
r being Relators of free_magma X,
g being Function of (free_magma X) ./. equ_rel r, M
st g is bijective & g is multiplicative
proof
let M be non empty multMagma;
set X = the carrier of M;
consider f be Function of free_magma X, M such that
A1: f is multiplicative & f extends (id X)*(canon_image(X,1)") by Th39;
consider r be Relators of free_magma X such that
A2: equ_kernel f = equ_rel r by A1,Th5;
reconsider R = equ_kernel f
as compatible Equivalence_Relation of free_magma X by A1,Th4;
the multF of M = (the multF of M)|[:the carrier of M,the carrier of M:]; then
the multF of M = (the multF of M)||the carrier of M by REALSET1:def 2; then
reconsider H = M as non empty multSubmagma of M by Def9;
for y being object st y in the carrier of M
ex x being object st x in dom f & y = f.x
proof
let y be object;
assume A3: y in the carrier of M;
reconsider x = [y,1] as set;
take x;
[:free_magma(X,1),{1}:] c= the carrier of free_magma X by Lm1; then
A4: [:X,{1}:] c= the carrier of free_magma X by Def13;
1 in {1} by TARSKI:def 1; then
x in [:X,{1}:] by A3,ZFMISC_1:def 2; then
x in the carrier of free_magma X by A4;
hence x in dom f by FUNCT_2:def 1;
A5: dom ((id X)*(canon_image(X,1)")) c= dom f &
f tolerates (id X)*(canon_image(X,1)") by A1;
A6: canon_image(X,1).y = x by A3,Lm3;
y in dom canon_image(X,1) by A3,Lm3; then
x in rng canon_image(X,1) by A6,FUNCT_1:3; then
A7: x in dom(canon_image(X,1)") by FUNCT_1:33;
dom canon_image(X,1) c= dom(id X) by Lm3; then
rng(canon_image(X,1)") c= dom(id X) by FUNCT_1:33; then
A8: x in dom((id X)*(canon_image(X,1)")) by A7,RELAT_1:27;
A9: y in dom canon_image(X,1) by A3,Lm3;
thus y = (id X).y by A3,FUNCT_1:18
.= (id X).((canon_image(X,1)").x) by A9,A6,FUNCT_1:34
.= ((id X)*(canon_image(X,1)")).x by A8,FUNCT_1:12
.= f.x by A8,A5,PARTFUN1:53;
end; then
the carrier of M c= rng f by FUNCT_1:9; then
the carrier of H = rng f by XBOOLE_0:def 10; then
consider g be Function of (free_magma X) ./. R, H such that
A10: f = g * nat_hom R & g is bijective & g is multiplicative by A1,Th41;
reconsider g as Function of (free_magma X) ./. equ_rel r, M by A2;
take X,r,g;
thus thesis by A10,A2;
end;
definition
let X,Y be non empty set;
let f be Function of X,Y;
func free_magmaF f -> Function of free_magma X, free_magma Y means :Def21:
it is multiplicative & it extends (canon_image(Y,1)*f)*(canon_image(X,1)");
existence
proof
reconsider f9=canon_image(Y,1)*f as Function of X, free_magma Y by Th38;
ex h being Function of free_magma X, free_magma Y st h is multiplicative &
h extends f9*(canon_image(X,1)") by Th39;
hence thesis;
end;
uniqueness
proof
let f1, f2 be Function of free_magma X,free_magma Y;
assume A1: f1 is multiplicative &
f1 extends (canon_image(Y,1)*f)*(canon_image(X,1)");
assume A2: f2 is multiplicative &
f2 extends (canon_image(Y,1)*f)*(canon_image(X,1)");
reconsider f9=canon_image(Y,1)*f as Function of X,free_magma Y by Th38;
f1 extends f9*(canon_image(X,1)") &
f2 extends f9*(canon_image(X,1)") by A1,A2;
hence f1 = f2 by A1,A2,Th40;
end;
end;
registration
let X,Y be non empty set;
let f be Function of X,Y;
cluster free_magmaF f -> multiplicative;
coherence by Def21;
end;
reserve f for Function of X,Y;
reserve g for Function of Y,Z;
theorem Th44:
free_magmaF(g*f) = free_magmaF(g)*free_magmaF(f)
proof
set f2=free_magmaF(g)*free_magmaF(f);
reconsider f9=canon_image(Z,1)*(g*f) as Function of X,free_magma Z by Th38;
for a, b being Element of free_magma X holds f2.(a*b) = f2.a * f2.b
proof
let a, b be Element of free_magma X;
a*b in the carrier of free_magma X; then
A1: a*b in dom f2 by FUNCT_2:def 1;
a in the carrier of free_magma X & b in the carrier of free_magma X; then
A2: a in dom(free_magmaF f) & b in dom(free_magmaF f) by FUNCT_2:def 1;
thus f2.(a*b) = (free_magmaF g).((free_magmaF f).(a*b)) by A1,FUNCT_1:12
.= (free_magmaF g).((free_magmaF f).a * (free_magmaF f).b)
by GROUP_6:def 6
.= (free_magmaF g).((free_magmaF f).a)*(free_magmaF g).((free_magmaF f).b)
by GROUP_6:def 6
.= f2.a * (free_magmaF g).((free_magmaF f).b) by A2,FUNCT_1:13
.= f2.a * f2.b by A2,FUNCT_1:13;
end; then
A3: f2 is multiplicative by GROUP_6:def 6;
A4: dom(f9*(canon_image(X,1)")) c= dom(canon_image(X,1)") by RELAT_1:25;
rng canon_image(X,1) c= the carrier of free_magma X; then
dom(canon_image(X,1)") c= the carrier of free_magma X by FUNCT_1:33; then
dom(f9*(canon_image(X,1)")) c= the carrier of free_magma X
by A4; then
A5: dom(f9*(canon_image(X,1)")) c= dom f2 by FUNCT_2:def 1;
for x being object st x in dom(f9*(canon_image(X,1)"))
holds f2.x = (f9*(canon_image(X,1)")).x
proof
let x be object;
assume A6: x in dom(f9*(canon_image(X,1)"));
free_magmaF(f) extends (canon_image(Y,1)*f)*(canon_image(X,1)")
by Def21; then
A7: dom((canon_image(Y,1)*f)*(canon_image(X,1)")) c= dom(free_magmaF f) &
(canon_image(Y,1)*f)*(canon_image(X,1)") tolerates free_magmaF f;
A8: x in dom(canon_image(X,1)") by A6,FUNCT_1:11;
X c= dom f by FUNCT_2:def 1; then
dom canon_image(X,1) c= dom f by Lm3; then
rng(canon_image(X,1)") c= dom f by FUNCT_1:33; then
A9: x in dom(f*(canon_image(X,1)")) by A8,RELAT_1:27;
rng(f*(canon_image(X,1)")) c= Y; then
rng(f*(canon_image(X,1)")) c= dom canon_image(Y,1) by Lm3; then
x in dom(canon_image(Y,1)*(f*(canon_image(X,1)"))) by A9,RELAT_1:27; then
A10: x in dom((canon_image(Y,1)*f)*(canon_image(X,1)")) by RELAT_1:36;
set y = (f*(canon_image(X,1)")).x;
free_magmaF(g) extends (canon_image(Z,1)*g)*(canon_image(Y,1)")
by Def21; then
A11: dom((canon_image(Z,1)*g)*(canon_image(Y,1)")) c= dom(free_magmaF g) &
(canon_image(Z,1)*g)*(canon_image(Y,1)") tolerates free_magmaF g;
y in rng(f*(canon_image(X,1)")) by A9,FUNCT_1:3; then
A12: y in Y; then
A13: y in dom canon_image(Y,1) by Lm3; then
A14: canon_image(Y,1).y in rng canon_image(Y,1) by FUNCT_1:3;
Y c= dom g by FUNCT_2:def 1; then
A15: dom canon_image(Y,1) c= dom g by Lm3;
rng g c= Z; then
rng g c= dom canon_image(Z,1) by Lm3; then
dom canon_image(Y,1) c= dom(canon_image(Z,1)*g) by A15,RELAT_1:27; then
A16: rng(canon_image(Y,1)") c= dom(canon_image(Z,1)*g) by FUNCT_1:33;
rng canon_image(Y,1) c= dom(canon_image(Y,1)") by FUNCT_1:33; then
A17: rng canon_image(Y,1) c=
dom((canon_image(Z,1)*g)*(canon_image(Y,1)")) by A16,RELAT_1:27;
A18: rng canon_image(Y,1) c= dom(canon_image(Y,1)") by FUNCT_1:33;
dom canon_image(Y,1) = Y by Lm3; then
A19: y in dom((canon_image(Y,1)")*canon_image(Y,1)) by A12,A18,RELAT_1:27;
A20: (canon_image(Z,1)*g)*(f*(canon_image(X,1)"))
= canon_image(Z,1)*(g*(f*(canon_image(X,1)"))) by RELAT_1:36
.= canon_image(Z,1)*((g*f)*(canon_image(X,1)")) by RELAT_1:36
.= (canon_image(Z,1)*(g*f))*(canon_image(X,1)") by RELAT_1:36;
thus f2.x = (free_magmaF g).((free_magmaF f).x) by A6,A5,FUNCT_1:12
.= (free_magmaF g).(((canon_image(Y,1)*f)*(canon_image(X,1)")).x)
by A10,A7,PARTFUN1:53
.= (free_magmaF g).((canon_image(Y,1)*(f*(canon_image(X,1)"))).x)
by RELAT_1:36
.= (free_magmaF g).(canon_image(Y,1).((f*(canon_image(X,1)")).x))
by A9,FUNCT_1:13
.= ((canon_image(Z,1)*g)*(canon_image(Y,1)")).(canon_image(Y,1).y)
by A17,A14,A11,PARTFUN1:53
.= (((canon_image(Z,1)*g)*(canon_image(Y,1)"))*canon_image(Y,1)).y
by A13,FUNCT_1:13
.= ((canon_image(Z,1)*g)*((canon_image(Y,1)")*canon_image(Y,1))).y
by RELAT_1:36
.= (canon_image(Z,1)*g).(((canon_image(Y,1)")*canon_image(Y,1)).y)
by A19,FUNCT_1:13
.= (canon_image(Z,1)*g).((f*(canon_image(X,1)")).x) by A13,FUNCT_1:34
.= (f9*(canon_image(X,1)")).x by A20,A9,FUNCT_1:13;
end; then
f2 tolerates f9*(canon_image(X,1)") by A5,PARTFUN1:53; then
f2 extends f9*(canon_image(X,1)") by A5;
hence free_magmaF(g*f) = free_magmaF(g)*free_magmaF(f) by Def21,A3;
end;
theorem Th45:
for g being Function of X,Z st Y c= Z & f=g
holds free_magmaF f = free_magmaF g
proof
let g be Function of X,Z;
assume A1: Y c= Z;
assume A2: f = g;
A3: the carrier of free_magma Y c= the carrier of free_magma Z
by A1,Th27; then
reconsider f9=free_magmaF f as Function of free_magma X, free_magma Z
by FUNCT_2:7;
for a, b being Element of free_magma X holds f9.(a * b) = (f9.a) * (f9.b)
proof
let a, b be Element of free_magma X;
set v = (free_magmaF f).a;
set w = (free_magmaF f).b;
reconsider v9=v, w9=w as Element of free_magma Z by A3;
A4: length v = v`2 by Def18 .= length v9 by Def18;
A5: length w = w`2 by Def18 .= length w9 by Def18;
thus f9.(a * b) = (free_magmaF f).a * (free_magmaF f).b by GROUP_6:def 6
.= [[[v9`1,w9`1],v9`2],(length v9) + (length w9)] by Th31,A4,A5
.= (f9.a) * (f9.b) by Th31;
end; then
A6: f9 is multiplicative by GROUP_6:def 6;
rng g c= Z; then
rng g c= dom canon_image(Z,1) by Lm3; then
A7: dom (canon_image(Z,1)*g) = dom g by RELAT_1:27;
X c= dom g by FUNCT_2:def 1; then
dom canon_image(X,1) c= dom (canon_image(Z,1)*g) by Lm3,A7; then
rng (canon_image(X,1)") c= dom (canon_image(Z,1)*g) by FUNCT_1:33; then
A8: dom((canon_image(Z,1)*g)*(canon_image(X,1)")) =
dom (canon_image(X,1)") by RELAT_1:27;
rng canon_image(X,1) c= the carrier of free_magma X; then
dom((canon_image(Z,1)*g)*(canon_image(X,1)")) c=
the carrier of free_magma X by A8,FUNCT_1:33; then
A9: dom((canon_image(Z,1)*g)*(canon_image(X,1)")) c= dom f9
by FUNCT_2:def 1;
for x being object st x in dom((canon_image(Z,1)*g)*(canon_image(X,1)"))
holds f9.x = ((canon_image(Z,1)*g)*(canon_image(X,1)")).x
proof
let x be object;
assume A10: x in dom((canon_image(Z,1)*g)*(canon_image(X,1)"));
free_magmaF(f) extends (canon_image(Y,1)*f)*(canon_image(X,1)")
by Def21; then
A11: dom((canon_image(Y,1)*f)*(canon_image(X,1)")) c= dom(free_magmaF f) &
(canon_image(Y,1)*f)*(canon_image(X,1)") tolerates free_magmaF f;
rng f c= Y; then
A12: rng f c= dom canon_image(Y,1) by Lm3;
rng f c= Z by A1; then
A13: rng f c= dom canon_image(Z,1) by Lm3;
A14: dom(canon_image(Y,1)*f) = dom f by A12,RELAT_1:27
.= dom(canon_image(Z,1)*f) by A13,RELAT_1:27;
for x being object st x in dom(canon_image(Y,1)*f)
holds (canon_image(Y,1)*f).x = (canon_image(Z,1)*f).x
proof
let x be object;
assume A15: x in dom(canon_image(Y,1)*f); then
A16: f.x in dom canon_image(Y,1) by FUNCT_1:11; then
A17: f.x in Y by Lm3;
thus (canon_image(Y,1)*f).x = canon_image(Y,1).(f.x) by A15,FUNCT_1:12
.= [f.x,1] by A16,Def19
.= canon_image(Z,1).(f.x) by A1,A17,Lm3
.= (canon_image(Z,1)*f).x by A14,A15,FUNCT_1:12;
end; then
canon_image(Y,1)*f = canon_image(Z,1)*g by A2,A14,FUNCT_1:2;
hence f9.x = ((canon_image(Z,1)*g)*(canon_image(X,1)")).x
by A10,A11,PARTFUN1:53;
end; then
f9 tolerates (canon_image(Z,1)*g)*(canon_image(X,1)")
by A9,PARTFUN1:53; then
f9 extends (canon_image(Z,1)*g)*(canon_image(X,1)") by A9;
hence free_magmaF f = free_magmaF g by A6,Def21;
end;
theorem Th46:
free_magmaF id X = id dom free_magmaF f
proof
dom free_magmaF id X = the carrier of free_magma X by FUNCT_2:def 1; then
A1: dom free_magmaF id X = dom free_magmaF f by FUNCT_2:def 1;
for x being object st x in dom free_magmaF f holds (free_magmaF id X).x = x
proof
let x be object;
assume A2: x in dom free_magmaF f;
defpred P[Nat] means for w being Element of free_magma X st length w = $1
holds (free_magmaF id X).w = w;
A3: for k being Nat st for n being Nat st n < k holds P[n] holds P[k]
proof
let k be Nat;
assume A4: for n being Nat st n < k holds P[n];
thus for w being Element of free_magma X st length w = k
holds (free_magmaF id X).w = w
proof
let w be Element of free_magma X;
assume A5: length w = k;
A6: w = [w`1,w`2] & length w >= 1 by Th32; then
length w = 1 or length w > 1 by XXREAL_0:1; then
A7: length w = 1 or length w +1 > 1+1 by XREAL_1:8;
per cases by A7,NAT_1:13;
suppose A8: length w = 1;
set y = w`1;
y in {w9`1 where w9 is Element of free_magma X: length w9 = 1}
by A8; then
A9: y in X by Th30; then
A10: y in dom id X;
(free_magmaF id X) extends
(canon_image(X,1)*id X)*(canon_image(X,1)") by Def21; then
A11: dom((canon_image(X,1)*id X)*(canon_image(X,1)")) c=
dom(free_magmaF id X) &
(canon_image(X,1)*id X)*(canon_image(X,1)") tolerates
free_magmaF id X;
A12: canon_image(X,1).y = [y,1] by A9,Lm3 .= w by Def18,A6,A8;
A13: y in dom canon_image(X,1) by A9,Lm3; then
w in rng canon_image(X,1) by A12,FUNCT_1:3; then
A14: w in dom(canon_image(X,1)") by FUNCT_1:33;
rng id X = dom canon_image(X,1) by Lm3; then
dom(canon_image(X,1)*id X) = dom id X by RELAT_1:27; then
X = dom(canon_image(X,1)*id X); then
dom canon_image(X,1) c= dom(canon_image(X,1)*id X) by Lm3; then
rng(canon_image(X,1)") c= dom(canon_image(X,1)*id X)
by FUNCT_1:33; then
A15: w in dom((canon_image(X,1)*id X)*(canon_image(X,1)"))
by A14,RELAT_1:27;
(canon_image(X,1)").w = y by A13,A12,FUNCT_1:34;
then ((canon_image(X,1)*id X)*(canon_image(X,1)")).w
= (canon_image(X,1)*id X).y by A15,FUNCT_1:12
.= canon_image(X,1).((id X).y) by A10,FUNCT_1:13
.= w by A12,A9,FUNCT_1:18;
hence (free_magmaF id X).w = w by A15,A11,PARTFUN1:53;
end;
suppose length w >= 2; then
consider w1,w2 be Element of free_magma X such that
A16: w = w1*w2 & length w1 < length w & length w2 < length w by Th34;
thus (free_magmaF id X).w
= (free_magmaF id X).w1 * (free_magmaF id X).w2
by A16,GROUP_6:def 6
.= w1 * (free_magmaF id X).w2 by A4,A5,A16
.= w by A4,A5,A16;
end;
end;
end;
A17: for k being Nat holds P[k] from NAT_1:sch 4(A3);
for w being Element of free_magma X holds (free_magmaF id X).w = w
proof
let w be Element of free_magma X;
reconsider k=length w as Nat;
P[k] by A17;
hence (free_magmaF id X).w = w;
end;
hence (free_magmaF id X).x = x by A2;
end;
hence free_magmaF id X = id dom free_magmaF f by A1,FUNCT_1:17;
end;
:: Ch I ?7.1 Pro.2 Algebra I Bourbaki
theorem
f is one-to-one implies free_magmaF f is one-to-one
proof
assume A1: f is one-to-one; then
A2: f"*f = id dom f by FUNCT_1:39;
set Y9 = rng f;
dom f = X by FUNCT_2:def 1; then
reconsider f1=f as Function of X, Y9 by FUNCT_2:1;
reconsider f2=f1" as Function of Y9, X by A1,FUNCT_2:25;
f2*f1 = id X by A2,FUNCT_2:def 1; then
(free_magmaF f2)*(free_magmaF f1) = free_magmaF(id X) by Th44; then
(free_magmaF f2)*(free_magmaF f) = free_magmaF(id X) by Th45; then
(free_magmaF f2)*(free_magmaF f) = id dom(free_magmaF f) by Th46;
hence free_magmaF f is one-to-one by FUNCT_1:31;
end;
:: Ch I ?7.1 Pro.2 Algebra I Bourbaki
theorem
f is onto implies free_magmaF f is onto
proof
assume A1: f is onto;
for y being object
st y in the carrier of free_magma Y holds y in rng free_magmaF f
proof
let y be object;
assume A2: y in the carrier of free_magma Y;
defpred P[Nat] means for w being Element of free_magma Y st length w = $1
holds ex v being Element of free_magma X st w = (free_magmaF f).v;
A3: for k being Nat st for n being Nat st n < k holds P[n] holds P[k]
proof
let k be Nat;
assume A4: for n being Nat st n < k holds P[n];
thus for w being Element of free_magma Y st length w = k
holds ex v being Element of free_magma X st w = (free_magmaF f).v
proof
let w be Element of free_magma Y;
assume A5: length w = k;
A6: w = [w`1,w`2] & length w >= 1 by Th32; then
length w = 1 or length w > 1 by XXREAL_0:1; then
A7: length w = 1 or length w +1 > 1+1 by XREAL_1:8;
per cases by A7,NAT_1:13;
suppose A8: length w = 1;
set y = w`1;
y in {w9`1 where w9 is Element of free_magma Y: length w9 = 1}
by A8; then
A9: y in Y by Th30;
(free_magmaF f) extends
(canon_image(Y,1)*f)*(canon_image(X,1)") by Def21; then
A10: dom((canon_image(Y,1)*f)*(canon_image(X,1)")) c=
dom(free_magmaF f) &
(canon_image(Y,1)*f)*(canon_image(X,1)") tolerates
free_magmaF f;
A11: canon_image(Y,1).y = [y,1] by A9,Lm3 .= w by Def18,A6,A8;
A12: rng f = Y by A1,FUNCT_2:def 3; then
consider x being object such that
A13: x in dom f & y = f.x by A9,FUNCT_1:def 3;
A14: 1 in {1} by TARSKI:def 1;
A15: x in X by A13; then
x in free_magma(X,1) by Def13; then
A16: [x,1] in [:free_magma(X,1),{1}:] by A14,ZFMISC_1:def 2;
[:free_magma(X,1),{1}:] c= free_magma_carrier X by Lm1; then
reconsider v = [x,1] as Element of free_magma X by A16;
take v;
A17: x in dom canon_image(X,1) by Lm3,A15;
A18: v = canon_image(X,1).x by Lm3,A13; then
v in rng canon_image(X,1) by A17,FUNCT_1:3; then
A19: v in dom(canon_image(X,1)") by FUNCT_1:33;
rng f = dom canon_image(Y,1) by Lm3,A12; then
dom f = dom(canon_image(Y,1)*f) by RELAT_1:27; then
X c= dom(canon_image(Y,1)*f) by FUNCT_2:def 1; then
dom canon_image(X,1) c= dom(canon_image(Y,1)*f) by Lm3; then
rng(canon_image(X,1)") c= dom(canon_image(Y,1)*f) by FUNCT_1:33; then
A20: v in dom((canon_image(Y,1)*f)*(canon_image(X,1)"))
by A19,RELAT_1:27; then
A21: (free_magmaF f).v
= ((canon_image(Y,1)*f)*(canon_image(X,1)")).v by A10,PARTFUN1:53
.= (canon_image(Y,1)*f).((canon_image(X,1)").v) by A20,FUNCT_1:12;
x in dom canon_image(X,1) by A15,Lm3; then
(canon_image(X,1)").v = x by A18,FUNCT_1:34;
hence thesis by A11,A13,A21,FUNCT_1:13;
end;
suppose length w >= 2; then
consider w1,w2 be Element of free_magma Y such that
A22: w = w1*w2 & length w1 < length w & length w2 < length w by Th34;
consider v1 be Element of free_magma X such that
A23: w1 = (free_magmaF f).v1 by A22,A4,A5;
consider v2 be Element of free_magma X such that
A24: w2 = (free_magmaF f).v2 by A22,A4,A5;
take v1*v2;
thus thesis by A23,A24,A22,GROUP_6:def 6;
end;
end;
end;
A25: for k being Nat holds P[k] from NAT_1:sch 4(A3);
A26: for w being Element of free_magma Y holds
ex v being Element of free_magma X st w = (free_magmaF f).v
proof
let w be Element of free_magma Y;
reconsider k=length w as Nat;
P[k] by A25;
hence thesis;
end;
ex x st x in dom free_magmaF f & y = (free_magmaF f).x
proof
consider x be Element of free_magma X such that
A27: y = (free_magmaF f).x by A2,A26;
take x;
x in the carrier of free_magma X;
hence x in dom free_magmaF f by FUNCT_2:def 1;
thus y = (free_magmaF f).x by A27;
end;
hence y in rng free_magmaF f by FUNCT_1:def 3;
end; then
the carrier of free_magma Y c= rng free_magmaF f; then
rng free_magmaF f = the carrier of free_magma Y by XBOOLE_0:def 10;
hence free_magmaF f is onto by FUNCT_2:def 3;
end;
:: added, SK 17.11.2024
registration
let M be empty multMagma;
let R be compatible Equivalence_Relation of M;
cluster M ./. R -> empty;
coherence;
end;
registration
let M be associative multMagma;
let R be compatible Equivalence_Relation of M;
cluster M ./. R -> associative;
coherence
proof
per cases;
suppose A1: M is non empty;
now
let X,Y,Z being Element of M ./. R;
consider x being Element of M such that
A2: X = Class(R,x) by A1, EQREL_1:36;
consider y being Element of M such that
A3: Y = Class(R,y) by A1, EQREL_1:36;
consider z being Element of M such that
A4: Z = Class(R,z) by A1, EQREL_1:36;
A5: Class(R,x*y) in Class R & Class(R,y*z) in Class R
by A1, EQREL_1:def 3;
thus (X*Y)*Z = (ClassOp R).(Class(R,x*y),Z) by A1, A2, A3, Def4
.= Class(R,(x*y)*z) by A1, A4, A5, Def4
.= Class(R,x*(y*z)) by GROUP_1:def 3
.= (ClassOp R).(X,Class(R,y*z)) by A1, A2, A5, Def4
.= X*(Y*Z) by A1, A3, A4, Def4;
end;
hence thesis by GROUP_1:def 3;
end;
suppose M is empty;
hence thesis;
end;
end;
end;
Lm1:
for M being unital non empty multMagma
for R be compatible Equivalence_Relation of M
for X,E being Element of M ./. R st E = Class(R,1_M)
holds X * E = X & E * X = X
proof
let M be unital non empty multMagma;
let R be compatible Equivalence_Relation of M;
let X,E be Element of M ./. R;
assume A1: E = Class(R,1_M);
consider x being Element of M such that
A2: X = Class(R,x) by EQREL_1:36;
thus X * E = Class(R,x*1_M) by A1, A2, Def4
.= X by A2, GROUP_1:def 4;
thus E * X = Class(R,1_M*x) by A1, A2, Def4
.= X by A2, GROUP_1:def 4;
end;
registration
let M be unital non empty multMagma;
let R be compatible Equivalence_Relation of M;
cluster M ./. R -> unital;
coherence
proof
reconsider E = Class(R,1_M) as Element of M ./. R by EQREL_1:def 3;
for X being Element of M ./. R holds X * E = X & E * X = X by Lm1;
hence thesis by GROUP_1:def 1;
end;
end;
theorem
for M being unital non empty multMagma
for R being compatible Equivalence_Relation of M
holds 1_(M ./. R) = Class(R,1_M)
proof
let M be unital non empty multMagma;
let R be compatible Equivalence_Relation of M;
reconsider E = Class(R,1_M) as Element of M ./. R by EQREL_1:def 3;
for X being Element of M ./. R holds X * E = X & E * X = X by Lm1;
hence thesis by GROUP_1:def 4;
end;