:: Groups
:: by Wojciech A. Trybulec
::
:: Received July 3, 1990
:: Copyright (c) 1990-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, NAT_1, INT_1, XBOOLE_0, ALGSTR_0, SUBSET_1, BINOP_2,
RELAT_1, REAL_1, ARYTM_3, CARD_1, ARYTM_1, BINOP_1, STRUCT_0, FUNCT_1,
SETWISEO, FINSEQOP, ZFMISC_1, NEWTON, COMPLEX1, XXREAL_0, FINSET_1,
TARSKI, RLVECT_1, SUPINF_2, GROUP_1, ORDINAL1, FUNCT_2;
notations TARSKI, ZFMISC_1,
XBOOLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0,
XXREAL_0, RELAT_1, FUNCT_1, XREAL_0, FUNCT_2, BINOP_2, BINOP_1, STRUCT_0,
ALGSTR_0, RLVECT_1, INT_1, NAT_1, FINSEQOP, SETWISEO, INT_2;
constructors BINOP_1, SETWISEO, XXREAL_0, REAL_1, NAT_1, NAT_D, BINOP_2,
FINSEQOP, RLVECT_1, RELSET_1;
registrations ORDINAL1, RELSET_1, FINSET_1, NUMBERS, XREAL_0, NAT_1, INT_1,
STRUCT_0, ALGSTR_0, CARD_1, BINOP_1, FUNCT_1, RELAT_1;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
definitions FUNCT_2, BINOP_1, FINSEQOP, RLVECT_1, SETWISEO, ALGSTR_0;
equalities BINOP_1, STRUCT_0, ALGSTR_0;
expansions BINOP_1, FINSEQOP;
theorems ABSVALUE, BINOP_1, CARD_1, FINSEQOP, INT_1, NAT_1, ZFMISC_1, BINOP_2,
XREAL_1, COMPLEX1, XXREAL_0, ORDINAL1, NAT_D, XREAL_0, STRUCT_0, FUNCT_1,
FUNCT_2;
schemes FUNCT_2, INT_1, NAT_1, CLASSES1;
begin
reserve m,n for Nat;
reserve i,j for Integer;
reserve S for non empty multMagma;
reserve r,r1,r2,s,s1,s2,t for Element of S;
Lm1: now
set G = multMagma (# REAL, addreal #);
thus for h,g,f being Element of G holds h * g * f = h * (g * f)
proof
let h,g,f be Element of G;
reconsider A = h, B = g, C = f as Real;
A1: g * f = B + C by BINOP_2:def 9;
h * g = A + B by BINOP_2:def 9;
hence h * g * f = A + B + C by BINOP_2:def 9
.= A + (B + C)
.= h * (g * f) by A1,BINOP_2:def 9;
end;
reconsider e = 0 as Element of G by XREAL_0:def 1;
take e;
let h be Element of G;
reconsider A = h as Real;
thus h * e = A + 0 by BINOP_2:def 9
.= h;
thus e * h = 0 + A by BINOP_2:def 9
.= h;
reconsider g = - A as Element of G by XREAL_0:def 1;
take g;
thus h * g = A + (- A) by BINOP_2:def 9
.= e;
thus g * h = (- A) + A by BINOP_2:def 9
.= e;
end;
definition
let IT be multMagma;
attr IT is unital means
ex e being Element of IT st
for h being Element of IT holds h * e = h & e * h = h;
attr IT is Group-like means :Def2:
ex e being Element of IT st
for h being Element of IT holds h * e = h & e * h = h &
ex g being Element of IT st h * g = e & g * h = e;
attr IT is associative means :Def3:
for x,y,z being Element of IT holds (x * y) * z = x * (y * z);
end;
registration
cluster Group-like -> unital for multMagma;
coherence;
end;
registration
cluster strict Group-like associative non empty for multMagma;
existence
proof
multMagma (# REAL, addreal #) is Group-like associative by Lm1;
hence thesis;
end;
end;
definition
mode Group is Group-like associative non empty multMagma;
end;
theorem
((for r,s,t holds (r * s) * t = r * (s * t)) &
ex t st for s1 holds s1 * t = s1 & t * s1 = s1 &
ex s2 st s1 * s2 = t & s2 * s1 = t) implies S is Group
by Def2,Def3;
theorem
(for r,s,t holds r * s * t = r * (s * t)) &
(for r,s holds (ex t st r * t = s) & (ex t st t * r = s)) implies
S is associative Group-like
proof
set r = the Element of S;
assume that
A1: for r,s,t holds r * s * t = r * (s * t) and
A2: for r,s holds (ex t st r * t = s) & ex t st t * r = s;
consider s1 such that
A3: r * s1 = r by A2;
thus for r,s,t holds r * s * t = r * (s * t) by A1;
take s1;
let s;
ex t st t * r = s by A2;
hence
A4: s * s1 = s by A1,A3;
consider s2 such that
A5: s2 * r = r by A2;
consider t1 being Element of S such that
A6: r * t1 = s1 by A2;
A7: ex t2 being Element of S st t2 * r = s2 by A2;
A8: s1 = s2 * (r * t1) by A1,A5,A6
.= s2 by A1,A3,A6,A7;
ex t st r * t = s by A2;
hence
A9: s1 * s = s by A1,A5,A8;
consider t1 being Element of S such that
A10: s * t1 = s1 by A2;
consider t2 being Element of S such that
A11: t2 * s = s1 by A2;
take t1;
consider r1 such that
A12: s * r1 = t1 by A2;
A13: ex r2 st r2 * s = t2 by A2;
t1 = s1 * (s * r1) by A1,A9,A12
.= t2 * (s * t1) by A1,A11,A12
.= t2 by A1,A4,A10,A13;
hence thesis by A10,A11;
end;
theorem Th3:
multMagma (# REAL, addreal #) is associative Group-like
proof
set G = multMagma (# REAL, addreal #);
thus for h,g,f being Element of G holds h * g * f = h * (g * f)
proof
let h,g,f be Element of G;
reconsider A = h, B = g, C = f as Real;
A1: g * f = B + C by BINOP_2:def 9;
h * g = A + B by BINOP_2:def 9;
hence h * g * f = A + B + C by BINOP_2:def 9
.= A + (B + C)
.= h * (g * f) by A1,BINOP_2:def 9;
end;
reconsider e = 0 as Element of G by XREAL_0:def 1;
take e;
let h be Element of G;
reconsider A = h as Real;
thus h * e = A + 0 by BINOP_2:def 9
.= h;
thus e * h = 0 + A by BINOP_2:def 9
.= h;
reconsider g = - A as Element of G by XREAL_0:def 1;
take g;
thus h * g = A + (- A) by BINOP_2:def 9
.= e;
thus g * h = (- A) + A by BINOP_2:def 9
.= e;
end;
reserve G for Group-like non empty multMagma;
reserve e,h for Element of G;
definition
let G be multMagma such that
A1: G is unital;
func 1_G -> Element of G means :Def4:
for h being Element of G holds h * it = h & it * h = h;
existence by A1;
uniqueness
proof
let e1,e2 be Element of G;
assume that
A2: for h being Element of G holds h * e1 = h & e1 * h = h and
A3: for h being Element of G holds h * e2 = h & e2 * h = h;
thus e1 = e2 * e1 by A3
.= e2 by A2;
end;
end;
theorem
(for h holds h * e = h & e * h = h) implies e = 1_G by Def4;
reserve G for Group;
reserve f,g,h for Element of G;
definition
let G, h;
func h" -> Element of G means :Def5:
h * it = 1_G & it * h = 1_G;
existence
proof
consider e being Element of G such that
A1: for h being Element of G holds h * e = h & e * h = h &
ex g being Element of G st h * g = e & g * h = e by Def2;
consider g being Element of G such that
A2: h * g = e & g * h = e by A1;
take g;
thus thesis by A1,A2,Def4;
end;
uniqueness
proof
let h1,h2 be Element of G;
assume that
A3: h * h1 = 1_G and
h1 * h = 1_G and
h * h2 = 1_G and
A4: h2 * h = 1_G;
thus h1 = 1_G * h1 by Def4
.= h2 * (h * h1) by A4,Def3
.= h2 by A3,Def4;
end;
involutiveness;
end;
registration
let G be non empty multMagma;
cluster the multMagma of G -> non empty;
coherence;
end;
registration
let G be associative non empty multMagma;
cluster the multMagma of G -> associative;
coherence
proof
set H = the multMagma of G;
for x,y,z being Element of H holds (x * y) * z = x * (y * z)
proof
let x,y,z be Element of H;
reconsider xx = x, yy = y, zz = z as Element of G;
(x * y) * z = (xx * yy) * zz
.= xx * (yy * zz) by Def3
.= x * (y * z);
hence thesis;
end;
hence H is associative;
end;
end;
registration
let G be Group;
cluster the multMagma of G -> Group-like;
coherence
proof
set H = the multMagma of G;
reconsider e = 1_G as Element of H;
take e;
let h be Element of H;
reconsider h9 = h as Element of G;
thus h * e = h9 * 1_G .= h by Def4;
thus e * h = 1_G * h9 .= h by Def4;
reconsider g = h9" as Element of H;
take g;
thus h * g = h9 * h9" .= e by Def5;
thus g * h = h9" * h9 .= e by Def5;
end;
end;
theorem
h * g = 1_G & g * h = 1_G implies g = h" by Def5;
theorem Th6:
h * g = h * f or g * h = f * h implies g = f
proof
assume h * g = h * f or g * h = f * h;
then h" * (h * g) = h" * h * f or g * h * h" = f * (h * h") by Def3;
then h" * (h * g) = 1_G * f or g * (h * h") = f * (h * h") by Def3,Def5;
then h" * (h * g) = f or g * 1_G = f * (h * h") by Def4,Def5;
then h" * h * g = f or g = f * (h * h") by Def3,Def4;
then h" * h * g = f or g = f * 1_G by Def5;
then 1_G * g = f or g = f by Def4,Def5;
hence thesis by Def4;
end;
theorem
h * g = h or g * h = h implies g = 1_G
proof
h * 1_G = h & 1_G * h = h by Def4;
hence thesis by Th6;
end;
theorem Th8:
(1_G)" = 1_G
proof
(1_G)" * 1_G = 1_G by Def5;
hence thesis by Def4;
end;
theorem
h" = g" implies h = g
proof
assume h" = g"; then
A1: h * g" = 1_G by Def5;
g * g" = 1_G by Def5;
hence thesis by A1,Th6;
end;
theorem
h" = 1_G implies h = 1_G
proof
(1_G)" = 1_G by Th8;
hence thesis;
end;
::$CT
theorem Th11:
h * g = 1_G implies h = g" & g = h"
proof
assume
A1: h * g = 1_G;
h * h" = 1_G & g" * g = 1_G by Def5;
hence thesis by A1,Th6;
end;
theorem Th12:
h * f = g iff f = h" * g
proof
h * (h" * g) = h * h" * g by Def3
.= 1_G * g by Def5
.= g by Def4;
hence h * f = g implies f = h" * g by Th6;
assume f = h" * g;
hence h * f = h * h" * g by Def3
.= 1_G * g by Def5
.= g by Def4;
end;
theorem Th13:
f * h = g iff f = g * h"
proof
g * h" * h = g * (h" * h) by Def3
.= g * 1_G by Def5
.= g by Def4;
hence f * h = g implies f = g * h" by Th6;
assume f = g * h";
hence f * h = g * (h" * h) by Def3
.= g * 1_G by Def5
.= g by Def4;
end;
theorem
ex f st g * f = h
proof
take g" * h;
thus thesis by Th12;
end;
theorem
ex f st f * g = h
proof
take h * g";
thus thesis by Th13;
end;
theorem Th16:
(h * g)" = g" * h"
proof
(g" * h") * (h * g) = g" * h" * h * g by Def3
.= g" * (h" * h) * g by Def3
.= g" * 1_G * g by Def5
.= g" * g by Def4
.= 1_G by Def5;
hence thesis by Th11;
end;
theorem Th17:
g * h = h * g iff (g * h)" = g" * h"
proof
thus g * h = h * g implies (g * h)" = g" * h" by Th16;
assume (g * h)" = g" * h";
then
A1: (h * g) * (g * h)" = h * g * g" * h" by Def3
.= h * (g * g") * h" by Def3
.= h * 1_G * h" by Def5
.= h * h" by Def4
.= 1_G by Def5;
(g * h) * (g * h)" = 1_G by Def5;
hence thesis by A1,Th6;
end;
theorem Th18:
g * h = h * g iff g" * h" = h" * g"
proof
thus g * h = h * g implies g" * h" = h" * g"
proof
assume
A1: g * h = h * g;
hence g" * h" = (g * h)" by Th16
.= h" * g" by A1,Th17;
end;
assume
A2: g" * h" = h" * g";
thus g * h = (g * h)"" .= (h" * g")" by Th16
.= h"" * g"" by A2,Th16
.= h * g;
end;
theorem Th19:
g * h = h * g iff g * h" = h" * g
proof
thus g * h = h * g implies g * h" = h" * g
proof
assume
A1: g * h = h * g;
(g * h") * (g" * h) = g * h" * g" * h by Def3
.= g * (h" * g") * h by Def3
.= g * (g" * h") * h by A1,Th18
.= g * g" * h" * h by Def3
.= 1_G * h" * h by Def5
.= h" * h by Def4
.= 1_G by Def5;
then g * h" = (g" * h)" by Th11
.= h" * g"" by Th16;
hence thesis;
end;
assume g * h" = h" * g;
then g * (h" * h) = h" * g * h by Def3;
then g * 1_G = h" * g * h by Def5;
then g = h" * g * h by Def4;
then g = h" * (g * h) by Def3;
then h * g = h * h" * (g * h) by Def3;
then h * g = 1_G * (g * h) by Def5;
hence thesis by Def4;
end;
reserve u for UnOp of G;
definition
let G;
func inverse_op(G) -> UnOp of G means :Def6:
it.h = h";
existence
proof
deffunc F(Element of G) = $1";
consider u such that
A1: for h being Element of G holds u.h = F(h) from FUNCT_2:sch 4;
take u;
let h;
thus thesis by A1;
end;
uniqueness
proof
let u1,u2 be UnOp of G;
assume that
A2: for h holds u1.h = h" and
A3: for h holds u2.h = h";
let h be Element of G;
thus u1.h = h" by A2
.= u2.h by A3;
end;
end;
registration
let G be associative non empty multMagma;
cluster the multF of G -> associative;
coherence
proof
let h,g,f be Element of G;
set o = the multF of G;
thus o.(h,o.(g,f)) = h * (g * f) .= h * g * f by Def3
.= o.(o.(h,g),f);
end;
end;
theorem Th20:
for G being unital non empty multMagma holds
1_G is_a_unity_wrt the multF of G
proof
let G be unital non empty multMagma;
set o = the multF of G;
now
let h be Element of G;
thus o.(1_G,h) = 1_G * h .= h by Def4;
thus o.(h,1_G) = h * 1_G .= h by Def4;
end;
hence thesis by BINOP_1:3;
end;
theorem Th21:
for G being unital non empty multMagma holds
the_unity_wrt the multF of G = 1_G
proof
let G be unital non empty multMagma;
1_G is_a_unity_wrt the multF of G by Th20;
hence thesis by BINOP_1:def 8;
end;
registration
let G be unital non empty multMagma;
cluster the multF of G -> having_a_unity;
coherence
proof
take 1_G;
thus thesis by Th20;
end;
end;
theorem Th22:
inverse_op(G) is_an_inverseOp_wrt the multF of G
proof
let h be Element of G;
thus (the multF of G).(h,inverse_op(G).h) = h * h" by Def6
.= 1_G by Def5
.= the_unity_wrt the multF of G by Th21;
thus (the multF of G).(inverse_op(G).h,h) = h" * h by Def6
.= 1_G by Def5
.= the_unity_wrt the multF of G by Th21;
end;
registration
let G;
cluster the multF of G -> having_an_inverseOp;
coherence
proof
inverse_op(G) is_an_inverseOp_wrt the multF of G by Th22;
hence thesis;
end;
end;
theorem
the_inverseOp_wrt the multF of G = inverse_op(G)
proof
set o = the multF of G;
o is having_an_inverseOp & inverse_op(G) is_an_inverseOp_wrt o by Th22;
hence thesis by FINSEQOP:def 3;
end;
definition
let G be non empty multMagma;
func power G -> Function of [:the carrier of G,NAT:], the carrier of G means
:Def7:
for h being Element of G holds it.(h,0) = 1_G &
for n being Nat holds it.(h,n + 1) = it.(h,n) * h;
existence
proof
defpred P[object,object] means
ex g0 being sequence of the carrier of G,
h being Element of G st
$1 = h & g0 = $2 & g0.0 = 1_G &
for n holds g0.(n + 1) = (g0.n) * h;
A1: for x be object st x in the carrier of G ex y be object st P[x,y]
proof
let x be object;
assume x in the carrier of G;
then reconsider b = x as Element of G;
deffunc F(Nat,Element of G) = $2 * b;
consider g0 being sequence of the carrier of G such that
A2: g0.0 = 1_G and
A3: for n being Nat holds g0.(n + 1) = F(n,g0.n) from NAT_1:sch 12;
reconsider y = g0 as set;
take y, g0, b;
thus x = b & g0 = y & g0.0 = 1_G by A2;
let n;
thus thesis by A3;
end;
consider f being Function such that
dom f = the carrier of G and
A4: for x be object st x in the carrier of G holds P[x,f.x]
from CLASSES1:sch 1(A1);
defpred P[Element of G,Nat,set] means
ex g0 being sequence of the carrier of G st g0 = f.$1 & $3 = g0.$2;
A5: for a being Element of G, n being Nat
ex b being Element of G st P[a,n,b]
proof
let a be Element of G, n be Nat;
consider g0 being sequence of the carrier of G,
h being Element of G such that
a = h and
A6: g0 = f.a and
g0.0 = 1_G and
for n holds g0.(n + 1) = (g0.n) * h by A4;
take g0.n, g0;
thus thesis by A6;
end;
consider F being Function of [:the carrier of G,NAT:], the carrier of G
such that
A7: for a being Element of G, n being Nat holds P[a,n,F.(a,n)]
from NAT_1:sch 19(A5);
take F;
let h be Element of G;
A8: ex g2 being sequence of the carrier of G,
b being Element of G st
h = b & g2 = f.h & g2.0 = 1_G &
for n holds g2.(n + 1) = (g2.n) * b by A4;
ex g1 being sequence of the carrier of G st g1 = f.h & F.(h,0) =
g1.0 by A7;
hence F.(h,0) = 1_G by A8;
let n be Nat;
A9: ex g2 being sequence of the carrier of G,
b being Element of G st
h = b & g2 = f.h & g2.0 = 1_G &
for n holds g2.(n + 1) = (g2.n) * b by A4;
(ex g0 being sequence of the carrier of G st g0 = f.h &
F.(h,n) = g0.n)&
ex g1 being sequence of the carrier of G st
g1 = f.h & F.(h,n + 1) = g1.(n + 1) by A7;
hence thesis by A9;
end;
uniqueness
proof
let f,g be Function of [:the carrier of G,NAT:], the carrier of G;
assume that
A10: for h being Element of G holds f.(h,0) = 1_G & for n being Nat
holds f.(h,n + 1) = (f.(h,n)) * h and
A11: for h being Element of G holds g.(h,0) = 1_G & for n being Nat
holds g.(h,n + 1) = (g.(h,n)) * h;
now
let h be Element of G, n be Element of NAT;
defpred P[Nat] means f.[h,$1] = g.[h,$1];
A12: now
let n be Nat;
assume
A13: P[n];
A14: g.[h,n] = g.(h,n);
f.[h,n + 1] = f.(h,n + 1) .= (f.(h,n)) * h by A10
.= g.(h,n + 1) by A11,A13,A14
.= g.[h,n + 1];
hence P[n+1];
end;
f.[h,0] = f.(h,0) .= 1_G by A10
.= g.(h,0) by A11
.= g.[h,0]; then
A15: P[0];
for n being Nat holds P[n] from NAT_1:sch 2(A15,A12);
hence f.(h,n) = g.(h,n);
end;
hence thesis;
end;
end;
definition
let G,h; let i be Integer;
func h |^ i -> Element of G equals :Def8:
power(G).(h,|.i.|) if 0 <= i
otherwise (power(G).(h,|.i.|))";
correctness;
end;
definition
let G,h; let n be natural Number;
redefine func h |^ n equals :: redefines |^ (GROUP_1, definition)
power(G).(h,n);
compatibility
proof
let g be Element of G;
|.n.| = n by ABSVALUE:def 1;
hence thesis by Def8;
end;
end;
Lm2: h |^ (n + 1) = h |^ n * h by Def7;
Lm3: h |^ 0 = 1_G by Def7;
Lm4: (1_G) |^ n = 1_G
proof
defpred P[Nat] means (1_G) |^ $1 = 1_G;
A1: now
let n;
assume P[n];
then (1_G) |^ (n + 1) = 1_G * 1_G by Def7
.= 1_G by Def4;
hence P[n+1];
end;
A2: P[0] by Def7;
for n holds P[n] from NAT_1:sch 2(A2,A1);
hence thesis;
end;
theorem
h |^ 0 = 1_G by Def7;
theorem Th25:
h |^ 1 = h
proof
thus h |^ 1 = h |^(0 + 1) .= h |^ 0 * h by Def7
.= 1_G * h by Def7
.= h by Def4;
end;
theorem Th26:
h |^ 2 = h * h
proof
thus h |^ 2 = h |^ (1 + 1) .= h |^ 1 * h by Def7
.= h * h by Th25;
end;
theorem
h |^ 3 = h * h * h
proof
thus h |^ 3 = h |^ (2 + 1) .= h |^ 2 * h by Def7
.= h * h * h by Th26;
end;
theorem
h |^ 2 = 1_G iff h" = h
proof
thus h |^ 2 = 1_G implies h = h"
proof
assume h |^ 2 = 1_G;
then h * h = 1_G by Th26;
hence thesis by Th11;
end;
assume h = h";
hence h |^ 2 = h * h" by Th26
.= 1_G by Def5;
end;
Lm5: h |^ (n + m) = h |^ n * (h |^ m)
proof
defpred P[Nat] means for n holds h |^ (n + $1) = h |^ n * (h |^ $1);
A1: for m st P[m] holds P[m+1]
proof
let m;
assume
A2: for n holds h |^ (n + m) = h |^ n * (h |^ m);
let n;
thus h |^ (n + (m + 1)) = h |^ (n + m + 1) .= h |^ (n + m) * h by Lm2
.= h |^ n * (h |^ m) * h by A2
.= h |^ n * (h |^ m * h) by Def3
.= h |^ n * (h |^ (m + 1)) by Lm2;
end;
A3: P[0]
proof
let n;
thus h |^ (n + 0) = h |^ n * 1_G by Def4
.= h |^ n * (h |^ 0) by Def7;
end;
for m holds P[m] from NAT_1:sch 2(A3,A1);
hence thesis;
end;
Lm6: h |^ (n + 1) = h |^ n * h & h |^ (n + 1) = h * (h |^ n)
proof
thus h |^ (n + 1) = h |^ n * h by Lm2;
thus h |^ (n + 1) = h |^ 1 * (h |^ n) by Lm5
.= h * (h |^ n) by Th25;
end;
Lm7: h |^ (n * m) = h |^ n |^ m
proof
defpred P[Nat] means for n holds h |^ (n * $1) = h |^ n |^ $1;
A1: for m st P[m] holds P[m+1]
proof
let m;
assume
A2: for n holds h |^ (n * m) = h |^ n |^ m;
let n;
thus h |^ (n * (m + 1)) = h |^ (n * m + n * 1)
.= h |^ (n * m) * (h |^ n) by Lm5
.= h |^ n |^ m * (h |^ n) by A2
.= h |^ n |^ m * (h |^ n |^ 1) by Th25
.= h |^ n |^ (m + 1) by Lm5;
end;
A3: P[0]
proof
let n;
thus h |^ (n * 0) = 1_G by Def7
.= h |^ n |^ 0 by Def7;
end;
for m holds P[m] from NAT_1:sch 2(A3,A1);
hence thesis;
end;
Lm8: h" |^ n = (h |^ n)"
proof
defpred P[Nat] means h" |^ $1 = (h |^ $1)";
A1: now
let n;
assume P[n];
then h" |^ (n + 1) = (h |^ n)" * h" by Lm2
.= (h * (h |^ n))" by Th16
.= (h |^ (n + 1))" by Lm6;
hence P[n+1];
end;
h" |^ 0 = 1_G by Def7
.= (1_G)" by Th8
.= (h |^ 0)" by Def7; then
A2: P[0];
for n holds P[n] from NAT_1:sch 2(A2,A1);
hence thesis;
end;
Lm9: g * h = h * g implies g * (h |^ n) = h |^ n * g
proof
defpred P[Nat] means g * h = h * g implies g * (h |^ $1) = h |^ $1 * g;
A1: for n st P[n] holds P[n+1]
proof
let n;
assume
A2: g * h = h * g implies g * (h |^ n) = h |^ n * g;
assume
A3: g * h = h * g;
thus g * (h |^ (n + 1)) = g * (h * (h |^ n)) by Lm6
.= g * h * (h |^ n) by Def3
.= h * ((h |^ n) * g)by A2,A3,Def3
.= h * (h |^ n) * g by Def3
.= h |^ (n + 1) * g by Lm6;
end;
A4: P[0]
proof
assume g * h = h * g;
thus g * (h |^ 0) = g * 1_G by Def7
.= g by Def4
.= 1_G * g by Def4
.= h |^ 0 * g by Def7;
end;
for n holds P[n] from NAT_1:sch 2(A4,A1);
hence thesis;
end;
Lm10: g * h = h * g implies g |^ n * (h |^ m) = h |^ m * (g |^ n)
proof
defpred P[Nat] means
for m st g * h = h * g holds
g |^ $1 * (h |^ m) = h |^ m * (g |^ $1);
A1: for n st P[n] holds P[n+1]
proof
let n;
assume
A2: for m st g * h = h * g holds g |^ n * (h |^ m) = h |^ m * (g |^ n);
let m;
assume
A3: g * h = h * g;
thus g |^ (n + 1) * (h |^ m) = g * (g |^ n) * (h |^ m) by Lm6
.= g * ((g |^ n) * (h |^ m)) by Def3
.= g * ((h |^ m) * (g |^ n)) by A2,A3
.= g * (h |^ m) * (g |^ n) by Def3
.= h |^ m * g * (g |^ n) by A3,Lm9
.= h |^ m * (g * (g |^ n)) by Def3
.= h |^ m * (g |^ (n + 1)) by Lm6;
end;
A4: P[0]
proof
let m;
assume g * h = h * g;
thus g |^ 0 * (h |^ m) = 1_G * (h |^ m) by Def7
.= h |^ m by Def4
.= h |^ m * 1_G by Def4
.= h |^ m * (g |^ 0) by Def7;
end;
for n holds P[n] from NAT_1:sch 2(A4,A1);
hence thesis;
end;
Lm11: g * h = h * g implies (g * h) |^ n = g |^ n * (h |^ n)
proof
defpred P[Nat] means
g * h = h * g implies (g * h) |^ $1 = g |^ $1 * (h |^ $1);
A1: for n st P[n] holds P[n+1]
proof
let n;
assume
A2: g * h = h * g implies (g * h) |^ n = g |^ n * (h |^ n);
assume
A3: g * h = h * g;
hence (g * h) |^ (n + 1) = g |^ n * (h |^ n) * (h * g) by A2,Lm6
.= g |^ n * (h |^ n) * h * g by Def3
.= g |^ n * ((h |^ n) * h) * g by Def3
.= g |^ n * (h |^ (n + 1)) * g by Lm6
.= h |^ (n + 1) * (g |^ n) * g by A3,Lm10
.= h |^ (n + 1) * ((g |^ n) * g) by Def3
.= h |^ (n + 1) * (g |^ (n + 1)) by Lm6
.= g |^ (n + 1) * (h |^ (n + 1)) by A3,Lm10;
end;
A4: P[0]
proof
assume g * h = h * g;
thus (g * h) |^ 0 = 1_G by Def7
.= 1_G * 1_G by Def4
.= g |^ 0 * 1_G by Def7
.= g |^ 0 * (h |^ 0) by Def7;
end;
for n holds P[n] from NAT_1:sch 2(A4,A1);
hence thesis;
end;
theorem Th29:
i <= 0 implies h |^ i = (h |^ |.i.|)"
proof
assume
A1: i <= 0;
per cases by A1;
suppose
i < 0;
hence thesis by Def8;
end;
suppose
A2: i = 0;
hence h |^ i = 1_G by Lm3
.= (1_G)" by Th8
.= (h |^ 0)" by Def7
.= (h |^ |.i.|)" by A2,ABSVALUE:def 1;
end;
end;
theorem
(1_G) |^ i = 1_G
proof
(1_G) |^ i = (1_G) |^ |.i.| or
(1_G) |^ i = ((1_G) |^ |.i.|)" & (1_G)" = 1_G by Def8,Th8;
hence thesis by Lm4;
end;
theorem Th31:
h |^ (-1) = h"
proof
|.-1.| = - (-1) by ABSVALUE:def 1;
hence h |^ (-1) = (h |^ 1)" by Def8
.= h" by Th25;
end;
Lm12: h |^ (- i) = (h |^ i)"
proof
per cases;
suppose
A1: i >= 0;
per cases by A1,XREAL_1:24;
suppose
A2: - i < -0;
hence h |^ (- i) = (h |^ |.- i .|)" by Def8
.= (h |^ (- (- i)))" by A2,ABSVALUE:def 1
.= (h |^ i)";
end;
suppose
A3: i = 0;
hence h |^ (- i) = 1_G by Lm3
.= (1_G)" by Th8
.= (h |^ i)" by A3,Lm3;
end;
end;
suppose
A4: i < 0;
then h |^ i = (h |^ |.i.|)" by Def8;
hence thesis by A4,ABSVALUE:def 1;
end;
end;
Lm13: j >= 1 or j = 0 or j < 0
proof
j < 0 or j is Element of NAT & (j <> 0 or j = 0) by INT_1:3;
hence thesis by NAT_1:14;
end;
Lm14: h |^ (j - 1) = h |^ j * (h |^ (-1))
proof
A1: now
per cases by Lm13;
suppose
A2: j >= 1 + 0; then
A3: j - 1 >= 0 by XREAL_1:19;
then
A4: |.j-1.| + 1 = j - 1 + 1 by ABSVALUE:def 1
.= j;
A5: |.j.| = j by A2,ABSVALUE:def 1;
A6: |.j.| = |.-j.| by COMPLEX1:52;
thus h|^(j - 1) * (h * (h|^(- j))) = h|^(j - 1) * h * (h|^(- j)) by Def3
.= h |^ |.j-1.| * h * (h |^ (- j)) by A3,Def8
.= h |^ |.j-1.| * h * ((h |^ |.-j.|)") by A2,Th29
.= h |^ (|.j-1.| + 1) * ((h |^ |.-j.|)") by Lm6
.= 1_G by A4,A5,A6,Def5;
end;
suppose
A7: j < 0;
A8: 1 - j = - (j - 1);
thus h |^ (j - 1) * (h * (h |^ (- j))) = (h |^ |.j-1.|)" * (h * (h
|^ (- j))) by A7,Def8
.= (h |^ |.j-1.|)" * (h * (h |^ |.-j.|)) by A7,Def8
.= (h |^ |.j-1.|)" * (h |^ (1 + |.-j.|)) by Lm6
.= (h |^ |.j-1.|)" * (h |^ (1 + (- j))) by A7,ABSVALUE:def 1
.= (h |^ |.j-1.|)" * (h |^ |.j-1.|) by A7,A8,ABSVALUE:def 1
.= 1_G by Def5;
end;
suppose
A9: j = 0;
hence h |^ (j - 1) * (h * (h |^ (- j))) = h" * (h * (h |^ (- j))) by Th31
.= h " * h * (h |^ (- j)) by Def3
.= 1_G * (h |^ (- j)) by Def5
.= h |^ 0 by A9,Def4
.= 1_G by Def7;
end;
end;
h|^(j - 1) * (h|^(1 - j)) = h|^(j - 1) * (h|^(- (j - 1)))
.= h |^ (j - 1) * (h |^ (j - 1))" by Lm12
.= 1_G by Def5;
then h * (h |^ (- j)) = h |^ (1 - j) by A1,Th6;
then (h |^ (1 - j))" = (h |^ (- j))" * h" by Th16
.= (h |^ (- (- j))) * h" by Lm12
.= h |^ j * (h |^ (-1)) by Th31;
then h |^ j * (h |^ (-1)) = h |^ (- (1 - j)) by Lm12;
hence thesis;
end;
Lm15: j >= 0 or j = - 1 or j < - 1
proof
per cases;
suppose
j >= 0;
hence thesis;
end;
suppose
A1: j < 0;
then reconsider n = -j as Element of NAT by INT_1:3;
n <> -0 by A1;
then n >= 1 by NAT_1:14;
then n > 1 or n = 1 by XXREAL_0:1;
then - 1 > - (- j) or - 1 = j by XREAL_1:24;
hence thesis;
end;
end;
Lm16: h |^ (j + 1) = h |^ j * (h |^ 1)
proof
A1: now
per cases by Lm15;
suppose
A2: j >= 0;
then reconsider n = j as Element of NAT by INT_1:3;
A3: n + 1 = |.j+1.| by ABSVALUE:def 1;
n + 1 >= 0;
hence
h |^ (j + 1) * ((h |^ (-1)) * (h |^ (- j))) = h |^ |.j+1.| * (
(h |^ (-1)) * (h |^ (- j))) by Def8
.= h |^ |.j+1.| * (h" * (h |^ (- j))) by Th31
.= h |^ |.j+1.| * (h" * (h |^ j)") by Lm12
.= h |^ |.j+1.| * (h" * (h |^ |.j.|)") by A2,Def8
.= h |^ |.j+1.| * ((h |^ |.j.| * h)") by Th16
.= h |^ |.j+1.| * (h |^ (|.j.| + 1))" by Lm6
.= h |^ |.j+1.| * (h |^ |.j+1.|)" by A3,ABSVALUE:def 1
.= 1_G by Def5;
end;
suppose
j < - 1;
then
A4: j + 1 < - 1 + 1 by XREAL_1:6;
hence h |^ (j + 1) * ((h |^ (-1)) * (h |^ (- j))) = (h |^ |.j+1.|)"
* ((h |^ (-1)) * (h |^ (- j))) by Def8
.= (h |^ |.j+1.|)" * (h" * (h |^ (- j))) by Th31
.= (h |^ |.j+1.|)" * h" * (h |^ (- j)) by Def3
.= (h * (h |^ |.j+1.|))" * (h |^ (- j)) by Th16
.= (h |^ (|.j+1.| + 1))" * (h |^ (- j)) by Lm6
.= (h |^ (- (j + 1) + 1))" * (h |^ (- j)) by A4,ABSVALUE:def 1
.= 1_G by Def5;
end;
suppose
A5: j = - 1;
hence h |^ (j + 1) * ((h |^ (-1)) * (h |^ (- j))) = 1_G * ((h |^ (-1)) *
(h |^ (- j))) by Lm3
.= (h |^ (-1)) * (h |^ (- j)) by Def4
.= h" * (h |^ (- j)) by Th31
.= h" * (h |^ j)" by Lm12
.= h" * h"" by A5,Th31
.= 1_G by Def5;
end;
end;
h |^ (j + 1) * (h |^ (- (j + 1))) = h |^ (j + 1) * (h |^ (j + 1))" by Lm12
.= 1_G by Def5;
then
A6: h |^ (- (j + 1)) = h |^ (-1) * (h |^ (- j)) by A1,Th6;
thus h |^ (j + 1) = h |^ (- (- (j + 1)))
.= ((h |^ (-1)) * (h |^ (- j)))" by A6,Lm12
.= (h |^ (- j))" * (h |^ (-1))" by Th16
.= h |^ (- (- j)) * (h |^ (-1))" by Lm12
.= h |^ j * (h |^ (- (-1))) by Lm12
.= h |^ j * (h |^ 1);
end;
theorem Th32:
h |^ (i + j) = (h |^ i) * (h |^ j)
proof
defpred P[Integer] means for i holds h |^ (i + $1) = h |^ i * (h |^ $1);
A1: for j holds P[j] implies P[j - 1] & P[j + 1]
proof
let j;
assume
A2: for i holds h |^ (i + j) = h |^ i * (h |^ j);
thus for i holds h |^ (i + (j - 1)) = h |^ i * (h |^ (j - 1))
proof
let i;
thus h |^ (i + (j - 1)) = h |^ ((i - 1) + j)
.= h |^ (i - 1) * (h |^ j) by A2
.= h |^ i * (h |^ (-1)) * (h |^ j) by Lm14
.= h |^ i * ((h |^ (-1)) * (h |^ j)) by Def3
.= h |^ i * (h |^ (j + (-1))) by A2
.= h |^ i * (h |^ (j - 1));
end;
let i;
thus h |^ (i + (j + 1)) = h |^ ((i + 1) + j)
.= h |^ (i + 1) * (h |^ j) by A2
.= h |^ i * (h |^ 1) * (h |^ j) by Lm16
.= h |^ i * ((h |^ 1) * (h |^ j)) by Def3
.= h |^ i * (h |^ (j + 1)) by A2;
end;
A3: P[0]
proof
let i;
thus h |^ (i + 0) = h |^ i * 1_G by Def4
.= h |^ i * (h |^ 0) by Def7;
end;
for j holds P[j] from INT_1:sch 4(A3,A1);
hence thesis;
end;
theorem
h |^ (i + 1) = h |^ i * h & h |^ (i + 1) = h * (h |^ i)
proof
h |^ 1 = h by Th25;
hence thesis by Th32;
end;
Lm17: h" |^ i = (h |^ i)"
proof
per cases;
suppose
i >= 0;
then reconsider n = i as Element of NAT by INT_1:3;
thus h" |^ i = (h |^ n)" by Lm8
.= (h |^ i)";
end;
suppose
A1: i < 0;
hence h" |^ i = (h" |^ |.i.|)" by Def8
.= (h |^ |.i.|)"" by Lm8
.= (h |^ i)" by A1,Def8;
end;
end;
theorem
h |^ (i * j) = h |^ i |^ j
proof
per cases;
suppose
i >= 0 & j >= 0;
then reconsider m = i, n = j as Element of NAT by INT_1:3;
thus h |^ (i * j) = h |^ m |^ n by Lm7
.= h |^ i |^ j;
end;
suppose
i >= 0 & j < 0;
then reconsider m = i, n = - j as Element of NAT by INT_1:3;
i * j = - (i * n);
hence h |^ (i * j) = (h |^ (i * n))" by Lm12
.= h" |^ (i * n) by Lm17
.= h" |^ m |^ n by Lm7
.= (h |^ i)" |^ n by Lm17
.= ((h |^ i)" |^ j)" by Lm12
.= (h |^ i |^ j)"" by Lm17
.= h |^ i |^ j;
end;
suppose
i < 0 & j >= 0;
then reconsider m = - i, n = j as Element of NAT by INT_1:3;
i * j = - (m * j);
hence h |^ (i * j) = (h |^ (m * j))" by Lm12
.= h" |^ (m * j) by Lm17
.= h" |^ m |^ n by Lm7
.= (h" |^ i)" |^ n by Lm12
.= (h |^ i)"" |^ j by Lm17
.= h |^ i |^ j;
end;
suppose
j < 0 & i < 0;
then reconsider m = - i, n = - j as Element of NAT by INT_1:3;
i * j * ((-1) * (-1)) = m * n;
hence h |^ (i * j) = h |^ m |^ n by Lm7
.= (h |^ (- i) |^ j)" by Lm12
.= ((h |^ i)" |^ j)" by Lm12
.= (h" |^ i |^ j)" by Lm17
.= ((h" |^ i)") |^ j by Lm17
.= h"" |^ i |^ j by Lm17
.= h |^ i |^ j;
end;
end;
theorem
h |^ -i = (h |^ i)" by Lm12;
theorem
h" |^ i = (h |^ i)" by Lm17;
theorem Th37:
g * h = h * g implies (g * h) |^ i = g |^ i * (h |^ i)
proof
assume
A1: g * h = h * g;
per cases;
suppose
A2: i >= 0;
then
A3: h |^ i = h |^ |.i.| by Def8;
(g * h) |^ i = (g * h) |^ |.i.| & g |^ i = g |^ |.i.| by A2,Def8;
hence thesis by A1,A3,Lm11;
end;
suppose
A4: i < 0;
hence (g * h) |^ i = ((h * g) |^ |.i.|)" by A1,Def8
.= (h |^ |.i.| * (g |^ |.i.|))" by A1,Lm11
.= (g |^ |.i.|)" * (h |^ |.i.|)" by Th16
.= g |^ i * (h |^ |.i.|)" by A4,Def8
.= g |^ i * (h |^ i) by A4,Def8;
end;
end;
theorem Th38:
g * h = h * g implies g |^ i * (h |^ j) = h |^ j * (g |^ i)
proof
assume
A1: g * h = h * g;
per cases;
suppose
i >= 0 & j >= 0;
then g |^ i = g |^ |.i.| & h |^ j = h |^ |.j.| by Def8;
hence thesis by A1,Lm10;
end;
suppose
A2: i >= 0 & j < 0;
A3: g|^|.i.| * (h|^|.j.|) = h|^|.j.| * (g|^|.i.|) by A1,Lm10;
g |^ i = g |^ |.i.| & h |^ j = (h |^ |.j.|)" by A2,Def8;
hence thesis by A3,Th19;
end;
suppose
A4: i < 0 & j >= 0;
A5: g|^|.i.| * (h|^|.j.|) = h|^|.j.| * (g|^|.i.|) by A1,Lm10;
g |^ i = (g |^ |.i.|)" & h |^ j = h |^ |.j.| by A4,Def8;
hence thesis by A5,Th19;
end;
suppose
i < 0 & j < 0;
then
A6: g |^ i = (g |^ |.i.|)" & h |^ j = (h |^ |.j.|)" by Def8;
hence g |^ i * (h |^ j) = (h |^ |.j.| * (g |^ |.i.|))" by Th16
.= (g |^ |.i.| * (h |^ |.j.|))" by A1,Lm10
.= h |^ j * (g |^ i) by A6,Th16;
end;
end;
theorem
g * h = h * g implies g * (h |^ i) = h |^ i * g
proof
assume
A1: g * h = h * g;
thus g * (h |^ i) = g |^ 1 * (h |^ i) by Th25
.= h |^ i * (g |^ 1) by A1,Th38
.= h |^ i * g by Th25;
end;
definition
let G,h;
attr h is being_of_order_0 means
h |^ n = 1_G implies n = 0;
end;
registration
let G;
cluster 1_G -> non being_of_order_0;
coherence
proof
(1_G) |^ 8 = 1_G by Lm4;
hence thesis;
end;
end;
definition
let G,h;
func ord h -> Element of NAT means :Def11:
it = 0 if h is being_of_order_0
otherwise
h |^ it = 1_G & it <> 0 & for m st h |^ m = 1_G & m <> 0 holds it <= m;
existence
proof
defpred P[Nat] means h |^ $1 = 1_G & $1 <> 0;
thus h is being_of_order_0 implies ex n being Element of NAT st n=0;
hereby
assume not h is being_of_order_0; then
A1: ex n being Nat st P[n];
consider k being Nat such that
A2: P[k] and
A3: for n being Nat st P[n] holds k <= n from NAT_1:sch 5(A1);
reconsider k as Element of NAT by ORDINAL1:def 12;
take k;
thus h |^ k = 1_G & k <> 0 by A2;
let m;
assume h |^ m = 1_G & m <> 0;
hence k <= m by A3;
end;
end;
uniqueness
proof
let n1,n2 be Element of NAT;
thus h is being_of_order_0 & n1 = 0 & n2 = 0 implies n1 = n2;
assume that
not h is being_of_order_0 and
A4: h |^ n1 = 1_G & n1 <> 0 &
( for m st h |^ m = 1_G & m <> 0 holds n1 <= m ) &
h |^ n2 = 1_G &( n2 <> 0 &
for m st h |^ m = 1_G & m <> 0 holds n2 <= m );
n1 <= n2 & n2 <= n1 by A4;
hence thesis by XXREAL_0:1;
end;
correctness;
end;
theorem Th40:
h |^ ord h = 1_G
proof
per cases;
suppose
h is being_of_order_0;
then ord h = 0 by Def11;
hence thesis by Def7;
end;
suppose
h is not being_of_order_0;
hence thesis by Def11;
end;
end;
theorem
ord 1_G = 1
proof
A1: for n st (1_G) |^ n = 1_G & n <> 0 holds 1 <= n by NAT_1:14;
(not 1_G is being_of_order_0) & (1_G) |^ 1 = 1_G by Lm4;
hence thesis by A1,Def11;
end;
theorem
ord h = 1 implies h = 1_G
proof
assume
A1: ord h = 1;
then not h is being_of_order_0 by Def11;
then h |^ 1 = 1_G by A1,Def11;
hence thesis by Th25;
end;
theorem
h |^ n = 1_G implies ord h divides n
proof
defpred P[Nat] means h |^ $1 = 1_G implies ord h divides $1;
A1: for n being Nat st for k being Nat st k < n holds P[k] holds P[n]
proof
let n be Nat;
assume
A2: for k being Nat st k < n holds P[k];
assume
A3: h |^ n = 1_G;
per cases;
suppose
n = 0;
hence thesis by NAT_D:6;
end;
suppose
A4: n <> 0;
per cases;
suppose
ord h = 0;
then h is being_of_order_0 by Def11;
hence thesis by A3,A4;
end;
suppose
A5: ord h <> 0;
then h is not being_of_order_0 by Def11;
then ord h <= n by A3,A4,Def11;
then consider m being Nat such that
A6: n = ord h + m by NAT_1:10;
h |^ n = h |^ ord h * (h |^ m) by A6,Lm5
.= 1_G * (h |^ m) by Th40
.= h |^ m by Def4;
then ord h divides m by A2,A3,A5,A6,NAT_1:16;
then consider i being Nat such that
A7: m = ord h * i by NAT_D:def 3;
n = ord h * (1 + i) by A6,A7;
hence thesis by NAT_D:def 3;
end;
end;
end;
for n being Nat holds P[n] from NAT_1:sch 4(A1);
hence thesis;
end;
definition
let G be finite 1-sorted;
redefine func card G -> Element of NAT; :: redefines card (STRUCT_0, definition)
coherence
proof
card the carrier of G in NAT;
hence thesis;
end;
end;
theorem
for G being non empty finite 1-sorted holds card G >= 1
proof
let G be non empty finite 1-sorted;
set g = the Element of G;
{g} c= the carrier of G & card {g} = 1 by CARD_1:30,ZFMISC_1:31;
hence thesis by NAT_1:43;
end;
definition
let IT be multMagma;
attr IT is commutative means :Def12:
for x, y being Element of IT holds x*y = y*x;
end;
registration
cluster strict commutative for Group;
existence
proof
reconsider G0 = multMagma (# REAL, addreal #) as Group by Th3;
take G0;
thus G0 is strict;
let a,g be Element of G0;
reconsider A = a, B = g as Real;
thus a * g = B + A by BINOP_2:def 9
.= g * a by BINOP_2:def 9;
end;
end;
definition
let FS be commutative non empty multMagma;
let x,y be Element of FS;
redefine func x*y; :: redefines * (ALGSTR_0, definition)
commutativity by Def12;
end;
theorem
multMagma (# REAL, addreal #) is commutative Group
proof
reconsider G = multMagma (# REAL, addreal #) as Group by Th3;
G is commutative
proof
let h,g be Element of G;
reconsider A = h, B = g as Real;
thus h * g = B + A by BINOP_2:def 9
.= g * h by BINOP_2:def 9;
end;
hence thesis;
end;
reserve A for commutative Group;
reserve a,b for Element of A;
theorem
(a * b)" = a" * b" by Th16;
theorem
(a * b) |^ i = a |^ i * (b |^ i) by Th37;
theorem
addLoopStr (# the carrier of A, the multF of A, 1_A #) is
Abelian add-associative right_zeroed right_complementable
proof
set G = addLoopStr (# the carrier of A, the multF of A, 1_A #);
thus G is Abelian
proof
let a,b be Element of G;
reconsider x = a, y = b as Element of A;
A1: for a,b be Element of G, x,y be Element of A st a = x & b = y holds a
+ b = x * y;
thus a + b = x * y .= b + a by A1;
end;
hereby
let a,b,c be Element of G;
reconsider x = a, y = b, z = c as Element of A;
thus a + b + c = x * y * z .= x * (y * z) by Def3
.= a + (b + c);
end;
hereby
let a be Element of G;
reconsider x = a as Element of A;
thus a + 0.G = x * 1_A .= a by Def4;
end;
let a be Element of G;
reconsider x = a as Element of A;
reconsider b = inverse_op(A).x as Element of G;
take b;
thus a + b = x * x" by Def6
.= 0.G by Def5;
end;
begin :: Addenda
:: from COMPTRIG, 2006.08.12, A.T.
theorem Th49:
for L be unital non empty multMagma for x be Element of L holds
(power L).(x,1) = x
proof
let L be unital non empty multMagma;
let x be Element of L;
0+1 = 1;
hence (power L).(x,1) = (power L).(x,0) * x by Def7
.= 1_L * x by Def7
.= x by Def4;
end;
theorem
for L be unital non empty multMagma
for x be Element of L holds (power L).(x,2) = x*x
proof
let L be unital non empty multMagma;
let x be Element of L;
1+1 = 2;
hence (power L).(x,2) = (power L).(x,1) * x by Def7
.= x * x by Th49;
end;
theorem
for L be associative commutative unital non empty multMagma
for x,y be Element of L
for n be Nat holds
(power L).(x*y,n) = (power L).(x,n) * (power L).(y,n)
proof
let L be associative commutative unital non empty multMagma;
let x,y be Element of L;
defpred P[Nat] means
(power L).(x*y,$1) = (power L).(x,$1) * (power L).(y,$1);
A1: now
let n be Nat;
assume P[n];
then (power L).(x*y,n+1) = (power L).(x,n) * (power L).(y,n) * (x*y) by
Def7
.= (power L).(x,n) * ((power L).(y,n) * (x*y)) by Def3
.= (power L).(x,n) * (x*((power L).(y,n)*y)) by Def3
.= (power L).(x,n) * (x*(power L).(y,n+1)) by Def7
.= (power L).(x,n)*x * (power L).(y,n+1) by Def3
.= (power L).(x,n+1) * (power L).(y,n+1) by Def7;
hence P[n+1];
end;
(power L).(x*y,0) = 1_L by Def7
.= 1_L * 1_L by Def4
.= (power L).(x,0) * 1_L by Def7
.= (power L).(x,0) * (power L).(y,0) by Def7;
then
A2: P[0];
thus for n be Nat holds P[n] from NAT_1:sch 2(A2,A1);
end;
:: Moved from ENDALG, 17.01_2006, AK
definition
let G,H be multMagma;
let IT be Function of G,H;
attr IT is unity-preserving means
IT.1_G = 1_H;
end;
:: SK, 15.11.2024
registration
cluster empty -> associative for multMagma;
coherence
proof
let M be multMagma;
assume M is empty; then
AA: the carrier of M is empty;
now
let x,y,z be Element of M;
thus (x*y)*z = {} by AA
.= (the multF of M).[x,y*z] by AA
.= x*(y*z);
end;
hence thesis;
end;
end;