Copyright (c) 1992 Association of Mizar Users
environ
vocabulary VECTSP_1, BINOP_1, FUNCT_1, FINSEQ_1, RELAT_1, FUNCT_2, PARTFUN1,
CAT_1, ALGSTR_1, SETWISEO, FUNCOP_1, GROUP_1, FINSEQOP, VECTSP_2,
MCART_1, REALSET1, GR_CY_1, INT_1, BOOLE, MONOID_0;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, REAL_1, MCART_1,
DOMAIN_1, NAT_1, STRUCT_0, RELAT_1, FINSEQOP, FUNCT_1, FINSEQ_1,
RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, FINSEQ_2, INT_1, VECTSP_1,
VECTSP_2, SETWISEO, FUNCOP_1, GROUP_1, FUNCT_4, GR_CY_1;
constructors DOMAIN_1, NAT_1, BINOP_1, PARTFUN1, SETWISEO, FINSEQOP, GR_CY_1,
VECTSP_2, REAL_1, MEMBERED, RELAT_2, XBOOLE_0;
clusters SUBSET_1, FUNCT_1, FINSEQ_1, INT_1, VECTSP_1, GROUP_1, RELSET_1,
STRUCT_0, PARTFUN1, FUNCOP_1, MEMBERED, ZFMISC_1, FUNCT_2, XBOOLE_0,
ORDINAL2;
requirements NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, BINOP_1, SETWISEO, FINSEQOP, GROUP_1, VECTSP_1, STRUCT_0,
VECTSP_2, XBOOLE_0;
theorems TARSKI, NAT_1, INT_1, LANG1, FINSEQ_1, BINOP_1, GROUP_1, FINSEQOP,
SETWISEO, VECTSP_1, MCART_1, ZFMISC_1, FUNCT_1, FUNCT_2, FUNCT_4,
FUNCOP_1, PARTFUN1, RVSUM_1, GR_CY_1, GRFUNC_1, RELAT_1, STRUCT_0,
RELSET_1, VECTSP_2, XBOOLE_1, XCMPLX_1;
schemes FUNCT_2, BINOP_1, XBOOLE_0;
begin :: Updating
reserve x,y,X,Y for set;
deffunc carr(1-sorted) = the carrier of $1;
deffunc op(HGrStr) = the mult of $1;
definition let G be 1-sorted;
mode BinOp of G is BinOp of the carrier of G;
end;
definition let IT be 1-sorted;
attr IT is constituted-Functions means:
Def1:
for a being Element of IT holds a is Function;
attr IT is constituted-FinSeqs means:
Def2:
for a being Element of IT holds a is FinSequence;
end;
definition
cluster constituted-Functions 1-sorted;
existence
proof consider f being Function; take X = 1-sorted(#{f}#);
let a be Element of X;
thus thesis by TARSKI:def 1;
end;
cluster constituted-FinSeqs 1-sorted;
existence
proof consider f being FinSequence; take X = 1-sorted(#{f}#);
let a be Element of X;
thus thesis by TARSKI:def 1;
end;
end;
definition let X be constituted-Functions 1-sorted;
cluster -> Function-like Relation-like Element of X;
coherence by Def1;
end;
definition
cluster constituted-FinSeqs -> constituted-Functions 1-sorted;
coherence
proof let X be 1-sorted such that
A1: X is constituted-FinSeqs;
let a be Element of carr(X);
thus thesis by A1,Def2;
end;
end;
definition
cluster constituted-FinSeqs -> constituted-Functions HGrStr;
coherence
proof
now let G be HGrStr; assume G is constituted-FinSeqs;
then G is constituted-FinSeqs 1-sorted;
hence G is constituted-Functions;
end;
hence thesis;
end;
end;
definition let X be constituted-FinSeqs 1-sorted;
cluster -> FinSequence-like Element of X;
coherence by Def2;
end;
definition let D be set, p,q be FinSequence of D;
redefine func p^q -> Element of D*;
coherence
proof thus p^q is Element of D* by FINSEQ_1:def 11;
end;
end;
Lm1: (for X for f,g being Function of X,X holds f*g is Function of X,X) &
(for X for f,g being Permutation of X holds f*g is Permutation of X) &
(for X,Y,Z be set for f being PartFunc of X,Y
for g being PartFunc of Y,Z holds g*f is PartFunc of X,Z) &
(for X for A,B be non empty set for f being Function of X,A
for g be Function of A,B holds g*f is Function of X,B);
definition let g,f be Function;
redefine func f*g; synonym f(*)g;
end;
definition let X be set, g,f be Function of X,X;
redefine func f*g -> Function of X,X;
coherence by Lm1;
end;
definition let X be set, g,f be Permutation of X;
redefine func f*g -> Permutation of X;
coherence by Lm1;
end;
definition let D be non empty set;
let IT be BinOp of D;
attr IT is left-invertible means
for a,b being Element of D
ex l being Element of D st IT.(l,a) = b;
attr IT is right-invertible means
for a,b being Element of D
ex r being Element of D st IT.(a,r) = b;
attr IT is invertible means:Def5:
for a,b being Element of D ex r,l being Element of D st
IT.(a,r) = b & IT.(l,a) = b;
attr IT is left-cancelable means
for a,b,c being Element of D st IT.(a,b) = IT.(a,c)
holds b = c;
attr IT is right-cancelable means
for a,b,c being Element of D st IT.(b,a) = IT.(c,a)
holds b = c;
attr IT is cancelable means
for a,b,c being Element of D st
IT.(a,b) = IT.(a,c) or IT.(b,a) = IT.(c,a) holds b = c;
attr IT is uniquely-decomposable means
IT has_a_unity & for a,b being Element of D st
IT.(a,b) = the_unity_wrt IT holds a = b & b = the_unity_wrt IT;
end;
theorem Th1:
for D be non empty set, f being BinOp of D holds
f is invertible iff f is left-invertible right-invertible
proof let D be non empty set, f be BinOp of D;
thus f is invertible implies f is left-invertible right-invertible
proof assume
A1: for a,b being Element of D
ex r,l being Element of D st
f.(a,r) = b & f.(l,a) = b;
now let a,b be Element of D;
consider r,l being Element of D such that
A2: f.(a,r) = b & f.(l,a) = b by A1;
take l; thus f.(l,a) = b by A2;
end;
hence
for a,b being Element of D
ex l being Element of D st f.(l,a) = b;
let a,b be Element of D;
consider r,l being Element of D such that
A3: f.(a,r) = b & f.(l,a) = b by A1;
take r; thus thesis by A3;
end;
assume that
A4: for a,b being Element of D
ex l being Element of D st f.(l,a) = b and
A5: for a,b being Element of D
ex r being Element of D st f.(a,r) = b;
let a,b be Element of D;
consider l being Element of D such that
A6: f.(l,a) = b by A4;
consider r being Element of D such that
A7: f.(a,r) = b by A5;
take r, l; thus thesis by A6,A7;
end;
theorem Th2:
for D be non empty set, f being BinOp of D holds
f is cancelable iff f is left-cancelable right-cancelable
proof let D be non empty set, f be BinOp of D;
thus f is cancelable implies f is left-cancelable right-cancelable
proof assume
A1: for a,b,c being Element of D st
f.(a,b) = f.(a,c) or f.(b,a) = f.(c,a) holds b = c;
hence
for a,b,c being Element of D st f.(a,b) = f.(a,c)
holds b = c;
thus
for a,b,c being Element of D st f.(b,a) = f.(c,a)
holds b = c by A1;
end;
assume that
A2: for a,b,c being Element of D st f.(a,b) = f.(a,c)
holds b = c and
A3: for a,b,c being Element of D st f.(b,a) = f.(c,a)
holds b = c;
thus for a,b,c being Element of D st
f.(a,b) = f.(a,c) or f.(b,a) = f.(c,a) holds b = c by A2,A3;
end;
theorem Th3:
for f being BinOp of {x} holds f = {[x,x]} --> x &
f has_a_unity & f is commutative & f is associative & f is idempotent &
f is invertible cancelable uniquely-decomposable
proof let f be BinOp of {x};
reconsider a = x as Element of {x} by TARSKI:def 1;
A1: dom f = [:{x},{x}:] & dom ({[x,x]} --> x) = {[x,x]} & [:{x},{x}:] = {[x,x]}
by FUNCOP_1:19,FUNCT_2:def 1,ZFMISC_1:35;
now let y; assume
A2: y in {[x,x]};
then reconsider b = y as Element of [:{x},{x}:] by ZFMISC_1:35;
thus f.y = f.b .= x by TARSKI:def 1
.= ({[x,x]} --> x).y by A2,FUNCOP_1:13;
end;
hence f = {[x,x]} --> x by A1,FUNCT_1:9;
A3: now let a,b be Element of {x};
a = x & b = x by TARSKI:def 1;
hence a = b;
end;
then for b being Element of {x} holds f.(a,b) = b & f.(b,a) = b;
then A4: a is_a_unity_wrt f by BINOP_1:11;
hence
ex a being Element of {x} st a is_a_unity_wrt f;
thus for a,b being Element of {x} holds f.(a,b) = f.(b,a)
by A3;
thus for a,b,c being Element of {x} holds
f.(a,f.(b,c)) = f.(f.(a,b),c) by A3;
thus for a being Element of {x} holds f.(a,a) = a by A3;
thus for a,b being Element of {x}
ex r,l being Element of {x} st
f.(a,r) = b & f.(l,a) = b
proof let a,b be Element of {x}; take a,a;
thus f.(a,a) = b & f.(a,a) = b by A3;
end;
thus for a,b,c being Element of {x} st
f.(a,b) = f.(a,c) or f.(b,a) = f.(c,a) holds b = c by A3;
thus ex a being Element of {x} st a is_a_unity_wrt f by A4;
let a,b be Element of {x}; thus thesis by A3;
end;
begin :: Semigroups
reserve G for non empty HGrStr, D for non empty set,
a,b,c,r,l for Element of G;
definition let IT be non empty HGrStr;
redefine
attr IT is unital means:
Def10:
the mult of IT has_a_unity;
compatibility
proof
thus IT is unital implies the mult of IT has_a_unity
proof given e being Element of IT such that
A1: for h being Element of IT holds
h * e = h & e * h = h;
take e;
for a being Element of IT
holds (the mult of IT).(e,a) = a & (the mult of IT).(a,e) = a
proof let a be Element of IT;
thus (the mult of IT).(e,a) = e*a by VECTSP_1:def 10 .= a by A1;
thus (the mult of IT).(a,e) = a*e by VECTSP_1:def 10 .= a by A1;
end;
hence e is_a_unity_wrt the mult of IT by BINOP_1:11;
end;
given x being Element of IT such that
A2: x is_a_unity_wrt the mult of IT;
take x;
let h be Element of IT;
for a holds (the mult of IT).(x,h) = h &
(the mult of IT).(h,x) = h by A2,BINOP_1:11;
hence h * x = h & x * h = h by VECTSP_1:def 10;
end;
end;
definition let G;
redefine attr G is commutative means:Def11:
the mult of G is commutative;
compatibility
proof
thus G is commutative implies the mult of G is commutative
proof
assume
A1: a*b = b*a;
let a,b;
op(G).(a,b) = a*b & op(G).(b,a) = b*a by VECTSP_1:def 10;
hence thesis by A1;
end;
assume
A2: for a,b holds op(G).(a,b) = op(G).(b,a);
let a,b;
op(G).(a,b) = a*b & op(G).(b,a) = b*a by VECTSP_1:def 10;
hence thesis by A2;
end;
attr G is associative means:
Def12:
the mult of G is associative;
compatibility
proof
thus G is associative implies the mult of G is associative
proof
assume
A3: a*b*c = a*(b*c);
let a,b,c;
op(G).(a,b) = a*b & op(G).(b,c) = b*c & op(G).(a*b,c) = a*b*c &
op(G).(a,b*c) = a*(b*c) by VECTSP_1:def 10;
hence thesis by A3;
end;
assume
A4: for a,b,c holds op(G).(a,op(G).(b,c)) = op(G).(op(G).(a,b),c);
let a,b,c;
op(G).(a,b) = a*b & op(G).(b,c) = b*c & op(G).(a*b,c) = a*b*c &
op(G).(a,b*c) = a*(b*c) by VECTSP_1:def 10;
hence thesis by A4;
end;
end;
definition let IT be non empty HGrStr;
attr IT is idempotent means
the mult of IT is idempotent;
attr IT is left-invertible means
the mult of IT is left-invertible;
attr IT is right-invertible means
the mult of IT is right-invertible;
attr IT is invertible means:Def16:
the mult of IT is invertible;
attr IT is left-cancelable means
the mult of IT is left-cancelable;
attr IT is right-cancelable means
the mult of IT is right-cancelable;
attr IT is cancelable means
the mult of IT is cancelable;
attr IT is uniquely-decomposable means:Def20:
the mult of IT is uniquely-decomposable;
end;
definition
cluster unital commutative associative cancelable idempotent invertible
uniquely-decomposable constituted-Functions constituted-FinSeqs
strict (non empty HGrStr);
existence
proof consider p being FinSequence, o being BinOp of {p};
take G = HGrStr(#{p},o#);
thus op(G) has_a_unity & op(G) is commutative & op(G) is associative &
op(G) is cancelable & op(G) is idempotent &
op(G) is invertible uniquely-decomposable by Th3;
thus (for x being Element of G holds x is Function) &
(for x being Element of G holds x is FinSequence)
by TARSKI:def 1;
thus thesis;
end;
end;
theorem Th4:
G is unital implies
the_unity_wrt the mult of G is_a_unity_wrt the mult of G
proof given a such that
A1: a is_a_unity_wrt op(G);
thus thesis by A1,BINOP_1:def 8;
end;
theorem
G is unital iff for a holds
(the_unity_wrt the mult of G)*a = a &
a*(the_unity_wrt the mult of G) = a
proof set u = the_unity_wrt the mult of G;
thus G is unital implies for b holds u*b = b & b*u = b
proof given a such that
A1: a is_a_unity_wrt op(G);
let b;
a*b = (op(G)).(a,b) & b*a = (op(G)).(b,a) & u = a
by A1,BINOP_1:def 8,VECTSP_1:def 10;
hence thesis by A1,BINOP_1:11;
end;
assume
A2: u*b = b & b*u = b;
take a = u;
thus a is_a_left_unity_wrt the mult of G
proof let b; a*b = b by A2;
hence thesis by VECTSP_1:def 10;
end;
let b; b*a = b by A2;
hence thesis by VECTSP_1:def 10;
end;
theorem Th6:
G is unital iff ex a st for b holds a*b = b & b*a = b
proof
thus G is unital implies ex a st for b holds a*b = b & b*a = b
proof given a such that
A1: a is_a_unity_wrt the mult of G;
take a; let b;
a*b = (op(G)).(a,b) & b*a = (op(G)).(b,a) &
a is_a_left_unity_wrt op(G) &
a is_a_right_unity_wrt the mult of G
by A1,BINOP_1:def 7,VECTSP_1:def 10;
hence thesis by BINOP_1:def 5,def 6;
end;
given a such that
A2: a*b = b & b*a = b;
take a;
thus a is_a_left_unity_wrt the mult of G
proof let b; a*b = b by A2;
hence thesis by VECTSP_1:def 10;
end;
let b; b*a = b by A2;
hence thesis by VECTSP_1:def 10;
end;
Lm2:
G is commutative iff for a,b holds a*b = b*a
proof
thus G is commutative implies for a,b holds a*b = b*a
proof assume
A1: for a,b holds op(G).(a,b) = op(G).(b,a);
let a,b;
op(G).(a,b) = a*b & op(G).(b,a) = b*a by VECTSP_1:def 10;
hence thesis by A1;
end;
assume
A2: a*b = b*a;
let a,b;
op(G).(a,b) = a*b & op(G).(b,a) = b*a by VECTSP_1:def 10;
hence thesis by A2;
end;
Lm3:
G is associative iff for a,b,c holds a*b*c = a*(b*c)
proof
thus G is associative implies for a,b,c holds a*b*c = a*(b*c)
proof assume
A1: for a,b,c holds op(G).(a,op(G).(b,c)) = op(G).(op(G).(a,b),c);
let a,b,c;
op(G).(a,b) = a*b & op(G).(b,c) = b*c & op(G).(a*b,c) = a*b*c &
op(G).(a,b*c) = a*(b*c) by VECTSP_1:def 10;
hence thesis by A1;
end;
assume
A2: a*b*c = a*(b*c);
let a,b,c;
op(G).(a,b) = a*b & op(G).(b,c) = b*c & op(G).(a*b,c) = a*b*c &
op(G).(a,b*c) = a*(b*c) by VECTSP_1:def 10;
hence thesis by A2;
end;
canceled 2;
theorem Th9:
G is idempotent iff for a holds a*a = a
proof
thus G is idempotent implies for a holds a*a = a
proof assume
A1: op(G).(a,a) = a;
let a; thus a*a = op(G).(a,a) by VECTSP_1:def 10 .= a by A1;
end;
assume
A2: a*a = a;
let a; thus op(G).(a,a) = a*a by VECTSP_1:def 10 .= a by A2;
end;
theorem
G is left-invertible iff for a,b ex l st l*a = b
proof
thus G is left-invertible implies for a,b ex l st l*a = b
proof assume
A1: for a,b ex l st op(G).(l,a) = b;
let a,b; consider l such that
A2: op(G).(l,a) = b by A1;
take l; thus thesis by A2,VECTSP_1:def 10;
end;
assume
A3: for a,b ex l st l*a = b;
let a,b; consider l such that
A4: l*a = b by A3;
take l; thus thesis by A4,VECTSP_1:def 10;
end;
theorem
G is right-invertible iff for a,b ex r st a*r = b
proof
thus G is right-invertible implies for a,b ex r st a*r = b
proof assume
A1: for a,b ex r st op(G).(a,r) = b;
let a,b; consider r such that
A2: op(G).(a,r) = b by A1;
take r; thus thesis by A2,VECTSP_1:def 10;
end;
assume
A3: for a,b ex r st a*r = b;
let a,b; consider r such that
A4: a*r = b by A3;
take r; thus thesis by A4,VECTSP_1:def 10;
end;
theorem Th12:
G is invertible iff for a,b ex r,l st a*r = b & l*a = b
proof
thus G is invertible implies for a,b ex r,l st a*r = b & l*a = b
proof assume
A1: for a,b ex r,l st op(G).(a,r) = b & op(G).(l,a) = b;
let a,b; consider r, l such that
A2: op(G).(a,r) = b & op(G).(l,a) = b by A1;
take r, l; thus thesis by A2,VECTSP_1:def 10;
end;
assume
A3: for a,b ex r,l st a*r = b & l*a = b;
let a,b; consider r, l such that
A4: a*r = b & l*a = b by A3;
take r, l; thus thesis by A4,VECTSP_1:def 10;
end;
theorem
G is left-cancelable iff for a,b,c st a*b = a*c holds b = c
proof
thus G is left-cancelable implies for a,b,c st a*b = a*c holds b = c
proof assume
A1: op(G).(a,b) = op(G).(a,c) implies b = c;
let a,b,c;
a*b = op(G).(a,b) & a*c = op(G).(a,c) by VECTSP_1:def 10;
hence thesis by A1;
end;
assume
A2: for a,b,c st a*b = a*c holds b = c;
let a,b,c;
a*b = op(G).(a,b) & a*c = op(G).(a,c) by VECTSP_1:def 10;
hence thesis by A2;
end;
theorem
G is right-cancelable iff for a,b,c st b*a = c*a holds b = c
proof
thus G is right-cancelable implies for a,b,c st b*a = c*a holds b = c
proof assume
A1: for a,b,c st op(G).(b,a) = op(G).(c,a) holds b = c;
let a,b,c;
b*a = op(G).(b,a) & c*a = op(G).(c,a) by VECTSP_1:def 10;
hence thesis by A1;
end;
assume
A2: for a,b,c st b*a = c*a holds b = c;
let a,b,c;
b*a = op(G).(b,a) & c*a = op(G).(c,a) by VECTSP_1:def 10;
hence thesis by A2;
end;
theorem Th15:
G is cancelable iff for a,b,c st a*b = a*c or b*a = c*a holds b = c
proof
thus G is cancelable implies for a,b,c st a*b = a*c or b*a = c*a holds b=c
proof assume
A1: op(G).(a,b) = op(G).(a,c) or op(G).(b,a) = op(G).(c,a) implies b = c;
let a,b,c;
a*b = op(G).(a,b) & a*c = op(G).(a,c) &
b*a = op(G).(b,a) & c*a = op(G).(c,a) by VECTSP_1:def 10;
hence thesis by A1;
end;
assume
A2: for a,b,c st a*b = a*c or b*a = c*a holds b = c;
let a,b,c;
a*b = op(G).(a,b) & a*c = op(G).(a,c) &
b*a = op(G).(b,a) & c*a = op(G).(c,a) by VECTSP_1:def 10;
hence thesis by A2;
end;
theorem Th16:
G is uniquely-decomposable iff the mult of G has_a_unity &
for a,b being Element of G
st a*b = the_unity_wrt the mult of G
holds a = b & b = the_unity_wrt the mult of G
proof
thus G is uniquely-decomposable implies op(G) has_a_unity &
for a,b being Element of G st a*b = the_unity_wrt op(G)
holds a = b & b = the_unity_wrt the mult of G
proof assume
A1: op(G) has_a_unity & for a,b being Element of G st
op(G).(a,b) = the_unity_wrt op(G) holds
a = b & b = the_unity_wrt op(G);
hence op(G) has_a_unity; let a,b be Element of G;
a*b = op(G).(a,b) by VECTSP_1:def 10;
hence thesis by A1;
end;
assume
A2: op(G) has_a_unity & for a,b being Element of G st
a*b = the_unity_wrt op(G) holds a = b & b = the_unity_wrt op(G);
hence op(G) has_a_unity; let a,b be Element of G;
a*b = op(G).(a,b) by VECTSP_1:def 10;
hence thesis by A2;
end;
theorem Th17:
G is associative implies
(G is invertible iff G is unital & the mult of G has_an_inverseOp)
proof assume
A1: G is associative;
thus G is invertible implies G is unital & op(G) has_an_inverseOp
proof assume
A2: G is invertible;
consider e being Element of G;
consider x,y being Element of G such that
A3: e*x = e & y*e = e by A2,Th12;
A4: now let a; consider b,c such that
A5: e*b = a & c*e = a by A2,Th12;
thus y*a = a by A1,A3,A5,Lm3;
thus a*x = a by A1,A3,A5,Lm3;
end;
then A6: y*x = x & y*x = y;
hence G is unital by A4,Th6;
defpred P[Element of G,Element of G]
means $1*$2 = x & $2*$1 = x;
A7: for a ex b st P[a,b]
proof let a; consider b,c such that
A8: a*b = x & c*a = x by A2,Th12;
take b;
c*(a*b) = c*a*b & x*b = b & c*x = c by A1,A4,A6,Lm3;
hence thesis by A8;
end;
ex f being Function of the carrier of G,the carrier of G
st for x being Element of G holds P[x,f.x]
from FuncExD(A7); then
consider u being UnOp of carr(G) such that
A9: for a being Element of G holds
P[a,(u.a)];:: from FuncExD(A7);
take u; let a;
now let b; x*b = op(G).(x,b) & b*x = op(G).(b,x) by VECTSP_1:def 10;
hence op(G).(x,b) = b & op(G).(b,x) = b by A4,A6;
end;
then x is_a_unity_wrt op(G) by BINOP_1:11;
then x = the_unity_wrt op(G) & op(G).(a,u.a) = a*(u.a) &
op(G).(u.a,a) = (u.a)*a by BINOP_1:def 8,VECTSP_1:def 10;
hence thesis by A9;
end;
assume
A10: op(G) has_a_unity;
given u being UnOp of carr(G) such that
A11: u is_an_inverseOp_wrt op(G);
let a,c;
take l = (u.a)*c, r = c*(u.a);
thus op(G).(a,l) = a*l by VECTSP_1:def 10 .= a*(u.a)*c by A1,Lm3
.= op(G).(a*(u.a),c) by VECTSP_1:def 10
.= op(G).(op(G).(a,u.a),c) by VECTSP_1:def 10
.= op(G).(the_unity_wrt op(G),c) by A11,FINSEQOP:def 1
.= c by A10,SETWISEO:23;
thus op(G).(r,a) = r*a by VECTSP_1:def 10 .= c*((u.a)*a) by A1,Lm3
.= op(G).(c,(u.a)*a) by VECTSP_1:def 10
.= op(G).(c,op(G).(u.a,a)) by VECTSP_1:def 10
.= op(G).(c,the_unity_wrt op(G)) by A11,FINSEQOP:def 1
.= c by A10,SETWISEO:23;
end;
Lm4: G is invertible iff G is left-invertible right-invertible
proof
thus G is invertible implies G is left-invertible right-invertible
proof assume op(G) is invertible;
hence op(G) is left-invertible right-invertible by Th1;
end;
assume op(G) is left-invertible right-invertible;
hence op(G) is invertible by Th1;
end;
Lm5: G is cancelable iff G is left-cancelable right-cancelable
proof
thus G is cancelable implies G is left-cancelable right-cancelable
proof assume op(G) is cancelable;
hence op(G) is left-cancelable right-cancelable by Th2;
end;
assume op(G) is left-cancelable right-cancelable;
hence op(G) is cancelable by Th2;
end;
Lm6: G is associative invertible implies G is Group-like
proof assume
A1: G is associative invertible;
then G is unital by Th17;
then consider a such that
A2: for b holds a*b = b & b*a = b by Th6;
take a; let b;
thus b*a = b & a*b = b by A2;
op(G) is invertible by A1,Def16;
then consider l,r being Element of G such that
A3: op(G).(b,l) = a & op(G).(r,b) = a by Def5;
A4: b*l = a & r*b = a by A3,VECTSP_1:def 10;
take l;
r = r*a by A2 .= a*l by A1,A4,Lm3 .= l by A2;
hence thesis by A3,VECTSP_1:def 10;
end;
definition
cluster associative Group-like -> invertible (non empty HGrStr);
coherence
proof let G be non empty HGrStr; assume
G is associative Group-like;
then reconsider G as associative Group-like (non empty HGrStr);
G is unital associative & op(G) has_an_inverseOp
by GROUP_1:36;
hence thesis by Th17;
end;
cluster associative invertible -> Group-like (non empty HGrStr);
coherence by Lm6;
end;
definition
cluster invertible -> left-invertible right-invertible (non empty HGrStr);
coherence by Lm4;
cluster left-invertible right-invertible -> invertible (non empty HGrStr);
coherence by Lm4;
cluster cancelable -> left-cancelable right-cancelable (non empty HGrStr);
coherence by Lm5;
cluster left-cancelable right-cancelable -> cancelable (non empty HGrStr);
coherence by Lm5;
cluster associative invertible -> unital cancelable (non empty HGrStr);
coherence
proof let G be non empty HGrStr;
assume G is associative invertible;
then reconsider G as associative invertible (non empty HGrStr);
for a,b,c being Element of G st
a*b = a*c or b*a = c*a holds b = c by GROUP_1:14;
hence thesis by Th15;
end;
end;
begin :: Monoids
deffunc un(multLoopStr) = the unity of $1;
reserve M for non empty multLoopStr;
definition let IT be non empty multLoopStr;
redefine attr IT is well-unital means:Def21:
the unity of IT is_a_unity_wrt the mult of IT;
compatibility
proof
thus IT is well-unital implies the unity of IT is_a_unity_wrt the mult of
IT
proof assume
A1: IT is well-unital;
thus the unity of IT is_a_left_unity_wrt the mult of IT
proof let a be Element of IT;
thus (the mult of IT).(the unity of IT,a)
= (the unity of IT)*a by VECTSP_1:def 10
.= (1_ IT)*a by VECTSP_1:def 9
.= a by A1,VECTSP_2:def 2;
end;
let a be Element of IT;
thus (the mult of IT).(a,the unity of IT)
= a*(the unity of IT) by VECTSP_1:def 10
.= a*(1_ IT) by VECTSP_1:def 9
.= a by A1,VECTSP_2:def 2;
end;
assume
A2: the unity of IT is_a_unity_wrt the mult of IT;
let x be Element of IT;
A3: the unity of IT is_a_right_unity_wrt the mult of IT by A2,BINOP_1:def 7;
thus x*(1_ IT) = x*(the unity of IT) by VECTSP_1:def 9
.= (the mult of IT).(x,the unity of IT) by VECTSP_1:def 10
.= x by A3,BINOP_1:def 6;
A4: the unity of IT is_a_left_unity_wrt the mult of IT by A2,BINOP_1:def 7;
thus (1_ IT)*x = (the unity of IT)*x by VECTSP_1:def 9
.= (the mult of IT).(the unity of IT,x) by VECTSP_1:def 10
.= x by A4,BINOP_1:def 5;
end;
end;
theorem Th18:
M is well-unital iff for a being Element of M holds
(the unity of M)*a = a & a*(the unity of M) = a
proof
A1: M is well-unital iff un(M) is_a_unity_wrt op(M) by Def21;
thus M is well-unital implies
for a being Element of M holds un(M)*a = a & a*un(M) = a
proof assume
A2: M is well-unital;
let a be Element of M;
op(M).(un(M),a) = a & (the mult of M).(a,un(M)) = a by A1,A2,BINOP_1:11;
hence thesis by VECTSP_1:def 10;
end;
assume
A3: for a being Element of M holds un(M)*a = a & a*un(M) = a;
now let a be Element of M;
un(M)*a = a & a*un(M) = a by A3;
hence op(M).(un(M),a) = a & op(M).(a,un(M)) = a by VECTSP_1:def 10;
end;
hence thesis by A1,BINOP_1:11;
end;
Lm7: for M being non empty multLoopStr st M is well-unital holds M is unital
proof let M be non empty multLoopStr;
assume un(M) is_a_unity_wrt the mult of M;
hence op(M) has_a_unity by SETWISEO:def 2;
end;
definition
cluster well-unital -> unital (non empty multLoopStr);
coherence by Lm7;
end;
theorem Th19:
for M being non empty multLoopStr st M is well-unital holds
the unity of M = the_unity_wrt the mult of M
proof let M be non empty multLoopStr;
assume un(M) is_a_unity_wrt the mult of M;
hence thesis by BINOP_1:def 8;
end;
definition let A be non empty set, m be BinOp of A,
u be Element of A;
cluster multLoopStr(#A,m,u#) -> non empty;
coherence by STRUCT_0:def 1;
end;
definition
cluster well-unital commutative associative cancelable idempotent invertible
uniquely-decomposable unital constituted-Functions
constituted-FinSeqs strict (non empty multLoopStr);
existence
proof consider p being FinSequence,
o being BinOp of {p}, e being Element of {p};
take G = multLoopStr(#{p},o,e#);
reconsider e as Element of G;
reconsider o as BinOp of G;
now let b be Element of G;
o.(e,b) = p & o.(b,e) = p & b = p by TARSKI:def 1;
hence o.(e,b) = b & o.(b,e) = b;
end;
hence un(G) is_a_unity_wrt op(G) by BINOP_1:11;
hence op(G) is commutative & op(G) is associative & op(G) is cancelable &
op(G) is idempotent & op(G) is invertible uniquely-decomposable &
ex e being Element of G st e is_a_unity_wrt op(G) by Th3;
thus (for x being Element of G holds x is Function) &
(for x being Element of G holds x is FinSequence)
by TARSKI:def 1;
thus thesis;
end;
end;
definition
mode Monoid is well-unital associative (non empty multLoopStr);
end;
definition let G be HGrStr;
mode MonoidalExtension of G -> multLoopStr means:Def22:
the HGrStr of it = the HGrStr of G;
existence
proof consider g being Element of G;
take M = multLoopStr(#carr(G), op(G), g#);
thus the HGrStr of M = the HGrStr of G;
end;
end;
definition let G be non empty HGrStr;
cluster -> non empty MonoidalExtension of G;
coherence
proof let M be MonoidalExtension of G;
the HGrStr of M = the HGrStr of G by Def22;
hence the carrier of M is non empty;
end;
end;
theorem Th20:
for M being MonoidalExtension of G holds
the carrier of M = the carrier of G &
the mult of M = the mult of G &
for a,b being Element of M,
a',b' being Element of G st a = a' & b = b'
holds a*b = a'*b'
proof let M be MonoidalExtension of G;
A1: the HGrStr of M = the HGrStr of G by Def22;
hence carr(M) = carr(G) & op(M) = op(G);
let a,b be Element of M,
a',b' be Element of G;
a*b = op(M).(a,b) & a'*b' = op(G).(a',b') by VECTSP_1:def 10;
hence thesis by A1;
end;
definition let G be HGrStr;
cluster strict MonoidalExtension of G;
existence
proof consider g being Element of G;
set M = multLoopStr(#carr(G), op(G), g#);
the HGrStr of M = the HGrStr of G;
then M is MonoidalExtension of G by Def22;
hence thesis;
end;
end;
theorem Th21:
for G being non empty HGrStr, M being MonoidalExtension of G holds
(G is unital implies M is unital) &
(G is commutative implies M is commutative) &
(G is associative implies M is associative) &
(G is invertible implies M is invertible) &
(G is uniquely-decomposable implies M is uniquely-decomposable) &
(G is cancelable implies M is cancelable)
proof let G be non empty HGrStr, M be MonoidalExtension of G;
A1: the HGrStr of M = the HGrStr of G by Def22;
thus G is unital implies M is unital
proof assume op(G) has_a_unity; hence op(M) has_a_unity by A1;
end;
thus G is commutative implies M is commutative
proof assume op(G) is commutative; hence op(M) is commutative by A1;
end;
thus G is associative implies M is associative
proof assume op(G) is associative; hence op(M) is associative by A1;
end;
thus G is invertible implies M is invertible
proof assume op(G) is invertible; hence op(M) is invertible by A1;
end;
thus G is uniquely-decomposable implies M is uniquely-decomposable
proof assume op(G) is uniquely-decomposable;
hence op(M) is uniquely-decomposable by A1;
end;
assume op(G) is cancelable;
hence op(M) is cancelable by A1;
end;
definition let G be constituted-Functions HGrStr;
cluster -> constituted-Functions MonoidalExtension of G;
coherence
proof let M be MonoidalExtension of G; let a be Element of M;
the HGrStr of M = the HGrStr of G by Def22;
then a is Element of G;
hence thesis;
end;
end;
definition let G be constituted-FinSeqs HGrStr;
cluster -> constituted-FinSeqs MonoidalExtension of G;
coherence
proof let M be MonoidalExtension of G; let a be Element of M;
the HGrStr of M = the HGrStr of G by Def22;
then a is Element of G;
hence thesis;
end;
end;
definition let G be unital (non empty HGrStr);
cluster -> unital MonoidalExtension of G;
coherence by Th21;
end;
definition let G be associative (non empty HGrStr);
cluster -> associative MonoidalExtension of G;
coherence by Th21;
end;
definition let G be commutative (non empty HGrStr);
cluster -> commutative MonoidalExtension of G;
coherence by Th21;
end;
definition let G be invertible (non empty HGrStr);
cluster -> invertible MonoidalExtension of G;
coherence by Th21;
end;
definition let G be cancelable (non empty HGrStr);
cluster -> cancelable MonoidalExtension of G;
coherence by Th21;
end;
definition let G be uniquely-decomposable (non empty HGrStr);
cluster -> uniquely-decomposable MonoidalExtension of G;
coherence by Th21;
end;
definition let G be unital (non empty HGrStr);
cluster well-unital strict MonoidalExtension of G;
existence
proof set M = multLoopStr(#carr(G), op(G), the_unity_wrt op(G)#);
M is MonoidalExtension of G
proof
thus the HGrStr of M = the HGrStr of G;
end;
then reconsider M as MonoidalExtension of G;
take M;
thus un(M) is_a_unity_wrt op(M) by Th4;
thus thesis;
end;
end;
theorem Th22:
for G being unital (non empty HGrStr)
for M1,M2 being well-unital strict MonoidalExtension of G holds M1 = M2
proof let G be unital (non empty HGrStr);
let M1,M2 be well-unital strict MonoidalExtension of G;
the HGrStr of M1 = the HGrStr of G & the HGrStr of M2 = the HGrStr of G &
un(M1) = the_unity_wrt op(M1) & un(M2) = the_unity_wrt op(M2)
by Def22,Th19;
hence thesis;
end;
begin :: Subsystems
definition let G be HGrStr;
mode SubStr of G -> HGrStr means:Def23:
the mult of it <= the mult of G;
existence;
end;
definition let G be HGrStr;
cluster strict SubStr of G;
existence
proof
the HGrStr of G is SubStr of G by Def23;
hence thesis;
end;
end;
definition let G be non empty HGrStr;
cluster strict non empty SubStr of G;
existence
proof
the HGrStr of G is SubStr of G by Def23;
hence thesis;
end;
end;
definition let G be unital (non empty HGrStr);
cluster unital associative commutative cancelable idempotent invertible
uniquely-decomposable strict (non empty SubStr of G);
existence
proof consider a being Element of G such that
A1: for b being Element of G holds a*b = b & b*a = b by Th6;
consider f being BinOp of {a};
set H = HGrStr(#{a},f#);
f = {[a,a]} --> a & a = a*a & a*a = op(G).(a,a) &
op(G).(a,a) = op(G).[a,a] & dom op(G) = [:carr(G),carr(G):]
by A1,Th3,BINOP_1:def 1,FUNCT_2:def 1,VECTSP_1:def 10;
then op(H) <= op(G) by FUNCT_4:8;
then reconsider H as non empty SubStr of G by Def23;
take H;
thus op(H) has_a_unity & op(H) is associative & op(H) is commutative &
op(H) is cancelable & op(H) is idempotent &
op(H) is invertible uniquely-decomposable by Th3;
thus thesis;
end;
end;
definition let G be HGrStr;
mode MonoidalSubStr of G -> multLoopStr means:Def24:
the mult of it <= the mult of G &
for M being multLoopStr st G = M holds the unity of it = the unity of M;
existence
proof consider M being MonoidalExtension of G;
A1: the HGrStr of M = the HGrStr of G by Def22;
A2: now given M being multLoopStr such that
A3: G = M;
take M; thus op(M) <= op(G) by A3;
thus for N being multLoopStr st G = N holds
un(M) = un(N) by A3;
end;
(ex M being multLoopStr st G = M) or for N being multLoopStr st G = N
holds
un(M) = un(N);
hence thesis by A1,A2;
end;
end;
definition let G be HGrStr;
cluster strict MonoidalSubStr of G;
existence
proof consider N being MonoidalSubStr of G;
op(the multLoopStr of N) <= op(G) &
for M being multLoopStr st G = M
holds un(the multLoopStr of N) = un(M) by Def24;
then reconsider N' = the multLoopStr of N as MonoidalSubStr of G by Def24;
take N'; thus thesis;
end;
end;
definition let G be non empty HGrStr;
cluster strict non empty MonoidalSubStr of G;
existence
proof
per cases;
suppose G is multLoopStr;
then reconsider L = G as multLoopStr;
for N being multLoopStr st G = N
holds the unity of the multLoopStr of L = the unity of N;
then reconsider M = the multLoopStr of L as MonoidalSubStr of G
by Def24;
take M;
thus M is strict;
the carrier of M = the carrier of G;
hence the carrier of M is non empty;
suppose
A1: G is not multLoopStr;
consider M being strict MonoidalExtension of G;
A2: the HGrStr of M = the HGrStr of G by Def22;
for N being multLoopStr st G = N holds the unity of M = the unity of N
by A1;
then reconsider M as MonoidalSubStr of G by A2,Def24;
take M;
thus thesis;
end;
end;
definition let M be multLoopStr;
redefine mode MonoidalSubStr of M means:Def25:
the mult of it <= the mult of M &
the unity of it = the unity of M;
compatibility
proof let N be multLoopStr;
thus N is MonoidalSubStr of M implies op(N) <= op(M) & un(N) = un(M)
proof assume
op(N) <= op(M) & for K being multLoopStr st M = K holds un(N) = un(K);
hence thesis;
end;
assume op(N) <= op(M) & un(N) = un(M);
hence op(N) <=
op(M) & for K being multLoopStr st M = K holds un(N) = un(K);
end;
end;
definition let G be well-unital (non empty multLoopStr);
cluster well-unital associative commutative cancelable idempotent invertible
uniquely-decomposable strict (non empty MonoidalSubStr of G);
existence
proof set a = un(G);
reconsider e = a as Element of {a} by TARSKI:def 1;
consider f being BinOp of {a};
set H = multLoopStr(#{a},f,e#);
f = {[a,a]} --> a & a = a*a & a*a = op(G).(a,a) &
op(G).(a,a) = op(G).[a,a] & dom op(G) = [:carr(G),carr(G):]
by Th3,Th18,BINOP_1:def 1,FUNCT_2:def 1,VECTSP_1:def 10;
then op(H) <= op(G) by FUNCT_4:8;
then reconsider H as non empty MonoidalSubStr of G by Def25;
take H;
now let b be Element of H; b = a by TARSKI:def 1;
hence op(H).(un(H),b) = b & op(H).(b,un(H)) = b by TARSKI:def 1;
end;
hence un(H) is_a_unity_wrt op(H) by BINOP_1:11;
thus op(H) is associative & op(H) is commutative &
op(H) is cancelable & op(H) is idempotent &
op(H) is invertible uniquely-decomposable by Th3;
thus thesis;
end;
end;
theorem Th23:
for G being HGrStr, M being MonoidalSubStr of G holds M is SubStr of G
proof let G be HGrStr, M be MonoidalSubStr of G;
thus op(M) <= op(G) by Def24;
end;
definition let G be HGrStr, M be MonoidalExtension of G;
redefine mode SubStr of M -> SubStr of G;
coherence
proof let N be SubStr of M;
the HGrStr of M = the HGrStr of G by Def22;
hence op(N) <= op(G) by Def23;
end;
end;
definition let G1 be HGrStr, G2 be SubStr of G1;
redefine mode SubStr of G2 -> SubStr of G1;
coherence
proof let G be SubStr of G2;
op(G) <= op(G2) & op(G2) <= op(G1) by Def23;
hence op(G) <= op(G1) by XBOOLE_1:1;
end;
end;
definition let G1 be HGrStr, G2 be MonoidalSubStr of G1;
redefine mode SubStr of G2 -> SubStr of G1;
coherence
proof let G be SubStr of G2;
reconsider H = G2 as SubStr of G1 by Th23;
G is SubStr of H;
hence thesis;
end;
end;
definition let G be HGrStr, M be MonoidalSubStr of G;
redefine mode MonoidalSubStr of M -> MonoidalSubStr of G;
coherence
proof let M' be MonoidalSubStr of M;
op(M') <= op(M) & op(M) <= op(G) & un(M') = un(M) &
for N being multLoopStr st G = N holds un(M) = un(N) by Def24;
hence
op(M') <= op(G) & for N being multLoopStr st G = N holds un(M') = un(N)
by XBOOLE_1:1;
end;
end;
theorem
G is SubStr of G & M is MonoidalSubStr of M
proof
thus op(G) <= op(G);
thus op(M) <= op(M);
thus thesis;
end;
reserve H for non empty SubStr of G, N for non empty MonoidalSubStr of G;
theorem Th25:
the carrier of H c= the carrier of G & the carrier of N c= the carrier of G
proof op(H) <= op(G) & op(N) <= op(G) by Def23,Def24;
then A1: dom op(H) c= dom op(G) & dom op(H) = [:carr(H), carr(H):] &
dom op(N) c= dom op(G) & dom op(N) = [:carr(N), carr(N):] &
dom op(G) = [:carr(G), carr(G):] by FUNCT_2:def 1,GRFUNC_1:8;
thus carr(H) c= carr(G)
proof let x; assume x in carr(H);
then [x,x] in dom op(H) by A1,ZFMISC_1:106; hence thesis by A1,ZFMISC_1:
106;
end;
let x; assume x in carr(N);
then [x,x] in dom op(N) by A1,ZFMISC_1:106; hence thesis by A1,ZFMISC_1:106
;
end;
theorem Th26:
for G being non empty HGrStr, H being non empty SubStr of G
holds the mult of H = (the mult of G)|[:the carrier of H,the carrier of H:]
proof let G be non empty HGrStr, H be non empty SubStr of G;
op(H) <= op(G) & dom op(H) = [:carr(H),carr(H):] by Def23,FUNCT_2:def 1;
hence thesis by GRFUNC_1:64;
end;
theorem Th27:
for a,b being Element of H,
a',b' being Element of G st
a = a' & b = b' holds a*b = a'*b'
proof let a,b be Element of H,
a',b' be Element of G such that
A1: a = a' & b = b';
A2: dom op(H) = [:carr(H), carr(H):] & op(H) <= op(G) by Def23,FUNCT_2:def 1;
thus a*b = op(H).(a,b) by VECTSP_1:def 10
.= op(H).[a,b] by BINOP_1:def 1
.= op(G).[a',b'] by A1,A2,GRFUNC_1:8
.= op(G).(a',b') by BINOP_1:def 1
.= a'*b' by VECTSP_1:def 10;
end;
theorem Th28:
for H1,H2 being non empty SubStr of G
st the carrier of H1 = the carrier of H2
holds the HGrStr of H1 = the HGrStr of H2
proof let H1,H2 be non empty SubStr of G; assume
A1: carr(H1) = carr(H2);
then op(H1) <= op(G) & op(H2) <= op(G) &
dom op(H1) = [:carr(H1), carr(H1):] &
dom op(H2) = [:carr(H1), carr(H1):] by Def23,FUNCT_2:def 1;
then the HGrStr of H1 = HGrStr(#carr(H1), op(H1)#) &
the HGrStr of H2 = HGrStr(#carr(H2), op(H2)#) &
op(H1) = op(G)|[:carr(H1), carr(H1):] &
op(H2) = op(G)|[:carr(H1), carr(H1):] by GRFUNC_1:64;
hence thesis by A1;
end;
theorem
for H1,H2 being non empty MonoidalSubStr of M st
the carrier of H1 = the carrier of H2 holds
the multLoopStr of H1 = the multLoopStr of H2
proof let H1,H2 be non empty MonoidalSubStr of M such that
A1: the carrier of H1 = the carrier of H2;
reconsider N1 = H1, N2 = H2 as SubStr of M by Th23;
the HGrStr of N1 = the HGrStr of N2 & un(H1) = un(M) & un(H2) = un(M)
by A1,Def25,Th28;
hence thesis;
end;
theorem Th30:
for H1,H2 being non empty SubStr of G
st the carrier of H1 c= the carrier of H2
holds H1 is SubStr of H2
proof let H1,H2 be non empty SubStr of G; assume carr(H1) c= carr(H2);
then op(H1) <= op(G) & op(H2) <= op(G) &
dom op(H1) = [:carr(H1), carr(H1):] &
[:carr(H1), carr(H1):] c= [:carr(H2), carr(H2):] &
dom op(H2) = [:carr(H2), carr(H2):]
by Def23,FUNCT_2:def 1,ZFMISC_1:119;
then (op(G)|[:carr(H2), carr(H2):])|[:carr(H1), carr(H1):] =
op(G)|[:carr(H1), carr(H1):] & op(H1) = op(G)|[:carr(H1), carr(H1):] &
op(H2) = op(G)|[:carr(H2), carr(H2):] by FUNCT_1:82,GRFUNC_1:64;
hence op(H1) <= op(H2) by RELAT_1:88;
end;
theorem
for H1,H2 being non empty MonoidalSubStr of M st
the carrier of H1 c= the carrier of H2 holds H1 is MonoidalSubStr of H2
proof let H1,H2 be non empty MonoidalSubStr of M such that
A1: carr(H1) c= carr(H2);
H1 is SubStr of M & H2 is SubStr of M by Th23;
then H1 is SubStr of H2 by A1,Th30;
hence op(H1) <= op(H2) by Def23;
un(H1) = un(M) & un(H2) = un(M) by Def25;
hence thesis;
end;
theorem Th32:
G is unital & the_unity_wrt the mult of G in the carrier of H implies
H is unital &
the_unity_wrt the mult of G = the_unity_wrt the mult of H
proof set e' = the_unity_wrt op(G); assume G is unital;
then A1: e' is_a_unity_wrt op(G) by Th4;
assume the_unity_wrt op(G) in carr(H);
then reconsider e = the_unity_wrt op(G) as Element of H;
A2: now let a be Element of H; carr(H) c= carr(G) by Th25;
then reconsider a' = a as Element of G by TARSKI:def 3;
thus e*a = e'*a' by Th27
.= op(G).(e',a') by VECTSP_1:def 10
.= a by A1,BINOP_1:11;
thus a*e = a'*e' by Th27
.= op(G).(a',e') by VECTSP_1:def 10
.= a by A1,BINOP_1:11;
end;
hence H is unital by Th6;
now let a be Element of H;
e*a = op(H).(e,a) & a*e = op(H).(a,e) by VECTSP_1:def 10;
hence op(H).(e,a) = a & op(H).(a,e) = a by A2;
end;
then e is_a_unity_wrt op(H) by BINOP_1:11;
hence thesis by BINOP_1:def 8;
end;
theorem Th33:
for M being well-unital (non empty multLoopStr)
for N being non empty MonoidalSubStr of M holds N is well-unital
proof let M be well-unital (non empty multLoopStr),
N be non empty MonoidalSubStr of M;
A1: N is SubStr of M by Th23;
A2: un(N) = un(M) & un(M) is_a_unity_wrt op(M)
by Def21,Def24;
now let a be Element of N;
carr(N) c= carr(M) by Th25;
then reconsider a' = a as Element of M by TARSKI:def 3;
thus op(N).(un(N),a) = (un(N))*a by VECTSP_1:def 10
.= (un(M))*a' by A1,A2,Th27
.= op(M).(un(M),a') by VECTSP_1:def 10
.= a by A2,BINOP_1:11;
thus op(N).(a,un(N)) = a*(un(N)) by VECTSP_1:def 10
.= a'*(un(M)) by A1,A2,Th27
.= op(M).(a',un(M)) by VECTSP_1:def 10
.= a by A2,BINOP_1:11;
end;
hence un(N) is_a_unity_wrt op(N) by BINOP_1:11;
end;
theorem Th34:
G is commutative implies H is commutative
proof assume A1: G is commutative;
now let a,b be Element of H; carr(H) c= carr(G) by Th25;
then reconsider a' = a, b' = b as Element of G by TARSKI:
def 3;
thus a*b = a'*b' by Th27 .= b'*a' by A1,Lm2 .= b*a by Th27;
end;
hence thesis by Lm2;
end;
theorem Th35:
G is associative implies H is associative
proof assume A1: G is associative;
now let a,b,c be Element of H; carr(H) c= carr(G) by Th25;
then reconsider a' = a, b' = b, c' = c, ab = a*b, bc = b*c as
Element of G by TARSKI:def 3;
thus a*b*c = ab*c' by Th27 .= a'*b'*c' by Th27
.= a'*(b'*c') by A1,Lm3 .= a'*bc by Th27 .= a*(b*c) by Th27;
end;
hence thesis by Lm3;
end;
theorem Th36:
G is idempotent implies H is idempotent
proof assume A1: G is idempotent;
then A2: carr(H) c= carr(G) & for a being Element of G holds a*
a = a
by Th9,Th25;
now let a be Element of H;
reconsider a' = a as Element of G by A2,TARSKI:def 3;
thus a*a = a'*a' by Th27 .= a by A1,Th9;
end;
hence thesis by Th9;
end;
theorem Th37:
G is cancelable implies H is cancelable
proof assume A1: G is cancelable;
then A2: carr(H) c= carr(G) &
for a,b,c being Element of G st a*b = a*c or b*a = c*a
holds b = c
by Th15,Th25;
now let a,b,c be Element of H;
reconsider a' = a, b' = b, c' = c as Element of G
by A2,TARSKI:def 3;
a*b = a'*b' & a*c = a'*c' & b*a = b'*a' & c*a = c'*a' by Th27;
hence a*b = a*c or b*a = c*a implies b = c by A1,Th15;
end;
hence thesis by Th15;
end;
theorem Th38:
the_unity_wrt the mult of G in the carrier of H &
G is uniquely-decomposable implies H is uniquely-decomposable
proof assume
A1: the_unity_wrt op(G) in carr(H);
assume
A2: op(G) has_a_unity &
for a,b being Element of G
st op(G).(a,b) = the_unity_wrt op(G) holds
a = b & b = the_unity_wrt op(G);
then G is unital by Def10;
then A3: H is unital & the_unity_wrt op(G) = the_unity_wrt op(H) by A1,Th32;
hence op(H) has_a_unity by Def10;
let a,b be Element of H; carr(H) c= carr(G) by Th25;
then reconsider a' = a, b' = b as Element of G by TARSKI:def
3;
op(H).(a,b) = a*b by VECTSP_1:def 10 .= a'*b' by Th27
.= op(G).(a',b') by VECTSP_1:def 10;
hence thesis by A2,A3;
end;
theorem Th39:
for M being well-unital uniquely-decomposable (non empty multLoopStr)
for N being non empty MonoidalSubStr of M holds N is uniquely-decomposable
proof let M be well-unital uniquely-decomposable (non empty multLoopStr);
let N be non empty MonoidalSubStr of M;
N is SubStr of M & un(M) = the_unity_wrt op(M) & un(M) = un(N)
by Def25,Th19,Th23;
hence thesis by Th38;
end;
definition let G be constituted-Functions non empty HGrStr;
cluster -> constituted-Functions (non empty SubStr of G);
coherence
proof let H be non empty SubStr of G; let a be Element of H;
carr(H) c= carr(G) by Th25;
then a is Element of G by TARSKI:def 3;
hence thesis;
end;
cluster -> constituted-Functions (non empty MonoidalSubStr of G);
coherence
proof let H be non empty MonoidalSubStr of G;
let a be Element of H;
carr(H) c= carr(G) by Th25;
then a is Element of G by TARSKI:def 3;
hence thesis;
end;
end;
definition let G be constituted-FinSeqs non empty HGrStr;
cluster -> constituted-FinSeqs (non empty SubStr of G);
coherence
proof let H be non empty SubStr of G; let a be Element of H;
carr(H) c= carr(G) by Th25;
then a is Element of G by TARSKI:def 3;
hence thesis;
end;
cluster -> constituted-FinSeqs (non empty MonoidalSubStr of G);
coherence
proof let H be non empty MonoidalSubStr of G;
let a be Element of H;
carr(H) c= carr(G) by Th25;
then a is Element of G by TARSKI:def 3;
hence thesis;
end;
end;
definition let M be well-unital (non empty multLoopStr);
cluster -> well-unital (non empty MonoidalSubStr of M);
coherence by Th33;
end;
definition let G be commutative (non empty HGrStr);
cluster -> commutative (non empty SubStr of G);
coherence by Th34;
cluster -> commutative (non empty MonoidalSubStr of G);
coherence
proof let N be non empty MonoidalSubStr of G; N is SubStr of G by Th23;
hence thesis by Th34;
end;
end;
definition let G be associative (non empty HGrStr);
cluster -> associative (non empty SubStr of G);
coherence by Th35;
cluster -> associative (non empty MonoidalSubStr of G);
coherence
proof let N be non empty MonoidalSubStr of G; N is SubStr of G by Th23;
hence thesis by Th35;
end;
end;
definition let G be idempotent (non empty HGrStr);
cluster -> idempotent (non empty SubStr of G);
coherence by Th36;
cluster -> idempotent (non empty MonoidalSubStr of G);
coherence
proof let N be non empty MonoidalSubStr of G; N is SubStr of G by Th23;
hence thesis by Th36;
end;
end;
definition let G be cancelable (non empty HGrStr);
cluster -> cancelable (non empty SubStr of G);
coherence by Th37;
cluster -> cancelable (non empty MonoidalSubStr of G);
coherence
proof let N be non empty MonoidalSubStr of G; N is SubStr of G by Th23;
hence thesis by Th37;
end;
end;
definition let M be well-unital uniquely-decomposable (non empty multLoopStr);
cluster -> uniquely-decomposable (non empty MonoidalSubStr of M);
coherence by Th39;
end;
scheme SubStrEx1 {G() -> non empty HGrStr,
D() -> non empty Subset of G()}:
ex H being strict non empty SubStr of G() st the carrier of H = D()
provided
A1: for x,y being Element of D() holds x*y in D()
proof set op = the mult of G(), carr = the carrier of G();
A2: [:D(),D():] c= [:carr,carr:] & dom op = [:carr,carr:]
by FUNCT_2:def 1;
then A3: dom (op|([:D(),D():] qua set)) = [:D(),D():] by RELAT_1:91;
rng (op|([:D(),D():] qua set)) c= D()
proof let x; assume x in rng (op|([:D(),D():] qua set));
then consider y such that
A4: y in dom (op|([:D(),D():] qua set)) &
x = (op|([:D(),D():] qua set)).y by FUNCT_1:def 5;
reconsider y as Element of [:D(),D():]
by A2,A4,RELAT_1:91;
reconsider y1 = y`1, y2 = y`2 as Element of D();
y = [y1,y2] by MCART_1:23;
then op.(y1,y2) = op.y by BINOP_1:def 1 .= x by A4,FUNCT_1:70;
then x = y1*y2 by VECTSP_1:def 10;
hence thesis by A1;
end;
then reconsider f = op|([:D(),D():] qua set) as BinOp of D() by A3,FUNCT_2:
def 1,RELSET_1:11;
f <= op by RELAT_1:88;
then reconsider H = HGrStr(#D(),f#) as strict non empty SubStr of G() by
Def23;
take H; thus thesis;
end;
scheme SubStrEx2 {G() -> non empty HGrStr, P[set]}:
ex H being strict non empty SubStr of G() st
for x being Element of G() holds x in
the carrier of H iff P[x]
provided
A1: for x,y being Element of G()
holds P[x] & P[y] implies P[x*y] and
A2: ex x being Element of G() st P[x]
proof
defpred Q[set] means P[$1];
consider X such that
A3: x in X iff x in carr(G()) & Q[x] from Separation;
consider x being Element of G() such that
A4: P[x] by A2;
reconsider X as non empty set by A3,A4;
X c= carr(G()) proof let x; thus thesis by A3; end;
then reconsider X as non empty Subset of G();
A5: now let x,y be Element of X;
P[x] & P[y] by A3;
then P[x*y] by A1;
hence x*y in X by A3;
end;
consider H being strict non empty SubStr of G() such that
A6: the carrier of H = X from SubStrEx1(A5);
take H; thus thesis by A3,A6;
end;
scheme MonoidalSubStrEx1 {G() -> non empty multLoopStr,
D() -> non empty Subset of G()}:
ex H being strict non empty MonoidalSubStr of G() st
the carrier of H = D()
provided
A1: for x,y being Element of D() holds x*y in D() and
A2: the unity of G() in D()
proof reconsider G = G() as non empty HGrStr;
reconsider D = D() as non empty Subset of G;
A3: for x,y being Element of D holds x*y in D by A1;
consider H being strict non empty SubStr of G such that
A4: the carrier of H = D from SubStrEx1(A3);
reconsider e = the unity of G() as Element of H by A2,A4;
set N = multLoopStr(#the carrier of H, the mult of H, e#);
N is MonoidalSubStr of G()
proof
thus op(N) <= op(G()) by Def23;
thus thesis;
end;
then reconsider N as strict non empty MonoidalSubStr of G();
take N; thus thesis by A4;
end;
scheme MonoidalSubStrEx2 {G() -> non empty multLoopStr, P[set]}:
ex M being strict non empty MonoidalSubStr of G() st
for x being Element of G() holds x in
the carrier of M iff P[x]
provided
A1: for x,y being Element of G()
holds P[x] & P[y] implies P[x*y] and
A2: P[the unity of G()]
proof
reconsider G = G() as non empty HGrStr;
defpred Q[set] means P[$1];
A3: for x,y being Element of G
holds Q[x] & Q[y] implies Q[x*y] by A1;
A4: ex x being Element of G st Q[x] by A2;
consider H being strict non empty SubStr of G such that
A5: for x being Element of G holds x in the carrier of H
iff Q[x] from SubStrEx2(A3,A4);
reconsider e = the unity of G() as Element of H by A2,A5;
the mult of H <= the mult of G() by Def23;
then reconsider M = multLoopStr(#carr(H), op(H), e#) as
strict non empty MonoidalSubStr of G() by Def25;
take M; thus thesis by A5;
end;
definition let G,a,b;
redefine func a*b -> Element of G; coherence; synonym a [*] b;
end;
begin :: Monoids on natural numbers
definition
func <REAL,+> -> unital associative invertible commutative cancelable strict
(non empty HGrStr) equals:Def26:
HGrStr(#REAL, addreal#);
coherence
proof HGrStr(#REAL, addreal#) is commutative Group by GROUP_1:92;
hence thesis;
end;
end;
theorem Th40:
the carrier of <REAL,+> = REAL &
the mult of <REAL,+> = addreal &
for a,b being Element of <REAL,+>, x,y being Real st
a = x & b = y holds a*b = x+y
proof thus
carr(<REAL,+>) = REAL & op(<REAL,+>) = addreal by Def26;
let a,b be Element of <REAL,+>, x,y be Real;
a*b = op(<REAL,+>).(a,b) & addreal.(x,y) = x+y
by VECTSP_1:def 4,def 10;
hence thesis by Def26;
end;
theorem
x is Element of <REAL,+> iff x is Real by Th40;
theorem
the_unity_wrt the mult of <REAL,+> = 0 by Th40,RVSUM_1:4;
theorem Th43:
for N being non empty SubStr of <REAL,+>
for a,b being Element of N,
x,y being Real st a = x & b = y holds a*b = x+y
proof let N be non empty SubStr of <REAL,+>;
let a,b be Element of N;
carr(N) c= carr(<REAL,+>) by Th25;
then reconsider a' = a, b' = b as Element of <REAL,+>
by TARSKI:def 3;
a*b = a'*b' by Th27;
hence thesis by Th40;
end;
theorem Th44:
for N being unital (non empty SubStr of <REAL,+>) holds
the_unity_wrt the mult of N = 0
proof let N be unital (non empty SubStr of <REAL,+>);
consider a be Element of N such that
A1: for b being Element of N holds a*b = b & b*a = b by Th6;
carr(N) c= REAL by Th25,Th40;
then reconsider x = a as Real by TARSKI:def 3;
x+0 = a*a by A1 .= x+x by Th43;
then A2: a = 0 by XCMPLX_1:2;
now let b be Element of N;
a*b = op(N).(a,b) & b*a = op(N).(b,a) by VECTSP_1:def 10;
hence op(N).(a,b) = b & op(N).(b,a) = b by A1;
end;
then a is_a_unity_wrt op(N) by BINOP_1:11;
hence thesis by A2,BINOP_1:def 8;
end;
definition let G be unital (non empty HGrStr);
cluster associative invertible -> unital cancelable Group-like
(non empty SubStr of G);
coherence
proof let H be non empty SubStr of G; assume
H is associative invertible;
then H is associative invertible (non empty HGrStr);
hence thesis;
end;
end;
definition
redefine func INT.Group -> unital invertible strict
(non empty SubStr of <REAL,+>);
coherence
proof
INT c= REAL proof let x; thus thesis by INT_1:11; end;
then A1: INT.Group = HGrStr(#INT,addint#) & dom addint = [:INT,INT:] &
[:INT,INT:] c= [:REAL,REAL:] & dom addreal = [:REAL,REAL:]
by FUNCT_2:def 1,GR_CY_1:def 4,ZFMISC_1:119;
then A2: dom (addreal|[:INT,INT:]) = [:INT,INT:] by RELAT_1:91;
now let x; assume
A3: x in [:INT,INT:];
then A4: x`1 in INT & x`2 in INT & x = [x`1,x`2] by MCART_1:10,23;
reconsider i1 = x`1, i2 = x`2 as Element of INT
by A3,MCART_1:10;
thus addint.x = addint.(i1,i2) by A4,BINOP_1:def 1
.= addreal.(i1,i2) by GR_CY_1:def 2
.= addreal.x by A4,BINOP_1:def 1
.= (addreal|[:INT,INT:]).x by A2,A3,FUNCT_1:70;
end;
then A5: addint = addreal|[:INT,INT:] by A1,A2,FUNCT_1:9;
INT.Group is SubStr of <REAL,+>
proof
thus op(INT.Group) <= op(<REAL,+>) by A5,Th40,GR_CY_1:def 4,RELAT_1:88;
end;
hence thesis;
end;
end;
:: corollary
:: INT.Group is unital commutative associative cancelable invertible;
canceled;
theorem
for G being strict non empty SubStr of <REAL,+> holds
G = INT.Group iff the carrier of G = INT by Th28,GR_CY_1:def 4;
theorem
x is Element of INT.Group iff x is Integer
by GR_CY_1:def 4,INT_1:12;
definition
func <NAT,+> ->
unital uniquely-decomposable strict (non empty SubStr of INT.Group) means:
Def27:
the carrier of it = NAT;
existence
proof set f = addint|([:NAT,NAT:] qua set);
[:NAT,NAT:] c= [:INT,INT:] & dom addint = [:INT,INT:]
by FUNCT_2:def 1,INT_1:14,ZFMISC_1:119;
then A1: dom f = [:NAT,NAT:] by RELAT_1:91;
rng f c= NAT
proof let x; assume x in rng f;
then consider y such that
A2: y in dom f & x = f.y by FUNCT_1:def 5;
reconsider n1 = y`1, n2 = y`2 as Nat by A1,A2,MCART_1:10;
reconsider i1 = n1, i2 = n2 as Integer;
x = addint.y by A2,FUNCT_1:70
.= addint.[n1,n2] by A2,MCART_1:23
.= addint.(i1,i2) by BINOP_1:def 1 .= n1+n2 by GR_CY_1:14;
hence thesis;
end;
then reconsider f as BinOp of NAT by A1,FUNCT_2:def 1,RELSET_1:11;
f <= op(INT.Group) by GR_CY_1:def 4,RELAT_1:88;
then reconsider N = HGrStr(#NAT,f#) as strict non empty SubStr of INT.Group
by Def23;
reconsider a = 0 as Element of N;
A3: now let b be Element of N; reconsider n = b as Nat;
thus a*b = 0+n by Th43 .= b;
thus b*a = n+0 by Th43 .= b;
end;
then A4: N is unital by Th6;
then A5: op(N) has_a_unity by Def10;
now let b be Element of N;
thus op(N).(a,b) = a*b by VECTSP_1:def 10 .= b by A3;
thus op(N).(b,a) = b*a by VECTSP_1:def 10 .= b by A3;
end;
then A6: a is_a_unity_wrt op(N) by BINOP_1:11;
then A7: the_unity_wrt op(N) = a by BINOP_1:def 8;
now let a,b be Element of N such that
A8: a*b = the_unity_wrt op(N);
reconsider n = a, m = b as Nat;
a*b = n+m by Th43;
then a = 0 & b = 0 by A7,A8,NAT_1:23;
hence a = b & b = the_unity_wrt op(N) by A6,BINOP_1:def 8;
end;
then N is uniquely-decomposable by A5,Th16;
hence thesis by A4;
end;
uniqueness by Th28;
end;
:: corollary
:: <NAT,+> is unital commutative associative cancelable uniquely-decomposable;
definition
func <NAT,+,0> -> well-unital strict (non empty MonoidalExtension of <NAT,+>)
means
not contradiction;
existence;
uniqueness by Th22;
end;
:: corollary
:: <NAT,+,0> is
:: well-unital commutative associative cancelable uniquely-decomposable;
definition
func addnat -> BinOp of NAT equals:Def29:
the mult of <NAT,+>;
coherence
proof carr(<NAT,+>) = NAT by Def27;
hence thesis;
end;
end;
canceled;
theorem Th49:
<NAT,+> = HGrStr(#NAT,addnat#) by Def27,Def29;
theorem
x is Element of <NAT,+,0> iff x is Nat
proof
carr(<NAT,+,0>) = carr(<NAT,+>) by Th20 .= NAT by Def27;
hence thesis;
end;
theorem
for n1,n2 being Nat, m1,m2 being Element of <NAT,+,0>
st n1 = m1 & n2 = m2
holds m1*m2 = n1+n2
proof
op(<NAT,+,0>) = op(<NAT,+>) by Th20;
then <NAT,+,0> is SubStr of <NAT,+> qua SubStr of <REAL,+> by Def23;
hence thesis by Th43;
end;
theorem
<NAT,+,0> = multLoopStr(#NAT,addnat,0#)
proof set N = <NAT,+,0>;
the HGrStr of N = <NAT,+> & the_unity_wrt op(N) = un(N) by Def22,Th19;
hence thesis by Th44,Th49;
end;
theorem
addnat = addreal|([:NAT,NAT:] qua set) & addnat = addint|([:NAT,NAT:] qua
set
)
proof
carr(<NAT,+>) = NAT & op(<REAL,+>) = addreal & op(INT.Group) = addint &
op(<NAT,+>) = addnat by Def26,Def27,Def29,GR_CY_1:def 4;
hence thesis by Th26;
end;
theorem
0 is_a_unity_wrt addnat & addnat has_a_unity & the_unity_wrt addnat = 0 &
addnat is commutative & addnat is associative &
addnat is uniquely-decomposable
proof
A1: addnat has_a_unity & the_unity_wrt addnat = 0 by Def10,Th44,Th49;
then ex n being Nat st n is_a_unity_wrt addnat by SETWISEO:def 2;
hence 0 is_a_unity_wrt addnat by A1,BINOP_1:def 8;
thus thesis by Def10,Def11,Def12,Def20,Th44,Th49;
end;
definition
func <REAL,*> -> unital commutative associative strict (non empty HGrStr)
equals:Def30:
HGrStr(#REAL,multreal#);
coherence
proof set R = HGrStr(#REAL,multreal#);
R is unital commutative associative
proof
thus op(R) has_a_unity & op(R) is commutative & op(R) is associative
by RVSUM_1:11,12,15;
end;
hence thesis;
end;
end;
theorem Th55:
the carrier of <REAL,*> = REAL &
the mult of <REAL,*> = multreal &
for a,b being Element of <REAL,*>, x,y being Real st
a = x & b = y holds a*b = x*y
proof thus
carr(<REAL,*>) = REAL & op(<REAL,*>) = multreal by Def30;
let a,b be Element of <REAL,*>, x,y be Real;
a*b = op(<REAL,*>).(a,b) & multreal.(x,y) = x*y
by VECTSP_1:def 10,def 14;
hence thesis by Def30;
end;
theorem
x is Element of <REAL,*> iff x is Real by Th55;
theorem
the_unity_wrt the mult of <REAL,*> = 1 by Th55,RVSUM_1:14;
theorem Th58:
for N being non empty SubStr of <REAL,*>
for a,b being Element of N, x,y being Real st a = x & b = y
holds a*b = x*y
proof let N be non empty SubStr of <REAL,*>;
let a,b be Element of N;
carr(N) c= carr(<REAL,*>) by Th25;
then reconsider a' = a, b' = b as Element of <REAL,*>
by TARSKI:def 3;
a*b = a'*b' by Th27;
hence thesis by Th55;
end;
canceled;
theorem
for N being unital (non empty SubStr of <REAL,*>) holds
the_unity_wrt the mult of N = 0 or
the_unity_wrt the mult of N = 1
proof let N be unital (non empty SubStr of <REAL,*>);
set e = the_unity_wrt op(N);
carr(N) c= carr(<REAL,*>) by Th25;
then reconsider x = e as Real by Th55,TARSKI:def 3;
e is_a_unity_wrt op(N) by Th4;
then e = op(N).(e,e)by BINOP_1:11 .= e*e by VECTSP_1:def 10
.= x*x by Th58;
then x*1 = x*x;
hence thesis by XCMPLX_1:5;
end;
definition
func <NAT,*> -> unital uniquely-decomposable strict
(non empty SubStr of <REAL,*>) means:Def31:
the carrier of it = NAT;
existence
proof set f = multreal|([:NAT,NAT:] qua set);
[:NAT,NAT:] c= [:REAL,REAL:] & dom multreal = [:REAL,REAL:]
by FUNCT_2:def 1;
then A1: dom f = [:NAT,NAT:] by RELAT_1:91;
rng f c= NAT
proof let x; assume x in rng f;
then consider y such that
A2: y in dom f & x = f.y by FUNCT_1:def 5;
reconsider n1 = y`1, n2 = y`2 as Nat by A1,A2,MCART_1:10;
x = multreal.y by A2,FUNCT_1:70
.= multreal.[n1,n2] by A2,MCART_1:23
.= multreal.(n1,n2) by BINOP_1:def 1 .= n1*n2 by VECTSP_1:def 14;
hence thesis;
end;
then reconsider f as BinOp of NAT by A1,FUNCT_2:def 1,RELSET_1:11;
f <= op(<REAL,*>) by Def30,RELAT_1:88;
then reconsider N = HGrStr(#NAT,f#) as strict (non empty SubStr of <REAL,*>
)
by Def23;
reconsider a = 1 as Element of N;
A3: now let b be Element of N; reconsider n = b as Nat;
thus a*b = 1*n by Th58 .= b;
thus b*a = n*1 by Th58 .= b;
end;
then A4: N is unital by Th6;
then A5: op(N) has_a_unity by Def10;
now let b be Element of N;
thus op(N).(a,b) = a*b by VECTSP_1:def 10 .= b by A3;
thus op(N).(b,a) = b*a by VECTSP_1:def 10 .= b by A3;
end;
then A6: a is_a_unity_wrt op(N) by BINOP_1:11;
then A7: the_unity_wrt op(N) = a by BINOP_1:def 8;
now let a,b be Element of N such that
A8: a*b = the_unity_wrt op(N);
reconsider n = a, m = b as Nat;
a*b = n*m by Th58;
then a = 1 & b = 1 by A7,A8,NAT_1:40;
hence a = b & b = the_unity_wrt op(N) by A6,BINOP_1:def 8;
end;
then N is uniquely-decomposable by A5,Th16;
hence thesis by A4;
end;
uniqueness by Th28;
end;
:: corollary
:: <NAT,*> is unital commutative associative uniquely-decomposable;
definition
func <NAT,*,1> -> well-unital strict (non empty MonoidalExtension of <NAT,*>)
means not contradiction;
uniqueness by Th22;
existence;
end;
:: corollary
:: <NAT,*,1> is well-unital commutative associative uniquely-decomposable;
definition
func multnat -> BinOp of NAT equals:Def33:
the mult of <NAT,*>;
coherence
proof carr(<NAT,*>) = NAT by Def31;
hence thesis;
end;
end;
theorem Th61:
<NAT,*> = HGrStr(#NAT,multnat#) by Def31,Def33;
theorem
for n1,n2 being Nat, m1,m2 being Element of <NAT,*>
st n1 = m1 & n2 = m2
holds m1*m2 = n1*n2 by Th58;
theorem Th63:
the_unity_wrt the mult of <NAT,*> = 1
proof carr(<NAT,*>) = NAT by Def31;
hence thesis by Th32,Th55,RVSUM_1:14;
end;
theorem
for n1,n2 being Nat, m1,m2 being Element of <NAT,*,1>
st n1 = m1 & n2 = m2
holds m1*m2 = n1*n2
proof let n1,n2 be Nat, m1,m2 be Element of <NAT,*,1>;
the HGrStr of <NAT,*,1> = <NAT,*> by Def22;
then reconsider x1 = m1, x2 = m2 as Element of <NAT,*>;
x1*x2 = m1*m2 by Th20;
hence thesis by Th58;
end;
theorem
<NAT,*,1> = multLoopStr(#NAT,multnat,1#)
proof set N = <NAT,*,1>;
the HGrStr of N = <NAT,*> & the_unity_wrt op(N) = un(N) by Def22,Th19;
hence thesis by Def31,Def33,Th63;
end;
theorem
multnat = multreal|([:NAT,NAT:] qua set) by Def30,Th26,Th61;
theorem
1 is_a_unity_wrt multnat & multnat has_a_unity & the_unity_wrt multnat = 1 &
multnat is commutative & multnat is associative &
multnat is uniquely-decomposable
proof
multnat has_a_unity by Def10,Th61;
then ex n being Nat st n is_a_unity_wrt multnat by SETWISEO:def 2;
hence 1 is_a_unity_wrt multnat by Th61,Th63,BINOP_1:def 8;
thus thesis by Def10,Def11,Def12,Def20,Th61,Th63;
end;
begin :: Monoid of finite sequences
definition
let D be non empty set;
func D*+^ -> unital associative cancelable uniquely-decomposable
constituted-FinSeqs strict (non empty HGrStr) means:Def34:
the carrier of it = D* &
for p,q being Element of it holds p [*] q = p^q;
existence
proof
deffunc F(Element of D*,Element of D*) = (($1 qua Element of D*)
^($2 qua Element of D*));
consider f being BinOp of D* such that
A1: for a,b being Element of D* holds
f.(a,b) = F(a,b) from BinOpLambda;
set G = HGrStr(#D*, f#);
G is constituted-FinSeqs
proof let x be Element of G;
x is Element of D*;
hence thesis;
end;
then reconsider G as constituted-FinSeqs strict (non empty HGrStr);
A2: now let p,q be Element of G;
reconsider p' = p, q' = q
as Element of D* qua non empty set;
thus p [*] q = f.(p',q') by VECTSP_1:def 10 .= p^q by A1;
end;
G is unital associative cancelable uniquely-decomposable
proof set N = G, f = op(N);
<*>D = {};
then reconsider a = {} as Element of N by FINSEQ_1:def 11
;
A3: now let b be Element of N;
thus a[*]b = a^b by A2 .= b by FINSEQ_1:47;
thus b[*]a = b^a by A2 .= b by FINSEQ_1:47;
end;
hence N is unital by Th6;
now let a,b,c be Element of N;
reconsider p = a[*]b, q = b[*]c as Element of N;
thus a*b*c = p^c by A2 .= a^b^c by A2 .= a^(b^c) by FINSEQ_1:45
.= a^q by A2 .= a*(b*c) by A2;
end;
hence N is associative by Lm3;
now let a,b,c be Element of N;
a*b = a^b & a*c = a^c & b*a = b^a & c*a = c^a by A2;
hence a*b = a*c or b*a = c*a implies b = c by FINSEQ_1:46;
end;
hence N is cancelable by Th15;
N is unital by A3,Th6;
hence op(N) has_a_unity by Def10;
now let b be Element of N;
a[*]b = f.(a,b) & b[*]a = f.(b,a) by VECTSP_1:def 10;
hence f.(a,b) = b & f.(b,a) = b by A3;
end;
then A4: a is_a_unity_wrt op(N) by BINOP_1:11;
then A5: the_unity_wrt op(N) = a by BINOP_1:def 8;
let a',b be Element of N;
assume f.(a',b) = the_unity_wrt op(N);
then {} = a'[*]b by A5,VECTSP_1:def 10 .= a'^b by A2;
then a = a' & a = b by FINSEQ_1:48;
hence thesis by A4,BINOP_1:def 8;
end;
then reconsider G as unital associative cancelable uniquely-decomposable
constituted-FinSeqs strict (non empty HGrStr);
take G; thus thesis by A2;
end;
uniqueness
proof let G1,G2 be unital associative cancelable uniquely-decomposable
constituted-FinSeqs strict (non empty HGrStr) such that
A6: carr(G1) = D* &
for p,q being Element of G1 holds p [*] q = p^q and
A7: carr(G2) = D* &
for p,q being Element of G2 holds p [*] q = p^q;
set f1 = op(G1), f2 = op(G2);
now let a,b be Element of D* qua non empty set;
reconsider p = a, q = b as Element of D*;
reconsider a1 = a, b1 = b as Element of G1 by A6;
reconsider a2 = a, b2 = b as Element of G2 by A7;
f2.(a,b) = a2[*]b2 & a2[*]b2 = p^q &
f1.(a,b) = a1[*]b1 & a1[*]b1 = p^q by A6,A7,VECTSP_1:def 10;
hence f1.(a,b) = f2.(a,b);
end;
hence thesis by A6,A7,BINOP_1:2;
end;
end;
definition let D;
func D*+^+<0> -> well-unital strict (non empty MonoidalExtension of D*+^)
means
not contradiction;
correctness by Th22;
func D-concatenation -> BinOp of D* equals:Def36:
the mult of D*+^;
correctness
proof carr(D*+^) = D* by Def34;
hence thesis;
end;
end;
theorem Th68:
D*+^ = HGrStr(#D*, D-concatenation#)
proof carr(D*+^) = D* by Def34;
hence thesis by Def36;
end;
theorem Th69:
the_unity_wrt the mult of D*+^ = {}
proof set N = D*+^, f = op(N);
A1: carr(N) = D* & for p,q being Element of D*+^
holds p[*]q = p^q by Def34;
{} = <*>D;
then reconsider a = {} as Element of N by A1,FINSEQ_1:def 11;
now let b be Element of N;
thus f.(a,b) = a[*]b by VECTSP_1:def 10
.= {}^b by Def34 .= b by FINSEQ_1:47;
thus f.(b,a) = b[*]a by VECTSP_1:def 10
.= b^{} by Def34 .= b by FINSEQ_1:47;
end;
then a is_a_unity_wrt op(N) by BINOP_1:11;
hence thesis by BINOP_1:def 8;
end;
theorem
the carrier of D*+^+<0> = D* & the mult of D*+^+<0> = D-concatenation &
the unity of D*+^+<0> = {}
proof set M = D*+^+<0>;
the HGrStr of M = D*+^ & the_unity_wrt op(M) = un(M) &
the_unity_wrt the mult of D*+^ = {} by Def22,Th19,Th69;
hence thesis by Def34,Def36;
end;
theorem
for a,b being Element of D*+^+<0> holds a [*] b = a^b
proof let a,b be Element of D*+^+<0>;
the HGrStr of D*+^+<0> = D*+^ by Def22;
then reconsider p = a, q = b as Element of D*+^;
thus a [*] b = p [*] q by Th20 .= a^b by Def34;
end;
theorem Th72:
for F being non empty SubStr of D*+^
for p,q being Element of F holds p[*]q = p^q
proof let F be non empty SubStr of D*+^, p,q be Element of F;
carr(F) c= carr(D*+^) by Th25;
then reconsider p' = p, q' = q as Element of D*+^ by TARSKI:
def 3;
thus p[*]q = p'[*]q' by Th27 .= p^q by Def34;
end;
theorem
for F being unital (non empty SubStr of D*+^) holds
the_unity_wrt the mult of F = {}
proof let F be unital (non empty SubStr of D*+^);
set p = the_unity_wrt op(F);
reconsider q = p as Element of F qua SubStr of D*+^;
A1: op(F) has_a_unity by Def10;
q^{} = p by FINSEQ_1:47 .= op(F).(p,p) by A1,SETWISEO:23
.= p[*]p by VECTSP_1:def 10 .= q^q by Th72;
hence thesis by FINSEQ_1:46;
end;
theorem
for F being non empty SubStr of D*+^
st {} is Element of F holds F is unital &
the_unity_wrt the mult of F = {}
proof let F be non empty SubStr of D*+^;
the_unity_wrt op(D*+^) = {} by Th69;
hence thesis by Th32;
end;
theorem
for A,B being non empty set st A c= B holds A*+^ is SubStr of B*+^
proof let A,B be non empty set; assume A c= B;
then A1: A* c= B* by LANG1:19;
then A2: [:A*,A*:] c= [:B*,B*:] by ZFMISC_1:119;
carr(A*+^) = A* & carr(B*+^) = B* by Def34;
then A3: dom op(A*+^) = [:A*,A*:] & dom op(B*+^) = [:B*,B*:] by FUNCT_2:def 1;
now let x; assume
A4: x in [:A*,A*:];
then A5: x`1 in A* & x`2 in A* by MCART_1:10;
then reconsider x1 = x`1, x2 = x`2 as Element of A*+^
by Def34;
reconsider y1 = x`1, y2 = x`2 as Element of B*+^
by A1,A5,Def34;
thus op(A*+^).x = op(A*+^).[x1,x2] by A4,MCART_1:23
.= op(A*+^).(x1,x2) by BINOP_1:def 1
.= x1[*]x2 by VECTSP_1:def 10
.= x1^x2 by Def34
.= y1[*]y2 by Def34
.= op(B*+^).(y1,y2) by VECTSP_1:def 10
.= op(B*+^).[x1,x2] by BINOP_1:def 1
.= op(B*+^).x by A4,MCART_1:23;
end;
hence op(A*+^) <= op(B*+^) by A2,A3,GRFUNC_1:8;
end;
theorem
D-concatenation has_a_unity & the_unity_wrt (D-concatenation) = {} &
D-concatenation is associative
proof HGrStr(#D*,D-concatenation#) = D*+^ by Th68;
hence thesis by Def10,Def12,Th69;
end;
begin :: Monoids of mappings
definition let X be set;
func GPFuncs X -> unital associative constituted-Functions strict
(non empty HGrStr)
means:
Def37:
the carrier of it = PFuncs(X,X) &
for f,g being Element of it holds f [*] g = f(*)g;
existence
proof set D = PFuncs(X,X);
defpred P[Element of D,Element of D,Element of D] means
ex f,g being PartFunc of X,X st $1 = f & $2 = g & $3 = f(*)g;
A1: for a,b being Element of D
ex c being Element of D st P[a,b,c]
proof let a,b be Element of D;
reconsider f = a, g = b as PartFunc of X,X by PARTFUN1:120;
dom(f*g) c= dom g & rng(f*g) c= rng f by RELAT_1:44,45;
then dom(f*g) c= X & rng(f*g) c= X by XBOOLE_1:1;
then f*g is Relation of X,X by RELSET_1:11;
then reconsider c = f*g as Element of D by PARTFUN1:119;
take c, f, g; thus thesis;
end;
consider f being BinOp of D such that
A2: for a,b being Element of D holds P[a,b,f.(a,b)]
from BinOpEx(A1);
set G = HGrStr(#D, f#);
G is constituted-Functions
proof let x be Element of G;
thus thesis by PARTFUN1:120;
end;
then reconsider G as constituted-Functions strict non empty HGrStr;
A3: now let a,b be Element of G;
consider g,h being PartFunc of X,X such that
A4: a = g & b = h & f.(a,b) = g(*)h by A2;
thus a[*]b = a(*)b by A4,VECTSP_1:def 10;
end;
reconsider g = id X as PartFunc of X,X;
reconsider f1 = g as Element of G by PARTFUN1:119;
A5: now let h be Element of G;
reconsider j = h as PartFunc of X,X by PARTFUN1:120;
thus f1[*]h = g(*)j by A3 .= h by PARTFUN1:37;
thus h[*]f1 = j(*)g by A3 .= h by PARTFUN1:36;
end;
now let f',g,h be Element of G;
reconsider fg = f'[*]g, gh = g[*]h as Element of G;
thus f'[*]g[*]h = fg(*)h by A3 .= f'(*)g(*)h by A3
.= f'(*)(g(*)h) by RELAT_1:55 .= f'(*)gh by A3
.= f'[*](g[*]h) by A3;
end;
then reconsider G as unital associative constituted-Functions strict
(non empty HGrStr)
by A5,Lm3,Th6;
take G; thus carr(G) = PFuncs(X,X);
let g,h be Element of G;
reconsider g' = g, h' = h as Element of D;
f.(g,h) = g [*] h &
ex g,h being PartFunc of X,X st g' = g & h' = h & f.(g',h') = g(*)h
by A2,VECTSP_1:def 10;
hence thesis;
end;
uniqueness
proof let G1,G2 be unital associative constituted-Functions strict
(non empty HGrStr)
such that
A6: carr(G1) = PFuncs(X,X) &
for f,g being Element of G1 holds f [*] g = f(*)g and
A7: carr(G2) = PFuncs(X,X) &
for f,g being Element of G2 holds f [*] g = f(*)g;
set f1 = op(G1), f2 = op(G2);
now let a,b be Element of G1;
reconsider a' = a, b' = b as Element of G2 by A6,A7;
f1.(a,b) = a[*]b & a[*]b = a(*)b & f2.(a',b') = a'[*]b' &
a'[*]b' = a'(*)b' by A6,A7,VECTSP_1:def 10;
hence f1.(a,b) = f2.(a,b);
end;
hence thesis by A6,A7,BINOP_1:2;
end;
end;
definition let X be set;
func MPFuncs X -> well-unital strict
(non empty MonoidalExtension of GPFuncs X) means
not contradiction;
existence;
uniqueness by Th22;
func X-composition -> BinOp of PFuncs(X,X) equals:Def39:
the mult of GPFuncs X;
correctness
proof carr(GPFuncs X) = PFuncs(X,X) by Def37;
hence thesis;
end;
end;
:: corollary
:: MPFuncs X is constituted-Functions strict Monoid;
theorem
x is Element of GPFuncs X iff x is PartFunc of X,X
proof carr(GPFuncs X) = PFuncs(X,X) by Def37;
hence thesis by PARTFUN1:119,120;
end;
theorem Th78:
the_unity_wrt the mult of GPFuncs X = id X
proof reconsider g = id X as PartFunc of X,X;
A1: g in PFuncs(X,X) & carr(GPFuncs X) = PFuncs(X,X)
by Def37,PARTFUN1:119;
then reconsider f = g as Element of GPFuncs X;
set op = op(GPFuncs X);
now let h be Element of GPFuncs X;
reconsider j = h as PartFunc of X,X by A1,PARTFUN1:120;
thus op.(f,h) = f[*]h by VECTSP_1:def 10 .= g(*)j by Def37
.= h by PARTFUN1:37;
thus op.(h,f) = h[*]f by VECTSP_1:def 10 .= j(*)g by Def37
.= h by PARTFUN1:36;
end;
then f is_a_unity_wrt op by BINOP_1:11;
hence thesis by BINOP_1:def 8;
end;
theorem Th79:
for F being non empty SubStr of GPFuncs X
for f,g being Element of F holds f [*] g = f (*) g
proof let F be non empty SubStr of GPFuncs X;
let f,g be Element of F;
carr(F) c= carr(GPFuncs X) by Th25;
then reconsider f' = f, g' = g as Element of GPFuncs X
by TARSKI:def 3;
f[*]g = f'[*]g' by Th27;
hence thesis by Def37;
end;
theorem Th80:
for F being non empty SubStr of GPFuncs X
st id X is Element of F holds
F is unital & the_unity_wrt the mult of F = id X
proof let F be non empty SubStr of GPFuncs X;
the_unity_wrt op(GPFuncs X) = id X by Th78;
hence thesis by Th32;
end;
theorem
Y c= X implies GPFuncs Y is SubStr of GPFuncs X
proof assume Y c= X;
then A1: PFuncs(Y,Y) c= PFuncs(X,X) by PARTFUN1:128;
then A2: [:PFuncs(Y,Y),PFuncs(Y,Y):] c= [:PFuncs(X,X),PFuncs(X,X):]
by ZFMISC_1:119;
carr(GPFuncs Y) = PFuncs(Y,Y) & carr(GPFuncs X) = PFuncs(X,X)
by Def37;
then A3: dom op(GPFuncs Y) = [:PFuncs(Y,Y),PFuncs(Y,Y):] &
dom op(GPFuncs X) = [:PFuncs(X,X),PFuncs(X,X):] by FUNCT_2:def 1;
now let x; assume
A4: x in [:PFuncs(Y,Y),PFuncs(Y,Y):];
then A5: x`1 in PFuncs(Y,Y) & x`2 in PFuncs(Y,Y) by MCART_1:10;
then reconsider x1 = x`1, x2 = x`2 as Element of GPFuncs Y
by Def37;
reconsider y1 = x`1, y2 = x`2 as Element of GPFuncs X
by A1,A5,Def37;
thus op(GPFuncs Y).x = op(GPFuncs Y).[x1,x2] by A4,MCART_1:23
.= op(GPFuncs Y).(x1,x2) by BINOP_1:def 1
.= x1[*]x2 by VECTSP_1:def 10
.= x1(*)x2 by Def37
.= y1[*]y2 by Def37
.= op(GPFuncs X).(y1,y2) by VECTSP_1:def 10
.= op(GPFuncs X).[x1,x2] by BINOP_1:def 1
.= op(GPFuncs X).x by A4,MCART_1:23;
end;
hence op(GPFuncs Y) <= op(GPFuncs X) by A2,A3,GRFUNC_1:8;
end;
Lm8: x in Funcs(X,X) implies x is Function of X,X
proof assume x in Funcs(X,X);
then ex f being Function st x = f & dom f = X & rng f c= X by FUNCT_2:def 2
;
hence thesis by FUNCT_2:4;
end;
definition let X be set;
func GFuncs X -> unital strict (non empty SubStr of GPFuncs X) means:Def40:
the carrier of it = Funcs(X,X);
existence
proof consider f being Function of X,X;
f in Funcs(X,X) & Funcs(X,X) c= PFuncs(X,X) &
carr(GPFuncs X) = PFuncs(X,X) by Def37,FUNCT_2:12,141;
then reconsider F = Funcs(X,X) as non empty Subset of
GPFuncs X;
A1: for x,y being Element of F holds x [*] y in F
proof let x,y be Element of F;
reconsider f = x, g = y as Function of X,X by Lm8;
x[*]y = f*g by Def37;
hence thesis by FUNCT_2:12;
end;
consider G being strict non empty SubStr of GPFuncs X such that
A2: the carrier of G = F from SubStrEx1(A1);
id X in F by FUNCT_2:12;
then reconsider G as unital strict (non empty SubStr of GPFuncs X) by A2,
Th80;
take G; thus thesis by A2;
end;
uniqueness by Th28;
end;
:: corollary
:: GFuncs X is unital associative constituted-Functions;
definition let X be set;
func MFuncs X -> well-unital strict MonoidalExtension of GFuncs X means
not contradiction;
correctness by Th22;
end;
:: corollary
:: GFuncs X is constituted-Functions Monoid;
theorem
x is Element of GFuncs X iff x is Function of X,X
proof carr(GFuncs X) = Funcs(X,X) by Def40;
hence thesis by Lm8,FUNCT_2:12;
end;
theorem Th83:
the mult of GFuncs X = (X-composition)|[:Funcs(X,X), Funcs(X,X):]
proof op(GFuncs X) <= op(GPFuncs X) & X-composition = op(GPFuncs X) &
dom op(GFuncs X) = [:carr(GFuncs X), carr(GFuncs X):] &
carr(GFuncs X) = Funcs(X,X) by Def23,Def39,Def40,FUNCT_2:def 1;
hence thesis by GRFUNC_1:64;
end;
theorem Th84:
the_unity_wrt the mult of GFuncs X = id X
proof id X in Funcs(X,X) & carr(GFuncs X) = Funcs(X,X) by Def40,FUNCT_2:12;
hence thesis by Th80;
end;
theorem
the carrier of MFuncs X = Funcs(X,X) &
the mult of MFuncs X = (X-composition)|[:Funcs(X,X), Funcs(X,X):] &
the unity of MFuncs X = id X
proof
the_unity_wrt op(GFuncs X) = id X & the HGrStr of MFuncs X = GFuncs X
by Def22,Th84;
hence thesis by Def40,Th19,Th83;
end;
definition let X be set;
func GPerms X -> unital invertible strict (non empty SubStr of GFuncs X)
means:Def42:
for f being Element of GFuncs X holds
f in the carrier of it iff f is Permutation of X;
existence
proof
defpred P[Element of GFuncs X] means
$1 is Permutation of X;
A1: for x,y being Element of GFuncs X
st P[x] & P[y] holds P[x [*] y]
proof let x,y be Element of GFuncs X; assume
x is Permutation of X & y is Permutation of X;
then reconsider f = x, g = y as Permutation of X;
x[*]y = f*g by Th79;
hence thesis;
end;
A2: ex x being Element of GFuncs X st P[x]
proof consider f being Permutation of X;
carr(GFuncs X) = Funcs(X,X) by Def40;
then reconsider x = f as Element of GFuncs X by FUNCT_2:
12;
take x; thus thesis;
end;
consider G being strict non empty SubStr of GFuncs X such that
A3: for f being Element of GFuncs X holds
f in the carrier of G iff P[f] from SubStrEx2(A1,A2);
A4: carr(GFuncs X) = Funcs(X,X) by Def40;
then reconsider f = id X as Element of GFuncs X by FUNCT_2:
12;
f in carr(G) by A3;
then reconsider G as unital strict (non empty SubStr of GFuncs X) by Th80;
now let a,b be Element of G;
carr(G) c= carr(GFuncs X) by Th25;
then reconsider a' = a, b' = b as Element of GFuncs X
by TARSKI:def 3;
reconsider i = f as Element of G by A3;
reconsider f = a', g = b' as Permutation of X by A3;
reconsider f' = f" as Element of GFuncs X
by A4,FUNCT_2:12;
reconsider f' as Element of G by A3;
reconsider r = f'[*]b, l = b[*]f' as Element of G;
take r,l;
i = f(*)(f") & i = f"(*)f & g(*)i = g & i(*)g = g & a[*]f' = f(*)(f")
&
f'[*]a = f"(*)f & i[*]b = (id X)(*)g & b[*]i = g(*)
id X by Th79,FUNCT_2:74,88;
hence a[*]r = b & l[*]a = b by Lm3;
end;
then reconsider G as unital invertible strict (non empty SubStr of GFuncs X
)
by Th12;
take G; thus thesis by A3;
end;
uniqueness
proof let G1,G2 be unital invertible strict (non empty SubStr of GFuncs X)
such that
A5: for f being Element of GFuncs X holds
f in carr(G1) iff f is Permutation of X and
A6: for f being Element of GFuncs X holds
f in carr(G2) iff f is Permutation of X;
A7: carr(G1) c= carr(GFuncs X) & carr(G2) c= carr(GFuncs X) by Th25;
carr(G1) = carr(G2)
proof
thus carr(G1) c= carr(G2)
proof let x; assume
A8: x in carr(G1);
then reconsider f = x as Element of GFuncs X by A7;
f is Permutation of X by A5,A8;
hence thesis by A6;
end;
let x; assume
A9: x in carr(G2);
then reconsider f = x as Element of GFuncs X by A7;
f is Permutation of X by A6,A9;
hence thesis by A5;
end;
hence thesis by Th28;
end;
end;
:: corollary
:: GPerms X is constituted-Functions Group;
theorem Th86:
x is Element of GPerms X iff x is Permutation of X
proof carr(GPerms X) c= carr(GFuncs X) by Th25;
then carr(GFuncs X) = Funcs(X,X) &
(x is Permutation of X implies x in Funcs(X,X)) &
(x is Element of GPerms X
implies x is Element of GFuncs X)
by Def40,FUNCT_2:12,TARSKI:def 3;
hence thesis by Def42;
end;
theorem Th87:
the_unity_wrt the mult of GPerms X = id X & 1.GPerms X = id X
proof reconsider i = id X as Element of GPerms X by Th86;
now let a be Element of GPerms X;
reconsider f = a as Permutation of X by Th86;
a[*]i = a(*)i & i[*]a = i(*)a by Th79;
then op(GPerms X).(a,i) = f(*)i & op(GPerms X).(i,a) = i(*)
f by VECTSP_1:def 10;
hence op(GPerms X).(i,a) = a & op(GPerms X).(a,i) = a by FUNCT_2:74;
end;
then i is_a_unity_wrt op(GPerms X) by BINOP_1:11;
hence the_unity_wrt op(GPerms X) = id X by BINOP_1:def 8;
hence thesis by GROUP_1:33;
end;
theorem
for f being Element of GPerms X holds f" = (f qua Function)"
proof let f be Element of GPerms X;
reconsider g = f as Permutation of X by Th86;
reconsider b = g" as Element of GPerms X by Th86;
reconsider b as Element of GPerms X;
g(*)(g") = id X & g"(*)g = id X & id X = 1.GPerms X & f[*]b = g(*)(g") &
b[*]f = g"(*)g by Th79,Th87,FUNCT_2:88;
hence thesis by GROUP_1:def 5;
end;