:: Groups -- Additive Notation
:: by Roland Coghetto
::
:: Received April 30, 2015
:: Copyright (c) 2015-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, COMPLEX1, XXREAL_0, FINSET_1, TARSKI,
RLVECT_1, SUPINF_2, GROUP_1, POLYNOM1, GROUP_1A, REALSET1, RLSUB_1,
SETFAM_1, CQC_SIM1, GROUP_2, PRE_TOPC, GROUP_3, FUNCT_2, VALUED_1,
ORDINAL2, CONNSP_2, TOPS_1, RCOMP_1, UNIALG_1, CARD_5, COMPTS_1,
RLVECT_3, TOPGRP_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1,
ORDINAL1, CARD_1, NUMBERS, XCMPLX_0,
XXREAL_0, RELAT_1, PARTFUN1, SETFAM_1, FINSUB_1, FINSET_1, REALSET1,
WELLORD2, DOMAIN_1, NAT_D, MCART_1, XREAL_0, PRE_TOPC, TOPS_1, TOPS_2,
FUNCT_1, RELSET_1, FUNCT_2, BINOP_2, BINOP_1, INT_1, NAT_1, INT_2,
FINSEQOP, SETWISEO, STRUCT_0, ALGSTR_0, RLVECT_1, CONNSP_2, COMPTS_1,
BORSUK_1, CANTOR_1, YELLOW_8, TOPGRP_1, IDEAL_1;
constructors SETWISEO, NAT_1, NAT_D, BINOP_2, FINSEQOP, RLVECT_1, SETFAM_1,
WELLORD2, MEMBERED, REALSET1, RELSET_1, INT_2, TOPS_1, TOPS_2, COMPTS_1,
BORSUK_1, GRCAT_1, CANTOR_1, YELLOW_8, TOPGRP_1, IDEAL_1;
registrations ORDINAL1, RELSET_1, FINSET_1, NUMBERS, XREAL_0, NAT_1, INT_1,
STRUCT_0, ALGSTR_0, CARD_1, SUBSET_1, REALSET1, XCMPLX_0, XBOOLE_0,
FUNCT_1, FUNCT_2, PRE_TOPC, TOPS_1, COMPTS_1, BORSUK_1, TOPGRP_1;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
definitions FUNCT_2, BINOP_1, FINSEQOP, RLVECT_1, SETWISEO, ALGSTR_0,
PRE_TOPC, TOPS_2, CONNSP_2, TOPGRP_1, FUNCT_1, STRUCT_0, TARSKI,
XBOOLE_0;
equalities BINOP_1, STRUCT_0, ALGSTR_0, REALSET1, SUBSET_1, TARSKI, COMPTS_1,
IDEAL_1;
expansions FUNCT_2, STRUCT_0, TARSKI, XBOOLE_0, RLVECT_1, BINOP_1, FINSEQOP;
theorems ABSVALUE, BINOP_1, CARD_1, FINSEQOP, INT_1, NAT_1, ZFMISC_1, BINOP_2,
XREAL_1, COMPLEX1, XXREAL_0, ORDINAL1, XREAL_0, GROUP_2, CARD_2,
ENUMSET1, FINSET_1, FUNCT_1, FUNCT_2, TARSKI, WELLORD2, RELAT_1,
RELSET_1, XBOOLE_0, XBOOLE_1, XCMPLX_1, NAT_D, STRUCT_0, RLVECT_1,
XTUPLE_0, PRE_TOPC, TOPS_1, TOPS_2, YELLOW_8, BORSUK_1, TEX_2, CONNSP_2,
YELLOW_9, TOPGRP_1;
schemes FUNCT_2, INT_1, NAT_1, CLASSES1, BINOP_1, FUNCT_1, SUBSET_1, XBOOLE_0,
XFAMILY;
begin ::: A copy of GROUP_1
reserve m,n for Nat;
reserve i,j for Integer;
reserve S for non empty addMagma;
reserve r,r1,r2,s,s1,s2,t,t1,t2 for Element of S;
scheme SeqEx2Dbis{X,Z() -> non empty set, P[set,set,set]}:
ex f being Function of [:NAT,X():],Z()
st for x being Nat, y being Element of X() holds P[x,y,f.(x,y)]
provided
A1: for x being Nat, y being Element of X()
ex z being Element of Z() st P[x,y,z];
A2: for x being Element of NAT,
y being Element of X()
ex z being Element of Z() st P[x,y,z] by A1;
consider f being Function of [:NAT,X():],Z() such that
A3: for x being Element of NAT, y being Element of X() holds P[x,y,f.(x,y)]
from BINOP_1:sch 3(A2);
take f;
let x be Nat,y be Element of X();
x in NAT by ORDINAL1:def 12;
hence thesis by A3;
end;
Lm1: now
set G = addMagma (# 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 addMagma;
attr IT is add-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 addGroup-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;
end;
registration
cluster addGroup-like -> add-unital for addMagma;
coherence;
end;
registration
cluster strict addGroup-like add-associative non empty for addMagma;
existence
proof
addMagma (# REAL, addreal #) is addGroup-like add-associative by Lm1;
hence thesis;
end;
end;
definition
mode addGroup is addGroup-like add-associative non empty addMagma;
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 addGroup
by Def2,RLVECT_1:def 3;
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 add-associative addGroup-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 such that
A6: r + t1 = s1 by A2;
A7: ex t2 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 such that
A10: s + t1 = s1 by A2;
consider t2 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:
addMagma (# REAL, addreal #) is add-associative addGroup-like
proof
set G = addMagma (# 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 addGroup-like non empty addMagma;
reserve e,h for Element of G;
definition
let G be addMagma such that
A1: G is add-unital;
func 0_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 = 0_G by Def4;
reserve G for addGroup;
reserve f,g,h for Element of G;
definition
let G,h;
func -h -> Element of G means
:Def5:
h + it = 0_G & it + h = 0_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 = 0_G and
h1 + h = 0_G and
h + h2 = 0_G and
A4: h2 + h = 0_G;
thus h1 = 0_G + h1 by Def4
.= h2 + (h + h1) by A4,RLVECT_1:def 3
.= h2 by A3,Def4;
end;
involutiveness;
end;
theorem
h + g = 0_G & g + h = 0_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 RLVECT_1:def 3;
then -h + (h + g) = 0_G + f or g + (h + -h) = f + (h + -h)
by RLVECT_1:def 3,Def5;
then -h + (h + g) = f or g + 0_G = f + (h + -h) by Def4,Def5;
then -h + h + g = f or g = f + (h + -h) by RLVECT_1:def 3,Def4;
then -h + h + g = f or g = f + 0_G by Def5;
then 0_G + g = f or g = f by Def4,Def5;
hence thesis by Def4;
end;
theorem Th7:
h + g = h or g + h = h implies g = 0_G
proof
h + 0_G = h & 0_G + h = h by Def4;
hence thesis by Th6;
end;
theorem Th8:
-(0_G) = 0_G
proof
-(0_G) + 0_G = 0_G by Def5;
hence thesis by Def4;
end;
theorem TH9:
-h = -g implies h = g
proof
assume -h = -g;
then
A1: h + -g = 0_G by Def5;
g + -g = 0_G by Def5;
hence thesis by A1,Th6;
end;
theorem
-h = 0_G implies h = 0_G
proof
-(0_G) = 0_G by Th8;
hence thesis;
end;
theorem Th11:
h + g = 0_G implies h = -g & g = -h
proof
assume
A1: h + g = 0_G;
h + -h = 0_G & -g + g = 0_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 RLVECT_1:def 3
.= 0_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 RLVECT_1:def 3
.= 0_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 RLVECT_1:def 3
.= g + 0_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 RLVECT_1:def 3
.= g + 0_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 RLVECT_1:def 3
.= -g + (-h + h) + g by RLVECT_1:def 3
.= -g + 0_G + g by Def5
.= -g + g by Def4
.= 0_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 RLVECT_1:def 3
.= h + (g + -g) + -h by RLVECT_1:def 3
.= h + 0_G + -h by Def5
.= h + -h by Def4
.= 0_G by Def5;
(g + h) + -(g + h) = 0_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 RLVECT_1:def 3
.= g + (-h + -g) + h by RLVECT_1:def 3
.= g + (-g + -h) + h by A1,Th18
.= g + -g + -h + h by RLVECT_1:def 3
.= 0_G + -h + h by Def5
.= -h + h by Def4
.= 0_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 RLVECT_1:def 3;
then g + 0_G = -h + g + h by Def5;
then g = -h + g + h by Def4;
then g = -h + (g + h) by RLVECT_1:def 3;
then h + g = h + -h + (g + h) by RLVECT_1:def 3;
then h + g = 0_G + (g + h) by Def5;
hence thesis by Def4;
end;
reserve u for UnOp of G;
definition
let G;
func add_inverse(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
A2: for h holds u1.h = -h;
assume
A3: for h holds u2.h = -h;
now let h be Element of G;
thus u1.h = -h by A2
.= u2.h by A3;
end;
hence thesis;
end;
end;
registration
let G be add-associative non empty addMagma;
cluster the addF of G -> associative;
coherence
proof
let h,g,f be Element of G;
set o = the addF of G;
thus o.(h,o.(g,f)) = h + (g + f) .= h + g + f by RLVECT_1:def 3
.= o.(o.(h,g),f);
end;
end;
theorem Th20:
for G being add-unital non empty addMagma holds 0_G is_a_unity_wrt
the addF of G
proof
let G be add-unital non empty addMagma;
set o = the addF of G;
now
let h be Element of G;
thus o.(0_G,h) = 0_G + h .= h by Def4;
thus o.(h,0_G) = h + 0_G .= h by Def4;
end;
hence thesis by BINOP_1:3;
end;
theorem Th21:
for G being add-unital non empty addMagma holds the_unity_wrt the
addF of G = 0_G
proof
let G be add-unital non empty addMagma;
0_G is_a_unity_wrt the addF of G by Th20;
hence thesis by BINOP_1:def 8;
end;
registration
let G be add-unital non empty addMagma;
cluster the addF of G -> having_a_unity;
coherence
proof
take 0_G;
thus thesis by Th20;
end;
end;
theorem Th22:
add_inverse(G) is_an_inverseOp_wrt the addF of G
proof
let h be Element of G;
thus (the addF of G).(h,add_inverse(G).h) = h + -h by Def6
.= 0_G by Def5
.= the_unity_wrt the addF of G by Th21;
thus (the addF of G).(add_inverse(G).h,h) = -h + h by Def6
.= 0_G by Def5
.= the_unity_wrt the addF of G by Th21;
end;
registration
let G;
cluster the addF of G -> having_an_inverseOp;
coherence
proof
add_inverse(G) is_an_inverseOp_wrt the addF of G by Th22;
hence thesis;
end;
end;
theorem
the_inverseOp_wrt the addF of G = add_inverse(G)
proof
set o = the addF of G;
o is having_an_inverseOp & add_inverse(G) is_an_inverseOp_wrt o by Th22;
hence thesis by FINSEQOP:def 3;
end;
definition
let G be non empty addMagma;
func mult G -> Function of [:NAT,the carrier of G:], the carrier of G means
:Def7:
for h being Element of G holds it.(0,h) = 0_G &
for n being Nat holds it.(n + 1, h) = it.(n,h) + 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 = 0_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 = 0_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;
take g0;
take b;
thus x = b & g0 = y & g0.0 = 0_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[Nat,Element of G,set] means ex g0 being sequence of
the carrier of G st g0 = f.$2 & $3 = g0.$1;
A5: for n being Nat, a being Element of G
ex b being Element of G st P[n,a,b]
proof
let n be Nat, a be Element of G;
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 = 0_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 [:NAT,the carrier of G:], the carrier of G
such that
A7: for n being Nat, a being Element of G holds P[n,a,F.(n,a)]
from SeqEx2Dbis(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 = 0_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.(0,h) =
g1.0 by A7;
hence F.(0,h) = 0_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 = 0_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.(n,h)
= g0.n)& ex g1 being sequence of the carrier of G st g1 = f.h &
F.(n+1,h) = g1.(n + 1) by A7;
hence thesis by A9;
end;
uniqueness
proof
let f,g be Function of [:NAT,the carrier of G:], the carrier of G;
assume that
A10: for h being Element of G holds f.(0,h) = 0_G & for n being Nat
holds f.(n + 1,h) = (f.(n,h)) + h and
A11: for h being Element of G holds g.(0,h) = 0_G & for n being Nat
holds g.(n + 1,h) = (g.(n,h)) + h;
now
let h be Element of G, n be Element of NAT;
defpred P[Nat] means f.[$1,h] = g.[$1,h];
A12: now
let n be Nat;
assume
A13: P[n];
A14: g.[n,h] = g.(n,h);
f.[n+1,h] = f.(n+1,h) .= (f.(n,h)) + h by A10
.= g.(n+1,h) by A11,A13,A14
.= g.[n+1,h];
hence P[n+1];
end;
f.[0,h] = f.(0,h) .= 0_G by A10
.= g.(0,h) by A11
.= g.[0,h];
then
A15: P[0];
for n being Nat holds P[n] from NAT_1:sch 2(A15,A12);
hence f.(n,h) = g.(n,h);
end;
hence thesis;
end;
end;
definition
let G,i,h;
func i * h -> Element of G equals
:Def8:
mult(G).(|.i.|,h) if 0 <= i
otherwise -(mult(G).(|.i.|,h));
correctness;
end;
definition
let G,n,h;
redefine func n * h equals :: redefines * (GROUP_1A, definition)
mult(G).(n,h);
compatibility
proof
let g be Element of G;
|.n.| = n by ABSVALUE:def 1;
hence thesis by Def8;
end;
end;
Lm3: 0 * h = 0_G by Def7;
Lm4: n * (0_G) = 0_G
proof
defpred P[Nat] means $1 * (0_G) = 0_G;
A1: now
let n;
assume P[n];
then (n + 1) * (0_G) = 0_G + 0_G by Def7
.= 0_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 ThA24:
0 * h = 0_G by Def7;
theorem Th25:
1 * h = h
proof
thus 1 * h = ( 0 + 1) * h.= 0 * h+ h by Def7
.= 0_G + h by Def7
.= h by Def4;
end;
theorem Th26:
2 * h = h + h
proof
thus 2 * h = (1 + 1) * h .= 1 * h + h by Def7
.= h + h by Th25;
end;
theorem
3 * h = h + h + h
proof
thus 3 * h = (2 + 1) * h.= 2 * h + h by Def7
.= h + h + h by Th26;
end;
theorem
2 * h = 0_G iff -h = h
proof
thus 2 * h = 0_G implies h = -h
proof
assume 2 * h = 0_G;
then h + h = 0_G by Th26;
hence thesis by Th11;
end;
assume h = -h;
hence 2 * h = h + -h by Th26
.= 0_G by Def5;
end;
Lm5: (n + m) * h = n * h + (m * h)
proof
defpred P[Nat] means for n holds (n + $1) * h = n * h + ($1 * h);
A1: for m st P[m] holds P[m+1]
proof
let m;
assume
A2: for n holds (n + m) * h = n * h + (m * h);
let n;
thus (n + (m + 1)) * h = (n + m + 1) * h.= (n + m) * h + h by Def7
.= n * h + (m * h) + h by A2
.= n * h + (m * h + h) by RLVECT_1:def 3
.= n * h + ((m + 1) * h) by Def7;
end;
A3: P[0]
proof
let n;
thus (n + 0) * h = n * h + 0_G by Def4
.= n * h + (0 * h) by Def7;
end;
for m holds P[m] from NAT_1:sch 2(A3,A1);
hence thesis;
end;
Lm6: (n + 1) * h = n * h + h & (n + 1) * h = h + (n * h)
proof
thus (n + 1) * h = n * h + h by Def7;
thus (n + 1) * h = 1 * h + (n * h) by Lm5
.= h + ( n * h) by Th25;
end;
Lm9: g + h = h + g implies g + ( n * h) = n * h + g
proof
defpred P[Nat] means g + h = h + g implies g + ( $1 * h) = $1 * h + g;
A1: for n st P[n] holds P[n+1]
proof
let n;
assume
A2: g + h = h + g implies g + ( n * h) = n * h+ g;
assume
A3: g + h = h + g;
thus g + ( (n + 1) * h) = g + (h + ( n * h)) by Lm6
.= g + h + ( n * h) by RLVECT_1:def 3
.= h + (( n * h) + g)by A2,A3,RLVECT_1:def 3
.= h + ( n * h) + g by RLVECT_1:def 3
.= (n + 1) * h + g by Lm6;
end;
A4: P[0]
proof
assume g + h = h + g;
thus g + ( 0 * h) = g + 0_G by Def7
.= g by Def4
.= 0_G + g by Def4
.= 0 * h+ 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 (n * g) + (m * h) = (m * h) + (n * g)
proof
defpred P[Nat] means for m st g + h = h + g holds ($1 * g) + (m * h) =
(m * h) + ($1 * g);
A1: for n st P[n] holds P[n+1]
proof
let n;
assume
A2: for m st g + h = h + g holds n * g + ( m * h) = m * h + ( n * g);
let m;
assume
A3: g + h = h + g;
thus (n + 1) * g + ( m * h) = g + (n * g) + ( m * h) by Lm6
.= g + (( n * g) + (m * h)) by RLVECT_1:def 3
.= g + (( m * h) + (n * g)) by A2,A3
.= g + ( m * h) + (n * g) by RLVECT_1:def 3
.= m * h + g + (n * g) by A3,Lm9
.= m * h + (g + (n * g)) by RLVECT_1:def 3
.= m * h + ((n + 1) * g) by Lm6;
end;
A4: P[0]
proof
let m;
assume g + h = h + g;
thus 0 * g + ( m * h) = 0_G + ( m * h) by Def7
.= m * h by Def4
.= m * h + 0_G by Def4
.= m * h + ( 0 * g) by Def7;
end;
for n holds P[n] from NAT_1:sch 2(A4,A1);
hence thesis;
end;
Lm11: g + h = h + g implies n * (g + h) = n * g + ( n * h)
proof
defpred P[Nat] means g + h = h + g implies $1 * (g + h) =
$1 * g + ( $1 * h);
A1: for n st P[n] holds P[n+1]
proof
let n;
assume
A2: g + h = h + g implies n * (g + h) = n * g + ( n * h);
assume
A3: g + h = h + g;
hence (n + 1) * (g + h) = n * g + ( n * h) + (h + g) by A2,Lm6
.= n * g+ ( n * h) + h + g by RLVECT_1:def 3
.= n * g+ (( n * h) + h) + g by RLVECT_1:def 3
.= n * g + ( (n + 1) * h) + g by Lm6
.= (n + 1) * h + ( n * g) + g by A3,Lm10
.= (n + 1) * h + (( n * g) + g) by RLVECT_1:def 3
.= (n + 1) * h + ( (n + 1) * g) by Lm6
.= (n + 1) * g + ( (n + 1) * h) by A3,Lm10;
end;
A4: P[0]
proof
assume g + h = h + g;
thus 0 * (g + h) = 0_G by Def7
.= 0_G + 0_G by Def4
.= 0 * g + 0_G by Def7
.= 0 * g + ( 0 * h) by Def7;
end;
for n holds P[n] from NAT_1:sch 2(A4,A1);
hence thesis;
end;
theorem Th29:
i <= 0 implies i * h = -( |.i.| * h)
proof
assume
A1: i <= 0;
per cases by A1;
suppose
i < 0;
hence thesis by Def8;
end;
suppose
A2: i = 0;
hence i * h = 0_G by Lm3
.= -(0_G) by Th8
.= -( 0 * h) by Def7
.= -( |.i.| * h) by A2,ABSVALUE:def 1;
end;
end;
theorem
i * (0_G) = 0_G
proof
i * (0_G) = |.i.| * (0_G) or i * (0_G) = -(|.i.| * (0_G)) & -(0_G)
= 0_G by Def8,Th8;
hence thesis by Lm4;
end;
theorem Th31:
(-1) * h = -h
proof
|.-1.| = - (-1) by ABSVALUE:def 1;
hence (-1) * h = -( 1 * h) by Def8
.= -h by Th25;
end;
Lm12: (- i) * h = -( i * h)
proof
per cases;
suppose
A1: i >= 0;
per cases by A1,XREAL_1:24;
suppose
A2: - i < -0;
hence (- i) * h = -( |.- i .| * h) by Def8
.= -( (- (- i)) * h) by A2,ABSVALUE:def 1
.= -( i * h);
end;
suppose
A3: i = 0;
hence (- i) * h = 0_G by Lm3
.= -(0_G) by Th8
.= -(i * h) by A3,Lm3;
end;
end;
suppose
A4: i < 0;
then i * h = -( |.i.| * h) 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: (j - 1) * h = j * h + ( (-1) * h)
proof
A1: now
per cases by Lm13;
suppose
A2: j >= 1;
then
A3: j >= 1 + 0;
A4: |.j-1.| + 1 = j - 1 + 1 by A3,XREAL_1:19,ABSVALUE:def 1
.= j;
A5: |.j.| = j by A2,ABSVALUE:def 1;
A6: |.j.| = |.-j.| by COMPLEX1:52;
thus (j - 1) * h + (h + ((- j) * h)) = (j - 1)*h + h + ((- j)*h)
by RLVECT_1:def 3
.= |.j-1.| * h + h + ( (- j) * h) by A3,Def8,XREAL_1:19
.= |.j-1.| * h + h + (-( |.-j.| * h)) by A2,Th29
.= (|.j-1.| + 1) * h + (-( |.-j.| * h)) by Lm6
.= 0_G by A4,A5,A6,Def5;
end;
suppose
A7: j < 0;
A8: 1 - j = - (j - 1);
thus (j - 1) * h + (h + ( (- j) * h)) = -( |.j-1.| * h) +
(h + ( (- j) * h)) by A7,Def8
.= -( |.j-1.| * h) + (h + ( |.-j.| * h)) by A7,Def8
.= -( |.j-1.| * h) + ( (1 + |.-j.|) * h) by Lm6
.= -( |.j-1.| * h) + ( (1 + (- j)) * h) by A7,ABSVALUE:def 1
.= -( |.j-1.| * h) + ( |.j-1.| * h) by A7,A8,ABSVALUE:def 1
.= 0_G by Def5;
end;
suppose
A9: j = 0;
hence (j - 1) * h + (h + ( (- j) * h)) =
-h + (h + ( (- j) * h)) by Th31
.= -h + h + ( (- j) * h) by RLVECT_1:def 3
.= 0_G + ( (- j) * h) by Def5
.= 0 * h by A9,Def4
.= 0_G by Def7;
end;
end;
(j - 1)*h + ((1 - j)*h) = (j - 1)*h + ((- (j - 1))*h)
.= (j - 1) * h + -( (j - 1) * h) by Lm12
.= 0_G by Def5;
then h + ((- j) * h) = (1 - j) * h by A1,Th6;
then -( (1 - j) * h) = -( (- j) * h) + -h by Th16
.= ( (- (- j)) * h) + -h by Lm12
.= j * h + ( (-1) * h) by Th31;
then j * h + ( (-1) * h) = (- (1 - j)) * h 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 >= 1 by A1,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: (j + 1) * h = j * h + ( 1 * h)
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
(j + 1) * h + (( (-1) * h) + ( (- j)) * h) = |.j+1.| * h+ (
( (-1) * h) + ( (- j)) * h) by Def8
.= |.j+1.| * h + (-h + ( (- j)) * h) by Th31
.= |.j+1.| * h + (-h + -( j * h)) by Lm12
.= |.j+1.| * h + (-h + -( |.j.| * h)) by A2,Def8
.= |.j+1.| * h + -(( |.j.| * h + h)) by Th16
.= |.j+1.| * h + -( (|.j.| + 1) * h) by Lm6
.= |.j+1.| * h + -( |.j+1.| * h) by A3,ABSVALUE:def 1
.= 0_G by Def5;
end;
suppose
j < - 1;
then
A4: j + 1 < - 1 + 1 by XREAL_1:6;
hence (j + 1) * h + (( (-1) * h) + ( (- j) * h)) = -( |.j+1.| * h)
+ (( (-1) * h) + ( (- j) * h)) by Def8
.= -( |.j+1.| * h) + (-h + ( (- j) * h)) by Th31
.= -( |.j+1.| * h) + -h + ( (- j) * h) by RLVECT_1:def 3
.= -(h + ( |.j+1.| * h)) + ( (- j) * h) by Th16
.= -( (|.j+1.| + 1) * h) + ( (- j) * h) by Lm6
.= -( (- (j + 1) + 1) * h) + ( (- j) * h) by A4,ABSVALUE:def 1
.= 0_G by Def5;
end;
suppose
A5: j = - 1;
hence (j + 1) * h + (( (-1) * h) + ( (- j) * h)) = 0_G + (( (-1) * h) +
( (- j)) * h) by Lm3
.= ( (-1) * h) + ( (- j) * h) by Def4
.= -h + ( (- j) * h) by Th31
.= -h + -( j * h) by Lm12
.= -h + - -h by A5,Th31
.= 0_G by Def5;
end;
end;
(j + 1) * h + ( (- (j + 1)) * h) = (j + 1) * h + -( (j + 1) * h) by Lm12
.= 0_G by Def5;
then
A6: (- (j + 1)) * h = (-1) * h + ( (- j) * h) by A1,Th6;
thus (j + 1) * h = (- (- (j + 1))) * h
.= -(( (-1) * h) + ( (- j) * h)) by A6,Lm12
.= -( (- j) * h) + -( (-1) * h) by Th16
.= (- (- j)) * h + -( (-1) * h) by Lm12
.= j * h + ( (- (-1)) * h) by Lm12
.= j * h + ( 1 * h);
end;
theorem Th32:
(i + j) * h = (i * h) + (j * h)
proof
defpred P[Integer] means for i holds (i + $1) * h = i * h + ( $1 * h);
A1: for j holds P[j] implies P[j - 1] & P[j + 1]
proof
let j;
assume
A2: for i holds (i + j) * h = i * h + ( j * h);
thus for i holds (i + (j - 1)) * h = i * h + ( (j - 1) * h)
proof
let i;
thus (i + (j - 1)) * h = ((i - 1) + j) * h
.= (i - 1) * h + ( j * h) by A2
.= i * h + ( (-1)) * h + ( j * h) by Lm14
.= i * h + (( (-1) * h) + ( j * h)) by RLVECT_1:def 3
.= i * h + ( (j + (-1)) * h) by A2
.= i * h + ( (j - 1) * h);
end;
let i;
thus (i + (j + 1)) * h = ((i + 1) + j) * h
.= (i + 1) * h + (j * h) by A2
.= i * h + (1 * h) + (j * h) by Lm16
.= i * h + (( 1 * h) + (j * h)) by RLVECT_1:def 3
.= i * h + ((j + 1) * h) by A2;
end;
A3: P[0]
proof
let i;
thus (i + 0) * h = i * h + 0_G by Def4
.= i * h + ( 0 * h) by Def7;
end;
for j holds P[j] from INT_1:sch 4(A3,A1);
hence thesis;
end;
theorem Th33:
(i + 1) * h = i * h + h & (i + 1) * h = h + ( i * h)
proof
1 * h = h by Th25;
hence thesis by Th32;
end;
theorem
-i * h = -(i * h);
theorem ThA37:
g + h = h + g implies i * (g + h) = i * g + ( i *h)
proof
assume
A1: g + h = h + g;
per cases;
suppose
A2: i >= 0;
then
A3: i * h = |.i.| * h by Def8;
i * (g + h) = |.i.| * (g + h) & i * g = |.i.| * g by A2,Def8;
hence thesis by A1,A3,Lm11;
end;
suppose
A4: i < 0;
hence i * (g + h) = -(|.i.| * (h + g)) by A1,Def8
.= -( |.i.| * h + ( |.i.| * g)) by A1,Lm11
.= -( |.i.| * g) + -( |.i.| * h) by Th16
.= i * g + -( |.i.| * h) by A4,Def8
.= i * g + ( i * h) by A4,Def8;
end;
end;
theorem Th38:
g + h = h + g implies i * g + ( j * h) = j * h + ( i * g)
proof
assume
A1: g + h = h + g;
per cases;
suppose
i >= 0 & j >= 0;
then i * g = |.i.| * g & j * h = |.j.| * h by Def8;
hence thesis by A1,Lm10;
end;
suppose
A2: i >= 0 & j < 0;
A3: |.i.|*g + (|.j.|*h) = |.j.|*h + (|.i.|*g) by A1,Lm10;
i * g = |.i.| * g & j * h = -( |.j.| * h) by A2,Def8;
hence thesis by A3,Th19;
end;
suppose
A4: i < 0 & j >= 0;
A5: |.i.|*g + (|.j.|*h) = |.j.|*h + (|.i.|*g) by A1,Lm10;
i * g = -( |.i.| * g) & j * h = |.j.| * h by A4,Def8;
hence thesis by A5,Th19;
end;
suppose
i < 0 & j < 0;
then
A6: i * g = -( |.i.| * g) & j * h= -( |.j.| * h) by Def8;
hence i * g + ( j * h) = -( |.j.| * h + ( |.i.|) * g) by Th16
.= -( |.i.| * g + ( |.j.| * h)) by A1,Lm10
.= j * h + ( i * g) by A6,Th16;
end;
end;
theorem
g + h = h + g implies g + ( i * h) = i * h + g
proof
assume
A1: g + h = h + g;
thus g + ( i * h) = 1 * g + ( i * h) by Th25
.= i * h + ( 1 * g) by A1,Th38
.= i * h + g by Th25;
end;
definition
let G,h;
attr h is being_of_order_0 means
n * h = 0_G implies n = 0;
end;
registration
let G;
cluster 0_G -> non being_of_order_0;
coherence
proof
8 * (0_G) = 0_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
it * h = 0_G & it <> 0 & for m st m * h = 0_G & m <> 0 holds it <= m;
existence
proof
defpred P[Nat] means $1 * h = 0_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 k * h = 0_G & k <> 0 by A2;
let m;
assume m * h = 0_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: n1 * h = 0_G & n1 <> 0 & ( for m st m * h = 0_G & m <> 0 holds
n1 <= m )& n2 * h = 0_G &( n2 <> 0 & for m st m * h = 0_G & m <> 0 holds n2
<= m );
n1 <= n2 & n2 <= n1 by A4;
hence thesis by XXREAL_0:1;
end;
correctness;
end;
theorem
ord h * h = 0_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 0_G = 1
proof
A1: for n st n * (0_G) = 0_G & n <> 0 holds 1 <= n by NAT_1:14;
( not 0_G is being_of_order_0)& 1 * (0_G) = 0_G by Lm4;
hence thesis by A1,Def11;
end;
theorem
ord h = 1 implies h = 0_G
proof
assume
A1: ord h = 1;
then not h is being_of_order_0 by Def11;
then 1 * h = 0_G by A1,Def11;
hence thesis by Th25;
end;
registration
cluster strict Abelian for addGroup;
existence
proof
reconsider G0 = addMagma (# REAL, addreal #) as addGroup 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;
theorem
addMagma (# REAL, addreal #) is Abelian addGroup
proof
reconsider G = addMagma (# REAL, addreal #) as addGroup by Th3;
G is Abelian
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 Abelian addGroup;
reserve a,b for Element of A;
theorem Th44:
-(a + b) = -a + -b by Th16;
theorem
i * (a + b) = i * a + (i * b) by ThA37;
theorem
addLoopStr (# the carrier of A, the addF of A, 0_A #) is Abelian
add-associative right_zeroed right_complementable
proof
set G = addLoopStr (# the carrier of A, the addF of A, 0_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 RLVECT_1:def 3
.= a + (b + c);
end;
hereby
let a be Element of G;
reconsider x = a as Element of A;
thus a + 0.G = x + 0_A .= a by Def4;
end;
let a be Element of G;
reconsider x = a as Element of A;
reconsider b = add_inverse(A).x as Element of G;
take b;
thus a + b = x + -x by Def6
.= 0.G by Def5;
end;
theorem Th49:
for L be add-unital non empty addMagma for x be Element of L holds
(mult L).(1,x) = x
proof
let L be add-unital non empty addMagma;
let x be Element of L;
0+1 = 1;
hence (mult L).(1,x) = (mult L).(0,x) + x by Def7
.= 0_L + x by Def7
.= x by Def4;
end;
theorem
for L be add-unital non empty addMagma for x be Element of L holds (mult
L).(2,x) = x+x
proof
let L be add-unital non empty addMagma;
let x be Element of L;
1+1 = 2;
hence (mult L).(2,x) = (mult L).(1,x) + x by Def7
.= x + x by Th49;
end;
theorem
for L be add-associative Abelian add-unital non empty addMagma for x,y be
Element of L for n be Nat holds (mult L).(n,x+y) = (mult L).(n,x)
+ (mult L).(n,y)
proof
let L be add-associative Abelian add-unital non empty addMagma;
let x,y be Element of L;
defpred P[Nat] means
(mult L).($1,x+y) = (mult L).($1,x) + (mult L).($1,y);
A1: now
let n be Nat;
assume P[n];
then (mult L).(n+1,x+y) = (mult L).(n,x) + (mult L).(n,y) + (x+y) by
Def7
.= (mult L).(n,x) + ((mult L).(n,y) + (x+y)) by RLVECT_1:def 3
.= (mult L).(n,x) + (x+((mult L).(n,y)+y)) by RLVECT_1:def 3
.= (mult L).(n,x) + (x+(mult L).(n+1,y)) by Def7
.= (mult L).(n,x)+x + (mult L).(n+1,y) by RLVECT_1:def 3
.= (mult L).(n+1,x) + (mult L).(n+1,y) by Def7;
hence P[n+1];
end;
(mult L).(0,x+y) = 0_L by Def7
.= 0_L + 0_L by Def4
.= (mult L).(0,x) + 0_L by Def7
.= (mult L).(0,x) + (mult L).(0,y) by Def7;
then
A2: P[0];
thus for n be Nat holds P[n] from NAT_1:sch 2(A2,A1);
end;
definition
let G,H be addMagma;
let IT be Function of G,H;
attr IT is zero-preserving means
IT.0_G = 0_H;
end;
begin ::: GROUP_2B
reserve x for object;
reserve y,y1,y2,Y,Z for set;
reserve k for Nat;
reserve G for addGroup;
reserve a,g,h for Element of G;
reserve A for Subset of G;
Lm1: x in A implies x is Element of G;
definition
let G,A;
func -A -> Subset of G equals
{-g : g in A};
coherence
proof
set F = {-g : g in A};
F c= the carrier of G
proof
let x be object;
assume x in F;
then ex g st x = -g & g in A;
hence thesis;
end;
hence thesis;
end;
involutiveness
proof
let R, B be Subset of G;
assume
A1: R = {-g : g in B};
thus B c= {-g : g in R}
proof
let a be object;
assume
A2: a in B;
then reconsider a as Element of G;
--a = a & -a in R by A1,A2;
hence thesis;
end;
let a be object;
assume a in {-g : g in R};
then consider g such that
A3: a = -g and
A4: g in R;
ex h st g = -h & h in B by A1,A4;
hence thesis by A3;
end;
end;
theorem Th2:
x in -A iff ex g st x = -g & g in A;
theorem ThB3:
-{g} = {-g}
proof
thus -{g} c= {-g}
proof
let x be object;
assume x in -{g};
then consider h such that
A1: x = -h and
A2: h in {g};
h = g by A2,TARSKI:def 1;
hence thesis by A1,TARSKI:def 1;
end;
let x be object;
assume x in {-g};
then
A3: x = -g by TARSKI:def 1;
g in {g} by TARSKI:def 1;
hence thesis by A3;
end;
theorem
-{g,h} = {-g,-h}
proof
thus -{g,h} c= {-g,-h}
proof
let x be object;
assume x in -{g,h};
then consider a such that
A1: x = -a and
A2: a in {g,h};
a = g or a = h by A2,TARSKI:def 2;
hence thesis by A1,TARSKI:def 2;
end;
let x be object;
assume x in {-g,-h};
then
A3: x = -g or x = -h by TARSKI:def 2;
g in {g,h} & h in {g,h} by TARSKI:def 2;
hence thesis by A3;
end;
theorem
-({}(the carrier of G)) = {}
proof
thus -({}(the carrier of G)) c= {}
proof
let x be object;
assume x in -({}(the carrier of G));
then ex a st x = -a & a in {}the carrier of G;
hence thesis;
end;
thus thesis;
end;
theorem
-([#](the carrier of G)) = the carrier of G
proof
thus -([#](the carrier of G)) c= the carrier of G;
let x be object;
assume x in the carrier of G;
then reconsider a = x as Element of G;
- -a in ([#](the carrier of G));
hence thesis;
end;
theorem ThX7:
A <> {} iff -A <> {}
proof
set x = the Element of -A;
thus A <> {} implies -A <> {}
proof
set x = the Element of A;
assume
A1: A <> {};
then reconsider x as Element of G by Lm1;
-x in -A by A1;
hence thesis;
end;
assume -A <> {};
then ex a st x = -a & a in A by Th2;
hence thesis;
end;
registration
let G;
let A be empty Subset of G;
cluster -A -> empty;
coherence by ThX7;
end;
registration
let G;
let A be non empty Subset of G;
cluster -A -> non empty;
coherence by ThX7;
end;
reserve G for non empty addMagma,
A,B,C for Subset of G;
reserve a,b,g,g1,g2,h,h1,h2 for Element of G;
definition
let G be Abelian non empty addMagma;
let A,B be Subset of G;
redefine func A + B; :: redefines + (IDEAL_1, definition)
commutativity
proof
let A,B be Subset of G;
thus A+B c= B+A
proof
let x be object;
assume x in A+B;
then ex g,h being Element of G st x = g+h & g in A & h in B;
hence thesis;
end;
let x be object;
assume x in B+A;
then ex g,h being Element of G st x = g+h & g in B & h in A;
hence thesis;
end;
end;
theorem ThX8:
x in A + B iff ex g,h st x = g + h & g in A & h in B;
theorem Th9:
A <> {} & B <> {} iff A + B <> {}
proof
thus A <> {} & B <> {} implies A + B <> {}
proof
assume
A1: A <> {};
then reconsider x = the Element of A as Element of G by TARSKI:def 3;
assume
A2: B <> {};
then reconsider y = the Element of B as Element of G by TARSKI:def 3;
x + y in A + B by A1,A2;
hence thesis;
end;
set x = the Element of A + B;
assume A + B <> {};
then ex a,b st x = a + b & a in A & b in B by ThX8;
hence thesis;
end;
theorem Th10:
G is add-associative implies A + B + C = A + (B + C)
proof
assume
A1: G is add-associative;
thus A + B + C c= A + (B + C)
proof
let x be object;
assume x in A + B + C;
then consider g,h such that
A2: x = g + h and
A3: g in A + B and
A4: h in C;
consider g1,g2 such that
A5: g = g1 + g2 and
A6: g1 in A and
A7: g2 in B by A3;
x = g1 + (g2 + h) & g2 + h in B + C by A1,A2,A4,A5,A7;
hence thesis by A6;
end;
let x be object;
assume x in A + (B + C);
then consider g,h such that
A8: x = g + h and
A9: g in A and
A10: h in B + C;
consider g1,g2 such that
A11: h = g1 + g2 and
A12: g1 in B and
A13: g2 in C by A10;
A14: g + g1 in A + B by A9,A12;
x = g + g1 + g2 by A1,A8,A11;
hence thesis by A13,A14;
end;
theorem
for G being addGroup, A,B being Subset of G holds -(A + B) = -B + -A
proof
let G be addGroup, A,B be Subset of G;
thus -(A + B) c= -B + -A
proof
let x be object;
assume x in -(A + B);
then consider g being Element of G such that
A1: x = -g and
A2: g in A + B;
consider g1,g2 being Element of G such that
A3: g = g1 + g2 and
A4: g1 in A & g2 in B by A2;
A5: -g1 in -A & -g2 in -B by A4;
x = -g2 + -g1 by A1,A3,Th16;
hence thesis by A5;
end;
let x be object;
assume x in -B + -A;
then consider g1,g2 being Element of G such that
A6: x = g1 + g2 and
A7: g1 in -B and
A8: g2 in -A;
consider b being Element of G such that
A9: g2 = -b and
A10: b in A by A8;
consider a being Element of G such that
A11: g1 = -a and
A12: a in B by A7;
A13: b + a in A + B by A12,A10;
x = -(b + a) by A6,A11,A9,Th16;
hence thesis by A13;
end;
theorem
A + (B \/ C) = (A + B) \/ (A + C)
proof
thus A + (B \/ C) c= (A + B) \/ (A + C)
proof
let x be object;
assume x in A + (B \/ C);
then consider g1,g2 such that
A1: x = g1 + g2 & g1 in A and
A2: g2 in B \/ C;
g2 in B or g2 in C by A2,XBOOLE_0:def 3;
then x in A + B or x in A + C by A1;
hence thesis by XBOOLE_0:def 3;
end;
let x be object;
assume
A3: x in (A + B) \/ (A + C);
now
per cases by A3,XBOOLE_0:def 3;
suppose
x in A + B;
then consider g1,g2 such that
A4: x = g1 + g2 & g1 in A and
A5: g2 in B;
g2 in B \/ C by A5,XBOOLE_0:def 3;
hence thesis by A4;
end;
suppose
x in A + C;
then consider g1,g2 such that
A6: x = g1 + g2 & g1 in A and
A7: g2 in C;
g2 in B \/ C by A7,XBOOLE_0:def 3;
hence thesis by A6;
end;
end;
hence thesis;
end;
theorem
(A \/ B) + C = (A + C) \/ (B + C)
proof
thus (A \/ B) + C c= (A + C) \/ (B + C)
proof
let x be object;
assume x in (A \/ B) + C;
then consider g1,g2 such that
A1: x = g1 + g2 and
A2: g1 in A \/ B and
A3: g2 in C;
g1 in A or g1 in B by A2,XBOOLE_0:def 3;
then x in A + C or x in B + C by A1,A3;
hence thesis by XBOOLE_0:def 3;
end;
let x be object;
assume
A4: x in (A + C) \/ (B + C);
now
per cases by A4,XBOOLE_0:def 3;
suppose
x in A + C;
then consider g1,g2 such that
A5: x = g1 + g2 and
A6: g1 in A and
A7: g2 in C;
g1 in A \/ B by A6,XBOOLE_0:def 3;
hence thesis by A5,A7;
end;
suppose
x in B + C;
then consider g1,g2 such that
A8: x = g1 + g2 and
A9: g1 in B and
A10: g2 in C;
g1 in A \/ B by A9,XBOOLE_0:def 3;
hence thesis by A8,A10;
end;
end;
hence thesis;
end;
theorem
A + (B /\ C) c= (A + B) /\ (A + C)
proof
let x be object;
assume x in A + (B /\ C);
then consider g1,g2 such that
A1: x = g1 + g2 & g1 in A and
A2: g2 in B /\ C;
g2 in C by A2,XBOOLE_0:def 4;
then
A3: x in A + C by A1;
g2 in B by A2,XBOOLE_0:def 4;
then x in A + B by A1;
hence thesis by A3;
end;
theorem
(A /\ B) + C c= (A + C) /\ (B + C)
proof
let x be object;
assume x in (A /\ B) + C;
then consider g1,g2 such that
A1: x = g1 + g2 and
A2: g1 in A /\ B and
A3: g2 in C;
g1 in B by A2,XBOOLE_0:def 4;
then
A4: x in B + C by A1,A3;
g1 in A by A2,XBOOLE_0:def 4;
then x in A + C by A1,A3;
hence thesis by A4;
end;
theorem ThA16:
{}(the carrier of G) + A = {} & A + {}(the carrier of G) = {}
proof
A1: now
set x = the Element of A + {}(the carrier of G);
assume A + {}(the carrier of G) <> {};
then ex g1,g2 st x = g1 + g2 & g1 in A & g2 in {}(the carrier of G)
by ThX8;
hence contradiction;
end;
now
set x = the Element of {}(the carrier of G) + A;
assume {}(the carrier of G) + A <> {};
then ex g1,g2 st x = g1 + g2 & g1 in {}(the carrier of G) & g2 in A
by ThX8;
hence contradiction;
end;
hence thesis by A1;
end;
theorem ThX17:
for G being addGroup, A being Subset of G holds
A <> {} implies [#](the carrier of G) + A = the carrier of G &
A + [#](the carrier of G) = the carrier of G
proof
let G be addGroup, A be Subset of G;
set y = the Element of A;
assume
A1: A <> {};
then reconsider y as Element of G by Lm1;
thus [#](the carrier of G) + A = the carrier of G
proof
set y = the Element of A;
reconsider y as Element of G by A1,Lm1;
thus [#](the carrier of G) + A c= the carrier of G;
let x be object;
assume x in the carrier of G;
then reconsider a = x as Element of G;
(a + -y) + y = a + (-y + y) by RLVECT_1:def 3
.= a + 0_G by Def5
.= a by Def4;
hence thesis by A1;
end;
thus A + [#](the carrier of G) c= the carrier of G;
let x be object;
assume x in the carrier of G;
then reconsider a = x as Element of G;
y + (-y + a) = (y + -y) + a by RLVECT_1:def 3
.= 0_G + a by Def5
.= a by Def4;
hence thesis by A1;
end;
theorem Th18:
{g} + {h} = {g + h}
proof
thus {g} + {h} c= {g + h}
proof
let x be object;
assume x in {g} + {h};
then consider g1,g2 such that
A1: x = g1 + g2 and
A2: g1 in {g} & g2 in {h};
g1 = g & g2 = h by A2,TARSKI:def 1;
hence thesis by A1,TARSKI:def 1;
end;
let x be object;
assume x in {g + h};
then
A3: x = g + h by TARSKI:def 1;
g in {g} & h in {h} by TARSKI:def 1;
hence thesis by A3;
end;
theorem
{g} + {g1,g2} = {g + g1,g + g2}
proof
thus {g} + {g1,g2} c= {g + g1,g + g2}
proof
let x be object;
assume x in {g} + {g1,g2};
then consider h1,h2 such that
A1: x = h1 + h2 and
A2: h1 in {g} and
A3: h2 in {g1,g2};
A4: h2 = g1 or h2 = g2 by A3,TARSKI:def 2;
h1 = g by A2,TARSKI:def 1;
hence thesis by A1,A4,TARSKI:def 2;
end;
let x be object;
A5: g2 in {g1,g2} by TARSKI:def 2;
assume x in {g + g1,g + g2};
then
A6: x = g + g1 or x = g + g2 by TARSKI:def 2;
g in {g} & g1 in {g1,g2} by TARSKI:def 1,def 2;
hence thesis by A6,A5;
end;
theorem
{g1,g2} + {g} = {g1 + g,g2 + g}
proof
thus {g1,g2} + {g} c= {g1 + g,g2 + g}
proof
let x be object;
assume x in {g1,g2} + {g};
then consider h1,h2 such that
A1: x = h1 + h2 and
A2: h1 in {g1,g2} and
A3: h2 in {g};
A4: h1 = g1 or h1 = g2 by A2,TARSKI:def 2;
h2 = g by A3,TARSKI:def 1;
hence thesis by A1,A4,TARSKI:def 2;
end;
let x be object;
A5: g2 in {g1,g2} by TARSKI:def 2;
assume x in {g1 + g,g2 + g};
then
A6: x = g1 + g or x = g2 + g by TARSKI:def 2;
g in {g} & g1 in {g1,g2} by TARSKI:def 1,def 2;
hence thesis by A6,A5;
end;
theorem
{g,h} + {g1,g2} = {g + g1, g + g2, h + g1, h + g2}
proof
set A = {g,h} + {g1,g2};
set B = {g + g1, g + g2, h + g1, h + g2};
thus A c= B
proof
let x be object;
assume x in A;
then consider h1,h2 such that
A1: x = h1 + h2 and
A2: h1 in {g,h} and
A3: h2 in {g1,g2};
A4: h2 = g1 or h2 = g2 by A3,TARSKI:def 2;
h1 = g or h1 = h by A2,TARSKI:def 2;
hence thesis by A1,A4,ENUMSET1:def 2;
end;
let x be object;
A5: g1 in {g1,g2} & g2 in {g1,g2} by TARSKI:def 2;
assume x in B;
then
A6: x = g + g1 or x = g + g2 or x = h + g1 or x = h + g2 by ENUMSET1:def 2;
g in {g,h} & h in {g,h} by TARSKI:def 2;
hence thesis by A6,A5;
end;
theorem Th22:
for G being addGroup, A being Subset of G holds (for g1,g2 being
Element of G st g1 in A & g2 in A holds g1 + g2 in A) & (for g being Element of
G st g in A holds -g in A) implies A + A = A
proof
let G be addGroup, A be Subset of G such that
A1: for g1,g2 being Element of G st g1 in A & g2 in A holds g1 + g2 in A and
A2: for g being Element of G st g in A holds -g in A;
thus A + A c= A
proof
let x be object;
assume x in A + A;
then ex g1,g2 being Element of G st x = g1 + g2 & g1 in A & g2 in A;
hence thesis by A1;
end;
let x be object;
assume
A3: x in A;
then reconsider a = x as Element of G;
-a in A by A2,A3;
then -a + a in A by A1,A3;
then
A4: 0_G in A by Def5;
0_G + a = a by Def4;
hence thesis by A3,A4;
end;
theorem Th23:
for G being addGroup, A being Subset of G holds (for g being
Element of G st g in A holds -g in A) implies -A = A
proof
let G be addGroup, A be Subset of G;
assume
A1: for g being Element of G st g in A holds -g in A;
thus -A c= A
proof
let x be object;
assume x in -A;
then ex g being Element of G st x = -g & g in A;
hence thesis by A1;
end;
let x be object;
assume
A2: x in A;
then reconsider a = x as Element of G;
A3: x = --a;
-a in A by A1,A2;
hence thesis by A3;
end;
theorem
(for a,b st a in A & b in B holds a + b = b + a) implies A + B = B + A
proof
assume
A1: for a,b st a in A & b in B holds a + b = b + a;
thus A + B c= B + A
proof
let x be object;
assume x in A + B;
then consider a,b such that
A2: x = a + b and
A3: a in A & b in B;
x = b + a by A1,A2,A3;
hence thesis by A3;
end;
let x be object;
assume x in B + A;
then consider b,a such that
A4: x = b + a and
A5: b in B & a in A;
x = a + b by A1,A4,A5;
hence thesis by A5;
end;
Lm2: for A be Abelian addGroup, a, b be Element of A holds a + b = b + a;
theorem Th25:
G is Abelian addGroup implies A + B = B + A
proof
assume
A1: G is Abelian addGroup;
thus A + B c= B + A
proof
let x be object;
assume x in A + B;
then consider g,h such that
A2: x = g + h and
A3: g in A & h in B;
x = h + g by A1,A2,Lm2;
hence thesis by A3;
end;
let x be object;
assume x in B + A;
then consider g,h such that
A4: x = g + h and
A5: g in B & h in A;
x = h + g by A1,A4,Lm2;
hence thesis by A5;
end;
theorem
for G being Abelian addGroup, A,B being Subset of G holds
-(A + B) = -A + -B
proof
let G be Abelian addGroup, A,B be Subset of G;
thus -(A + B) c= -A + -B
proof
let x be object;
assume x in -(A + B);
then consider g being Element of G such that
A1: x = -g and
A2: g in A + B;
consider g1,g2 being Element of G such that
A3: g = g1 + g2 and
A4: g1 in A & g2 in B by A2;
A5: -g1 in -A & -g2 in -B by A4;
x = -g1 + -g2 by A1,A3,Th44;
hence thesis by A5;
end;
let x be object;
assume x in -A + -B;
then consider g1,g2 being Element of G such that
A6: x = g1 + g2 and
A7: g1 in -A and
A8: g2 in -B;
consider b being Element of G such that
A9: g2 = -b and
A10: b in B by A8;
consider a being Element of G such that
A11: g1 = -a and
A12: a in A by A7;
A13: a + b in A + B by A12,A10;
x = -(a + b) by A6,A11,A9,Th44;
hence thesis by A13;
end;
definition
let G,g,A;
func g + A -> Subset of G equals
{g} + A;
correctness;
func A + g -> Subset of G equals
A + {g};
correctness;
end;
theorem Th27:
x in g + A iff ex h st x = g + h & h in A
proof
thus x in g + A implies ex h st x = g + h & h in A
proof
assume x in g + A;
then consider g1,g2 such that
A1: x = g1 + g2 and
A2: g1 in {g} and
A3: g2 in A;
g1 = g by A2,TARSKI:def 1;
hence thesis by A1,A3;
end;
given h such that
A4: x = g + h & h in A;
g in {g} by TARSKI:def 1;
hence thesis by A4;
end;
theorem Th28:
x in A + g iff ex h st x = h + g & h in A
proof
thus x in A + g implies ex h st x = h + g & h in A
proof
assume x in A + g;
then consider g1,g2 such that
A1: x = g1 + g2 & g1 in A and
A2: g2 in {g};
g2 = g by A2,TARSKI:def 1;
hence thesis by A1;
end;
given h such that
A3: x = h + g & h in A;
g in {g} by TARSKI:def 1;
hence thesis by A3;
end;
theorem ThB29:
G is add-associative implies g + A + B = g + (A + B) by Th10;
theorem ThA30:
G is add-associative implies A + g + B = A + (g + B) by Th10;
theorem ThB31:
G is add-associative implies A + B + g = A + (B + g) by Th10;
theorem Th32:
G is add-associative implies g + h + A = g + (h + A)
proof
assume
A1: G is add-associative;
thus g + h + A = {g} + {h} + A by Th18
.= g + (h + A) by A1,Th10;
end;
theorem ThA33:
G is add-associative implies g + A + h = g + (A + h) by Th10;
theorem ThB34:
G is add-associative implies A + g + h = A + (g + h)
proof
assume G is add-associative;
hence A + g + h = A + ({g} + {h}) by Th10
.= A + (g + h) by Th18;
end;
theorem
{}(the carrier of G) + a = {} & a + {}(the carrier of G) = {} by ThA16;
reserve G for addGroup-like non empty addMagma;
reserve h,g,g1,g2 for Element of G;
reserve A for Subset of G;
theorem
for G being addGroup, a being Element of G holds [#](the carrier of G) +
a = the carrier of G & a + [#](the carrier of G) = the carrier of G
by ThX17;
theorem Th37:
0_G + A = A & A + 0_G = A
proof
thus 0_G + A = A
proof
thus 0_G + A c= A
proof
let x be object;
assume x in 0_G + A;
then ex h st x = 0_G + h & h in A by Th27;
hence thesis by Def4;
end;
let x be object;
assume
A1: x in A;
then reconsider a = x as Element of G;
0_G + a = a by Def4;
hence thesis by A1,Th27;
end;
thus A + 0_G c= A
proof
let x be object;
assume x in A + 0_G;
then ex h st x = h + 0_G & h in A by Th28;
hence thesis by Def4;
end;
let x be object;
assume
A2: x in A;
then reconsider a = x as Element of G;
a + 0_G = a by Def4;
hence thesis by A2,Th28;
end;
theorem
G is Abelian addGroup implies g + A = A + g by Th25;
definition
let G be addGroup-like non empty addMagma;
mode Subgroup of G -> addGroup-like non empty addMagma means
:DefA5:
the carrier of it c= the carrier of G &
the addF of it = (the addF of G)||the carrier of it;
existence
proof
take G;
dom(the addF of G) = [:the carrier of G,the carrier of G:] by
FUNCT_2:def 1;
hence thesis by RELAT_1:68;
end;
end;
reserve H for Subgroup of G;
reserve h,h1,h2 for Element of H;
theorem Th39:
G is finite implies H is finite
proof
assume
A1: G is finite;
the carrier of H c= the carrier of G by DefA5;
hence the carrier of H is finite by A1;
end;
theorem Th40:
x in H implies x in G
proof
assume
A1: x in H;
the carrier of H c= the carrier of G by DefA5;
hence thesis by A1;
end;
theorem Th41:
h in G by Th40,STRUCT_0:def 5;
theorem Th42:
h is Element of G by Th41,STRUCT_0:def 5;
theorem Th43:
h1 = g1 & h2 = g2 implies h1 + h2 = g1 + g2
proof
assume
A1: h1 = g1 & h2 = g2;
h1 + h2 = ((the addF of G)||the carrier of H).[h1,h2] by DefA5;
hence thesis by A1,FUNCT_1:49;
end;
registration
let G be addGroup;
cluster -> add-associative for Subgroup of G;
coherence
proof
let H be Subgroup of G;
let x, y, z be Element of H;
y+z in the carrier of H & the carrier of H c= the carrier of G by DefA5;
then reconsider
a = x, b = y, c = z, ab = x+y, bc = y+z as Element of G;
thus x+y+z = ab+c by Th43
.= a+b+c by Th43
.= a+(b+c) by RLVECT_1:def 3
.= a+bc by Th43
.= x+(y+z) by Th43;
end;
end;
reserve G,G1,G2,G3 for addGroup;
reserve a,a1,a2,b,b1,b2,g,g1,g2 for Element of G;
reserve A,B for Subset of G;
reserve H,H1,H2,H3 for Subgroup of G;
reserve h,h1,h2 for Element of H;
theorem Th44:
0_H = 0_G
proof
set h = the Element of H;
reconsider g = h, g9 = 0_H as Element of G by Th41,STRUCT_0:def 5;
h + 0_H = h by Def4;
then g + g9 = g by Th43;
hence thesis by Th7;
end;
theorem
0_H1 = 0_H2
proof
thus 0_H1 = 0_G by Th44
.= 0_H2 by Th44;
end;
theorem Th46:
0_G in H
proof
0_H in H;
hence thesis by Th44;
end;
theorem
0_H1 in H2
proof
0_H1 = 0_G by Th44;
hence thesis by Th46;
end;
theorem Th48:
h = g implies -h = -g
proof
reconsider g9 = -h as Element of G by Th41,STRUCT_0:def 5;
A1: h + -h = 0_H by Def5;
assume h = g;
then g + g9 = 0_H by A1,Th43
.= 0_G by Th44;
hence thesis by Th11;
end;
theorem
add_inverse(H) = add_inverse(G) | the carrier of H
proof
A1: (the carrier of G) /\ (the carrier of H) = the carrier of H
by DefA5,XBOOLE_1:28;
A2: now
let x be object;
assume x in dom(add_inverse(H));
then reconsider a = x as Element of H;
reconsider b = a as Element of G by Th41,STRUCT_0:def 5;
thus add_inverse(H).x = -a by Def6
.= -b by Th48
.= add_inverse(G).x by Def6;
end;
dom(add_inverse(H)) = the carrier of H & dom(add_inverse(G)) = the carrier
of G by FUNCT_2:def 1;
hence thesis by A1,A2,FUNCT_1:46;
end;
theorem Th50:
g1 in H & g2 in H implies g1 + g2 in H
proof
assume g1 in H & g2 in H;
then reconsider h1 = g1, h2 = g2 as Element of H;
h1 + h2 in H;
hence thesis by Th43;
end;
theorem Th51:
g in H implies -g in H
proof
assume g in H;
then reconsider h = g as Element of H;
-h in H;
hence thesis by Th48;
end;
registration
let G;
cluster strict for Subgroup of G;
existence
proof
set H = addMagma (#the carrier of G, the addF of G#);
H is addGroup-like
proof
reconsider t = 0_G as Element of H;
take t;
let a be Element of H;
reconsider x = a as Element of G;
thus a + t = x + 0_G .= a by Def4;
thus t + a = 0_G + x .= a by Def4;
reconsider s = -x as Element of H;
take s;
thus a + s = x + -x .= t by Def5;
thus s + a = -x + x .= t by Def5;
end;
then reconsider H as addGroup-like non empty addMagma;
the addF of H = (the addF of G)||the carrier of H by RELSET_1:19;
then H is Subgroup of G by DefA5;
hence thesis;
end;
end;
theorem Th52:
A <> {} & (for g1,g2 st g1 in A & g2 in A holds g1 + g2 in A) &
(for g st g in A holds -g in A) implies ex H being strict Subgroup of G st the
carrier of H = A
proof
assume that
A1: A <> {} and
A2: for g1,g2 st g1 in A & g2 in A holds g1 + g2 in A and
A3: for g st g in A holds -g in A;
reconsider D = A as non empty set by A1;
set o = (the addF of G)||A;
A4: dom o = dom(the addF of G) /\ [:A,A:] by RELAT_1:61;
dom(the addF of G) = [:the carrier of G,the carrier of G:] by FUNCT_2:def 1;
then
A5: dom o = [:A,A:] by A4,XBOOLE_1:28;
rng o c= A
proof
let x be object;
assume x in rng o;
then consider y being object such that
A6: y in dom o and
A7: o.y = x by FUNCT_1:def 3;
consider y1,y2 being object such that
A8: [y1,y2] = y by A4,A6,RELAT_1:def 1;
A9: y1 in A & y2 in A by A5,A6,A8,ZFMISC_1:87;
reconsider y1,y2 as Element of G by A4,A6,A8,ZFMISC_1:87;
x = y1 + y2 by A6,A7,A8,FUNCT_1:47;
hence thesis by A2,A9;
end;
then reconsider o as BinOp of D by A5,FUNCT_2:def 1,RELSET_1:4;
set H = addMagma (# D,o #);
A10: now
let g1,g2;
let h1,h2 be Element of H;
A11: h1 + h2 = ((the addF of G)||A).[h1,h2];
assume g1 = h1 & g2 = h2;
hence g1 + g2 = h1 + h2 by A11,FUNCT_1:49;
end;
H is addGroup-like
proof
set a = the Element of H;
reconsider x = a as Element of G by Lm1;
-x in A by A3;
then x + -x in A by A2;
then reconsider t = 0_G as Element of H by Def5;
take t;
let a be Element of H;
reconsider x = a as Element of G by Lm1;
thus a + t = x + 0_G by A10
.= a by Def4;
thus t + a = 0_G + x by A10
.= a by Def4;
reconsider s = -x as Element of H by A3;
take s;
thus a + s = x + -x by A10
.= t by Def5;
thus s + a = -x + x by A10
.= t by Def5;
end;
then reconsider H as addGroup-like non empty addMagma;
reconsider H as strict Subgroup of G by DefA5;
take H;
thus thesis;
end;
theorem Th53:
G is Abelian addGroup implies H is Abelian
proof
assume
A1: G is Abelian addGroup;
thus for h1,h2 holds h1 + h2 = h2 + h1
proof
let h1,h2;
reconsider g1 = h1, g2 = h2 as Element of G by Th41,STRUCT_0:def 5;
thus h1 + h2 = g1 + g2 by Th43
.= g2 + g1 by A1,Lm2
.= h2 + h1 by Th43;
end;
end;
registration
let G be Abelian addGroup;
cluster -> Abelian for Subgroup of G;
coherence by Th53;
end;
theorem ThA54:
G is Subgroup of G
proof
dom(the addF of G) = [:the carrier of G,the carrier of G:] by FUNCT_2:def 1;
hence the carrier of G c= the carrier of G &
the addF of G = (the addF of G)||the carrier of G by RELAT_1:68;
end;
theorem Th55:
G1 is Subgroup of G2 & G2 is Subgroup of G1 implies the
addMagma of G1 = the addMagma of G2
proof
assume that
A1: G1 is Subgroup of G2 and
A2: G2 is Subgroup of G1;
set g = the addF of G2;
set f = the addF of G1;
set B = the carrier of G2;
set A = the carrier of G1;
A3: A c= B & B c= A by A1,A2,DefA5;
A4: A = B by A1,A2,DefA5;
f = g||A by A1,DefA5
.= (f||B)||A by A2,DefA5
.= f||B by A4,RELAT_1:72
.= g by A2,DefA5;
hence thesis by A3,XBOOLE_0:def 10;
end;
theorem Th56:
G1 is Subgroup of G2 & G2 is Subgroup of G3 implies G1 is Subgroup of G3
proof
assume that
A1: G1 is Subgroup of G2 and
A2: G2 is Subgroup of G3;
set h = the addF of G3;
set C = the carrier of G3;
set B = the carrier of G2;
set A = the carrier of G1;
A3: A c= B by A1,DefA5;
then
A4: [:A,A:] c= [:B,B:] by ZFMISC_1:96;
B c= C by A2,DefA5;
then
A5: A c= C by A3;
the addF of G1 = (the addF of G2)||A by A1,DefA5
.= (h||B)||A by A2,DefA5
.= h||A by A4,FUNCT_1:51;
hence thesis by A5,DefA5;
end;
theorem Th57:
the carrier of H1 c= the carrier of H2 implies H1 is Subgroup of H2
proof
set A = the carrier of H1;
set B = the carrier of H2;
set h = the addF of G;
assume
A1: the carrier of H1 c= the carrier of H2;
hence the carrier of H1 c= the carrier of H2;
A2: [:A,A:] c= [:B,B:] by A1,ZFMISC_1:96;
the addF of H1 = h||A & the addF of H2 = h||B by DefA5;
hence thesis by A2,FUNCT_1:51;
end;
theorem Th58:
(for g st g in H1 holds g in H2) implies H1 is Subgroup of H2
proof
assume
A1: for g st g in H1 holds g in H2;
the carrier of H1 c= the carrier of H2
proof
let x be object;
assume x in the carrier of H1;
then reconsider g = x as Element of H1;
reconsider g as Element of G by Th41,STRUCT_0:def 5;
g in H1;
then g in H2 by A1;
hence thesis;
end;
hence thesis by Th57;
end;
theorem Th59:
the carrier of H1 = the carrier of H2 implies the addMagma of
H1 = the addMagma of H2
proof
assume the carrier of H1 = the carrier of H2;
then H1 is Subgroup of H2 & H2 is Subgroup of H1 by Th57;
hence thesis by Th55;
end;
theorem Th60:
(for g holds g in H1 iff g in H2) implies the addMagma of H1 =
the addMagma of H2
proof
assume for g holds g in H1 iff g in H2;
then H1 is Subgroup of H2 & H2 is Subgroup of H1 by Th58;
hence thesis by Th55;
end;
definition
let G;
let H1,H2 be strict Subgroup of G;
redefine pred H1 = H2 means :: redefines = (XBOOLE_0, redefinition) → = (HIDDEN, definition)
for g holds g in H1 iff g in H2;
compatibility by Th60;
end;
theorem Th61:
for G being addGroup, H being Subgroup of G st the carrier of G c=
the carrier of H holds the addMagma of H = the addMagma of G
proof
let G be addGroup, H be Subgroup of G;
assume
A1: the carrier of G c= the carrier of H;
A2: G is Subgroup of G by ThA54;
the carrier of G = the carrier of H by A1,DefA5;
hence thesis by A2,Th59;
end;
theorem Th62:
(for g being Element of G holds g in H) implies the addMagma of
H = the addMagma of G
proof
assume for g being Element of G holds g in H;
then
A1: for g be Element of G holds ( g in H implies g in G) &( g in G implies g
in H);
G is Subgroup of G by ThA54;
hence thesis by A1,Th60;
end;
definition
let G;
func (0).G -> strict Subgroup of G means
:Def7:
the carrier of it = {0_G};
existence
proof
A1: now
let g;
assume g in {0_G};
then g = 0_G by TARSKI:def 1;
then -g = 0_G by Th8;
hence -g in {0_G} by TARSKI:def 1;
end;
now
let g1,g2;
assume g1 in {0_G} & g2 in {0_G};
then g1 = 0_G & g2 = 0_G by TARSKI:def 1;
then g1 + g2 = 0_G by Def4;
hence g1 + g2 in {0_G} by TARSKI:def 1;
end;
hence thesis by A1,Th52;
end;
uniqueness by Th59;
end;
definition
let G;
func (Omega).G -> strict Subgroup of G equals
the addMagma of G;
coherence
proof
set H = the addMagma of G;
H is addGroup-like
proof
consider e9 being Element of G such that
A1: for h being Element of G holds h + e9 = h & e9 + h = h & ex g
being Element of G st h + g = e9 & g + h = e9 by Def2;
reconsider e = e9 as Element of H;
take e;
let h be Element of H;
reconsider h9 = h as Element of G;
consider g9 being Element of G such that
A2: h9 + g9 = e9 & g9 + h9 = e9 by A1;
h9 + e9 = h9 & e9 + h9 = h9 by A1;
hence h + e = h & e + h = h;
reconsider g = g9 as Element of H;
take g;
thus thesis by A2;
end;
then reconsider H as addGroup-like non empty addMagma;
dom(the addF of G) = [:the carrier of G,the carrier of G:] by
FUNCT_2:def 1;
then the addF of H = (the addF of G)||the carrier of H by RELAT_1:68;
hence thesis by DefA5;
end;
projectivity;
end;
theorem Th63:
(0).H = (0).G
proof
A1: 0_H = 0_G by Th44;
(0).H is Subgroup of G & the carrier of (0).H = {0_H} by Def7,Th56;
hence thesis by A1,Def7;
end;
theorem
(0).H1 = (0).H2
proof
thus (0).H1 = (0).G by Th63
.= (0).H2 by Th63;
end;
theorem Th65:
(0).G is Subgroup of H
proof
(0).G = (0).H by Th63;
hence thesis;
end;
theorem
for G being strict addGroup, H being Subgroup of G holds H is Subgroup of
(Omega).G;
theorem
for G being strict addGroup holds G is Subgroup of (Omega).G;
theorem Th68:
(0).G is finite
proof
the carrier of (0).G = {0_G} by Def7;
hence thesis;
end;
registration
let G;
cluster (0).G -> finite;
coherence by Th68;
cluster strict finite for Subgroup of G;
existence
proof
take (0).G;
thus thesis;
end;
end;
registration
cluster strict finite for addGroup;
existence
proof
set G = the addGroup;
take (0).G;
thus thesis;
end;
end;
registration
let G be finite addGroup;
cluster -> finite for Subgroup of G;
coherence by Th39;
end;
theorem Th69:
card (0).G = 1
proof
the carrier of (0).G = {0_G} by Def7;
hence thesis by CARD_1:30;
end;
theorem Th70:
for H being strict finite Subgroup of G holds card H = 1 implies H = (0).G
proof
let H be strict finite Subgroup of G;
assume card H = 1;
then consider x being object such that
A1: the carrier of H = {x} by CARD_2:42;
0_G in H by Th46;
then x = 0_G by A1,TARSKI:def 1;
hence thesis by A1,Def7;
end;
theorem
card H c= card G by DefA5,CARD_1:11;
theorem
for G being finite addGroup, H being Subgroup of G holds card H <= card G
by DefA5,NAT_1:43;
theorem
for G being finite addGroup, H being Subgroup of G holds card G = card H
implies the addMagma of H = the addMagma of G
proof
let G be finite addGroup, H be Subgroup of G;
assume
A1: card G = card H;
the carrier of H = the carrier of G
proof
assume the carrier of H <> the carrier of G;
then the carrier of H c< the carrier of G by DefA5;
hence thesis by A1,CARD_2:48;
end;
hence thesis by Th61;
end;
definition
let G,H;
func carr(H) -> Subset of G equals
the carrier of H;
coherence by DefA5;
end;
theorem Th74:
g1 in carr(H) & g2 in carr(H) implies g1 + g2 in carr(H)
proof
assume g1 in carr(H) & g2 in carr(H);
then g1 in H & g2 in H;
then g1 + g2 in H by Th50;
hence thesis;
end;
theorem Th75:
g in carr(H) implies -g in carr(H)
proof
assume g in carr(H);
then g in H;
then -g in H by Th51;
hence thesis;
end;
theorem
carr(H) + carr(H) = carr(H)
proof
A1: g in carr(H) implies -g in carr(H) by Th75;
g1 in carr(H) & g2 in carr(H) implies g1 + g2 in carr(H) by Th74;
hence thesis by A1,Th22;
end;
theorem
-carr(H) = carr H
proof
g in carr H implies -g in carr H by Th75;
hence thesis by Th23;
end;
theorem Th78:
(carr H1 + carr H2 = carr H2 + carr H1 implies ex H being strict
Subgroup of G st the carrier of H = carr H1 + carr H2) & ((ex H st the carrier
of H = carr H1 + carr H2) implies carr H1 + carr H2 = carr H2 + carr H1)
proof
thus carr(H1) + carr(H2) = carr(H2) + carr(H1) implies ex H being strict
Subgroup of G st the carrier of H = carr(H1) + carr(H2)
proof
assume
A1: carr H1 + carr H2 = carr H2 + carr H1;
A2: now
let g;
assume
A3: g in carr H1 + carr H2;
then consider a,b such that
A4: g = a + b and
a in carr H1 and
b in carr H2;
consider b1,a1 such that
A5: a + b = b1 + a1 and
A6: b1 in carr H2 & a1 in carr H1 by A1,A3,A4;
A7: -a1 in carr H1 & -b1 in carr H2 by A6,Th75;
-g = -a1 + -b1 by A4,A5,Th16;
hence -g in carr H1 + carr H2 by A7;
end;
now
let g1,g2;
assume that
A9: g1 in carr(H1) + carr(H2) and
A10: g2 in carr(H1) + carr(H2);
consider a1,b1 such that
A11: g1 = a1 + b1 and
A12: a1 in carr(H1) and
A13: b1 in carr(H2) by A9;
consider a2,b2 such that
A14: g2 = a2 + b2 and
A15: a2 in carr H1 and
A16: b2 in carr H2 by A10;
b1 + a2 in carr H1 + carr H2 by A1,A13,A15;
then consider a,b such that
A17: b1 + a2 = a + b and
A18: a in carr H1 and
A19: b in carr H2;
A20: b + b2 in carr H2 by A16,A19,Th74;
g1 + g2 = a1 + b1 + a2 + b2 by A11,A14,RLVECT_1:def 3
.= a1 + (b1 + a2) + b2 by RLVECT_1:def 3;
then
A21: g1 + g2 = a1 + a + b + b2 by A17,RLVECT_1:def 3
.= a1 + a + (b + b2) by RLVECT_1:def 3;
a1 + a in carr H1 by A12,A18,Th74;
hence g1 + g2 in carr H1 + carr H2 by A21,A20;
end;
hence thesis by A2,Th9,Th52;
end;
given H such that
A22: the carrier of H = carr H1 + carr H2;
thus carr H1 + carr H2 c= carr H2 + carr H1
proof
let x be object;
assume
A23: x in carr H1 + carr H2;
then reconsider y = x as Element of G;
-y in carr H by A22,A23,Th75;
then consider a,b such that
A24: -y = a + b and
A25: a in carr H1 & b in carr H2 by A22;
A26: y = - -y .= -b + -a by A24,Th16;
-a in carr H1 & -b in carr H2 by A25,Th75;
hence thesis by A26;
end;
let x be object;
assume
A27: x in carr H2 + carr H1;
then reconsider y = x as Element of G;
consider a,b such that
A28: x = a + b & a in carr H2 and
A29: b in carr H1 by A27;
now
A30: -b in carr H1 by A29,Th75;
assume
A31: not -y in carr H;
-y = -b + -a & -a in carr H2 by A28,Th16,Th75;
hence contradiction by A22,A31,A30;
end;
then - -y in carr H by Th75;
hence thesis by A22;
end;
theorem
G is Abelian addGroup implies ex H being strict Subgroup of G st the
carrier of H = carr(H1) + carr(H2)
proof
assume G is Abelian addGroup;
then carr(H1) + carr(H2) = carr(H2) + carr(H1) by Th25;
hence thesis by Th78;
end;
definition
let G,H1,H2;
func H1 /\ H2 -> strict Subgroup of G means
:Def10:
the carrier of it = carr (H1) /\ carr(H2);
existence
proof
set A = carr(H1) /\ carr(H2);
A1: 0_G in H2 by Th46;
A2: now
let g1,g2;
assume
A3: g1 in A & g2 in A;
then g1 in carr(H2) & g2 in carr(H2) by XBOOLE_0:def 4;
then
A4: g1 + g2 in carr(H2) by Th74;
g1 in carr(H1) & g2 in carr(H1) by A3,XBOOLE_0:def 4;
then g1 + g2 in carr(H1) by Th74;
hence g1 + g2 in A by A4;
end;
A5: now
let g;
assume
A6: g in A;
then g in carr(H2) by XBOOLE_0:def 4;
then
A7: -g in carr(H2) by Th75;
g in carr(H1) by A6,XBOOLE_0:def 4;
then -g in carr(H1) by Th75;
hence -g in A by A7;
end;
0_G in H1 by Th46;
then A <> {} by A1,XBOOLE_0:def 4;
hence thesis by A2,A5,Th52;
end;
uniqueness by Th59;
end;
theorem Th80:
(for H being Subgroup of G st H = H1 /\ H2 holds the carrier of
H = (the carrier of H1) /\ (the carrier of H2)) & for H being strict Subgroup
of G holds the carrier of H = (the carrier of H1) /\ (the carrier of H2)
implies H = H1 /\ H2
proof
A1: the carrier of H1 = carr(H1) & the carrier of H2 = carr(H2);
thus for H being Subgroup of G st H = H1 /\ H2 holds the carrier of H = (the
carrier of H1) /\ (the carrier of H2)
proof
let H be Subgroup of G;
assume H = H1 /\ H2;
hence the carrier of H = carr(H1) /\ carr(H2) by Def10
.= (the carrier of H1) /\ (the carrier of H2);
end;
let H be strict Subgroup of G;
assume the carrier of H = (the carrier of H1) /\ (the carrier of H2);
hence thesis by A1,Def10;
end;
theorem
carr(H1 /\ H2) = carr(H1) /\ carr(H2) by Def10;
theorem Th82:
x in H1 /\ H2 iff x in H1 & x in H2
proof
thus x in H1 /\ H2 implies x in H1 & x in H2
proof
assume x in H1 /\ H2;
then x in carr(H1) /\ carr(H2) by Def10;
hence thesis by XBOOLE_0:def 4;
end;
assume x in H1 & x in H2;
then x in carr(H1) /\ carr(H2);
hence thesis by Def10;
end;
theorem
for H being strict Subgroup of G holds H /\ H = H
proof
let H be strict Subgroup of G;
the carrier of H /\ H = carr(H) /\ carr(H) by Def10
.= the carrier of H;
hence thesis by Th59;
end;
definition
let G,H1,H2;
redefine func H1 /\ H2; :: redefines /\ (GROUP_1A, definition)
commutativity
proof let H1,H2;
the carrier of H1 /\ H2 = carr(H2) /\ carr(H1) by Def10
.= the carrier of H2 /\ H1 by Def10;
hence thesis by Th59;
end;
end;
theorem
H1 /\ H2 /\ H3 = H1 /\ (H2 /\ H3)
proof
the carrier of H1 /\ H2 /\ H3 = carr(H1 /\ H2) /\ carr(H3) by Def10
.= carr(H1) /\ carr(H2) /\ carr(H3) by Def10
.= carr(H1) /\ (carr(H2) /\ carr(H3)) by XBOOLE_1:16
.= carr(H1) /\ carr(H2 /\ H3) by Def10
.= the carrier of H1 /\ (H2 /\ H3) by Def10;
hence thesis by Th59;
end;
Lm3: for H1 being Subgroup of G holds H1 is Subgroup of H2 iff the addMagma
of (H1 /\ H2) = the addMagma of H1
proof
let H1 be Subgroup of G;
thus H1 is Subgroup of H2 implies the addMagma of (H1 /\ H2) = the
addMagma of H1
proof
assume H1 is Subgroup of H2;
then
A1: the carrier of H1 c= the carrier of H2 by DefA5;
the carrier of H1 /\ H2 = carr(H1) /\ carr (H2) by Def10;
hence thesis by A1,Th59,XBOOLE_1:28;
end;
assume the addMagma of (H1 /\ H2) = the addMagma of H1;
then the carrier of H1 = carr(H1) /\ carr(H2) by Def10
.= (the carrier of H1) /\ (the carrier of H2);
hence thesis by Th57,XBOOLE_1:17;
end;
theorem
(0).G /\ H = (0).G & H /\ (0).G = (0).G
proof
A1: (0).G is Subgroup of H by Th65;
hence (0).G /\ H = (0).G by Lm3;
thus thesis by A1,Lm3;
end;
theorem
for G being strict addGroup, H being strict Subgroup of G holds H /\
(Omega).G = H & (Omega).G /\ H = H by Lm3;
theorem
for G being strict addGroup holds (Omega).G /\ (Omega).G = G by Lm3;
Lm4: H1 /\ H2 is Subgroup of H1
proof
the carrier of H1 /\ H2 = (the carrier of H1) /\ (the carrier of H2) by Th80;
hence thesis by Th57,XBOOLE_1:17;
end;
theorem
H1 /\ H2 is Subgroup of H1 & H1 /\ H2 is Subgroup of H2 by Lm4;
theorem
for H1 being Subgroup of G holds H1 is Subgroup of H2 iff the
addMagma of (H1 /\ H2) = the addMagma of H1 by Lm3;
theorem
H1 is Subgroup of H2 implies H1 /\ H3 is Subgroup of H2
proof
assume
A1: H1 is Subgroup of H2;
H1 /\ H3 is Subgroup of H1 by Lm4;
hence thesis by A1,Th56;
end;
theorem
H1 is Subgroup of H2 & H1 is Subgroup of H3 implies H1 is Subgroup of
H2 /\ H3
proof
assume
A1: H1 is Subgroup of H2 & H1 is Subgroup of H3;
now
let g;
assume g in H1;
then g in H2 & g in H3 by A1,Th40;
hence g in H2 /\ H3 by Th82;
end;
hence thesis by Th58;
end;
theorem
H1 is Subgroup of H2 implies H1 /\ H3 is Subgroup of H2 /\ H3
proof
assume H1 is Subgroup of H2;
then (the carrier of H1) /\ (the carrier of H3) c= (the carrier of H2) /\ (
the carrier of H3) by DefA5,XBOOLE_1:26;
then
the carrier of H1 /\ H3 c= (the carrier of H2) /\ (the carrier of H3) by Th80
;
then the carrier of H1 /\ H3 c= the carrier of H2 /\ H3 by Th80;
hence thesis by Th57;
end;
theorem
H1 is finite or H2 is finite implies H1 /\ H2 is finite
proof
assume
A1: H1 is finite or H2 is finite;
H1 /\ H2 is Subgroup of H1 & H1 /\ H2 is Subgroup of H2 by Lm4;
hence thesis by A1;
end;
definition
let G,H,A;
func A + H -> Subset of G equals
A + carr H;
correctness;
func H + A -> Subset of G equals
carr H + A;
correctness;
end;
theorem Th94:
x in A + H iff ex g1,g2 st x = g1 + g2 & g1 in A & g2 in H
proof
thus x in A + H implies ex g1,g2 st x = g1 + g2 & g1 in A & g2 in H
proof
assume x in A + H;
then consider g1,g2 such that
A1: x = g1 + g2 & g1 in A and
A2: g2 in carr H;
g2 in H by A2;
hence thesis by A1;
end;
given g1,g2 such that
A3: x = g1 + g2 & g1 in A and
A4: g2 in H;
thus thesis by A3,A4;
end;
theorem ThB95:
x in H + A iff ex g1,g2 st x = g1 + g2 & g1 in H & g2 in A
proof
thus x in H + A implies ex g1,g2 st x = g1 + g2 & g1 in H & g2 in A
proof
assume x in H + A;
then consider g1,g2 such that
A1: x = g1 + g2 and
A2: g1 in carr H and
A3: g2 in A;
g1 in H by A2;
hence thesis by A1,A3;
end;
given g1,g2 such that
A4: x = g1 + g2 and
A5: g1 in H and
A6: g2 in A;
thus thesis by A4,A5,A6;
end;
theorem Th96:
A + B + H = A + (B + H) by Th10;
theorem Th97:
A + H + B = A + (H + B) by Th10;
theorem Th98:
H + A + B = H + (A + B) by Th10;
theorem
A + H1 + H2 = A + (H1 + carr H2) by Th10;
theorem
H1 + A + H2 = H1 + (A + H2) by Th10;
theorem
H1 + carr(H2) + A = H1 + (H2 + A) by Th10;
theorem
G is Abelian addGroup implies A + H = H + A by Th25;
definition
let G,H,a;
func a + H -> Subset of G equals
a + carr(H);
correctness;
func H + a -> Subset of G equals
carr(H) + a;
correctness;
end;
theorem Th103:
x in a + H iff ex g st x = a + g & g in H
proof
thus x in a + H implies ex g st x = a + g & g in H
proof
assume x in a + H;
then consider g such that
A1: x = a + g & g in carr(H) by Th27;
take g;
thus thesis by A1;
end;
given g such that
A2: x = a + g and
A3: g in H;
thus thesis by A2,A3,Th27;
end;
theorem Th104:
x in H + a iff ex g st x = g + a & g in H
proof
thus x in H + a implies ex g st x = g + a & g in H
proof
assume x in H + a;
then consider g such that
A1: x = g + a & g in carr(H) by Th28;
take g;
thus thesis by A1;
end;
given g such that
A2: x = g + a and
A3: g in H;
thus thesis by A2,A3,Th28;
end;
theorem ThB105:
a + b + H = a + (b + H) by Th32;
theorem ThB106:
a + H + b = a + (H + b) by Th10;
theorem ThA107:
H + a + b = H + (a + b) by ThB34;
theorem Th108:
a in a + H & a in H + a
proof
A1: 0_G + a = a by Def4;
0_G in H & a + 0_G = a by Th46,Def4;
hence thesis by A1,Th103,Th104;
end;
theorem ThB109:
0_G + H = carr(H) & H + 0_G = carr(H) by Th37;
theorem Th110:
(0).G + a = {a} & a + (0).G = {a}
proof
A1: the carrier of (0).G = {0_G} by Def7;
hence (0).G + a = {0_G + a} by Th18
.= {a} by Def4;
thus a + (0).G = {a + 0_G} by A1,Th18
.= {a} by Def4;
end;
theorem Th111:
a + (Omega).G = the carrier of G & (Omega).G + a = the carrier of G
proof
[#](the carrier of G) + a = the carrier of G by ThX17;
hence thesis by ThX17;
end;
theorem Th112:
G is Abelian addGroup implies a + H = H + a by Th25;
theorem Th113:
a in H iff a + H = carr(H)
proof
thus a in H implies a + H = carr(H)
proof
assume
A1: a in H;
thus a + H c= carr(H)
proof
let x be object;
assume x in a + H;
then consider g such that
A2: x = a + g and
A3: g in H by Th103;
a + g in H by A1,A3,Th50;
hence thesis by A2;
end;
let x be object;
assume
A4: x in carr(H);
then
A5: x in H;
reconsider b = x as Element of G by A4;
A6: a + (-a + b) = a + -a + b by RLVECT_1:def 3
.= 0_G + b by Def5
.= x by Def4;
-a in H by A1,Th51;
hence thesis by A5,A6,Th50,Th103;
end;
assume
A7: a + H = carr(H);
a + 0_G = a & 0_G in H by Th46,Def4;
hence thesis by A7,Th103;
end;
theorem Th114:
a + H = b + H iff -b + a in H
proof
thus a + H = b + H implies -b + a in H
proof
assume
A1: a + H = b + H;
-b + a + H = -b + (a + H) by Th32
.= -b + b + H by A1,Th32
.= 0_G + H by Def5
.= carr(H) by Th37;
hence thesis by Th113;
end;
assume
A2: -b + a in H;
thus a + H = 0_G + (a + H) by Th37
.= 0_G + a + H by Th32
.= b + -b + a + H by Def5
.= b + (-b + a) + H by RLVECT_1:def 3
.= b + ((-b + a) + H) by Th32
.= b + H by A2,Th113;
end;
theorem Th115:
a + H = b + H iff a + H meets b + H
proof
thus a + H = b + H implies a + H meets b + H by Th108;
assume a + H meets b + H;
then consider x being object such that
A1: x in a + H and
A2: x in b + H by XBOOLE_0:3;
reconsider x as Element of G by A2;
consider g such that
A3: x = a + g and
A4: g in H by A1,Th103;
A5: -g in H by A4,Th51;
consider h being Element of G such that
A6: x = b + h and
A7: h in H by A2,Th103;
a = b + h + -g by A3,A6,Th13
.= b + (h + -g) by RLVECT_1:def 3;
then -b + a = h + -g by Th12;
hence thesis by A5,A7,Th50,Th114;
end;
theorem Th116:
a + b + H c= (a + H) + (b + H)
proof
let x be object;
assume x in a + b + H;
then consider g such that
A1: x = a + b + g and
A2: g in H by Th103;
A3: x = a + 0_G + b + g by A1,Def4
.= (a + 0_G) + (b + g) by RLVECT_1:def 3;
A4: a + 0_G in a + H by Th46,Th103;
b + g in b + H by A2,Th103;
hence thesis by A3,A4;
end;
theorem
carr(H) c= (a + H) + (-a + H) & carr(H) c= (-a + H) + (a + H)
proof
A1: -a + a + H = 0_G + H by Def5
.= carr(H) by Th37;
a + -a + H = 0_G + H by Def5
.= carr(H) by Th37;
hence thesis by A1,Th116;
end;
theorem
2 * a + H c= (a + H) + (a + H)
proof
2 * a + H = a + a + H by Th26;
hence thesis by Th116;
end;
theorem Th119:
a in H iff H + a = carr(H)
proof
thus a in H implies H + a = carr(H)
proof
assume
A1: a in H;
thus H + a c= carr(H)
proof
let x be object;
assume x in H + a;
then consider g such that
A2: x = g + a and
A3: g in H by Th104;
g + a in H by A1,A3,Th50;
hence thesis by A2;
end;
let x be object;
assume
A4: x in carr(H);
then
A5: x in H;
reconsider b = x as Element of G by A4;
A6: (b + -a) + a = b + (-a + a) by RLVECT_1:def 3
.= b + 0_G by Def5
.= x by Def4;
-a in H by A1,Th51;
hence thesis by A5,A6,Th50,Th104;
end;
assume
A7: H + a = carr(H);
0_G + a = a & 0_G in H by Th46,Def4;
hence thesis by A7,Th104;
end;
theorem Th120:
H + a = H + b iff b + -a in H
proof
thus H + a = H + b implies b + -a in H
proof
assume
A1: H + a = H + b;
carr(H) = H + 0_G by Th37
.= H + (a + -a) by Def5
.= H + b + -a by A1,ThB34
.= H + (b + -a) by ThB34;
hence thesis by Th119;
end;
assume b + -a in H;
hence H + a = H + (b + -a) + a by Th119
.= H + (b + -a + a) by ThB34
.= H + (b + (-a + a)) by RLVECT_1:def 3
.= H + (b + (0_G)) by Def5
.= H + b by Def4;
end;
theorem Th121:
H + a = H + b iff H + a meets H + b
proof
thus H + a = H + b implies H + a meets H + b by Th108;
assume H + a meets H + b;
then consider x being object such that
A1: x in H + a and
A2: x in H + b by XBOOLE_0:3;
reconsider x as Element of G by A2;
consider g such that
A3: x = g + a and
A4: g in H by A1,Th104;
A5: -g in H by A4,Th51;
consider h being Element of G such that
A6: x = h + b and
A7: h in H by A2,Th104;
a = -g + (h + b) by A3,A6,Th12
.= -g + h + b by RLVECT_1:def 3;
then a + -b = -g + h by Th13;
hence thesis by A5,A7,Th50,Th120;
end;
theorem Th122:
H + a + b c= (H + a) + (H + b)
proof
let x be object;
A1: 0_G + b in H + b by Th46,Th104;
assume x in H + a + b;
then x in H + (a + b) by ThB34;
then consider g such that
A2: x = g + (a + b) and
A3: g in H by Th104;
A4: x = g + a + b by A2,RLVECT_1:def 3
.= g + a + (0_G + b) by Def4;
g + a in H + a by A3,Th104;
hence thesis by A1,A4;
end;
theorem
carr(H) c= (H + a) + (H + -a) & carr(H) c= (H + -a) + (H + a)
proof
A1: H + -a+ a = H + (-a+ a) by ThB34
.= H + 0_G by Def5
.= carr(H) by Th37;
H + a + -a = H + (a + -a) by ThB34
.= H + 0_G by Def5
.= carr(H) by Th37;
hence thesis by A1,Th122;
end;
theorem
H + (2 * a) c= (H + a) + (H + a)
proof
2 * a = a + a & H + a + a = H + (a + a) by ThB34,Th26;
hence thesis by Th122;
end;
theorem
a + (H1 /\ H2) = (a + H1) /\ (a + H2)
proof
thus a + (H1 /\ H2) c= (a + H1) /\ (a + H2)
proof
let x be object;
assume x in a + (H1 /\ H2);
then consider g such that
A1: x = a + g and
A2: g in H1 /\ H2 by Th103;
g in H2 by A2,Th82;
then
A3: x in a + H2 by A1,Th103;
g in H1 by A2,Th82;
then x in a + H1 by A1,Th103;
hence thesis by A3;
end;
let x be object;
assume
A4: x in (a + H1) /\ (a + H2);
then x in a + H1 by XBOOLE_0:def 4;
then consider g such that
A5: x = a + g and
A6: g in H1 by Th103;
x in a + H2 by A4,XBOOLE_0:def 4;
then consider g1 such that
A7: x = a + g1 and
A8: g1 in H2 by Th103;
g = g1 by A5,A7,Th6;
hence thesis by A5,A6,A8,Th82,Th103;
end;
theorem
(H1 /\ H2) + a = (H1 + a) /\ (H2 + a)
proof
thus (H1 /\ H2) + a c= (H1 + a) /\ (H2 + a)
proof
let x be object;
assume x in (H1 /\ H2) + a;
then consider g such that
A1: x = g + a and
A2: g in H1 /\ H2 by Th104;
g in H2 by A2,Th82;
then
A3: x in H2 + a by A1,Th104;
g in H1 by A2,Th82;
then x in H1 + a by A1,Th104;
hence thesis by A3;
end;
let x be object;
assume
A4: x in (H1 + a) /\ (H2 + a);
then x in H1 + a by XBOOLE_0:def 4;
then consider g such that
A5: x = g + a and
A6: g in H1 by Th104;
x in H2 + a by A4,XBOOLE_0:def 4;
then consider g1 such that
A7: x = g1 + a and
A8: g1 in H2 by Th104;
g = g1 by A5,A7,Th6;
hence thesis by A5,A6,A8,Th82,Th104;
end;
theorem Th127:
ex H1 being strict Subgroup of G st the carrier of H1 = a + H2 + -a
proof
set A = a + H2 + -a;
set x = the Element of a + H2;
A1: a + H2 <> {} by Th108;
then reconsider x as Element of G by Lm1;
A2: now
let g;
assume g in A;
then consider g1 such that
A3: g = g1 + -a and
A4: g1 in a + H2 by Th28;
consider g2 such that
A5: g1 = a + g2 and
A6: g2 in H2 by A4,Th103;
A7: -g2 + -a in H2 + -a by A6,Th51,Th104;
-g = -(g1 + -a) by A3
.= --a + -(a + g2) by A5,Th16
.= a + (-g2 + -a) by Th16;
then -g in a + (H2 + -a) by A7,Th27;
hence -g in A by Th10;
end;
A8: now
let g1,g2;
assume that
A9: g1 in A and
A10: g2 in A;
consider g such that
A11: g1 = g + -a and
A12: g in a + H2 by A9,Th28;
consider h being Element of G such that
A13: g = a + h and
A14: h in H2 by A12,Th103;
A = a + (H2 + -a) by Th10;
then consider b such that
A15: g2 = a + b and
A16: b in H2 + -a by A10,Th27;
consider c being Element of G such that
A17: b = c + -a and
A18: c in H2 by A16,Th104;
A19: a + (h + c) in a + H2 by A14,A18,Th50,Th103;
g1 + g2 = (a + h) + (-a + (a + (c + -a))) by A11,A15,A13,A17,RLVECT_1:def 3
.= (a + h) + (-a + a + (c + -a)) by RLVECT_1:def 3
.= (a + h) + (0_G + (c + -a)) by Def5
.= (a + h) + (c + -a) by Def4
.= a + h + c + -a by RLVECT_1:def 3
.= a + (h + c) + -a by RLVECT_1:def 3;
hence g1 + g2 in A by A19,Th28;
end;
x + -a in A by A1,Th28;
hence thesis by A8,A2,Th52;
end;
theorem Th128:
a + H,b + H are_equipotent
proof
defpred P[object,object] means ex g1 st $1 = g1 & $2 = b + -a + g1;
A1: for x being object st x in a + H ex y being object st P[x,y]
proof
let x be object;
assume x in a + H;
then reconsider g = x as Element of G;
reconsider y = b + -a + g as set;
take y;
take g;
thus thesis;
end;
consider f being Function such that
A2: dom f = a + H and
A3: for x being object st x in a + H holds P[x,f.x] from CLASSES1:sch 1(A1);
A4: rng f = b + H
proof
thus rng f c= b + H
proof
let x be object;
assume x in rng f;
then consider y being object such that
A5: y in dom f and
A6: f.y = x by FUNCT_1:def 3;
consider g such that
A7: y = g and
A8: x = b + -a + g by A2,A3,A5,A6;
consider g1 such that
A9: g = a + g1 and
A10: g1 in H by A2,A5,A7,Th103;
x = b + -a + a + g1 by A8,A9,RLVECT_1:def 3
.= b + (-a + a) + g1 by RLVECT_1:def 3
.= b + 0_G + g1 by Def5
.= b + g1 by Def4;
hence thesis by A10,Th103;
end;
let x be object;
assume x in b + H;
then consider g such that
A11: x = b + g and
A12: g in H by Th103;
A13: a + g in dom f by A2,A12,Th103;
ex g1 st g1 = a + g & f.(a + g) = b + -a + g1 by A3,A12,Th103;
then f.(a + g) = b + -a + a + g by RLVECT_1:def 3
.= b + (-a + a) + g by RLVECT_1:def 3
.= b + 0_G + g by Def5
.= x by A11,Def4;
hence thesis by A13,FUNCT_1:def 3;
end;
f is one-to-one
proof
let x,y be object;
assume that
A14: x in dom f & y in dom f and
A15: f.x = f.y;
( ex g1 st x = g1 & f.x = b + -a + g1)& ex g2 st y = g2 & f.y = b + -a
+ g2 by A2,A3,A14;
hence thesis by A15,Th6;
end;
hence thesis by A2,A4,WELLORD2:def 4;
end;
theorem Th129:
a + H,H + b are_equipotent
proof
defpred P[object,object] means ex g1 st $1 = g1 & $2 = -a + g1 + b;
A1: for x being object st x in a + H ex y being object st P[x,y]
proof
let x be object;
assume x in a + H;
then reconsider g = x as Element of G;
reconsider y = -a + g + b as set;
take y;
take g;
thus thesis;
end;
consider f being Function such that
A2: dom f = a + H and
A3: for x being object st x in a + H holds P[x,f.x] from CLASSES1:sch 1(A1);
A4: rng f = H + b
proof
thus rng f c= H + b
proof
let x be object;
assume x in rng f;
then consider y being object such that
A5: y in dom f and
A6: f.y = x by FUNCT_1:def 3;
consider g such that
A7: y = g and
A8: x = -a + g + b by A2,A3,A5,A6;
consider g1 such that
A9: g = a + g1 and
A10: g1 in H by A2,A5,A7,Th103;
x = -a + a + g1 + b by A8,A9,RLVECT_1:def 3
.= 0_G + g1 + b by Def5
.= g1 + b by Def4;
hence thesis by A10,Th104;
end;
let x be object;
assume x in H + b;
then consider g such that
A11: x = g + b and
A12: g in H by Th104;
A13: a + g in dom f by A2,A12,Th103;
ex g1 st g1 = a + g & f.(a + g) = -a + g1 + b by A3,A12,Th103;
then f.(a + g) = -a + a + g + b by RLVECT_1:def 3
.= 0_G + g + b by Def5
.= x by A11,Def4;
hence thesis by A13,FUNCT_1:def 3;
end;
f is one-to-one
proof
let x,y be object;
assume that
A14: x in dom f and
A15: y in dom f and
A16: f.x = f.y;
consider g2 such that
A17: y = g2 and
A18: f.y = -a + g2 + b by A2,A3,A15;
consider g1 such that
A19: x = g1 and
A20: f.x = -a + g1 + b by A2,A3,A14;
-a + g1 = -a + g2 by A16,A20,A18,Th6;
hence thesis by A19,A17,Th6;
end;
hence thesis by A2,A4,WELLORD2:def 4;
end;
theorem Th130:
H + a,H + b are_equipotent
proof
H + a,b + H are_equipotent & b + H,H + b are_equipotent by Th129;
hence thesis by WELLORD2:15;
end;
theorem Th131:
carr(H),a + H are_equipotent & carr(H),H + a are_equipotent
proof
carr(H) = 0_G + H & carr(H) = H + 0_G by Th37;
hence thesis by Th128,Th130;
end;
theorem
card(H) = card(a + H) & card(H) = card(H + a)
by Th131,CARD_1:5;
theorem Th133:
for H being finite Subgroup of G ex B,C being finite set st B =
a + H & C = H + a & card H = card B & card H = card C
proof
let H be finite Subgroup of G;
reconsider B = a + H, C = H + a as finite set by Th131,CARD_1:38;
take B,C;
thus thesis by Th131,CARD_1:5;
end;
definition
let G,H;
func Left_Cosets H -> Subset-Family of G means
:Def15:
A in it iff ex a st A = a + H;
existence
proof
defpred P[set] means ex a st $1 = a + H;
ex F be Subset-Family of G st for A being Subset of G holds A in F iff
P[A] from SUBSET_1:sch 3;
hence thesis;
end;
uniqueness
proof
defpred P[set] means ex a st $1 = a + H;
let F1,F2 be Subset-Family of G;
assume
A1: for A holds A in F1 iff P[A];
assume
A2: for A holds A in F2 iff P[A];
thus thesis from SUBSET_1:sch 4(A1,A2);
end;
func Right_Cosets H -> Subset-Family of G means
:Def16:
A in it iff ex a st A = H + a;
existence
proof
defpred P[set] means ex a st $1 = H + a;
ex F be Subset-Family of G st for A being Subset of G holds A in F iff
P[A] from SUBSET_1:sch 3;
hence thesis;
end;
uniqueness
proof
defpred P[set] means ex a st $1 = H + a;
let F1,F2 be Subset-Family of G;
assume
A3: for A holds A in F1 iff P[A];
assume
A4: for A holds A in F2 iff P[A];
thus thesis from SUBSET_1:sch 4(A3,A4);
end;
end;
theorem
G is finite implies Right_Cosets H is finite & Left_Cosets H is finite;
theorem Th135:
carr H in Left_Cosets H & carr H in Right_Cosets H
proof
carr H = 0_G + H & carr H = H + 0_G by Th37;
hence thesis by Def15,Def16;
end;
theorem Th136:
Left_Cosets H, Right_Cosets H are_equipotent
proof
defpred P[object,object] means ex g st $1 = g + H & $2 = H + -g;
A1: for x being object st x in Left_Cosets H ex y being object st P[x,y]
proof
let x be object;
assume x in Left_Cosets H;
then consider g such that
A2: x = g + H by Def15;
reconsider y = H + -g as set;
take y;
take g;
thus thesis by A2;
end;
consider f being Function such that
A3: dom f = Left_Cosets H and
A4: for x being object st x in Left_Cosets H holds P[x,f.x]
from CLASSES1:sch 1(A1);
A5: rng f = Right_Cosets H
proof
thus rng f c= Right_Cosets H
proof
let x be object;
assume x in rng f;
then consider y being object such that
A6: y in dom f and
A7: f.y = x by FUNCT_1:def 3;
ex g st y = g + H & f.y = H + -g by A3,A4,A6;
hence thesis by A7,Def16;
end;
let x be object;
assume
A8: x in Right_Cosets H;
then reconsider A = x as Subset of G;
consider g such that
A9: A = H + g by A8,Def16;
A10: -g + H in Left_Cosets H by Def15;
then
A11: f.(-g + H) in rng f by A3,FUNCT_1:def 3;
consider a such that
A12: -g + H = a + H and
A13: f.(-g + H) = H + -a by A4,A10;
-a + -g in H by A12,Th114;
hence thesis by A9,A11,A13,Th120;
end;
f is one-to-one
proof
let x,y be object;
assume that
A14: x in dom f and
A15: y in dom f and
A16: f.x = f.y;
consider b such that
A17: y = b + H and
A18: f.y = H + -b by A3,A4,A15;
consider a such that
A19: x = a + H and
A20: f.x = H + -a by A3,A4,A14;
-b + --a in H by A16,A20,A18,Th120;
hence thesis by A19,A17,Th114;
end;
hence thesis by A3,A5,WELLORD2:def 4;
end;
theorem Th137:
union Left_Cosets H = the carrier of G & union Right_Cosets H =
the carrier of G
proof
thus union Left_Cosets H = the carrier of G
proof
set h = the Element of H;
reconsider g = h as Element of G by Th41,STRUCT_0:def 5;
thus union Left_Cosets H c= the carrier of G;
let x be object;
assume x in the carrier of G;
then reconsider a = x as Element of G;
A1: a = a + 0_G by Def4
.= a + (-g + g) by Def5
.= a + -g + g by RLVECT_1:def 3;
A2: a + -g + H in Left_Cosets H by Def15;
h in H;
then a in a + -g + H by A1,Th103;
hence thesis by A2,TARSKI:def 4;
end;
set h = the Element of H;
reconsider g = h as Element of G by Th41,STRUCT_0:def 5;
thus union Right_Cosets H c= the carrier of G;
let x be object;
assume x in the carrier of G;
then reconsider a = x as Element of G;
A3: a = 0_G + a by Def4
.= g + -g + a by Def5
.= g + (-g + a) by RLVECT_1:def 3;
A4: H + (-g + a) in Right_Cosets H by Def16;
h in H;
then a in H + (-g + a) by A3,Th104;
hence thesis by A4,TARSKI:def 4;
end;
theorem Th138:
Left_Cosets (0).G = the set of all {a}
proof
set A = the set of all {a} ;
thus Left_Cosets (0).G c= A
proof
let x be object;
assume
A1: x in Left_Cosets (0).G;
then reconsider X = x as Subset of G;
consider g such that
A2: X = g + (0).G by A1,Def15;
x = {g} by A2,Th110;
hence thesis;
end;
let x be object;
assume x in A;
then consider a such that
A3: x = {a};
a + (0).G = {a} by Th110;
hence thesis by A3,Def15;
end;
theorem
Right_Cosets (0).G = the set of all {a}
proof
set A = the set of all {a} ;
thus Right_Cosets (0).G c= A
proof
let x be object;
assume
A1: x in Right_Cosets (0).G;
then reconsider X = x as Subset of G;
consider g such that
A2: X = (0).G + g by A1,Def16;
x = {g} by A2,Th110;
hence thesis;
end;
let x be object;
assume x in A;
then consider a such that
A3: x = {a};
(0).G + a = {a} by Th110;
hence thesis by A3,Def16;
end;
theorem
for H being strict Subgroup of G holds Left_Cosets H = the set of all {a}
implies H = (0).G
proof
let H be strict Subgroup of G;
assume
A1: Left_Cosets H = the set of all {a} ;
A2: the carrier of H c= {0_G}
proof
set a = the Element of G;
let x be object;
assume x in the carrier of H;
then reconsider h = x as Element of H;
A3: h in H;
reconsider h as Element of G by Th41,STRUCT_0:def 5;
a + H in Left_Cosets H by Def15;
then consider b such that
A4: a + H = {b} by A1;
a + h in a + H by A3,Th103;
then
A5: a + h = b by A4,TARSKI:def 1;
a + 0_G in a + H by Th46,Th103;
then a + 0_G = b by A4,TARSKI:def 1;
then h = 0_G by A5,Th6;
hence thesis by TARSKI:def 1;
end;
0_G in H by Th46;
then {0_G} = the carrier of H by A2,ZFMISC_1:31;
hence thesis by Def7;
end;
theorem
for H being strict Subgroup of G holds Right_Cosets H = the set of all {a}
implies H = (0).G
proof
let H be strict Subgroup of G;
assume
A1: Right_Cosets H = the set of all {a} ;
A2: the carrier of H c= {0_G}
proof
set a = the Element of G;
let x be object;
assume x in the carrier of H;
then reconsider h = x as Element of H;
A3: h in H;
reconsider h as Element of G by Th41,STRUCT_0:def 5;
H + a in Right_Cosets H by Def16;
then consider b such that
A4: H + a = {b} by A1;
h + a in H + a by A3,Th104;
then
A5: h + a = b by A4,TARSKI:def 1;
0_G + a in H + a by Th46,Th104;
then 0_G + a = b by A4,TARSKI:def 1;
then h = 0_G by A5,Th6;
hence thesis by TARSKI:def 1;
end;
0_G in H by Th46;
then {0_G} = the carrier of H by A2,ZFMISC_1:31;
hence thesis by Def7;
end;
theorem Th142:
Left_Cosets (Omega).G = {the carrier of G} & Right_Cosets
(Omega).G = {the carrier of G}
proof
set a = the Element of G;
A1: Left_Cosets (Omega).G c= {the carrier of G}
proof
let x be object;
assume
A2: x in Left_Cosets (Omega).G;
then reconsider X = x as Subset of G;
consider a such that
A3: X = a + (Omega).G by A2,Def15;
a + (Omega).G = the carrier of G by Th111;
hence thesis by A3,TARSKI:def 1;
end;
A4: Right_Cosets (Omega).G c= {the carrier of G}
proof
let x be object;
assume
A5: x in Right_Cosets (Omega).G;
then reconsider X = x as Subset of G;
consider a such that
A6: X = (Omega).G + a by A5,Def16;
(Omega).G + a = the carrier of G by Th111;
hence thesis by A6,TARSKI:def 1;
end;
(Omega). G + a = the carrier of G by Th111;
then
A7: the carrier of G in Right_Cosets(Omega).G by Def16;
a + (Omega).G = the carrier of G by Th111;
then the carrier of G in Left_Cosets (Omega).G by Def15;
hence thesis by A7,ZFMISC_1:31,A1,A4;
end;
theorem Th143:
for G being strict addGroup, H being strict Subgroup of G holds
Left_Cosets H = {the carrier of G} implies H = G
proof
let G be strict addGroup, H be strict Subgroup of G;
assume Left_Cosets H = {the carrier of G};
then
A1: the carrier of G in Left_Cosets H by TARSKI:def 1;
then reconsider T = the carrier of G as Subset of G;
consider a being Element of G such that
A2: T = a + H by A1,Def15;
now
let g be Element of G;
ex b being Element of G st a + g = a + b & b in H by A2,Th103;
hence g in H by Th6;
end;
hence thesis by Th62;
end;
theorem
for G being strict addGroup, H being strict Subgroup of G holds
Right_Cosets H = {the carrier of G} implies H = G
proof
let G be strict addGroup, H be strict Subgroup of G;
assume Right_Cosets H = {the carrier of G};
then
A1: the carrier of G in Right_Cosets H by TARSKI:def 1;
then reconsider T = the carrier of G as Subset of G;
consider a being Element of G such that
A2: T = H + a by A1,Def16;
now
let g be Element of G;
ex b being Element of G st g + a = b + a & b in H by A2,Th104;
hence g in H by Th6;
end;
hence thesis by Th62;
end;
definition
let G,H;
func Index H -> Cardinal equals
card Left_Cosets H;
correctness;
end;
theorem Th145:
Index H = card Left_Cosets H & Index H = card Right_Cosets H
by Th136,CARD_1:5;
definition
let G,H;
assume
A1: Left_Cosets(H) is finite;
func index H -> Element of NAT means
:Def18:
ex B being finite set st B = Left_Cosets H & it = card B;
existence
proof
reconsider B = Left_Cosets(H) as finite set by A1;
take card B, B;
thus thesis;
end;
uniqueness;
end;
theorem Th146:
Left_Cosets H is finite implies (ex B being finite set st B =
Left_Cosets H & index H = card B) & ex C being finite set st C = Right_Cosets H
& index H = card C
proof
assume Left_Cosets H is finite;
then reconsider B = Left_Cosets H as finite set;
hereby
take B;
thus B = Left_Cosets H & index H = card B by Def18;
end;
then reconsider C = Right_Cosets H as finite set by Th136,CARD_1:38;
take C;
index H = card B & B, C are_equipotent by Def18,Th136;
hence thesis by CARD_1:5;
end;
::$N Lagrange theorem for addGroups
theorem Th147:
for G being finite addGroup, H being Subgroup of G holds card G =
card H * index H
proof
let G be finite addGroup, H be Subgroup of G;
reconsider C = Left_Cosets H as finite set;
now
let X be set;
assume
A1: X in C;
then reconsider x = X as Subset of G;
x is finite;
then reconsider B = X as finite set;
take B;
thus B = X;
consider a being Element of G such that
A2: x = a + H by A1,Def15;
ex B,C being finite set st B = a + H & C = H + a & card H = card B &
card H = card C by Th133;
hence card B = card H by A2;
let Y;
assume that
A3: Y in C and
A4: X <> Y;
reconsider y = Y as Subset of G by A3;
A5: ex b being Element of G st y = b + H by A3,Def15;
hence X,Y are_equipotent by A2,Th128;
thus X misses Y by A2,A4,A5,Th115;
end;
then
A6: ex D being finite set st D = union C & card D = card H * card C
by GROUP_2:156;
union Left_Cosets H = the carrier of G by Th137;
hence thesis by A6,Def18;
end;
theorem
for G being finite addGroup, H being Subgroup of G holds
card H divides card G
proof
let G be finite addGroup, H being Subgroup of G;
card G = card H * index H by Th147;
hence thesis by NAT_D:def 3;
end;
theorem
for G being finite addGroup, I, H being Subgroup of G, J being Subgroup
of H holds I = J implies index I = index J * index H
proof
let G be finite addGroup, I, H be Subgroup of G, J be Subgroup of H;
assume
A1: I = J;
card G = card H * index H & card H = card J * index J by Th147;
then card I * (index J * index H) = card I * index I by A1,Th147;
hence thesis by XCMPLX_1:5;
end;
theorem
index (Omega).G = 1
proof
Left_Cosets (Omega).G = {the carrier of G} by Th142;
hence index (Omega).G = card{the carrier of G} by Def18
.= 1 by CARD_1:30;
end;
theorem
for G being strict addGroup, H being strict Subgroup of G holds
Left_Cosets H is finite & index H = 1 implies H = G
proof
let G be strict addGroup, H be strict Subgroup of G;
assume that
A1: Left_Cosets H is finite and
A2: index H = 1;
reconsider B = Left_Cosets H as finite set by A1;
card B = 1 by A2,Def18;
then consider x being object such that
A3: Left_Cosets H = {x} by CARD_2:42;
union {x} = x & union Left_Cosets H = the carrier of G by Th137,ZFMISC_1:25;
hence thesis by A3,Th143;
end;
theorem
Index (0).G = card G
proof
deffunc F(object) = {$1};
consider f being Function such that
A1: dom f = the carrier of G and
A2: for x being object st x in the carrier of G holds f.x = F(x)
from FUNCT_1:sch 3;
A3: rng f = Left_Cosets (0).G
proof
thus rng f c= Left_Cosets (0).G
proof
let x be object;
assume x in rng f;
then consider y being object such that
A4: y in dom f and
A5: f.y = x by FUNCT_1:def 3;
reconsider y as Element of G by A1,A4;
x = {y} by A2,A5;
then x in the set of all {a} ;
hence thesis by Th138;
end;
let x be object;
assume x in Left_Cosets (0).G;
then x in the set of all {a} by Th138;
then consider a such that
A6: x = {a};
f.a = {a} by A2;
hence thesis by A1,A6,FUNCT_1:def 3;
end;
f is one-to-one
proof
let x,y be object;
assume that
A7: x in dom f & y in dom f and
A8: f.x = f.y;
f.y = {y} & f.x = {x} by A1,A2,A7;
hence thesis by A8,ZFMISC_1:3;
end;
hence thesis by A1,A3,WELLORD2:def 4,CARD_1:5;
end;
theorem
for G being finite addGroup holds index (0).G = card G
proof
let G be finite addGroup;
thus card G = card (0).G * index (0).G by Th147
.= 1 * index (0).G by Th69
.= index (0).G;
end;
theorem Th154:
for G being finite addGroup, H being strict Subgroup of G holds
index H = card G implies H = (0).G
proof
let G be finite addGroup, H be strict Subgroup of G;
assume index H = card G;
then 1 * card G = card H * card G by Th147;
hence thesis by Th70,XCMPLX_1:5;
end;
theorem
for H being strict Subgroup of G holds Left_Cosets H is finite & Index
H = card G implies G is finite & H = (0).G
proof
let H be strict Subgroup of G;
assume that
A1: Left_Cosets H is finite and
A2: Index H = card G;
thus
A3: G is finite by A1,A2;
ex B being finite set st B = Left_Cosets H & index H = card B by A1,Def18;
hence thesis by A2,A3,Th154;
end;
begin ::: GROUP_3B
reserve x,y,y1,y2 for set;
reserve G for addGroup;
reserve a,b,c,d,g,h for Element of G;
reserve A,B,C,D for Subset of G;
reserve H,H1,H2,H3 for Subgroup of G;
reserve n for Nat;
reserve i for Integer;
theorem Th1:
a + b + (-b) = a & a + (-b) + b = a & (-b) + b + a = a & b + (-b) + a = a
& a + (b + (-b)) = a & a + ((-b) + b) = a & (-b) + (b + a) = a &
b + ((-b) + a) = a
proof
thus
A1: a + b + (-b) = a + (b + (-b)) by RLVECT_1:def 3
.= a + 0_G by Def5
.= a by Def4;
thus
A2: a + (-b) + b = a + ((-b) + b) by RLVECT_1:def 3
.= a + 0_G by Def5
.= a by Def4;
thus
A3: (-b) + b + a = 0_G + a by Def5
.= a by Def4;
thus b + (-b) + a = 0_G + a by Def5
.= a by Def4;
hence thesis by A1,A2,A3,RLVECT_1:def 3;
end;
Lm1: for A be Abelian addGroup, a, b be Element of A holds a + b = b + a;
theorem
G is Abelian addGroup iff the addF of G is commutative
proof
thus G is Abelian addGroup implies the addF of G is commutative
proof
assume
A1: G is Abelian addGroup;
let a,b;
thus (the addF of G).(a,b) = a + b .= b + a by A1,Lm1
.= (the addF of G).(b,a);
end;
assume
A2: the addF of G is commutative;
G is Abelian by A2;
hence thesis;
end;
theorem
(0).G is Abelian
proof
let a,b be Element of (0).G;
a in the carrier of (0).G;
then a in {0_G} by Def7;
then
A1: a = 0_G by TARSKI:def 1;
b in the carrier of (0).G;
then b in {0_G} by Def7;
hence thesis by A1,TARSKI:def 1;
end;
theorem Th4:
A c= B & C c= D implies A + C c= B + D
proof
assume
A1: A c= B & C c= D;
let x be object;
assume x in A + C;
then ex a,c st x = a + c & a in A & c in C;
hence thesis by A1;
end;
theorem
A c= B implies a + A c= a + B & A + a c= B + a by Th4;
theorem ThB6:
H1 is Subgroup of H2 implies a + H1 c= a + H2 & H1 + a c= H2 + a
proof
assume H1 is Subgroup of H2;
then the carrier of H1 c= the carrier of H2 by DefA5;
hence thesis by Th4;
end;
theorem
a + H = {a} + H;
theorem
H + a = H + {a};
theorem Th9:
A + a + H = A + (a + H)
proof
thus A + a + H = A + ({a} + H) by Th96
.= A + (a + H);
end;
theorem
a + H + A = a + (H + A)
proof
thus a + H + A = {a} + H + A .= a + (H + A) by Th97;
end;
theorem
A + H + a = A + (H + a)
proof
thus A + H + a = A + (H + {a}) by Th97
.= A + (H + a);
end;
theorem
H + a + A = H + (a + A)
proof
thus H + a + A = H + {a} + A .= H + (a + A) by Th98;
end;
theorem
H1 + a + H2 = H1 + (a + H2) by Th9;
definition
let G;
func Subgroups G -> set means
:Def1:
for x being object holds x in it iff x is strict Subgroup of G;
existence
proof
defpred P[object,object] means
ex H being strict Subgroup of G st $2 = H & $1 = the carrier of H;
defpred P[set] means ex H being strict Subgroup of G st $1 = the carrier
of H;
consider B being set such that
A1: for x holds x in B iff x in bool the carrier of G & P[x] from
XFAMILY:sch 1;
A2: for x,y1,y2 being object st P[x,y1] & P[x,y2] holds y1 = y2 by Th59;
consider f being Function such that
A3: for x,y being object holds [x,y] in f iff x in B & P[x,y]
from FUNCT_1:sch 1(A2);
for x being object holds x in B iff ex y being object st [x,y] in f
proof
let x be object;
thus x in B implies ex y being object st [x,y] in f
proof
assume
A4: x in B;
then consider H being strict Subgroup of G such that
A5: x = the carrier of H by A1;
take H;
thus thesis by A3,A4,A5;
end;
thus thesis by A3;
end;
then
A6: B = dom f by XTUPLE_0:def 12;
for y being object holds y in rng f iff y is strict Subgroup of G
proof
let y be object;
thus y in rng f implies y is strict Subgroup of G
proof
assume y in rng f;
then consider x being object such that
A7: x in dom f & y = f.x by FUNCT_1:def 3;
[x,y] in f by A7,FUNCT_1:def 2;
then ex H being strict Subgroup of G st y = H & x = the carrier of H
by A3;
hence thesis;
end;
assume y is strict Subgroup of G;
then reconsider H = y as strict Subgroup of G;
A8: y is set by TARSKI:1;
reconsider x = the carrier of H as set;
A8a: the carrier of H c= the carrier of G by DefA5;
then
A9: x in dom f by A1,A6;
[x,y] in f by A1,A3,A8a;
then y = f.x by A9,FUNCT_1:def 2,A8;
hence thesis by A9,FUNCT_1:def 3;
end;
hence thesis;
end;
uniqueness
proof
defpred P[object] means $1 is strict Subgroup of G;
let A1,A2 be set;
assume
A10: for x being object holds x in A1 iff P[x];
assume
A11: for x being object holds x in A2 iff P[x];
thus thesis from XBOOLE_0:sch 2(A10,A11);
end;
end;
registration
let G;
cluster Subgroups G -> non empty;
coherence
proof
set x = the strict Subgroup of G;
x in Subgroups G by Def1;
hence thesis;
end;
end;
theorem
for G being strict addGroup holds G in Subgroups G
proof
let G be strict addGroup;
G is Subgroup of G by ThA54;
hence thesis by Def1;
end;
theorem Th15:
G is finite implies Subgroups G is finite
proof
defpred P[object,object] means
ex H being strict Subgroup of G st $1 = H & $2 =
the carrier of H;
assume
A1: G is finite;
A2: for x being object st x in Subgroups G ex y being object st P[x,y]
proof
let x be object;
assume x in Subgroups G;
then reconsider F = x as strict Subgroup of G by Def1;
reconsider y = the carrier of F as set;
take y;
take F;
thus thesis;
end;
consider f being Function such that
A3: dom f = Subgroups G and
A4: for x being object st x in Subgroups G holds P[x,f.x]
from CLASSES1:sch 1(A2);
A5: rng f c= bool the carrier of G
proof
let x be object;
assume x in rng f;
then consider y being object such that
A6: y in dom f & f.y = x by FUNCT_1:def 3;
consider H being strict Subgroup of G such that
y = H and
A7: x = the carrier of H by A3,A4,A6;
the carrier of H c= the carrier of G by DefA5;
hence thesis by A7;
end;
f is one-to-one
proof
let x,y be object;
assume that
A8: x in dom f & y in dom f and
A9: f.x = f.y;
( ex H1 being strict Subgroup of G st x = H1 & f.x = the carrier of
H1)& ex H2 being strict Subgroup of G st y = H2 & f.y = the carrier of H2 by A3
,A4,A8;
hence thesis by A9,Th59;
end;
then card Subgroups G c= card bool the carrier of G by A3,A5,CARD_1:10;
hence thesis by A1;
end;
definition
let G,a,b;
func a * b -> Element of G equals
(-b) + a + b;
correctness;
end;
theorem ThB16:
a * g = b * g implies a = b
proof
assume a * g = b * g;
then (-g) + a = (-g) + b by Th6;
hence thesis by Th6;
end;
theorem Th17:
(0_G) * a = 0_G
proof
thus (0_G) * a = (-a) + a by Def4
.= 0_G by Def5;
end;
theorem ThB18:
a * b = 0_G implies a = 0_G
proof
assume a * b = 0_G;
then (-b) = (-b) + a by Th11;
hence thesis by Th7;
end;
theorem Th19:
a * 0_G = a
proof
thus a * 0_G = -(0_G) + a by Def4
.= 0_G + a by Th8
.= a by Def4;
end;
theorem Th20:
a * a = a
proof
thus a * a = 0_G + a by Def5
.= a by Def4;
end;
theorem
a * (-a) = a & (-a) * a = (-a) by Th1;
theorem Th22:
a * b = a iff a + b = b + a
proof
thus a * b = a implies a + b = b + a
proof
assume a * b = a;
then a = (-b) + (a + b) by RLVECT_1:def 3;
hence thesis by Th12;
end;
assume a + b = b + a;
then a = (-b) + (a + b) by Th12;
hence thesis by RLVECT_1:def 3;
end;
theorem Th23:
(a + b) * g = a * g + (b * g)
proof
thus (a + b) * g = (-g) + (a + 0_G + b) + g by Def4
.= (-g) + (a + (g + (-g)) + b) + g by Def5
.= (-g) + (a + g + (-g) + b) + g by RLVECT_1:def 3
.= (-g) + (a + g + ((-g) + b)) + g by RLVECT_1:def 3
.= (-g) + (a + g) + ((-g) + b) + g by RLVECT_1:def 3
.= a * g + ((-g) + b) + g by RLVECT_1:def 3
.= a * g + (b * g) by RLVECT_1:def 3;
end;
theorem Th24:
a * g * h = a * (g + h)
proof
thus a * g * h = (-h) + ((-g) + a) + g + h by RLVECT_1:def 3
.= (-h) + (-g) + a + g + h by RLVECT_1:def 3
.= -(g + h) + a + g + h by Th16
.= a * (g + h) by RLVECT_1:def 3;
end;
theorem ThB25:
a * b * (-b) = a & a * (-b) * b = a
proof
thus a * b * (-b) = a * (b + (-b)) by Th24
.= a * 0_G by Def5
.= a by Th19;
thus a * (-b) * b = a * ((-b) + b) by Th24
.= a * 0_G by Def5
.= a by Th19;
end;
theorem Th26:
(-a) * b = -(a * b)
proof
thus (-a) * b = -(a + b) + -(-b) by Th16
.= -((-b) + (a + b)) by Th16
.= -(a * b) by RLVECT_1:def 3;
end;
Lm2: now
let G,a,b;
thus (0 * a) * b = (0_G) * b by ThA24
.= 0_G by Th17
.= 0 * (a * b) by ThA24;
end;
Lm3: now
let n;
assume
A1: for G,a,b holds (n * a) * b = n * (a * b);
let G,a,b;
thus ((n + 1) * a) * b = (n * a+ a) * b by Th33
.= ((n * a) * b) + (a * b) by Th23
.= (n * (a * b)) + (a * b) by A1
.= (n + 1) * (a * b) by Th33;
end;
Lm4: for n,G,a,b holds (n * a) * b = n * (a * b)
proof
defpred P[Nat] means ($1 * a) * b = $1 * (a * b);
A1: for k be Nat st P[k] holds P[k+1] by Lm3;
A2: P[0] by Lm2;
for k be Nat holds P[k] from NAT_1:sch 2(A2,A1);
hence thesis;
end;
theorem
(n * a) * b = n * (a * b) by Lm4;
theorem
(i * a) * b = i * (a * b)
proof
per cases;
suppose
i >= 0;
then i = |.i.| by ABSVALUE:def 1;
hence thesis by Lm4;
end;
suppose
A1: i < 0;
hence (i * a) * b = (-(|.i.| * a)) * b by Th29
.= -((|.i.| * a) * b) by Th26
.= -(|.i.| * (a * b)) by Lm4
.= i * (a * b) by A1,Th29;
end;
end;
theorem Th29:
G is Abelian addGroup implies a * b = a
proof
assume G is Abelian addGroup;
hence a * b = a + (-b) + b by Lm1
.= a by Th1;
end;
theorem ThB30:
(for a,b holds a * b = a) implies G is Abelian
proof
assume
A1: for a,b holds a * b = a;
let a,b;
a * b = a by A1;
hence thesis by Th22;
end;
definition
let G,A,B;
func A * B -> Subset of G equals
{g * h : g in A & h in B};
coherence
proof
set X = {g * h : g in A & h in B};
X c= the carrier of G
proof
let x be object;
assume x in X;
then ex g,h st x = g * h & g in A & h in B;
hence thesis;
end;
hence thesis;
end;
end;
theorem Th31:
x in A * B iff ex g,h st x = g * h & g in A & h in B;
theorem ThB32:
A * B <> {} iff A <> {} & B <> {}
proof
set x = the Element of A;
set y = the Element of B;
thus A * B <> {} implies A <> {} & B <> {}
proof
set x = the Element of A * B;
assume A * B <> {};
then ex a,b st x = a * b & a in A & b in B by Th31;
hence thesis;
end;
assume
A1: A <> {};
assume
A2: B <> {};
then reconsider x,y as Element of G by A1,TARSKI:def 3;
x * y in A * B by A1,A2;
hence thesis;
end;
theorem ThB33:
A * B c= (-B) + A + B
proof
let x be object;
assume x in A * B;
then consider a,b such that
A1: x = a * b and
A2: a in A and
A3: b in B;
(-b) in (-B) by A3;
then (-b) + a in (-B) + A by A2;
hence thesis by A1,A3;
end;
theorem Th34:
(A + B) * C c= A * C + (B * C)
proof
let x be object;
assume x in (A + B) * C;
then consider a,b such that
A1: x = a * b and
A2: a in A + B and
A3: b in C;
consider g,h such that
A4: a = g + h & g in A and
A5: h in B by A2;
A6: h * b in B * C by A3,A5;
x = (g * b) + (h * b) & g * b in A * C by A1,A3,A4,Th23;
hence thesis by A6;
end;
theorem Th35:
A * B * C = A * (B + C)
proof
thus A * B * C c= A * (B + C)
proof
let x be object;
assume x in A * B * C;
then consider a,c such that
A1: x = a * c and
A2: a in A * B and
A3: c in C;
consider g,h such that
A4: a = g * h and
A5: g in A and
A6: h in B by A2;
x = g * (h + c) & h + c in B + C by A1,A3,A4,A6,Th24;
hence thesis by A5;
end;
let x be object;
assume x in A * (B + C);
then consider a,b such that
A7: x = a * b & a in A and
A8: b in B + C;
consider g,h such that
A9: b = g + h & g in B and
A10: h in C by A8;
a * g in A * B & x = a * g * h by A7,A9,Th24;
hence thesis by A10;
end;
theorem
(-A) * B = -(A * B)
proof
thus (-A) * B c= -(A * B)
proof
let x be object;
assume x in (-A) * B;
then consider a,b such that
A1: x = a * b and
A2: a in (-A) and
A3: b in B;
consider c such that
A4: a = -c & c in A by A2;
x = -(c * b) & c * b in A * B by A1,A3,A4,Th26;
hence thesis;
end;
let x be object;
assume x in -(A * B);
then consider a such that
A5: x = (-a) and
A6: a in A * B;
consider b,c such that
A7: a = b * c and
A8: b in A and
A9: c in B by A6;
A10: (-b) in (-A) by A8;
x = (-b) * c by A5,A7,Th26;
hence thesis by A9,A10;
end;
theorem ThB37:
{a} * {b} = {a * b}
proof
A1: -{b} + {a} + {b} = {(-b)} + {a} + {b} by ThB3
.= {(-b) + a} + {b} by Th18
.= {a * b} by Th18;
{a} * {b} c= -{b} + {a} + {b} & {a} * {b} <> {} by ThB32,ThB33;
hence thesis by A1,ZFMISC_1:33;
end;
theorem
{a} * {b,c} = {a * b,a * c}
proof
thus {a} * {b,c} c= {a * b,a * c}
proof
let x be object;
assume x in {a} * {b,c};
then consider g,h such that
A1: x = g * h and
A2: g in {a} and
A3: h in{b,c};
A4: h = b or h = c by A3,TARSKI:def 2;
g = a by A2,TARSKI:def 1;
hence thesis by A1,A4,TARSKI:def 2;
end;
let x be object;
A5: c in {b,c} by TARSKI:def 2;
assume x in {a * b,a * c};
then
A6: x = a * b or x = a * c by TARSKI:def 2;
a in {a} & b in {b,c} by TARSKI:def 1,def 2;
hence thesis by A6,A5;
end;
theorem
{a,b} * {c} = {a * c,b * c}
proof
thus {a,b} * {c} c= {a * c,b * c}
proof
let x be object;
assume x in {a,b} * {c};
then consider g,h such that
A1: x = g * h and
A2: g in {a,b} and
A3: h in {c};
A4: g = b or g = a by A2,TARSKI:def 2;
h = c by A3,TARSKI:def 1;
hence thesis by A1,A4,TARSKI:def 2;
end;
let x be object;
A5: c in {c} by TARSKI:def 1;
assume x in {a * c,b * c};
then
A6: x = a * c or x = b * c by TARSKI:def 2;
a in {a,b} & b in {a,b} by TARSKI:def 2;
hence thesis by A6,A5;
end;
theorem
{a,b} * {c,d} = {a * c,a * d,b * c,b * d}
proof
thus {a,b} * {c,d} c= {a * c,a * d,b * c,b * d}
proof
let x be object;
assume x in {a,b} * {c,d};
then consider g,h such that
A1: x = g * h and
A2: g in {a,b} and
A3: h in {c,d};
A4: h = c or h = d by A3,TARSKI:def 2;
g = a or g = b by A2,TARSKI:def 2;
hence thesis by A1,A4,ENUMSET1:def 2;
end;
let x be object;
A5: c in {c,d} & d in {c,d} by TARSKI:def 2;
assume x in {a * c,a * d,b * c,b * d};
then
A6: x = a * c or x = a * d or x = b * c or x = b * d by ENUMSET1:def 2;
a in {a,b} & b in {a,b} by TARSKI:def 2;
hence thesis by A6,A5;
end;
definition
let G,A,g;
func A * g -> Subset of G equals
A * {g};
correctness;
func g * A -> Subset of G equals
{g} * A;
correctness;
end;
theorem Th41:
x in A * g iff ex h st x = h * g & h in A
proof
thus x in A * g implies ex h st x = h * g & h in A
proof
assume x in A * g;
then consider a,b such that
A1: x = a * b & a in A and
A2: b in {g};
b = g by A2,TARSKI:def 1;
hence thesis by A1;
end;
given h such that
A3: x = h * g & h in A;
g in {g} by TARSKI:def 1;
hence thesis by A3;
end;
theorem ThB42:
x in g * A iff ex h st x = g * h & h in A
proof
thus x in g * A implies ex h st x = g * h & h in A
proof
assume x in g * A;
then consider a,b such that
A1: x = a * b and
A2: a in {g} and
A3: b in A;
a = g by A2,TARSKI:def 1;
hence thesis by A1,A3;
end;
given h such that
A4: x = g * h & h in A;
g in {g} by TARSKI:def 1;
hence thesis by A4;
end;
theorem
g * A c= (-A) + g + A
proof
let x be object;
assume x in g * A;
then consider a such that
A1: x = g * a and
A2: a in A by ThB42;
(-a) in (-A) by A2;
then (-a) + g in (-A) + g by Th28;
hence thesis by A1,A2;
end;
theorem
A * B * g = A * (B + g) by Th35;
theorem
A * g * B = A * (g + B) by Th35;
theorem
g * A * B = g * (A + B) by Th35;
theorem Th47:
A * a * b = A * (a + b)
proof
thus A * a * b = A * (a + {b}) by Th35
.= A * (a + b) by Th18;
end;
theorem
a * A * b = a * (A + b) by Th35;
theorem
a * b * A = a * (b + A)
proof
thus a * b * A = {a} * {b} * A by ThB37
.= a * (b + A) by Th35;
end;
theorem Th50:
A * g = (-g) + A + g
proof
A * g c= -{g} + A + {g} by ThB33;
hence A * g c= (-g) + A + g by ThB3;
let x be object;
assume x in (-g) + A + g;
then consider a such that
A1: x = a + g and
A2: a in (-g) + A by Th28;
consider b such that
A3: a = (-g) + b and
A4: b in A by A2,Th27;
x = b * g by A1,A3;
hence thesis by A4,Th41;
end;
theorem
(A + B) * a c= (A * a) + (B * a) by Th34;
theorem ThB52:
A * 0_G = A
proof
thus A * 0_G = -(0_G) + A + 0_G by Th50
.= -(0_G) + A by Th37
.= 0_G + A by Th8
.= A by Th37;
end;
theorem
A <> {} implies (0_G) * A = {0_G}
proof
set y = the Element of A;
assume
A1: A <> {};
then reconsider y as Element of G by TARSKI:def 3;
thus (0_G) * A c= {0_G}
proof
let x be object;
assume x in (0_G) * A;
then ex a st x = (0_G) * a & a in A by ThB42;
then x = 0_G by Th17;
hence thesis by TARSKI:def 1;
end;
let x be object;
assume x in {0_G};
then x = 0_G by TARSKI:def 1;
then (0_G) * y = x by Th17;
hence thesis by A1,ThB42;
end;
theorem Th54:
A * a * (-a) = A & A * (-a) * a = A
proof
thus A * a * (-a) = A * (a + (-a)) by Th47
.= A * 0_G by Def5
.= A by ThB52;
thus A * (-a) * a = A * ((-a) + a) by Th47
.= A * 0_G by Def5
.= A by ThB52;
end;
theorem Th55:
G is Abelian addGroup iff for A,B st B <> {} holds A * B = A
proof
thus G is Abelian addGroup implies for A,B st B <> {} holds A * B = A
proof
assume
A1: G is Abelian addGroup;
let A,B;
set y = the Element of B;
assume
A2: B <> {};
then reconsider y as Element of G by TARSKI:def 3;
thus A * B c= A
proof
let x be object;
assume x in A * B;
then ex a,b st x = a * b & a in A & b in B;
hence thesis by A1,Th29;
end;
let x be object;
assume
A3: x in A;
then reconsider a = x as Element of G;
a * y = x by A1,Th29;
hence thesis by A2,A3;
end;
assume
A4: for A,B st B <> {} holds A * B = A;
now
let a,b;
{a} = {a} * {b} by A4
.= {a * b} by ThB37;
hence a = a * b by ZFMISC_1:3;
end;
hence thesis by ThB30;
end;
theorem
G is Abelian addGroup iff for A,g holds A * g = A
proof
thus G is Abelian addGroup implies for A,g holds A * g = A by Th55;
assume
A1: for A,g holds A * g = A;
now
let a,b;
{a} = {a} * b by A1
.= {a * b} by ThB37;
hence a = a * b by ZFMISC_1:3;
end;
hence thesis by ThB30;
end;
theorem
G is Abelian addGroup iff for A,g st A <> {} holds g * A = {g}
proof
thus G is Abelian addGroup implies for A,g st A <> {} holds
g * A = {g} by
Th55;
assume
A1: for A,g st A <> {} holds g * A = {g};
now
let a,b;
{a} = a * {b} by A1
.= {a * b} by ThB37;
hence a = a * b by ZFMISC_1:3;
end;
hence thesis by ThB30;
end;
definition
let G,H,a;
func H * a -> strict Subgroup of G means
:Def6A:
the carrier of it = carr(H) * a;
existence
proof
consider H1 being strict Subgroup of G such that
A1: the carrier of H1 = (-a) + H + -(-a) by Th127;
the carrier of H1 = carr(H) * a by A1,Th50;
hence thesis;
end;
correctness by Th59;
end;
theorem Th58:
x in H * a iff ex g st x = g * a & g in H
proof
thus x in H * a implies ex g st x = g * a & g in H
proof
assume x in H * a;
then x in carr H * a by Def6A;
then consider b such that
A1: x = b * a & b in carr H by Th41;
take b;
thus thesis by A1;
end;
given g such that
A2: x = g * a and
A3: g in H;
x in carr H * a by A2,A3,Th41;
hence thesis by Def6A;
end;
theorem ThB59:
the carrier of H * a = (-a) + H + a
proof
thus the carrier of H * a = carr(H) * a by Def6A
.= (-a) + H + a by Th50;
end;
theorem Th60:
H * a * b = H * (a + b)
proof
the carrier of H * a * b = carr(H * a) * b by Def6A
.= (carr H * a) * b by Def6A
.= carr H * (a + b) by Th47
.= the carrier of H * (a + b) by Def6A;
hence thesis by Th59;
end;
theorem Th61:
for H being strict Subgroup of G holds H * 0_G = H
proof
let H be strict Subgroup of G;
the carrier of H * 0_G = carr H * 0_G by Def6A
.= the carrier of H by ThB52;
hence thesis by Th59;
end;
theorem ThB62:
for H being strict Subgroup of G holds H * a * (-a) = H & H * (-a) * a = H
proof
let H be strict Subgroup of G;
thus H * a * (-a) = H * (a + (-a)) by Th60
.= H * 0_G by Def5
.= H by Th61;
thus H * (-a) * a = H * ((-a) + a) by Th60
.= H * 0_G by Def5
.= H by Th61;
end;
theorem Th63:
(H1 /\ H2) * a = (H1 * a) /\ (H2 * a)
proof
let g;
thus g in (H1 /\ H2) * a implies g in (H1 * a) /\ (H2 * a)
proof
assume g in (H1 /\ H2) * a;
then consider h such that
A1: g = h * a and
A2: h in H1 /\ H2 by Th58;
h in H2 by A2,Th82;
then
A3: g in H2 * a by A1,Th58;
h in H1 by A2,Th82;
then g in H1 * a by A1,Th58;
hence thesis by A3,Th82;
end;
assume
A4: g in (H1 * a) /\ (H2 * a);
then g in H1 * a by Th82;
then consider b such that
A5: g = b * a and
A6: b in H1 by Th58;
g in H2 * a by A4,Th82;
then consider c such that
A7: g = c * a and
A8: c in H2 by Th58;
b = c by A5,A7,ThB16;
then b in (H1 /\ H2) by A6,A8,Th82;
hence thesis by A5,Th58;
end;
theorem Th64:
card H = card(H * a)
proof
deffunc F(Element of G) = $1 * a;
consider f being Function of the carrier of G, the carrier of G such that
A1: for g holds f.g = F(g) from FUNCT_2:sch 4;
set g = f | (the carrier of H);
A2: dom f = the carrier of G & the carrier of H c= the carrier of G by
FUNCT_2:def 1,DefA5;
then
A3: dom g = the carrier of H by RELAT_1:62;
A4: rng g = the carrier of H * a
proof
thus rng g c= the carrier of H * a
proof
let x be object;
assume x in rng g;
then consider y being object such that
A5: y in dom g and
A6: g.y = x by FUNCT_1:def 3;
reconsider y as Element of H by A2,A5,RELAT_1:62;
reconsider y as Element of G by Th42;
f.y = y * a by A1;
then x in carr H * a by A5,A6,Th41,FUNCT_1:47;
hence thesis by Def6A;
end;
let x be object;
assume x in the carrier of H * a;
then x in carr H * a by Def6A;
then consider b such that
A8: x = b * a and
A9: b in carr H by Th41;
A10: f.b = b * a by A1;
g.b = f.b by A3,A9,FUNCT_1:47;
hence thesis by A3,A8,A9,A10,FUNCT_1:def 3;
end;
g is one-to-one
proof
let x,y be object;
assume that
A11: x in dom g and
A12: y in dom g and
A13: g.x = g.y;
reconsider b = x, c = y as Element of H by A2,A11,A12,RELAT_1:62;
reconsider b,c as Element of G by Th42;
A14: f.x = b * a & f.y = c * a by A1;
f.x = g.x by A11,FUNCT_1:47;
hence thesis by A12,A13,A14,ThB16,FUNCT_1:47;
end;
hence thesis by A3,A4,WELLORD2:def 4,CARD_1:5;
end;
theorem Th65:
H is finite iff H * a is finite
proof
card H = card(H * a) by Th64;
hence thesis;
end;
registration
let G,a;
let H be finite Subgroup of G;
cluster H * a -> finite;
coherence by Th65;
end;
theorem
for H being finite Subgroup of G holds card H = card(H * a) by Th64;
theorem Th67:
(0).G * a = (0).G
proof
A1: the carrier of (0).G = {0_G} by Def7;
the carrier of (0).G * a = (carr (0).G) * a by Def6A
.= {(0_G) * a} by A1,ThB37
.= {0_G} by Th17;
hence thesis by Def7;
end;
theorem
for H being strict Subgroup of G holds H * a = (0).G implies H = (0).G
proof
let H be strict Subgroup of G;
assume
A1: H * a = (0).G;
then reconsider H as finite Subgroup of G by Th65;
card (0).G = 1 by Th69;
then card H = 1 by A1,Th64;
hence thesis by Th70;
end;
theorem Th69:
for G being addGroup, a being Element of G holds (Omega).G * a = (Omega).G
proof
let G be addGroup, a be Element of G;
let h be Element of G;
(h * (-a)) * a = h * ((-a) + a) by Th24
.= h * 0_G by Def5
.= h by Th19;
hence thesis by Th58,STRUCT_0:def 5;
end;
theorem
for H being strict Subgroup of G holds H * a = G implies H = G
proof
let H be strict Subgroup of G;
assume
A1: H * a = G;
now
let g;
assume
A2: not g in H;
now
assume g * a in H * a;
then ex h st g * a = h * a & h in H by Th58;
hence contradiction by A2,ThB16;
end;
hence contradiction by A1;
end;
hence thesis by A1,Th62;
end;
theorem Th71:
Index H = Index(H * a)
proof
defpred P[object,object] means
ex b st $1 = b + H & $2 = (b * a) + (H * a);
A1: for x being object st x in Left_Cosets H ex y being object st P[x,y]
proof
let x be object;
assume x in Left_Cosets H;
then consider b such that
A2: x = b + H by Def15;
reconsider y = (b * a) + (H * a) as set;
take y;
take b;
thus thesis by A2;
end;
consider f being Function such that
A3: dom f = Left_Cosets H and
A4: for x being object st x in Left_Cosets H holds P[x,f.x]
from CLASSES1:sch 1(A1);
A5: for x,y1,y2 st x in Left_Cosets H & P[x,y1] & P[x,y2] holds y1 = y2
proof
set A = carr H;
let x,y1,y2;
assume x in Left_Cosets H;
given b such that
A6: x = b + H and
A7: y1 = (b * a) + (H * a);
given c such that
A8: x = c + H and
A9: y2 = (c * a) + (H * a);
thus y1 = ((-a) + b + a) + ((-a) + H + a) by A7,ThB59
.= ((-a) + b + a) + ((-a) + A) + a by ThA33
.= ((-a) + b) + (a + ((-a) + A)) + a by Th32
.= (-a) + b + (a + (-a) + A) + a by Th32
.= (-a) + b + (0_G + A) + a by Def5
.= (-a) + b + A + a by Th37
.= (-a) + (c + H) + a by A6,A8,Th32
.= (-a) + c + A + a by Th32
.= (-a) + c + (0_G + A) + a by Th37
.= (-a) + c + (a + (-a) + A) + a by Def5
.= ((-a) + c) + (a + ((-a) + A)) + a by Th32
.= ((-a) + c + a) + ((-a) + A) + a by Th32
.= ((-a) + c + a) + ((-a) + H + a) by ThA33
.= y2 by A9,ThB59;
end;
A10: rng f = Left_Cosets(H * a)
proof
thus rng f c= Left_Cosets(H * a)
proof
let x be object;
assume x in rng f;
then consider y being object such that
A11: y in dom f & f.y = x by FUNCT_1:def 3;
ex b st y = b + H & x = (b * a) + (H * a) by A3,A4,A11;
hence thesis by Def15;
end;
let x be object;
assume x in Left_Cosets(H * a);
then consider b such that
A12: x = b + (H * a) by Def15;
set c = b * (-a);
A13: x = (c * a) + (H * a) by A12,ThB25;
A14: c + H in Left_Cosets H by Def15;
then consider d such that
A15: c + H = d + H and
A16: f.(c + H) = (d * a) + (H * a) by A4;
(c * a) + (H * a) = (d * a) + (H * a) by A5,A14,A15;
hence thesis by A3,A13,A14,A16,FUNCT_1:def 3;
end;
f is one-to-one
proof
let x,y be object;
assume that
A17: x in dom f and
A18: y in dom f and
A19: f.x = f.y;
consider c such that
A20: y = c + H and
A21: f.y = (c * a) + (H * a) by A3,A4,A18;
consider b such that
A22: x = b + H and
A23: f.x = (b * a) + (H * a) by A3,A4,A17;
A24: -(c * a) + (b * a) = ((-c) * a) + (b * a) by Th26
.= ((-c) + b) * a by Th23;
consider d such that
A25: (-c + b) * a = d * a and
A26: d in H by A24,Th58,A19,A23,A21,Th114;
(-c) + b = d by A25,ThB16;
hence thesis by A22,A20,A26,Th114;
end;
hence thesis by A3,A10,WELLORD2:def 4,CARD_1:5;
end;
theorem
Left_Cosets H is finite implies index H = index(H * a)
proof
assume
A1: Left_Cosets H is finite;
then
A2: ex B being finite set st B = Left_Cosets H & index H = card B
by Def18;
A3: Index H = Index(H * a) by Th71;
then Left_Cosets(H * a) is finite by A1;
hence thesis by A2,A3,Def18;
end;
theorem Th73:
G is Abelian addGroup implies for H being strict Subgroup of G
for a holds H * a = H
proof
assume
A1: G is Abelian addGroup;
let H be strict Subgroup of G;
let a;
the carrier of H * a = (-a) + H + a by ThB59
.= H + (-a) + a by A1,Th112
.= H + ((-a) + a) by ThA107
.= H + 0_G by Def5
.= the carrier of H by ThB109;
hence thesis by Th59;
end;
definition
let G,a,b;
pred a,b are_conjugated means
:Def7:
ex g st a = b * g;
end;
notation
let G,a,b;
antonym a,b are_not_conjugated for a,b are_conjugated;
end;
theorem Th74:
a,b are_conjugated iff ex g st b = a * g
proof
thus a,b are_conjugated implies ex g st b = a * g
proof
given g such that
A1: a = b * g;
a * (-g) = b by A1,ThB25;
hence thesis;
end;
given g such that
A2: b = a * g;
a = b * (-g) by A2,ThB25;
hence thesis;
end;
Th75:
a,a are_conjugated
proof
take 0_G;
thus thesis by Th19;
end;
Th76:
a,b are_conjugated implies b,a are_conjugated
proof
given g such that
A1: a = b * g;
b = a * (-g) by A1,ThB25;
hence thesis;
end;
definition
let G,a,b;
redefine pred a,b are_conjugated; :: redefines are_conjugated (GROUP_1A, definition)
reflexivity by Th75;
symmetry by Th76;
end;
theorem Th77:
a,b are_conjugated & b,c are_conjugated implies a,c are_conjugated
proof
given g such that
A1: a = b * g;
given h such that
A2: b = c * h;
a = c * (h + g) by A1,A2,Th24;
hence thesis;
end;
theorem ThB78:
a,0_G are_conjugated or 0_G,a are_conjugated implies a = 0_G
proof
assume
A1: a,0_G are_conjugated or 0_G,a are_conjugated;
now
per cases by A1;
suppose
a,0_G are_conjugated;
then ex g st 0_G = a * g by Th74;
hence thesis by ThB18;
end;
suppose
0_G,a are_conjugated;
hence thesis by ThB18;
end;
end;
hence thesis;
end;
theorem Th79:
a * carr (Omega).G = {b : a,b are_conjugated}
proof
set A = a * carr (Omega).G;
set B = {b : a,b are_conjugated};
thus A c= B
proof
let x be object;
assume
A1: x in A;
then reconsider b = x as Element of G;
ex g st x = a * g & g in carr(Omega).G by A1,ThB42;
then b,a are_conjugated;
hence thesis;
end;
let x be object;
assume x in B;
then consider b such that
A2: x = b and
A3: a,b are_conjugated;
ex g st b = a * g by A3,Def7;
hence thesis by A2,ThB42;
end;
definition
let G,a;
func con_class a -> Subset of G equals
a * carr (Omega).G;
correctness;
end;
theorem Th80:
x in con_class a iff ex b st b = x & a,b are_conjugated
proof
thus x in con_class a implies ex b st b = x & a,b are_conjugated
proof
assume x in con_class a;
then x in {b : a,b are_conjugated} by Th79;
hence thesis;
end;
given b such that
A1: b = x & a,b are_conjugated;
x in {c : a,c are_conjugated} by A1;
hence thesis by Th79;
end;
theorem Th81:
a in con_class b iff a,b are_conjugated
proof
thus a in con_class b implies a,b are_conjugated
proof
assume a in con_class b;
then ex c st a = c & b,c are_conjugated by Th80;
hence thesis;
end;
assume a,b are_conjugated;
hence thesis by Th80;
end;
theorem
a * g in con_class a by Th80,Th74;
theorem
a in con_class a by Th81;
theorem
a in con_class b implies b in con_class a
proof
assume a in con_class b;
then a,b are_conjugated by Th81;
hence thesis by Th81;
end;
theorem
con_class a = con_class b iff con_class a meets con_class b
proof
thus con_class a = con_class b implies con_class a meets con_class b
by Th81;
assume con_class a meets con_class b;
then consider x being object such that
A1: x in con_class a and
A2: x in con_class b by XBOOLE_0:3;
reconsider x as Element of G by A1;
A3: a,x are_conjugated by A1,Th81;
thus con_class a c= con_class b
proof
let y be object;
assume y in con_class a;
then consider g such that
A4: g = y and
A5: a,g are_conjugated by Th80;
A6: b,x are_conjugated by A2,Th81;
x,a are_conjugated by A1,Th81;
then x,g are_conjugated by A5,Th77;
hence thesis by A4,A6,Th77,Th80;
end;
let y be object;
assume y in con_class b;
then consider g such that
A7: g = y and
A8: b,g are_conjugated by Th80;
x,b are_conjugated by A2,Th81;
then x,g are_conjugated by A8,Th77;
hence thesis by A3,A7,Th77,Th80;
end;
theorem
con_class a = {0_G} iff a = 0_G
proof
thus con_class a = {0_G} implies a = 0_G
proof
assume
A1: con_class a = {0_G};
a in con_class a by Th81;
hence thesis by A1,TARSKI:def 1;
end;
assume
A2: a = 0_G;
thus con_class a c= {0_G}
proof
let x be object;
assume x in con_class a;
then consider b such that
A3: b = x and
A4: a,b are_conjugated by Th80;
b = 0_G by A2,A4,ThB78;
hence thesis by A3,TARSKI:def 1;
end;
thus thesis by A2,Th81,ZFMISC_1:31;
end;
theorem
con_class a + A = A + con_class a
proof
thus con_class a + A c= A + con_class a
proof
let x be object;
assume x in con_class a + A;
then consider b,c such that
A1: x = b + c and
A2: b in con_class a and
A3: c in A;
reconsider h = x as Element of G by A1;
b,a are_conjugated by A2,Th81;
then consider g such that
A4: b = a * g;
h * (-c) = c + (((a * g) + c) + -c) by A1,A4,RLVECT_1:def 3
.= c + (a * g) by Th1;
then
A5: x = (c + (a * g)) * c by ThB25
.= (c * c) + (a * g * c) by Th23
.= c + (a * g * c) by Th20
.= c + (a * (g + c)) by Th24;
a * (g + c) in con_class a by Th80,Th74;
hence thesis by A3,A5;
end;
let x be object;
assume x in A + con_class a;
then consider b,c such that
A6: x = b + c and
A7: b in A and
A8: c in con_class a;
reconsider h = x as Element of G by A6;
c,a are_conjugated by A8,Th81;
then consider g such that
A9: c = a * g;
h * b = (a * g) + b by A6,A9,Th1;
then
A10: x = ((a * g) + b) * (-b) by ThB25
.= (a * g) * (-b) + (b * (-b)) by Th23
.= a * (g + (-b)) + (b * (-b)) by Th24
.= a * (g + (-b)) + b by Th1;
a * (g + (-b)) in con_class a by Th80,Th74;
hence thesis by A7,A10;
end;
definition
let G,A,B;
pred A,B are_conjugated means
ex g st A = B * g;
end;
notation
let G,A,B;
antonym A,B are_not_conjugated for A,B are_conjugated;
end;
theorem Th88:
A,B are_conjugated iff ex g st B = A * g
proof
thus A,B are_conjugated implies ex g st B = A * g
proof
given g such that
A1: A = B * g;
A * (-g) = B by A1,Th54;
hence thesis;
end;
given g such that
A2: B = A * g;
A = B * (-g) by A2,Th54;
hence thesis;
end;
theorem Th89:
A,A are_conjugated
proof
take 0_G;
thus thesis by ThB52;
end;
theorem Th90:
A,B are_conjugated implies B,A are_conjugated
proof
given g such that
A1: A = B * g;
B = A * (-g) by A1,Th54;
hence thesis;
end;
definition
let G,A,B;
redefine pred A,B are_conjugated; :: redefines are_conjugated (GROUP_1A, definition)
reflexivity by Th89;
symmetry by Th90;
end;
theorem Th91:
A,B are_conjugated & B,C are_conjugated implies A,C are_conjugated
proof
given g such that
A1: A = B * g;
given h such that
A2: B = C * h;
A = C * (h + g) by A1,A2,Th47;
hence thesis;
end;
theorem Th92:
{a},{b} are_conjugated iff a,b are_conjugated
proof
thus {a},{b} are_conjugated implies a,b are_conjugated
proof
assume {a},{b} are_conjugated;
then consider g such that
A1: {a} * g = {b} by Th88;
{b} = {a * g} by A1,ThB37;
hence thesis by Th74,ZFMISC_1:3;
end;
assume a,b are_conjugated;
then consider g such that
A2: a * g = b by Th74;
{b} = {a} * g by A2,ThB37;
hence thesis by Th88;
end;
theorem Th93:
A,carr H1 are_conjugated implies
ex H2 being strict Subgroup of G st the carrier of H2 = A
proof
assume A,carr H1 are_conjugated;
then consider g such that
A1: A = carr H1 * g;
A = the carrier of H1 * g by A1,Def6A;
hence thesis;
end;
definition
let G,A;
func con_class A -> Subset-Family of G equals
{B : A,B are_conjugated};
coherence
proof
set X = {B: A,B are_conjugated};
X c= bool the carrier of G
proof
let x be object;
assume x in X;
then ex B st x = B & A,B are_conjugated;
hence thesis;
end;
hence thesis;
end;
end;
theorem
x in con_class A iff ex B st x = B & A,B are_conjugated;
theorem Th95:
A in con_class B iff A,B are_conjugated
proof
thus A in con_class B implies A,B are_conjugated
proof
assume A in con_class B;
then ex C st A = C & B,C are_conjugated;
hence thesis;
end;
assume A,B are_conjugated;
hence thesis;
end;
theorem
A * g in con_class A
proof
A,A * g are_conjugated by Th88;
hence thesis;
end;
theorem
A in con_class A;
theorem
A in con_class B implies B in con_class A
proof
assume A in con_class B;
then A,B are_conjugated by Th95;
hence thesis;
end;
theorem
con_class A = con_class B iff con_class A meets con_class B
proof
thus con_class A = con_class B implies con_class A meets con_class B
proof
A1: A in con_class A;
assume con_class A = con_class B;
hence thesis by A1;
end;
assume con_class A meets con_class B;
then consider x being object such that
A2: x in con_class A and
A3: x in con_class B by XBOOLE_0:3;
reconsider x as Subset of G by A2;
A4: A,x are_conjugated by A2,Th95;
thus con_class A c= con_class B
proof
let y be object;
assume y in con_class A;
then consider C such that
A5: C = y and
A6: A,C are_conjugated;
A7: B,x are_conjugated by A3,Th95;
x,A are_conjugated by A2,Th95;
then x,C are_conjugated by A6,Th91;
then B,C are_conjugated by A7,Th91;
hence thesis by A5;
end;
let y be object;
assume y in con_class B;
then consider C such that
A8: C = y and
A9: B,C are_conjugated;
x,B are_conjugated by A3,Th95;
then x,C are_conjugated by A9,Th91;
then A,C are_conjugated by A4,Th91;
hence thesis by A8;
end;
theorem Th100:
con_class{a} = {{b} : b in con_class a}
proof
set A = {{b} : b in con_class a};
thus con_class{a} c= A
proof
let x be object;
assume x in con_class{a};
then consider B such that
A1: x = B and
A2: {a},B are_conjugated;
consider b such that
A3: {a} * b = B by A2,Th88;
a,a * b are_conjugated by Th74; then
A4: a * b in con_class a by Th81;
B = {a * b} by A3,ThB37;
hence thesis by A1,A4;
end;
let x be object;
assume x in A;
then consider b such that
A5: x = {b} and
A6: b in con_class a;
{b},{a} are_conjugated by A6,Th81,Th92;
hence thesis by A5;
end;
theorem
G is finite implies con_class A is finite;
definition
let G,H1,H2;
pred H1,H2 are_conjugated means
ex g st the addMagma of H1 = H2 * g;
end;
notation
let G,H1,H2;
antonym H1,H2 are_not_conjugated for H1,H2 are_conjugated;
end;
theorem Th102:
for H1,H2 being strict Subgroup of G holds H1,H2 are_conjugated
iff ex g st H2 = H1 * g
proof
let H1,H2 be strict Subgroup of G;
thus H1,H2 are_conjugated implies ex g st H2 = H1 * g
proof
given g such that
A1: the addMagma of H1 = H2 * g;
H1 * (-g) = H2 by A1,ThB62;
hence thesis;
end;
given g such that
A2: H2 = H1 * g;
H1 = H2 * (-g) by A2,ThB62;
hence thesis;
end;
theorem ThB103:
for H1 being strict Subgroup of G holds H1,H1 are_conjugated
proof
let H1 be strict Subgroup of G;
take 0_G;
thus thesis by Th61;
end;
theorem ThB104:
for H1,H2 being strict Subgroup of G holds H1,H2 are_conjugated
implies H2,H1 are_conjugated
proof
let H1,H2 be strict Subgroup of G;
given g such that
A1: the addMagma of H1 = H2 * g;
H2 = H1 * (-g) by A1,ThB62;
hence thesis;
end;
definition
let G;
let H1,H2 be strict Subgroup of G;
redefine pred H1,H2 are_conjugated; :: redefines are_conjugated (GROUP_1A, definition)
reflexivity by ThB103;
symmetry by ThB104;
end;
theorem Th105:
for H1,H2 being strict Subgroup of G holds H1,H2 are_conjugated
& H2,H3 are_conjugated implies H1,H3 are_conjugated
proof
let H1,H2 be strict Subgroup of G;
given g such that
A1: the addMagma of H1 = H2 * g;
given h such that
A2: the addMagma of H2 = H3 * h;
H1 = H3 * (h + g) by A1,A2,Th60;
hence thesis;
end;
reserve L for Subset of Subgroups G;
definition
let G,H;
func con_class H -> Subset of Subgroups G means
:Def12:
for x being object holds x in it iff
ex H1 being strict Subgroup of G st x = H1 & H,H1 are_conjugated;
existence
proof
defpred P[set] means ex H1 being strict Subgroup of G st $1 = H1 & H,H1
are_conjugated;
consider L such that
A1: x in L iff x in Subgroups G & P[x] from SUBSET_1:sch 1;
take L;
let x be object;
thus x in L implies ex H1 being strict Subgroup of G st x = H1 & H,H1
are_conjugated by A1;
given H1 being strict Subgroup of G such that
A2: x = H1 and
A3: H,H1 are_conjugated;
x in Subgroups G by A2,Def1;
hence thesis by A1,A2,A3;
end;
uniqueness
proof
defpred P[object] means
ex H3 being strict Subgroup of G st $1 = H3 & H,H3 are_conjugated;
let A1,A2 be Subset of Subgroups G;
assume
A4: for x being object holds x in A1 iff P[x];
assume
A5: for x being object holds x in A2 iff P[x];
thus thesis from XBOOLE_0:sch 2(A4,A5);
end;
end;
theorem Th106:
x in con_class H implies x is strict Subgroup of G
proof
assume x in con_class H;
then ex H1 being strict Subgroup of G st x = H1 & H,H1 are_conjugated by
Def12;
hence thesis;
end;
theorem Th107:
for H1,H2 being strict Subgroup of G holds H1 in con_class H2
iff H1,H2 are_conjugated
proof
let H1,H2 be strict Subgroup of G;
thus H1 in con_class H2 implies H1,H2 are_conjugated
proof
assume H1 in con_class H2; then
ex H3 being strict Subgroup of G st H1 = H3 & H2,H3 are_conjugated by Def12
;
hence thesis;
end;
assume H1,H2 are_conjugated;
hence thesis by Def12;
end;
theorem Th108:
for H being strict Subgroup of G holds H * g in con_class H
proof
let H be strict Subgroup of G;
H,H * g are_conjugated by Th102;
hence thesis by Def12;
end;
theorem Th109:
for H being strict Subgroup of G holds H in con_class H
proof
let H be strict Subgroup of G;
H,H are_conjugated;
hence thesis by Def12;
end;
theorem
for H1,H2 being strict Subgroup of G holds H1 in con_class H2 implies
H2 in con_class H1
proof
let H1,H2 be strict Subgroup of G;
assume H1 in con_class H2;
then H1,H2 are_conjugated by Th107;
hence thesis by Th107;
end;
theorem
for H1,H2 being strict Subgroup of G holds con_class H1 = con_class H2
iff con_class H1 meets con_class H2
proof
let H1,H2 be strict Subgroup of G;
thus con_class H1 = con_class H2 implies con_class H1 meets con_class H2
by Th109;
assume con_class H1 meets con_class H2;
then consider x being object such that
A1: x in con_class H1 and
A2: x in con_class H2 by XBOOLE_0:3;
reconsider x as strict Subgroup of G by A1,Th106;
A3: H1,x are_conjugated by A1,Th107;
thus con_class H1 c= con_class H2
proof
let y be object;
assume y in con_class H1;
then consider H3 being strict Subgroup of G such that
A4: H3 = y and
A5: H1,H3 are_conjugated by Def12;
A6: H2,x are_conjugated by A2,Th107;
x,H1 are_conjugated by A1,Th107;
then x,H3 are_conjugated by A5,Th105;
then H2,H3 are_conjugated by A6,Th105;
hence thesis by A4,Def12;
end;
let y be object;
assume y in con_class H2;
then consider H3 being strict Subgroup of G such that
A7: H3 = y and
A8: H2,H3 are_conjugated by Def12;
x,H2 are_conjugated by A2,Th107;
then x,H3 are_conjugated by A8,Th105;
then H1,H3 are_conjugated by A3,Th105;
hence thesis by A7,Def12;
end;
theorem
G is finite implies con_class H is finite by Th15,FINSET_1:1;
theorem ThB113:
for H1 being strict Subgroup of G holds H1,H2 are_conjugated
iff carr H1,carr H2 are_conjugated
proof
let H1 be strict Subgroup of G;
thus H1,H2 are_conjugated implies carr H1,carr H2 are_conjugated
proof
given a such that
A1: the addMagma of H1 = H2 * a;
carr H1 = carr H2 * a by A1,Def6A;
hence thesis;
end;
given a such that
A2: carr H1 = carr H2 * a;
H1 = H2 * a by A2,Def6A;
hence thesis;
end;
definition
let G;
let IT be Subgroup of G;
attr IT is normal means :Def13:
for a holds IT * a = the addMagma of IT;
end;
registration let G;
cluster strict normal for Subgroup of G;
existence
proof
(0).G is normal by Th67;
hence thesis;
end;
end;
reserve N2 for normal Subgroup of G;
theorem Th114:
(0).G is normal & (Omega).G is normal by Th67,Th69;
theorem
for N1,N2 being strict normal Subgroup of G holds N1 /\ N2 is normal
proof
let N1,N2 be strict normal Subgroup of G;
let a;
thus (N1 /\ N2) * a = (N1 * a) /\ (N2 * a) by Th63
.= N1 /\ (N2 * a) by Def13
.= the addMagma of (N1 /\ N2) by Def13;
end;
theorem
for H being strict Subgroup of G holds G is Abelian addGroup implies
H is normal by Th73;
theorem Th117:
H is normal Subgroup of G iff for a holds a + H = H + a
proof
thus H is normal Subgroup of G implies for a holds a + H = H + a
proof
assume
A1: H is normal Subgroup of G;
let a;
A2: carr(H * a) = (-a) + H + a by ThB59;
carr(H * a) = the carrier of the addMagma of H by A1,Def13
.= carr H;
hence a + H = a + ((-a) + H) + a by A2,ThA33
.= a + (-a) + H + a by ThB105
.= 0_G + H + a by Def5
.= H + a by Th37;
end;
assume
A3: for a holds a + H = H + a;
H is normal
proof
let a;
the carrier of H * a = (-a) + H + a by ThB59
.= H + (-a) + a by A3
.= H + ((-a) + a) by ThA107
.= H + 0_G by Def5
.= the carrier of H by ThB109;
hence thesis by Th59;
end;
hence thesis;
end;
theorem Th118:
for H being Subgroup of G holds H is normal Subgroup of G iff
for a holds a + H c= H + a
proof
let H be Subgroup of G;
thus H is normal Subgroup of G implies for a holds a + H c= H + a by Th117;
assume
A1: for a holds a + H c= H + a;
now
let a;
(-a) + H c= H + (-a) by A1;
then a + ((-a) + H) c= a + (H + (-a)) by Th4;
then a + (-a) + H c= a + (H + (-a)) by ThB105;
then 0_G + H c= a + (H + (-a)) by Def5;
then carr H c= a + (H + (-a)) by ThB109;
then carr H c= a + H + (-a) by ThB106;
then carr H + a c= a + H + (-a) + a by Th4;
then H + a c= a + H + ((-a) + a) by ThB34;
then H + a c= a + H + 0_G by Def5;
hence H + a c= a + H by Th37;
end;
then for a holds a + H = H + a by A1;
hence thesis by Th117;
end;
theorem ThB119:
for H being Subgroup of G holds H is normal Subgroup of G iff
for a holds H + a c= a + H
proof
let H be Subgroup of G;
thus H is normal Subgroup of G implies for a holds H + a c= a + H by Th117;
assume
A1: for a holds H + a c= a + H;
now
let a;
H + (-a) c= (-a) + H by A1;
then a + (H + (-a)) c= a + ((-a) + H) by Th4;
then a + (H + (-a)) c= a + (-a) + H by ThB105;
then a + (H + (-a)) c= 0_G + H by Def5;
then a + (H + (-a)) c= carr H by ThB109;
then a + H + (-a) c= carr H by ThB106;
then a + H + (-a) + a c= carr H + a by Th4;
then a + H + ((-a) + a) c= H + a by ThB34;
then a + H + 0_G c= H + a by Def5;
hence a + H c= H + a by Th37;
end;
then for a holds a + H = H + a by A1;
hence thesis by Th117;
end;
theorem
for H being Subgroup of G holds H is normal Subgroup of G iff for A
holds A + H = H + A
proof
let H be Subgroup of G;
thus H is normal Subgroup of G implies for A holds A + H = H + A
proof
assume
A1: H is normal Subgroup of G;
let A;
thus A + H c= H + A
proof
let x be object;
assume x in A + H;
then consider a,h such that
A2: x = a + h and
A3: a in A and
A4: h in H by Th94;
x in a + H by A2,A4,Th103;
then x in H + a by A1,Th117;
then ex g st x = g + a & g in H by Th104;
hence thesis by A3;
end;
let x be object;
assume x in H + A;
then consider h,a such that
A5: x = h + a & h in H and
A6: a in A by ThB95;
x in H + a by A5,Th104;
then x in a + H by A1,Th117;
then ex g st x = a + g & g in H by Th103;
hence thesis by A6;
end;
assume
A7: for A holds A + H = H + A;
now
let a;
thus a + H = {a} + H .= H + {a} by A7
.= H + a;
end;
hence thesis by Th117;
end;
theorem
for H being strict Subgroup of G holds H is normal Subgroup of G iff
for a holds H is Subgroup of H * a
proof
let H be strict Subgroup of G;
thus H is normal Subgroup of G implies for a holds H is Subgroup of H * a
proof
assume
A1: H is normal Subgroup of G;
let a;
H * a = the addMagma of H by A1,Def13;
hence thesis by ThA54;
end;
assume
A2: for a holds H is Subgroup of H * a;
now
let a;
A3: H * (-a) + a = -(-a) + H + (-a) + a by ThB59
.= -(-a) + H + ((-a) + a) by ThB34
.= -(-a) + H + 0_G by Def5
.= a + H by Th37;
H is Subgroup of H * (-a) by A2;
hence H + a c= a + H by A3,ThB6;
end;
hence thesis by ThB119;
end;
theorem
for H being strict Subgroup of G holds H is normal Subgroup of G iff
for a holds H * a is Subgroup of H
proof
let H be strict Subgroup of G;
thus H is normal Subgroup of G implies for a holds H * a is Subgroup of H
proof
assume
A1: H is normal Subgroup of G;
let a;
H * a = the addMagma of H by A1,Def13;
hence thesis by ThA54;
end;
assume
A2: for a holds H * a is Subgroup of H;
now
let a;
A3: H * (-a) + a = -(-a) + H + (-a) + a by ThB59
.= -(-a) + H + ((-a) + a) by ThB34
.= -(-a) + H + 0_G by Def5
.= a + H by Th37;
H * (-a) is Subgroup of H by A2;
hence a + H c= H + a by A3,ThB6;
end;
hence thesis by Th118;
end;
theorem
for H being strict Subgroup of G holds H is normal Subgroup of G iff
con_class H = {H}
proof
let H be strict Subgroup of G;
thus H is normal Subgroup of G implies con_class H = {H}
proof
assume
A1: H is normal Subgroup of G;
thus con_class H c= {H}
proof
let x be object;
assume x in con_class H;
then consider H1 being strict Subgroup of G such that
A2: x = H1 and
A3: H,H1 are_conjugated by Def12;
ex g st H1 = H * g by A3,Th102;
then x = H by A1,A2,Def13;
hence thesis by TARSKI:def 1;
end;
thus thesis by Th109,ZFMISC_1:31;
end;
assume
A4: con_class H = {H};
H is normal
proof
let a;
H * a in con_class H by Th108;
hence thesis by A4,TARSKI:def 1;
end;
hence thesis;
end;
theorem
for H being strict Subgroup of G holds H is normal Subgroup of G iff
for a st a in H holds con_class a c= carr H
proof
let H be strict Subgroup of G;
thus H is normal Subgroup of G implies for a st a in H holds con_class a c=
carr H
proof
assume
A1: H is normal Subgroup of G;
let a;
assume
A2: a in H;
let x be object;
assume x in con_class a;
then consider b such that
A3: x = b and
A4: a,b are_conjugated by Th80;
consider c such that
A5: b = a * c by A4,Th74;
x in H * c by A2,A3,A5,Th58;
hence thesis by A1,Def13;
end;
assume
A6: for a st a in H holds con_class a c= carr H;
H is normal
proof
let a;
H * a = H
proof
let b;
thus b in H * a implies b in H
proof
assume b in H * a;
then consider c such that
A7: b = c * a & c in H by Th58;
b in con_class c & con_class c c= carr H by A6,A7,Th80,Th74;
hence thesis;
end;
assume b in H; then
A8: con_class b c= carr H by A6;
b * (-a) in con_class b by Th80,Th74;
then b * (-a) in H by A8;
then b * (-a) * a in H * a by Th58;
hence thesis by ThB25;
end;
hence thesis;
end;
hence thesis;
end;
Lm5: for N1 being strict normal Subgroup of G holds carr N1 + carr N2 c= carr
N2 + carr N1
proof
let N1 be strict normal Subgroup of G;
let x be object;
assume x in carr N1 + carr N2;
then consider a,b such that
A1: x = a + b and
A2: a in carr N1 and
A3: b in carr N2;
a in N1 by A2;
then a * b in N1 * b by Th58; then
A4: a * b in carr N1 by Def13;
b + (a * b) = b + ((-b) + (a + b)) by RLVECT_1:def 3
.= a + b by Th1;
hence thesis by A1,A3,A4;
end;
theorem
for N1,N2 being strict normal Subgroup of G holds
carr N1 + carr N2 = carr N2 + carr N1 by Lm5;
theorem
for N1,N2 being strict normal Subgroup of G ex N being strict normal
Subgroup of G st the carrier of N = carr N1 + carr N2
proof
let N1,N2 be strict normal Subgroup of G;
set A = carr N1 + carr N2;
set B = carr N1;
set C = carr N2;
carr N1 + carr N2 = carr N2 + carr N1 by Lm5;
then consider H being strict Subgroup of G such that
A1: the carrier of H = A by Th78;
now
let a;
thus a + H = a + N1 + C by A1,ThB29
.= N1 + a + C by Th117
.= B + (a + N2) by ThA30
.= B + (N2 + a) by Th117
.= H + a by A1,ThB31;
end;
then H is normal Subgroup of G by Th117;
hence thesis by A1;
end;
theorem
for N being normal Subgroup of G holds Left_Cosets N = Right_Cosets N
proof
let N be normal Subgroup of G;
thus Left_Cosets N c= Right_Cosets N
proof
let x be object;
assume x in Left_Cosets N;
then consider a such that
A1: x = a + N by Def15;
x = N + a by A1,Th117;
hence thesis by Def16;
end;
let x be object;
assume x in Right_Cosets N;
then consider a such that
A2: x = N + a by Def16;
x = a + N by A2,Th117;
hence thesis by Def15;
end;
theorem
for H being Subgroup of G holds Left_Cosets H is finite & index H = 2
implies H is normal Subgroup of G
proof
let H be Subgroup of G;
assume that
A1: Left_Cosets H is finite and
A2: index H = 2;
ex B being finite set st B = Left_Cosets H & index H = card B by A1,
Th146;
then consider x,y being object such that
A3: x <> y and
A4: Left_Cosets H = {x,y} by A2,CARD_2:60;
carr H in Left_Cosets H by Th135;
then {x,y} = {x,carr H} or {x,y} = {carr H,y} by A4,TARSKI:def 2;
then consider z3 being object such that
A5: {x,y} = {carr H,z3};
reconsider z3 as set by TARSKI:1;
A6: carr H misses z3
proof
z3 in Left_Cosets H by A4,A5,TARSKI:def 2;
then
A7: ex a st z3 = a + H by Def15;
A8: carr H = 0_G + H by ThB109;
assume not thesis;
then carr H = z3 by A7,A8,Th115;
then
A9: {x,y} = {carr H} by A5,ENUMSET1:29;
then x = carr H by ZFMISC_1:4;
hence thesis by A3,A9,ZFMISC_1:4;
end;
union Left_Cosets H = the carrier of G & union Left_Cosets H = carr H
\/ z3 by A4,A5,Th137,ZFMISC_1:75;
then
A10: union Right_Cosets H = the carrier of G & z3 = (the carrier of G) \
carr H by A6,Th137,XBOOLE_1:88;
ex C being finite set st C = Right_Cosets H & index H = card C by A1,
Th146;
then consider z1,z2 being object such that
A11: z1 <> z2 and
A12: Right_Cosets H = {z1,z2} by A2,CARD_2:60;
carr H in Right_Cosets H by Th135;
then {z1,z2} = {z1,carr H} or {z1,z2} = {carr H,z2} by A12,TARSKI:def 2;
then consider z4 being object such that
A13: {z1,z2} = {carr H,z4};
reconsider z4 as set by TARSKI:1;
A14: carr H misses z4
proof
z4 in Right_Cosets H by A12,A13,TARSKI:def 2;
then
A15: ex a st z4 = H + a by Def16;
A16: carr H = H + 0_G by ThB109;
assume not thesis;
then carr H = z4 by A15,A16,Th121;
then
A17: {z1,z2} = {carr H} by A13,ENUMSET1:29;
then z1 = carr H by ZFMISC_1:4;
hence thesis by A11,A17,ZFMISC_1:4;
end;
A18: union Right_Cosets H = carr H \/ z4 by A12,A13,ZFMISC_1:75;
now
let c;
now
per cases;
suppose c + H = carr H;
hence c + H = H + c by Th113,Th119;
end;
suppose
A20: c + H <> carr H;
then
A21: H + c <> carr H by Th113,Th119;
c + H in Left_Cosets H by Def15;
then
A22: c + H = z3 by A4,A5,A20,TARSKI:def 2;
H + c in Right_Cosets H by Def16;
then H + c = z4 by A12,A13,A21,TARSKI:def 2;
hence c + H = H + c by A10,A18,A14,A22,XBOOLE_1:88;
end;
end;
hence c + H = H + c;
end;
hence thesis by Th117;
end;
definition
let G, A;
func Normalizer A -> strict Subgroup of G means
:Def14:
the carrier of it = {h : A * h = A};
existence
proof
set X = {h : A * h = A};
X c= the carrier of G
proof
let x be object;
assume x in X;
then ex h st x = h & A * h = A;
hence thesis;
end;
then reconsider X as Subset of G;
A1: now
let a,b;
assume a in X & b in X;
then ( ex g st a = g & A * g = A)& ex h st b = h & A * h = A;
then A * (a + b) = A by Th47;
hence a + b in X;
end;
A2: now
let a;
assume a in X;
then ex b st a = b & A * b = A;
then A = A * (-a) by Th54;
hence (-a) in X;
end;
A * 0_G = A by ThB52;
then 0_G in X;
hence thesis by A1,A2,Th52;
end;
uniqueness by Th59;
end;
theorem Th129:
x in Normalizer A iff ex h st x = h & A * h = A
proof
thus x in Normalizer A implies ex h st x = h & A * h = A
proof
assume x in Normalizer A;
then x in {h : A * h = A} by Def14;
hence thesis;
end;
given h such that
A1: x = h & A * h = A;
x in {b : A * b = A} by A1;
hence thesis by Def14;
end;
theorem Th130:
card con_class A = Index Normalizer A
proof
defpred P[object,object] means
ex a st $1 = A * a & $2 = Normalizer A + a;
A1: for x being object st x in con_class A ex y being object st P[x,y]
proof
let x be object;
assume x in con_class A;
then consider B such that
A2: x = B and
A3: A,B are_conjugated;
consider g such that
A4: B = A * g by A3,Th88;
reconsider y = Normalizer A + g as set;
take y;
take g;
thus thesis by A2,A4;
end;
consider f being Function such that
A5: dom f = con_class A and
A6: for x being object st x in con_class A holds P[x,f.x]
from CLASSES1:sch 1(A1);
A7: for x,y1,y2 st x in con_class A & P[x,y1] & P[x,y2] holds y1 = y2
proof
let x,y1,y2;
assume x in con_class A;
given a such that
A8: x = A * a and
A9: y1 = Normalizer A + a;
given b such that
A10: x = A * b and
A11: y2 = Normalizer A + b;
A = A * b * (-a) by A8,A10,Th54
.= A * (b + (-a)) by Th47;
hence thesis by A9,A11,Th129,Th120;
end;
A12: rng f = Right_Cosets Normalizer A
proof
thus rng f c= Right_Cosets Normalizer A
proof
let x be object;
assume x in rng f;
then consider y being object such that
A13: y in dom f & f.y = x by FUNCT_1:def 3;
ex a st y = A * a & x = Normalizer A + a by A5,A6,A13;
hence thesis by Def16;
end;
let x be object;
assume x in Right_Cosets Normalizer A;
then consider a such that
A14: x = Normalizer A + a by Def16;
set y = A * a;
A,A * a are_conjugated by Th88;
then
A15: y in con_class A;
then ex b st y = A * b & f.y = Normalizer A + b by A6;
then x = f.y by A7,A14,A15;
hence thesis by A5,A15,FUNCT_1:def 3;
end;
f is one-to-one
proof
let x,y be object;
assume that
A16: x in dom f and
A17: y in dom f and
A18: f.x = f.y;
consider b such that
A19: y = A * b and
A20: f.y = Normalizer A + b by A5,A6,A17;
consider a such that
A21: x = A * a and
A22: f.x = Normalizer A + a by A5,A6,A16;
ex h st b + (-a) = h & A * h = A by A18,A20,A22,Th129,Th120;
then A = A * b * (-a) by Th47;
hence thesis by A21,A19,Th54;
end;
hence card con_class A = card Right_Cosets Normalizer A
by A5,A12,WELLORD2:def 4,CARD_1:5
.= Index Normalizer A by Th145;
end;
theorem
con_class A is finite or Left_Cosets Normalizer A is finite implies
ex C being finite set st C = con_class A & card C = index Normalizer A
proof
A1: card con_class A = Index Normalizer A by Th130
.= card Left_Cosets Normalizer A;
assume
A3: con_class A is finite or Left_Cosets Normalizer A is finite;
then reconsider C = con_class A as finite set by A1;
take C;
thus C = con_class A;
Left_Cosets Normalizer A is finite by A3,A1;
hence thesis by A1,Def18;
end;
theorem Th132:
card con_class a = Index Normalizer{a}
proof
deffunc F(object) = {$1};
consider f being Function such that
A1: dom f = con_class a and
A2: for x being object st x in con_class a holds f.x = F(x)
from FUNCT_1:sch 3;
A3: rng f = con_class{a}
proof
thus rng f c= con_class{a}
proof
let x be object;
assume x in rng f;
then consider y being object such that
A4: y in dom f and
A5: f.y = x by FUNCT_1:def 3;
reconsider y as Element of G by A1,A4;
f.y = {y} by A1,A2,A4;
then x in {{d} : d in con_class a} by A1,A4,A5;
hence thesis by Th100;
end;
let x be object;
assume x in con_class{a};
then x in {{b} : b in con_class a} by Th100;
then consider b such that
A6: x = {b} and
A7: b in con_class a;
f.b = {b} by A2,A7;
hence thesis by A1,A6,A7,FUNCT_1:def 3;
end;
f is one-to-one
proof
let x,y be object;
assume that
A8: x in dom f & y in dom f and
A9: f.x = f.y;
f.x = {x} & f.y = {y} by A1,A2,A8;
hence thesis by A9,ZFMISC_1:3;
end;
hence card con_class a = card con_class{a} by A1,A3,WELLORD2:def 4,CARD_1:5
.= Index Normalizer{a} by Th130;
end;
theorem
con_class a is finite or Left_Cosets Normalizer{a} is finite implies
ex C being finite set st C = con_class a & card C = index Normalizer{a}
proof
A1: card con_class a = Index Normalizer {a} by Th132
.= card Left_Cosets Normalizer {a};
assume
A3: con_class a is finite or Left_Cosets Normalizer {a} is finite;
then reconsider C = con_class a as finite set by A1;
take C;
thus C = con_class a;
Left_Cosets Normalizer {a} is finite by A3,A1;
hence thesis by A1,Def18;
end;
definition
let G,H;
func Normalizer H -> strict Subgroup of G equals
Normalizer carr H;
correctness;
end;
theorem Th134:
for H being strict Subgroup of G holds
x in Normalizer H iff ex h st x = h & H * h = H
proof
let H be strict Subgroup of G;
thus x in Normalizer H implies ex h st x = h & H * h = H
proof
assume x in Normalizer H;
then consider a such that
A1: x = a and
A2: carr H * a = carr H by Th129;
H * a = H by A2,Def6A;
hence thesis by A1;
end;
given h such that
A3: x = h and
A4: H * h = H;
carr H * h = carr H by A4,Def6A;
hence thesis by A3,Th129;
end;
theorem Th135:
for H being strict Subgroup of G holds
card con_class H = Index Normalizer H
proof
let H be strict Subgroup of G;
defpred P[object,object] means
ex H1 being strict Subgroup of G st $1 = H1 & $2 = carr H1;
A1: for x being object st x in con_class H ex y being object st P[x,y]
proof
let x be object;
assume x in con_class H;
then reconsider H = x as strict Subgroup of G by Def1;
reconsider y = carr H as set;
take y;
take H;
thus thesis;
end;
consider f being Function such that
A2: dom f = con_class H and
A3: for x being object st x in con_class H holds P[x,f.x]
from CLASSES1:sch 1(A1);
A4: rng f = con_class carr H
proof
thus rng f c= con_class carr H
proof
let x be object;
assume x in rng f;
then consider y being object such that
A5: y in dom f and
A6: f.y = x by FUNCT_1:def 3;
consider H1 being strict Subgroup of G such that
A7: y = H1 and
A8: x = carr H1 by A2,A3,A5,A6;
carr H1,carr H are_conjugated by A2,A5,A7,Th107,ThB113;
hence thesis by A8;
end;
let x be object;
assume x in con_class carr H;
then consider B such that
A9: B = x and
A10: carr H,B are_conjugated;
consider H1 being strict Subgroup of G such that
A11: the carrier of H1 = B by A10,Th93;
B = carr H1 by A11;
then
A12: H1 in con_class H by A10,Th107,ThB113;
then ex H2 being strict Subgroup of G st H1 = H2 & f.H1 = carr H2 by A3;
hence thesis by A2,A9,A11,A12,FUNCT_1:def 3;
end;
f is one-to-one
proof
let x,y be object;
assume that
A13: x in dom f & y in dom f and
A14: f.x = f.y;
(ex H1 being strict Subgroup of G st x = H1 & f.x = carr H1 )& ex H2
being strict Subgroup of G st y = H2 & f.y = carr H2 by A2,A3,A13;
hence thesis by A14,Th59;
end;
hence card con_class H = card con_class carr H
by A2,A4,WELLORD2:def 4,CARD_1:5
.= Index Normalizer H by Th130;
end;
theorem
for H being strict Subgroup of G holds
con_class H is finite or Left_Cosets Normalizer H is finite implies
ex C being finite set st
C = con_class H & card C = index Normalizer H
proof
let H be strict Subgroup of G;
A1: card con_class H = Index Normalizer H by Th135
.= card Left_Cosets Normalizer H;
assume
A3: con_class H is finite or Left_Cosets Normalizer H is finite;
then reconsider C = con_class H as finite set by A1;
take C;
thus C = con_class H;
Left_Cosets Normalizer H is finite by A3,A1;
hence thesis by A1,Def18;
end;
theorem Th137:
for G being strict addGroup, H being strict Subgroup of G holds
H is normal Subgroup of G iff Normalizer H = G
proof
let G be strict addGroup, H be strict Subgroup of G;
thus H is normal Subgroup of G implies Normalizer H = G
proof
assume
A1: H is normal Subgroup of G;
now
let a be Element of G;
H * a = H by A1,Def13;
hence a in Normalizer H by Th134;
end;
hence thesis by Th62;
end;
assume
A2: Normalizer H = G;
H is normal
proof
let a be Element of G;
a in Normalizer H by A2;
then ex b being Element of G st b = a & H * b = H by Th134;
hence thesis;
end;
hence thesis;
end;
theorem
for G being strict addGroup holds Normalizer (0).G = G
proof
let G be strict addGroup;
(0).G is normal Subgroup of G by Th114;
hence thesis by Th137;
end;
theorem
for G being strict addGroup holds Normalizer (Omega).G = G
proof
let G be strict addGroup;
(Omega).G is normal Subgroup of G by Th114;
hence thesis by Th137;
end;
begin ::: TOPGRP1B
reserve S, R for 1-sorted,
X for Subset of R,
T for TopStruct,
x for set;
reserve H for non empty addMagma,
P, Q, P1, Q1 for Subset of H,
h for Element of H;
theorem Th4:
P c= P1 & Q c= Q1 implies P + Q c= P1 + Q1
proof
assume
A1: P c= P1 & Q c= Q1;
let x be object;
assume x in P + Q;
then ex g, t being Element of H st x = g + t & g in P & t in Q;
hence thesis by A1;
end;
theorem Th5:
P c= Q implies P + h c= Q + h
proof
assume
A1: P c= Q;
let x be object;
assume x in P + h;
then ex g being Element of H st x = g + h & g in P by Th28;
hence thesis by A1,Th28;
end;
theorem
P c= Q implies h + P c= h + Q
proof
assume
A1: P c= Q;
let x be object;
assume x in h + P;
then ex g being Element of H st x = h + g & g in P by Th27;
hence thesis by A1,Th27;
end;
reserve a for Element of G;
theorem Th7:
a in -A iff -a in A
proof
- -a = a & - -A = A;
hence thesis;
end;
Lm1: A c= B implies -A c= -B
proof
assume
A1: A c= B;
let a be object;
assume a in -A;
then ex g being Element of G st a = -g & g in A;
hence thesis by A1;
end;
theorem ThB8:
A c= B iff -A c= -B
proof
- -A = A & - -B = B;
hence thesis by Lm1;
end;
theorem Th9:
(add_inverse G).:A = -A
proof
set f = add_inverse G;
hereby
let y be object;
assume y in f.:A;
then consider x being object such that
A1: x in the carrier of G and
A2: x in A and
A3: y = f.x by FUNCT_2:64;
reconsider x as Element of G by A1;
y = -x by A3,Def6;
hence y in -A by A2;
end;
let y be object;
assume y in -A;
then consider g being Element of G such that
A4: y = -g & g in A;
f.g = -g by Def6;
hence thesis by A4,FUNCT_2:35;
end;
theorem Th10:
(add_inverse G)" A = -A
proof
set f = add_inverse G;
A1: dom f = the carrier of G by FUNCT_2:def 1;
hereby
let x be object;
assume
A2: x in f"A;
then reconsider g = x as Element of G;
f.x in A by A2,FUNCT_1:def 7;
then -(f.g) in -A;
then - -g in -A by Def6;
hence x in -A;
end;
let x be object;
assume x in -A;
then consider g being Element of G such that
A3: x = -g & g in A;
f.(-g) = - -g by Def6
.= g;
hence thesis by A1,A3,FUNCT_1:def 7;
end;
theorem Th11:
add_inverse G is one-to-one
proof
set f = add_inverse G;
let x1, x2 be object;
assume that
A1: x1 in dom f & x2 in dom f and
A2: f.x1 = f.x2;
reconsider a = x1, b = x2 as Element of G by A1;
f.a = -a & f.b = -b by Def6;
hence thesis by A2,TH9;
end;
theorem Th12:
rng add_inverse G = the carrier of G
proof
set f = add_inverse G;
thus rng f c= the carrier of G;
let x be object;
A1: dom f = the carrier of G by FUNCT_2:def 1;
assume x in the carrier of G;
then reconsider a = x as Element of G;
f.(-a) = - -a by Def6
.= a;
hence thesis by A1,FUNCT_1:def 3;
end;
registration
let G be addGroup;
cluster add_inverse G -> one-to-one onto;
coherence by Th11,Th12;
end;
theorem Th13:
(add_inverse G)" = add_inverse G
proof
set f = add_inverse G;
A1: dom f = the carrier of G by FUNCT_2:def 1;
now
let x be object;
assume x in dom f;
then reconsider g = x as Element of G;
A3: f.(-g) = - -g by Def6
.= g;
thus f.x = -g by Def6
.= f".x by A1,A3,FUNCT_1:32;
end;
hence thesis by A1;
end;
theorem Th14:
(the addF of H).:[:P,Q:] = P + Q
proof
set f = the addF of H;
hereby
let y be object;
assume y in f.:[:P,Q:];
then consider x being object such that
x in [:the carrier of H,the carrier of H:] and
A1: x in [:P,Q:] and
A2: y = f.x by FUNCT_2:64;
consider a, b being object such that
A3: a in P & b in Q and
A4: x = [a,b] by A1,ZFMISC_1:def 2;
reconsider a, b as Element of H by A3;
y = a+b by A2,A4;
hence y in P+Q by A3;
end;
let y be object;
assume y in P + Q;
then consider g, h being Element of H such that
A5: y = g+h and
A6: g in P & h in Q;
[g,h] in [:P,Q:] by A6,ZFMISC_1:87;
hence thesis by A5,FUNCT_2:35;
end;
definition
let G be non empty addMagma, a be Element of G;
func a+ -> Function of G, G means
:Def1:
for x being Element of G holds it.x = a + x;
existence
proof
deffunc U(Element of G) = a + $1;
consider f being Function of the carrier of G, the carrier of G such that
A1: for x being Element of G holds f.x = U(x) from FUNCT_2:sch 4;
reconsider f as Function of G, G;
take f;
thus thesis by A1;
end;
uniqueness
proof
let f, g be Function of G, G such that
A2: for x being Element of G holds f.x = a + x and
A3: for x being Element of G holds g.x = a + x;
now
let x be object;
assume x in the carrier of G;
then reconsider y = x as Element of G;
thus f.x = a + y by A2
.= g.x by A3;
end;
hence thesis;
end;
func +a -> Function of G, G means
:Def2:
for x being Element of G holds it.x = x + a;
existence
proof
deffunc U(Element of G) = $1 +a;
consider f being Function of the carrier of G, the carrier of G such that
A4: for x being Element of G holds f.x = U(x) from FUNCT_2:sch 4;
reconsider f as Function of G, G;
take f;
thus thesis by A4;
end;
uniqueness
proof
let f, g be Function of G, G such that
A5: for x being Element of G holds f.x = x + a and
A6: for x being Element of G holds g.x = x + a;
now
let x be object;
assume x in the carrier of G;
then reconsider y = x as Element of G;
thus f.x = y + a by A5
.= g.x by A6;
end;
hence thesis;
end;
end;
registration
let G be addGroup, a be Element of G;
cluster a+ -> one-to-one onto;
coherence
proof
set f = a+;
A1: dom f = the carrier of G by FUNCT_2:def 1;
hereby
let x1, x2 be object;
assume that
A2: x1 in dom f & x2 in dom f and
A3: f.x1 = f.x2;
reconsider y1 = x1, y2 = x2 as Element of G by A2;
A4: f.y1 = a + y1 & f.y2 = a + y2 by Def1;
thus x1 = 0_G + y1 by Def4
.= -a + a + y1 by Def5
.= -a + (a + y1) by RLVECT_1:def 3
.= -a + a + y2 by A3,A4,RLVECT_1:def 3
.= 0_G + y2 by Def5
.= x2 by Def4;
end;
thus rng f c= the carrier of G;
let y be object;
assume y in the carrier of G;
then reconsider y1 = y as Element of G;
f.(-a + y1) = a + (-a + y1) by Def1
.= a + (-a) + y1 by RLVECT_1:def 3
.= 0_G + y1 by Def5
.= y by Def4;
hence thesis by A1,FUNCT_1:def 3;
end;
cluster +a -> one-to-one onto;
coherence
proof
set f = +a;
A5: dom f = the carrier of G by FUNCT_2:def 1;
hereby
let x1, x2 be object;
assume that
A6: x1 in dom f & x2 in dom f and
A7: f.x1 = f.x2;
reconsider y1 = x1, y2 = x2 as Element of G by A6;
A8: f.y1 = y1 + a & f.y2 = y2 + a by Def2;
thus x1 = y1 + 0_G by Def4
.= y1 + (a + (-a)) by Def5
.= y1 + a + (-a) by RLVECT_1:def 3
.= y2 + (a + (-a)) by A7,A8,RLVECT_1:def 3
.= y2 + 0_G by Def5
.= x2 by Def4;
end;
thus rng f c= the carrier of G;
let y be object;
assume y in the carrier of G;
then reconsider y1 = y as Element of G;
f.(y1+(-a)) = y1 + (-a) + a by Def2
.= y1 + ((-a) + a) by RLVECT_1:def 3
.= y1 + 0_G by Def5
.= y by Def4;
hence thesis by A5,FUNCT_1:def 3;
end;
end;
theorem Th15:
h+.:P = h + P
proof
set f = h+;
hereby
let y be object;
assume y in f.:P;
then consider x being object such that
A1: x in dom f and
A2: x in P & y = f.x by FUNCT_1:def 6;
reconsider x as Element of H by A1;
f.x = h + x by Def1;
hence y in h + P by A2,Th27;
end;
let y be object;
assume y in h + P;
then consider s being Element of H such that
A3: y = h + s & s in P by Th27;
dom f = the carrier of H & f.s = h + s by Def1,FUNCT_2:def 1;
hence thesis by A3,FUNCT_1:def 6;
end;
theorem Th16:
(+h).:P = P + h
proof
set f = +h;
hereby
let y be object;
assume y in f.:P;
then consider x being object such that
A1: x in dom f and
A2: x in P & y = f.x by FUNCT_1:def 6;
reconsider x as Element of H by A1;
f.x = x + h by Def2;
hence y in P + h by A2,Th28;
end;
let y be object;
assume y in P + h;
then consider s being Element of H such that
A3: y = s + h & s in P by Th28;
dom f = the carrier of H & f.s = s + h by Def2,FUNCT_2:def 1;
hence thesis by A3,FUNCT_1:def 6;
end;
theorem Th17:
a+/" = (-a)+
proof
set f = a+, g = -a+;
A1: now
reconsider h = f as Function;
let y be object;
assume y in the carrier of G;
then reconsider y1 = y as Element of G;
rng f = the carrier of G by FUNCT_2:def 3;
then
A2: y1 in rng f;
dom f = the carrier of G by FUNCT_2:def 1;
then
A3: g.y1 in dom f & f/".y1 in dom f;
f.(g.y) = a+(g.y1) by Def1
.= a+(-a + y1) by Def1
.= a+ (-a) +y1 by RLVECT_1:def 3
.= 0_G + y1 by Def5
.= y by Def4
.= h.(h".y) by A2,FUNCT_1:35
.= f.(f/".y) by TOPS_2:def 4;
hence f/".y = g.y by A3,FUNCT_1:def 4;
end;
thus thesis by A1;
end;
theorem Th18:
(+a)/" = +(-a)
proof
set f = +a, g = +(-a);
A1: now
reconsider h = f as Function;
let y be object;
assume y in the carrier of G;
then reconsider y1 = y as Element of G;
rng f = the carrier of G by FUNCT_2:def 3;
then
A2: y1 in rng f;
dom f = the carrier of G by FUNCT_2:def 1;
then
A3: g.y1 in dom f & f/".y1 in dom f;
f.(g.y) = (g.y1)+a by Def2
.= y1+(-a)+a by Def2
.= y1+(-a+a) by RLVECT_1:def 3
.= y1+(0_G) by Def5
.= y by Def4
.= h.(h".y) by A2,FUNCT_1:35
.= f.(f/".y) by TOPS_2:def 4;
hence f/".y = g.y by A3,FUNCT_1:def 4;
end;
thus thesis by A1;
end;
:: On the topological groups
definition
struct (addMagma, TopStruct) TopaddGrStr (# carrier -> set,
addF -> BinOp of the carrier,
topology -> Subset-Family of the carrier #);
end;
registration
let A be non empty set, R be BinOp of A, T be Subset-Family of A;
cluster TopaddGrStr (#A, R, T#) -> non empty;
coherence;
end;
registration
let x be set, R be BinOp of {x}, T be Subset-Family of {x};
cluster TopaddGrStr (#{x}, R, T#) -> trivial;
coherence;
end;
registration
cluster -> addGroup-like add-associative Abelian for 1-element addMagma;
coherence
proof
let H be 1-element addMagma;
thus H is addGroup-like
proof
now
set e = the Element of H;
take e;
let h be Element of H;
thus h + e = h & e + h = h by STRUCT_0:def 10;
take g = e;
thus h + g = e & g + h = e by STRUCT_0:def 10;
end;
hence thesis;
end;
thus H is add-associative by STRUCT_0:def 10;
thus H is Abelian by STRUCT_0:def 10;
end;
end;
registration
cluster strict non empty for TopaddGrStr;
existence
proof
set R = the BinOp of {{}},T = the Subset-Family of {{}};
take TopaddGrStr (#{{}},R,T#);
thus thesis;
end;
end;
registration
cluster strict TopSpace-like 1-element for TopaddGrStr;
existence
proof
set R = the BinOp of {{}};
take TopaddGrStr (#{{}}, R, bool {{}}#);
the carrier of 1TopSp {{}} is 1-element;
hence thesis by TEX_2:7;
end;
end;
definition
let G be addGroup-like add-associative non empty TopaddGrStr;
attr G is UnContinuous means
:Def7:
add_inverse G is continuous;
end;
definition
let G be TopSpace-like TopaddGrStr;
attr G is BinContinuous means
:Def8:
for f being Function of [:G,G:], G st f
= the addF of G holds f is continuous;
end;
registration
cluster strict Abelian UnContinuous BinContinuous for TopSpace-like
addGroup-like add-associative 1-element TopaddGrStr;
existence
proof
set R = the BinOp of {{}};
1TopSp {{}} is 1-element;
then reconsider
T = TopaddGrStr (#{{}}, R, bool {{}}#) as strict TopSpace-like
1-element TopaddGrStr by TEX_2:7;
take T;
thus T is strict Abelian;
hereby
set f = add_inverse T;
thus f is continuous
proof
let P1 be Subset of T such that
P1 is closed;
per cases by ZFMISC_1:33;
suppose
f"P1 = {};
hence thesis;
end;
suppose
f"P1 = {{}};
then f"P1 = [#]T;
hence thesis;
end;
end;
end;
let f be Function of [:T,T:], T such that
f = the addF of T;
A1: the carrier of [:T,T:] = [:{{}},{{}}:] by BORSUK_1:def 2
.= {[{},{}]} by ZFMISC_1:29;
let P1 be Subset of T such that
P1 is closed;
per cases by A1,ZFMISC_1:33;
suppose
f"P1 = {};
hence thesis;
end;
suppose
f"P1 = {[{},{}]};
then f"P1 = [#][:T,T:] by A1;
hence thesis;
end;
end;
end;
definition
mode TopaddGroup is TopSpace-like addGroup-like add-associative
non empty TopaddGrStr;
end;
definition
mode TopologicaladdGroup is UnContinuous BinContinuous TopaddGroup;
end;
theorem Th36:
for T being BinContinuous non empty TopSpace-like TopaddGrStr, a,
b being Element of T, W being a_neighborhood of a+b ex A being open
a_neighborhood of a, B being open a_neighborhood of b st A+B c= W
proof
let T be BinContinuous non empty TopSpace-like TopaddGrStr, a, b be Element
of T, W be a_neighborhood of a+b;
the carrier of [:T,T:] = [:the carrier of T,the carrier of T:] by
BORSUK_1:def 2;
then reconsider f = the addF of T as Function of [:T,T:], T;
consider H being a_neighborhood of [a,b] such that
A1: f.:H c= W by Def8,BORSUK_1:def 1;
consider F being Subset-Family of [:T,T:] such that
A2: Int H = union F and
A3: for e being set st e in F ex X1, Y1 being Subset of T st e = [:X1,Y1
:] & X1 is open & Y1 is open by BORSUK_1:5;
[a,b] in Int H by CONNSP_2:def 1;
then consider M being set such that
A4: [a,b] in M and
A5: M in F by A2,TARSKI:def 4;
consider A, B being Subset of T such that
A6: M = [:A,B:] and
A7: A is open and
A8: B is open by A3,A5;
a in A by A4,A6,ZFMISC_1:87;
then
A9: a in Int A by A7,TOPS_1:23;
b in B by A4,A6,ZFMISC_1:87;
then b in Int B by A8,TOPS_1:23;
then reconsider B as open a_neighborhood of b by A8,CONNSP_2:def 1;
reconsider A as open a_neighborhood of a by A7,A9,CONNSP_2:def 1;
take A, B;
let x be object;
assume x in A+B;
then consider g, h being Element of T such that
A10: x = g+h and
A11: g in A & h in B;
A12: Int H c= H by TOPS_1:16;
[g,h] in M by A6,A11,ZFMISC_1:87;
then [g,h] in Int H by A2,A5,TARSKI:def 4;
then x in f.:H by A10,A12,FUNCT_2:35;
hence thesis by A1;
end;
theorem ThW37:
for T being TopSpace-like non empty TopaddGrStr st (for a, b being
Element of T, W being a_neighborhood of a+b ex A being a_neighborhood of a, B
being a_neighborhood of b st A+B c= W) holds T is BinContinuous
proof
let T be TopSpace-like non empty TopaddGrStr such that
A1: for a, b being Element of T, W being a_neighborhood of a+b ex A
being a_neighborhood of a, B being a_neighborhood of b st A+B c= W;
let f be Function of [:T,T:], T such that
A2: f = the addF of T;
for W being Point of [:T,T:], G being a_neighborhood of f.W ex H being
a_neighborhood of W st f.:H c= G
proof
let W be Point of [:T,T:], G be a_neighborhood of f.W;
consider a, b being Point of T such that
A3: W = [a,b] by BORSUK_1:10;
f.W = a+b by A2,A3;
then consider
A being a_neighborhood of a, B being a_neighborhood of b such that
A4: A+B c= G by A1;
reconsider H = [:A,B:] as a_neighborhood of W by A3;
take H;
thus thesis by A2,A4,Th14;
end;
hence thesis by BORSUK_1:def 1;
end;
theorem Th38:
for T being UnContinuous TopaddGroup, a being Element of T, W being
a_neighborhood of -a ex A being open a_neighborhood of a st -A c= W
proof
let T be UnContinuous TopaddGroup, a be Element of T,
W be a_neighborhood of -a;
reconsider f = add_inverse T as Function of T, T;
f.a = -a & f is continuous by Def7,Def6;
then consider H being a_neighborhood of a such that
A1: f.:H c= W by BORSUK_1:def 1;
a in Int Int H by CONNSP_2:def 1;
then reconsider A = Int H as open a_neighborhood of a by CONNSP_2:def 1;
take A;
let x be object;
assume x in -A;
then consider g being Element of T such that
A2: x = -g and
A3: g in A;
Int H c= H & f.g = -g by Def6,TOPS_1:16;
then -g in f.:H by A3,FUNCT_2:35;
hence thesis by A1,A2;
end;
theorem Th39:
for T being TopaddGroup st for a being Element of T, W being
a_neighborhood of -a ex A being a_neighborhood of a st -A c= W holds T is
UnContinuous
proof
let T be TopaddGroup such that
A1: for a being Element of T, W being a_neighborhood of -a ex A being
a_neighborhood of a st -A c= W;
set f = add_inverse T;
for W being Point of T, G being a_neighborhood of f.W ex H being
a_neighborhood of W st f.:H c= G
proof
let a be Point of T, G be a_neighborhood of f.a;
f.a = -a by Def6;
then consider A being a_neighborhood of a such that
A2: -A c= G by A1;
take A;
thus thesis by A2,Th9;
end;
hence f is continuous by BORSUK_1:def 1;
end;
theorem Th40:
for T being TopologicaladdGroup, a, b being Element of T for W
being a_neighborhood of a+ (-b) ex A being open a_neighborhood of a, B being
open a_neighborhood of b st A + (-B) c= W
proof
let T be TopologicaladdGroup, a, b be Element of T,
W be a_neighborhood of a+(-b);
consider A being open a_neighborhood of a, B being open a_neighborhood of -b
such that
A1: A+B c= W by Th36;
consider C being open a_neighborhood of b such that
A2: -C c= B by Th38;
take A, C;
let x be object;
assume x in A+(-C);
then consider g, h being Element of T such that
A3: x = g+h and
A4: g in A and
A5: h in -C;
consider k being Element of T such that
A6: h = -k and
k in C by A5;
g+(-k) in A+B by A2,A4,A5,A6;
hence thesis by A1,A3,A6;
end;
theorem
for T being TopaddGroup st for a, b being Element of T, W being
a_neighborhood of a+(-b) ex A being a_neighborhood of a, B being a_neighborhood
of b st A+(-B) c= W holds T is TopologicaladdGroup
proof
let T be TopaddGroup such that
A1: for a, b being Element of T, W being a_neighborhood of a+(-b) ex A
being a_neighborhood of a, B being a_neighborhood of b st A+(-B) c= W;
A2: for a being Element of T, W being a_neighborhood of -a ex A being
a_neighborhood of a st -A c= W
proof
let a be Element of T, W be a_neighborhood of -a;
W is a_neighborhood of 0_T+(-a) by Def4;
then consider
A being a_neighborhood of 0_T, B being a_neighborhood of a such
that
A3: A+(-B) c= W by A1;
take B;
let x be object;
assume
A4: x in -B;
then consider g being Element of T such that
A5: x = -g and
g in B;
0_T in A by CONNSP_2:4;
then 0_T + (-g) in A+(-B) by A4,A5;
then -g in A+(-B) by Def4;
hence thesis by A3,A5;
end;
for a, b being Element of T, W being a_neighborhood of a+b ex A being
a_neighborhood of a, B being a_neighborhood of b st A+B c= W
proof
let a, b be Element of T, W be a_neighborhood of a+b;
W is a_neighborhood of a+(- -b);
then consider
A being a_neighborhood of a, B being a_neighborhood of -b such
that
A6: A+(-B) c= W by A1;
consider B1 being a_neighborhood of b such that
A7: -B1 c= B by A2;
take A, B1;
let x be object;
assume x in A + B1;
then consider g, h being Element of T such that
A8: x = g + h & g in A and
A9: h in B1;
-h in -B1 by A9;
then h in -B by A7,Th7;
then x in A+(-B) by A8;
hence thesis by A6;
end;
hence thesis by A2,ThW37,Th39;
end;
registration
let G be BinContinuous non empty TopSpace-like TopaddGrStr,
a be Element of G;
cluster a+ -> continuous;
coherence
proof
set f = a+;
for w being Point of G, A being a_neighborhood of f.w ex W being
a_neighborhood of w st f.:W c= A
proof
let w be Point of G, A be a_neighborhood of f.w;
f.w = a + w by Def1;
then consider
B being open a_neighborhood of a, W being open a_neighborhood
of w such that
A1: B+W c= A by Th36;
take W;
let k be object;
assume k in f.:W;
then k in a + W by Th15;
then
A2: ex h being Element of G st k = a + h & h in W by Th27;
a in B by CONNSP_2:4;
then k in B + W by A2;
hence thesis by A1;
end;
hence thesis by BORSUK_1:def 1;
end;
cluster +a -> continuous;
coherence
proof
set f = +a;
for w being Point of G, A being a_neighborhood of f.w ex W being
a_neighborhood of w st f.:W c= A
proof
let w be Point of G, A be a_neighborhood of f.w;
f.w = w + a by Def2;
then consider
W being open a_neighborhood of w, B being open a_neighborhood
of a such that
A3: W+B c= A by Th36;
take W;
let k be object;
assume k in f.:W;
then k in W + a by Th16;
then
A4: ex h being Element of G st k = h + a & h in W by Th28;
a in B by CONNSP_2:4;
then k in W + B by A4;
hence thesis by A3;
end;
hence thesis by BORSUK_1:def 1;
end;
end;
theorem Th42:
for G being BinContinuous TopaddGroup, a being Element of G holds
a+ is Homeomorphism of G
proof
let G be BinContinuous TopaddGroup, a be Element of G;
set f = a+;
thus dom f = [#]G & rng f = [#]G & f is one-to-one by FUNCT_2:def 1,def 3;
thus f is continuous;
f/" = ((-a)+) by Th17;
hence thesis;
end;
theorem Th43:
for G being BinContinuous TopaddGroup, a being Element of G holds +
a is Homeomorphism of G
proof
let G be BinContinuous TopaddGroup, a be Element of G;
set f = +a;
thus dom f = [#]G & rng f = [#]G & f is one-to-one by FUNCT_2:def 1,def 3;
thus f is continuous;
f/" = +(-a) by Th18;
hence thesis;
end;
definition
let G be BinContinuous TopaddGroup, a be Element of G;
redefine func a+ -> Homeomorphism of G; :: redefines + (GROUP_1A, definition)
coherence by Th42;
redefine func +a -> Homeomorphism of G; :: redefines + (GROUP_1A, definition)
coherence by Th43;
end;
theorem Th44:
for G being UnContinuous TopaddGroup holds
add_inverse G is Homeomorphism of G
proof
let G be UnContinuous TopaddGroup;
set f = add_inverse G;
thus
dom f = [#]G & rng f = [#]G & f is one-to-one by FUNCT_2:def 1,def 3;
thus f is continuous by Def7;
f = f" by Th13
.= f/" by TOPS_2:def 4;
hence thesis by Def7;
end;
definition
let G be UnContinuous TopaddGroup;
redefine func add_inverse G -> Homeomorphism of G; :: redefines add_inverse (GROUP_1A, definition)
coherence by Th44;
end;
registration
cluster BinContinuous -> homogeneous for TopaddGroup;
coherence
proof
let T be TopaddGroup;
assume T is BinContinuous;
then reconsider G = T as BinContinuous TopaddGroup;
G is homogeneous
proof
let p, q be Point of G;
take +((-p)+q);
thus (+((-p)+q)).p = p+((-p)+q) by Def2
.= p+(-p)+q by RLVECT_1:def 3
.= 0_G+q by Def5
.= q by Def4;
end;
hence thesis;
end;
end;
theorem Th45:
for G being BinContinuous TopaddGroup, F being closed Subset of G,
a being Element of G holds F + a is closed
proof
let G be BinContinuous TopaddGroup, F be closed Subset of G,
a be Element of G;
F + a = (+a).:F by Th16;
hence thesis by TOPS_2:58;
end;
theorem Th46:
for G being BinContinuous TopaddGroup, F being closed Subset of G,
a being Element of G holds a + F is closed
proof
let G be BinContinuous TopaddGroup, F be closed Subset of G,
a be Element of G;
a + F = (a+).:F by Th15;
hence thesis by TOPS_2:58;
end;
registration
let G be BinContinuous TopaddGroup, F be closed Subset of G,
a be Element of G;
cluster F + a -> closed;
coherence by Th45;
cluster a + F -> closed;
coherence by Th46;
end;
theorem Th47:
for G being UnContinuous TopaddGroup, F being closed Subset of G
holds -F is closed
proof
let G be UnContinuous TopaddGroup, F be closed Subset of G;
-F = (add_inverse G).:F by Th9;
hence thesis by TOPS_2:58;
end;
registration
let G be UnContinuous TopaddGroup, F be closed Subset of G;
cluster -F -> closed;
coherence by Th47;
end;
theorem Th48:
for G being BinContinuous TopaddGroup, O being open Subset of G, a
being Element of G holds O + a is open
proof
let G be BinContinuous TopaddGroup, O be open Subset of G, a be Element of G;
O + a = (+a).:O by Th16;
hence thesis by TOPGRP_1:25;
end;
theorem Th49:
for G being BinContinuous TopaddGroup, O being open Subset of G, a
being Element of G holds a + O is open
proof
let G be BinContinuous TopaddGroup, O be open Subset of G, a be Element of G;
a + O = (a+).:O by Th15;
hence thesis by TOPGRP_1:25;
end;
registration
let G be BinContinuous TopaddGroup, A be open Subset of G, a be Element of G;
cluster A + a -> open;
coherence by Th48;
cluster a + A -> open;
coherence by Th49;
end;
theorem Th50:
for G being UnContinuous TopaddGroup, O being open Subset of G holds
-O is open
proof
let G be UnContinuous TopaddGroup, O be open Subset of G;
-O = (add_inverse G).:O by Th9;
hence thesis by TOPGRP_1:25;
end;
registration
let G be UnContinuous TopaddGroup, A be open Subset of G;
cluster -A -> open;
coherence by Th50;
end;
theorem Th51:
for G being BinContinuous TopaddGroup, A, O being Subset of G st O
is open holds O + A is open
proof
let G be BinContinuous TopaddGroup, A, O be Subset of G such that
A1: O is open;
Int (O + A) = O + A
proof
thus Int (O + A) c= O + A by TOPS_1:16;
let x be object;
assume x in O + A;
then consider o, a being Element of G such that
A2: x = o + a & o in O and
A3: a in A;
set Q = O + a;
A4: Q c= O + A
proof
let q be object;
assume q in Q;
then ex h being Element of G st q = h + a & h in O by Th28;
hence thesis by A3;
end;
x in Q by A2,Th28;
hence thesis by A1,A4,TOPS_1:22;
end;
hence thesis;
end;
theorem Th52:
for G being BinContinuous TopaddGroup, A, O being Subset of G st O
is open holds A + O is open
proof
let G be BinContinuous TopaddGroup, A, O be Subset of G such that
A1: O is open;
Int (A + O) = A + O
proof
thus Int (A + O) c= A + O by TOPS_1:16;
let x be object;
assume x in A + O;
then consider a, o being Element of G such that
A2: x = a + o and
A3: a in A and
A4: o in O;
set Q = a + O;
A5: Q c= A + O
proof
let q be object;
assume q in Q;
then ex h being Element of G st q = a + h & h in O by Th27;
hence thesis by A3;
end;
x in Q by A2,A4,Th27;
hence thesis by A1,A5,TOPS_1:22;
end;
hence thesis;
end;
registration
let G be BinContinuous TopaddGroup, A be open Subset of G, B be Subset of G;
cluster A + B -> open;
coherence by Th51;
cluster B + A -> open;
coherence by Th52;
end;
theorem Th53:
for G being UnContinuous TopaddGroup, a being Point of G, A being
a_neighborhood of a holds -A is a_neighborhood of -a
proof
let G be UnContinuous TopaddGroup, a be Point of G, A be a_neighborhood of a;
a in Int A by CONNSP_2:def 1;
then consider Q being Subset of G such that
A1: Q is open and
A2: Q c= A & a in Q by TOPS_1:22;
-Q c= -A & -a in -Q by A2,ThB8;
hence -a in Int (-A) by A1,TOPS_1:22;
end;
theorem Th54:
for G being TopologicaladdGroup, a being Point of G, A being
a_neighborhood of a + (-a) ex B being open a_neighborhood of a st
B + (-B) c= A
proof
let G be TopologicaladdGroup, a be Point of G, A be
a_neighborhood of a + (-a);
consider X, Y being open a_neighborhood of a such that
A1: X+ (-Y) c= A by Th40;
reconsider B = X /\ Y as open a_neighborhood of a by CONNSP_2:2;
take B;
let x be object;
assume x in B+ (-B);
then consider g, h being Point of G such that
A2: x = g+h and
A3: g in B and
A4: h in -B;
-h in B by A4,Th7;
then -h in Y by XBOOLE_0:def 4;
then
A5: h in -Y by Th7;
g in X by A3,XBOOLE_0:def 4;
then x in X + (-Y) by A2,A5;
hence thesis by A1;
end;
theorem Th55:
for G being UnContinuous TopaddGroup, A being dense Subset of G
holds -A is dense
proof
let G be UnContinuous TopaddGroup, A be dense Subset of G;
(add_inverse G)"A = -A by Th10;
hence thesis by TOPGRP_1:29;
end;
registration
let G be UnContinuous TopaddGroup, A be dense Subset of G;
cluster -A -> dense;
coherence by Th55;
end;
theorem Th56:
for G being BinContinuous TopaddGroup, A being dense Subset of G,
a being Point of G holds a+A is dense
proof
let G be BinContinuous TopaddGroup, A be dense Subset of G, a be Point of G;
(a+).:A = a+A by Th15;
hence thesis by TOPGRP_1:28;
end;
theorem Th57:
for G being BinContinuous TopaddGroup, A being dense Subset of G,
a being Point of G holds A+a is dense
proof
let G be BinContinuous TopaddGroup, A be dense Subset of G, a be Point of G;
(+a).:A = A+a by Th16;
hence thesis by TOPGRP_1:28;
end;
registration
let G be BinContinuous TopaddGroup, A be dense Subset of G, a be Point of G;
cluster A + a -> dense;
coherence by Th57;
cluster a + A -> dense;
coherence by Th56;
end;
theorem
for G being TopologicaladdGroup, B being Basis of 0_G,
M being dense Subset of G holds
{ V + x where V is Subset of G, x is Point of G: V in B & x in M }
is Basis of G
proof
let G be TopologicaladdGroup, B be Basis of 0_G, M be dense Subset of G;
set Z = { V + x where V is Subset of G, x is Point of G: V in B & x in M };
A1: Z c= the topology of G
proof
let a be object;
assume a in Z;
then consider V being Subset of G, x being Point of G such that
A2: a = V+x and
A3: V in B and
x in M;
reconsider V as Subset of G;
V is open by A3,YELLOW_8:12;
hence thesis by A2,PRE_TOPC:def 2;
end;
A4: for W being Subset of G st W is open for a being Point of G st a in W ex
V being Subset of G st V in Z & a in V & V c= W
proof
A5: 0_G + (- 0_G) = 0_G + 0_G by Th8
.= 0_G by Def4;
let W be Subset of G such that
A6: W is open;
let a be Point of G such that
A7: a in W;
0_G = a+(-a) by Def5;
then W +(-a) is a_neighborhood of 0_G + (- 0_G)
by A7,A6,A5,CONNSP_2:3,Th28;
then consider V being open a_neighborhood of 0_G such that
A8: V + (-V) c= W + (-a) by Th54;
consider E being Subset of G such that
A9: E in B and
A10: E c= V by CONNSP_2:4,YELLOW_8:13;
E is open & E <> {} by A9,YELLOW_8:12;
then consider d being object such that
A11: d in (a + (-M)) /\ E by XBOOLE_0:4,TOPS_1:45;
reconsider d as Point of G by A11;
take I = E+( (-d) +a);
d in a + (-M) by A11,XBOOLE_0:def 4;
then consider m being Point of G such that
A12: d = a+m and
A13: m in -M by Th27;
(-d)+a = (-d)+a+0_G by Def4
.= (-d)+a+(m+(-m)) by Def5
.= (-d)+a+m+(-m) by RLVECT_1:def 3
.= (-d)+d+(-m) by A12,RLVECT_1:def 3
.= 0_G+(-m) by Def5
.= (-m) by Def4;
then (-d)+a in M by A13,Th7;
hence I in Z by A9;
A14: 0_G+a = a by Def4;
A15: d in E by A11,XBOOLE_0:def 4;
E+(-d) c= V+(-V)
proof
let q be object;
assume q in E+(-d);
then
A16: ex v being Point of G st q = v+(-d) & v in E by Th28;
(-d) in (-V) by A10,A15;
hence thesis by A10,A16;
end;
then E + (-d) c= W + (-a) by A8;
then
A17: E + (-d) + a c= W + (-a) + a by Th5;
d+(-d) = 0_G by Def5;
then 0_G in E+(-d) by A15,Th28;
then a in E+(-d)+a by A14,Th28;
hence a in I by ThB34;
W +(-a)+a = W+(-a+a) by ThB34
.= W+0_G by Def5
.= W by Th37;
hence thesis by A17,ThB34;
end;
Z c= bool the carrier of G
proof
let a be object;
assume a in Z;
then
ex V being Subset of G, x being Point of G st a = V+x & V in B & x in M;
hence thesis;
end;
hence thesis by A1,A4,YELLOW_9:32;
end;
Th59:
for G being TopologicaladdGroup holds G is regular
proof
let G be TopologicaladdGroup;
ex p being Point of G st for A being Subset of G st A is open & p in A
holds ex B being Subset of G st p in B & B is open & Cl B c= A
proof
set e = 0_G;
take e;
let A be Subset of G;
assume A is open & e in A;
then e in Int A by TOPS_1:23;
then
A1: A is a_neighborhood of e by CONNSP_2:def 1;
e = e+ (-e) by Def5;
then consider
C being open a_neighborhood of e, B being open a_neighborhood of
(-e) such that
A2: C + B c= A by A1,Th36;
- -e = e;
then -B is a_neighborhood of e by Th53;
then reconsider W = C /\ (-B) as a_neighborhood of e by CONNSP_2:2;
-W c= - -B by ThB8,XBOOLE_1:17;
then
A3: C + (-W) c= C+B by Th4;
take W;
A4: Int W = W by TOPS_1:23;
hence e in W & W is open by CONNSP_2:def 1;
let p be object;
assume
A5: p in Cl W;
then reconsider r = p as Point of G;
r = r+e by Def4;
then p in r + W by A4,CONNSP_2:def 1,Th27;
then (r+W) meets W by A5,PRE_TOPC:def 7;
then consider a being object such that
A6: a in (r+W) /\ W by XBOOLE_0:4;
A7: a in W by A6,XBOOLE_0:def 4;
A8: a in r+W by A6,XBOOLE_0:def 4;
reconsider a as Point of G by A6;
consider b being Element of G such that
A9: a = r + b and
A10: b in W by A8,Th27;
A11: W c= C & -b in (- W) by A10,XBOOLE_1:17;
r = r + e by Def4
.= r + (b + (-b)) by Def5
.= a + (-b) by A9,RLVECT_1:def 3;
then p in C + (- W) by A7,A11;
hence thesis by A2,A3;
end;
hence thesis by TOPGRP_1:36;
end;
registration
cluster -> regular for TopologicaladdGroup;
coherence by Th59;
end;