Copyright (c) 1994 Association of Mizar Users
environ
vocabulary REALSET1, FINSEQ_1, GROUP_3, FUNCT_1, RLSUB_1, GROUP_2, RELAT_1,
GROUP_6, BINOP_1, BOOLE, QC_LANG1, WELLORD1, GROUP_1, VECTSP_1, GRAPH_1,
GRSOLV_1;
notation TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, XREAL_0, NAT_1, STRUCT_0,
BINOP_1, RELAT_1, FUNCT_1, FUNCT_2, RLVECT_1, GR_CY_1, VECTSP_1,
FINSEQ_1, GROUP_1, GROUP_2, GROUP_3, GROUP_6;
constructors DOMAIN_1, BINOP_1, GR_CY_1, GROUP_6, PARTFUN1, XCMPLX_0,
MEMBERED, XBOOLE_0;
clusters FUNCT_1, GROUP_1, GROUP_2, GROUP_3, GROUP_6, GR_CY_1, STRUCT_0,
RELSET_1, FINSEQ_1, ARYTM_3, MEMBERED, ZFMISC_1, XBOOLE_0;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
theorems FINSEQ_1, BINOP_1, GROUP_2, GROUP_3, TARSKI, GROUP_6, FINSEQ_2,
RLVECT_1, FUNCT_1, FUNCT_2, VECTSP_1, RELAT_1, XBOOLE_0, XBOOLE_1;
schemes MATRIX_2;
begin
reserve i,j,k for Nat;
definition let IT be Group;
attr IT is solvable means
:Def1:
ex F being FinSequence of Subgroups IT st len F>0 & F.1=(Omega).IT &
F.(len F)=(1).IT
& for i st i in dom F & i+1 in dom F
for G1,G2 being strict Subgroup of IT st G1=F.i & G2=F.(i+1) holds
G2 is strict normal Subgroup of G1 &
for N being normal Subgroup of G1 st N=G2 holds G1./.N is commutative;
end;
definition
cluster solvable strict Group;
existence
proof
consider G being Group;
take H=(1).G;
thus H is solvable
proof
<*H*> is FinSequence of Subgroups H
proof
rng <*H*> c=Subgroups H
proof
now let x be set;
assume A1:x in rng<*H*>;
rng <*H*> ={ H } by FINSEQ_1:56;
then x=H by A1,TARSKI:def 1;
then x is strict Subgroup of H by GROUP_2:63;
hence x in Subgroups H by GROUP_3:def 1;
end;
hence thesis by TARSKI:def 3;
end;
hence thesis by FINSEQ_1:def 4;
end;
then reconsider F=<*H*> as FinSequence of Subgroups H;
take F;
A2:len F=1 by FINSEQ_1:56;
A3:F.1=H by FINSEQ_1:57
.=(Omega).H by GROUP_2:def 8;
A4:F.(len F)=H by A2,FINSEQ_1:57
.=(1).H by GROUP_2:75;
for i st i in dom F & i+1 in dom F
for G1,G2 being Subgroup of H st G1=F.i & G2=F.(i+1) holds
G2 is normal Subgroup of G1 &
for N being normal Subgroup of G1 st N=G2 holds G1./.N is commutative
proof
let i;
assume A5:i in dom F & i+1 in dom F;
let G1,G2 be Subgroup of H;
assume G1=F.i & G2=F.(i+1);
dom F={1} by A2,FINSEQ_1:4,def 3;
then i=1 & i+1=1 by A5,TARSKI:def 1;
hence thesis;
end;
hence thesis by A2,A3,A4;
end;
thus thesis;
end;
end;
theorem
Th1:for G being strict Group for H,F1,F2 being strict Subgroup of G st
F1 is normal Subgroup of F2 holds F1 /\ H is normal Subgroup of F2 /\ H
proof
let G be strict Group;
let H,F1,F2 be strict Subgroup of G;
assume A1:F1 is normal Subgroup of F2;
then A2:F1 /\ H=(F1 /\ F2) /\ H by GROUP_2:107
.=F1 /\ (F2 /\ H) by GROUP_2:102;
reconsider F1 as normal Subgroup of F2 by A1;
reconsider F=F2 /\ H as Subgroup of F2 by GROUP_2:106;
F1/\F is normal Subgroup of F;
hence thesis by A2,GROUP_6:3;
end;
theorem
for G being strict Group for F2 being strict Subgroup of G
for F1 being strict normal Subgroup of F2
for a,b being Element of F2
holds (a*F1) *(b*F1)=a *b *F1
proof
let G be strict Group;
let F2 be strict Subgroup of G;
let F1 be strict normal Subgroup of F2;
let a,b be Element of F2;
A1:(nat_hom F1).a=(a*F1 ) by GROUP_6:def 9;
A2:(nat_hom F1).b=(b*F1 ) by GROUP_6:def 9;
A3:@((nat_hom F1).a)=(nat_hom F1).a by GROUP_6:def 6;
A4:@((nat_hom F1).b)=(nat_hom F1).b by GROUP_6:def 6;
thus a*b*F1 =(nat_hom F1).(a*b) by GROUP_6:def 9
.=((nat_hom F1).a) *((nat_hom F1).b) by GROUP_6:def 7
.=(a*F1 )*(b*F1) by A1,A2,A3,A4,GROUP_6:24;
end;
theorem
for G being strict Group for H,F2 being strict Subgroup of G
for F1 being strict normal Subgroup of F2 holds
for G2 being strict Subgroup of G st G2=H/\F2
for G1 being normal Subgroup of G2 st G1=H /\ F1
ex G3 being Subgroup of F2./.F1 st
G2./.G1, G3 are_isomorphic
proof
let G be strict Group;
let H,F2 be strict Subgroup of G;
let F1 be strict normal Subgroup of F2;
reconsider G2=H /\ F2 as strict Subgroup of G;
consider f being Function such that A1:f=(nat_hom F1)|(the carrier of H);
reconsider f1=nat_hom F1 as Function of
the carrier of F2,the carrier of F2./.F1;
A2:the carrier of F2=carr(F2) by GROUP_2:def 9;
A3:the carrier of H= carr(H) by GROUP_2:def 9;
A4:dom f1=the carrier of F2 by FUNCT_2:def 1;
then A5:dom f=(the carrier of F2) /\ (the carrier of H) by A1,RELAT_1:90
.=carr(F2/\ H) by A2,A3,GROUP_2:98
.= the carrier of (H /\ F2) by GROUP_2:def 9;
rng f c=the carrier of F2./.F1
proof
rng ((nat_hom F1)|(the carrier of H)) c=rng (nat_hom F1)
by FUNCT_1:76;
hence thesis by A1,XBOOLE_1:1;
end;
then reconsider f as Function of
the carrier of H/\F2,the carrier of F2./.F1 by A5,FUNCT_2:4;
for a,b being Element of H /\F2 holds f.(a * b) = f.a * f
.
b
proof
let a,b be Element of H /\F2;
the carrier of H /\F2=carr(H) /\ carr(F2) by GROUP_2:def 10;
then A6:a in carr(H) & a in carr(F2) & b in carr(H) & b in carr(F2)&
a*b in carr(H) & a*b in carr(F2) by XBOOLE_0:def 3;
then A7:a in the carrier of H & b in the carrier of H & a*b in the carrier
of H
by GROUP_2:def 9;
reconsider a'=a , b'=b as Element of F2 by A6,GROUP_2:def 9;
H /\ F2 is Subgroup of F2 by GROUP_2:106;
then A8:a*b=a' *b' by GROUP_2:52;
((nat_hom F1)|(the carrier of H)).a=(nat_hom F1).a &
((nat_hom F1)|(the carrier of H)).b=(nat_hom F1).b &
((nat_hom F1)|(the carrier of H)).(a*b)=(nat_hom F1).(a*b)
by A7,FUNCT_1:72;
hence thesis by A1,A8,GROUP_6:def 7;
end;
then reconsider f as Homomorphism of H/\F2,F2./.F1 by GROUP_6:def 7;
A9:(the carrier of H) /\ (the carrier of F2)
=carr(H/\ F2) by A2,A3,GROUP_2:98
.= the carrier of (H /\ F2) by GROUP_2:def 9;
A10:Ker f=H /\ F1
proof
reconsider L=Ker f as Subgroup of G by GROUP_2:65;
for g be Element of G holds g in L iff g in H /\ F1
proof
let x be Element of G;
thus x in L implies x in H /\ F1
proof
assume A11: x in L;
then x in carr(Ker f) by GROUP_2:88;
then reconsider a=x as Element of H/\F2;
the carrier of H /\F2=carr(H) /\ carr(F2) by GROUP_2:def 10;
then A12:a in carr(H) & a in carr(F2) by XBOOLE_0:def 3;
then A13:a in dom (nat_hom F1) & a in H by A4,GROUP_2:88,def 9;
a in the carrier of H by A12,GROUP_2:def 9;
then A14:((nat_hom F1)|(the carrier of H)).a=(nat_hom F1).a
by FUNCT_1:72;
reconsider a'=a as Element of F2 by A12,GROUP_2:def 9;
A15:f.a =1.(F2./.F1) by A11,GROUP_6:50
.=carr F1 by GROUP_6:29;
f.a= a' *F1 by A1,A14,GROUP_6:def 9;
then a' in F1 by A15,GROUP_2:136;
hence x in H /\ F1 by A13,GROUP_2:99;
end;
thus x in H /\ F1 implies x in L
proof
assume x in H /\ F1;
then x in carr(H /\F1) by GROUP_2:88;
then A16:x in the carrier of H /\ F1 by GROUP_2:def 9;
A17:the carrier of F1 c= the carrier of F2 by GROUP_2:def 5;
reconsider F1'=F1 as strict Subgroup of G;
A18:(the carrier of H) /\ (the carrier of F1)
=carr(H) /\ carr(F1') by A3,GROUP_2:def 9
.= the carrier of (H /\ F1) by GROUP_2:def 10;
then A19:x in the carrier of F1 by A16,XBOOLE_0:def 3;
the carrier of (H /\ F1) c= the carrier of (H /\ F2) by A9,A17,A18,
XBOOLE_1:26;
then reconsider a=x as Element of H/\F2 by A16;
a in carr(F1) by A19,GROUP_2:def 9;
then A20:a in F1 by GROUP_2:88;
the carrier of H /\F2=carr(H) /\ carr(F2) by GROUP_2:def 10;
then A21:a in carr(H) & a in carr(F2) by XBOOLE_0:def 3;
then a in the carrier of H by GROUP_2:def 9;
then A22:((nat_hom F1)|(the carrier of H)).a=(nat_hom F1).a
by FUNCT_1:72;
reconsider a'=a as Element of F2 by A21,GROUP_2:def 9;
f.a= a' *F1 by A1,A22,GROUP_6:def 9
.=carr F1 by A20,GROUP_2:136
.=1.(F2./.F1) by GROUP_6:29;
hence thesis by GROUP_6:50;
end;
end;
hence thesis by GROUP_2:def 6;
end;
reconsider G1=Ker f as strict normal Subgroup of G2;
G2 ./. G1,Image f are_isomorphic by GROUP_6:90;
hence thesis by A10;
end;
theorem
Th4:for G being strict Group for H,F2 being strict Subgroup of G
for F1 being strict normal Subgroup of F2 holds
for G2 being strict Subgroup of G st G2=F2/\H
for G1 being normal Subgroup of G2 st G1=F1/\H
ex G3 being Subgroup of F2./.F1 st
G2./.G1, G3 are_isomorphic
proof
let G be strict Group;
let H,F2 be strict Subgroup of G;
let F1 be strict normal Subgroup of F2;
reconsider G2=F2 /\ H as strict Subgroup of G;
consider f being Function such that A1:f=(nat_hom F1)|(the carrier of H);
reconsider f1=nat_hom F1 as Function of
the carrier of F2,the carrier of F2./.F1;
A2:the carrier of F2=carr(F2) by GROUP_2:def 9;
A3:the carrier of H= carr(H) by GROUP_2:def 9;
A4:dom f1=the carrier of F2 by FUNCT_2:def 1;
then A5:dom f=(the carrier of F2) /\ (the carrier of H) by A1,RELAT_1:90
.=the carrier of (F2 /\ H) by A2,A3,GROUP_2:def 10;
rng f c=the carrier of F2./.F1
proof
rng ((nat_hom F1)|(the carrier of H)) c=rng (nat_hom F1)
by FUNCT_1:76;
hence thesis by A1,XBOOLE_1:1;
end;
then reconsider f as Function of
the carrier of F2 /\ H,the carrier of F2./.F1 by A5,FUNCT_2:4;
for a,b being Element of F2 /\
H holds f.(a * b) = f.a * f.b
proof
let a,b be Element of F2 /\ H;
the carrier of F2 /\ H=carr(H) /\ carr(F2) by GROUP_2:def 10;
then A6:a in carr(H) & a in carr(F2) & b in carr(H) & b in carr(F2)&
a*b in carr(H) & a*b in carr(F2) by XBOOLE_0:def 3;
then A7:a in the carrier of H & b in the carrier of H & a*b in the carrier
of H
by GROUP_2:def 9;
reconsider a'=a, b'=b as Element of F2 by A6,GROUP_2:def 9;
F2 /\ H is Subgroup of F2 by GROUP_2:106;
then A8:a*b=a' *b' by GROUP_2:52;
((nat_hom F1)|(the carrier of H)).a=(nat_hom F1).a &
((nat_hom F1)|(the carrier of H)).b=(nat_hom F1).b &
((nat_hom F1)|(the carrier of H)).(a*b)=(nat_hom F1).(a*b)
by A7,FUNCT_1:72;
hence thesis by A1,A8,GROUP_6:def 7;
end;
then reconsider f as Homomorphism of F2 /\ H,F2./.F1 by GROUP_6:def 7;
A9:(the carrier of H) /\ (the carrier of F2)
=carr(F2 /\ H) by A2,A3,GROUP_2:98
.= the carrier of (F2 /\ H) by GROUP_2:def 9;
A10:Ker f=F1 /\ H
proof
reconsider L=Ker f as Subgroup of G by GROUP_2:65;
for g be Element of G holds g in L iff g in F1 /\ H
proof
let x be Element of G;
thus x in L implies x in F1 /\ H
proof
assume A11: x in L;
then x in carr(Ker f) by GROUP_2:88;
then reconsider a=x as Element of F2 /\ H;
the carrier of F2 /\ H=carr(H) /\ carr(F2) by GROUP_2:def 10;
then A12:a in carr(H) & a in carr(F2)
by XBOOLE_0:def 3;
then A13:a in dom (nat_hom F1) & a in H by A4,GROUP_2:88,def 9;
a in the carrier of H by A12,GROUP_2:def 9;
then A14:((nat_hom F1)|(the carrier of H)).a=(nat_hom F1).a
by FUNCT_1:72;
reconsider a'=a as Element of F2 by A12,GROUP_2:def 9;
A15:f.a =1.(F2./.F1) by A11,GROUP_6:50
.=carr F1 by GROUP_6:29;
f.a= a' *F1 by A1,A14,GROUP_6:def 9;
then a' in F1 by A15,GROUP_2:136;
hence x in F1 /\ H by A13,GROUP_2:99;
end;
thus x in F1 /\ H implies x in L
proof
assume x in F1 /\ H;
then x in carr(F1 /\ H) by GROUP_2:88;
then A16:x in the carrier of F1 /\ H by GROUP_2:def 9;
A17:the carrier of F1 c= the carrier of F2 by GROUP_2:def 5;
reconsider F1'=F1 as strict Subgroup of G;
A18:(the carrier of H) /\ (the carrier of F1)
=carr(H) /\ carr(F1') by A3,GROUP_2:def 9
.= the carrier of (F1 /\ H) by GROUP_2:def 10;
then A19:x in the carrier of F1 by A16,XBOOLE_0:def 3;
the carrier of (F1 /\ H) c= the carrier of (F2 /\ H) by A9,A17,A18,
XBOOLE_1:26;
then reconsider a=x as Element of F2 /\ H by A16;
a in carr(F1) by A19,GROUP_2:def 9;
then A20:a in F1 by GROUP_2:88;
the carrier of F2 /\ H=carr(H) /\ carr(F2) by GROUP_2:def 10;
then A21:a in carr(H) & a in carr(F2)
by XBOOLE_0:def 3;
then a in the carrier of H by GROUP_2:def 9;
then A22:((nat_hom F1)|(the carrier of H)).a=(nat_hom F1).a
by FUNCT_1:72;
reconsider a'=a as Element of F2 by A21,GROUP_2:def 9;
f.a= a' *F1 by A1,A22,GROUP_6:def 9
.=carr F1 by A20,GROUP_2:136
.=1.(F2./.F1) by GROUP_6:29;
hence thesis by GROUP_6:50;
end;
end;
hence thesis by GROUP_2:def 6;
end;
reconsider G1=Ker f as strict normal Subgroup of G2;
G2 ./. G1,Image f are_isomorphic by GROUP_6:90;
hence thesis by A10;
end;
theorem
for G being solvable strict Group for H being strict Subgroup of G holds
H is solvable
proof
let G be solvable strict Group;
let H be strict Subgroup of G;
consider F being FinSequence of Subgroups G such that
A1:len F>0 & F.1=(Omega).G & F.(len F)=(1).G &
for i st i in dom F & i+1 in dom F
for G1,G2 being strict Subgroup of G st G1=F.i & G2=F.(i+1) holds
G2 is strict normal Subgroup of G1 &
for N being normal Subgroup of G1 st N=G2 holds G1./.N is commutative
by Def1;
defpred P[set,set] means ex I being strict Subgroup of G st I=F.$1 &
$2=I /\ H;
A2:for k st k in Seg len F ex x being Element of Subgroups H st P[k,x]
proof
let k;
assume k in Seg len F;
then k in dom F by FINSEQ_1:def 3;
then F.k in Subgroups G by FINSEQ_2:13;
then reconsider I=F.k as strict Subgroup of G by GROUP_3:def 1;
reconsider x=I /\ H as strict Subgroup of H by GROUP_2:106;
reconsider y=x as Element of Subgroups H by GROUP_3:def 1;
take y;take I;
thus thesis;
end;
consider R being FinSequence of Subgroups H such that
A3:dom R=Seg len F &
for i st i in Seg len F holds P[i,R.i] from SeqDEx(A2);
A4:len R=len F by A3,FINSEQ_1:def 3;
A5:len R >0 by A1,A3,FINSEQ_1:def 3;
A6:R.1=(Omega).H
proof
1<=len R by A5,RLVECT_1:99;
then 1 in Seg len F by A4,FINSEQ_1:3;
then consider I being strict Subgroup of G such that A7:I=F.1 &
R.1=I /\ H by A3;
thus R.1= H by A1,A7,GROUP_2:104
.= (Omega).H by GROUP_2:def 8;
end;
A8:R.(len R)= (1).H
proof
len R in Seg len F by A1,A4,FINSEQ_1:5;
then consider I being strict Subgroup of G such that
A9:I=F.(len R) & R.(len R)=I /\ H by A3;
thus R.(len R)=(1).G by A1,A4,A9,GROUP_2:103
.=(1).H by GROUP_2:75;
end;
A10: for i st i in dom R & i+1 in dom R
for H1,H2 being strict Subgroup of H st H1=R.i & H2=R.(i+1) holds
H2 is strict normal Subgroup of H1 &
for N being normal Subgroup of H1 st N=H2 holds H1./.N is commutative
proof
let i;
assume A11: i in dom R & i+1 in dom R;
let H1,H2 be strict Subgroup of H;
assume A12: H1=R.i & H2=R.(i+1);
consider I being strict Subgroup of G such that
A13:I=F.i & R.i=I /\ H by A3,A11;
consider J being strict Subgroup of G such that
A14:J=F.(i+1) & R.(i+1)=J /\ H by A3,A11;
A15:i in dom F & i+1 in dom F by A3,A11,FINSEQ_1:def 3;
then reconsider J1=J as strict normal Subgroup of I by A1,A13,A14;
A16:H1=I /\ H & H2=J1/\H by A12,A13,A14;
for N being strict normal Subgroup of H1 st N=H2 holds
H1./.N is commutative
proof
let N be strict normal Subgroup of H1;
assume N=H2;
then consider G3 being Subgroup of I./.J1 such that
A17:H1 ./. N, G3 are_isomorphic by A12,A13,A14,Th4;
consider h being Homomorphism of H1./. N ,G3
such that A18:h is_isomorphism by A17,GROUP_6:def 15;
A19:h is_epimorphism & h is_monomorphism by A18,GROUP_6:def 14;
I ./.J1 is commutative by A1,A13,A14,A15;
then A20:G3 is commutative by GROUP_2:62;
H1./.N is commutative
proof
now let a,b be Element of H1./.N;
consider a' being Element of G3 such that
A21:a'=h.a;
consider b' being Element of G3 such that
A22:b'=h.b;
A23:the mult of G3 is commutative by A20,GROUP_3:2;
A24:a'*b'=(the mult of G3).(a',b') by VECTSP_1:def 10
.=(the mult of G3).(b',a') by A23,BINOP_1:def 2
.=b'*a' by VECTSP_1:def 10;
thus (the mult of H1./.N).(a,b)=a*b by VECTSP_1:def 10
.=h".(h.(a*b)) by A19,GROUP_6:64
.=h".(h.b*h.a) by A21,A22,A24,GROUP_6:def 7
.=h".(h.(b*a)) by GROUP_6:def 7
.=b*a by A19,GROUP_6:64
.=(the mult of H1./.N).(b,a) by VECTSP_1:def 10;
end;
then the mult of (H1./.N) is commutative by BINOP_1:def 2;
hence thesis by GROUP_3:2;
end;
hence thesis;
end;
hence thesis by A16,Th1;
end;
take R;
thus thesis by A1,A3,A6,A8,A10,FINSEQ_1:def 3;
end;
theorem
for G being strict Group st
ex F being FinSequence of Subgroups G st
len F>0 & F.1=(Omega).G & F.(len F)=(1).G &
for i st i in dom F & i+1 in dom F
for G1,G2 being strict Subgroup of G st G1=F.i & G2=F.(i+1) holds
G2 is strict normal Subgroup of G1 &
for N being normal Subgroup of G1 st N=G2 holds G1./.N is cyclic Group
holds G is solvable
proof
let G be strict Group;
given F being FinSequence of Subgroups G such that
A1:len F>0 & F.1=(Omega).G & F.(len F)=(1).G &
for i st i in dom F & i+1 in dom F
for G1,G2 being strict Subgroup of G st G1=F.i & G2=F.(i+1) holds
G2 is strict normal Subgroup of G1 & for N being normal Subgroup of G1
st N=G2 holds G1./.N is cyclic Group;
take F;
thus thesis by A1;
end;
theorem
for G being strict commutative Group holds G is strict solvable
proof
let G be strict commutative Group;
(Omega).G in Subgroups G & (1).G in Subgroups G by GROUP_3:def 1;
then <*(Omega).G,(1).G*>is FinSequence of Subgroups G by FINSEQ_2:15;
then consider F being FinSequence of Subgroups G such that
A1:F=<*(Omega).G,(1).G*>;
A2:len F=2 & F.1=(Omega).G & F.2=(1).G by A1,FINSEQ_1:61;
for i st i in dom F & i+1 in dom F
for G1,G2 being strict Subgroup of G st G1=F.i & G2=F.(i+1) holds
G2 is strict normal Subgroup of G1 &
for N being normal Subgroup of G1 st N=G2 holds G1./.N is commutative
proof
let i;
assume A3:i in dom F & i+1 in dom F;
now let G1,G2 be strict Subgroup of G;
assume A4: G1=F.i & G2=F.(i+1);
A5: dom F={1,2} by A2,FINSEQ_1:4,def 3;
A6:i in {1,2} & i+1 in{1,2}by A2,A3,FINSEQ_1:4,def 3;
A7:i=1 or i=2 by A3,A5,TARSKI:def 2;
for N being normal Subgroup of G1 st
N=G2 holds G1./.N is commutative
proof
let N be normal Subgroup of G1;
assume N=G2;
then N=(1).G1 by A2,A4,A6,A7,GROUP_2:75,TARSKI:def 2;
then G1,G1./.N are_isomorphic by GROUP_6:82;
hence G1./.N is commutative by GROUP_6:89;
end;
hence G2 is strict normal Subgroup of G1 &
for N being normal Subgroup of G1 st
N=G2 holds G1./.N is commutative by A2,A4,A6,A7,GROUP_2:78,GROUP_6:9,TARSKI
:def 2;
end;
hence thesis;
end;
hence thesis by A2,Def1;
end;
definition let G,H be strict Group;
let g be Homomorphism of G,H; let A be Subgroup of G;
func g|A -> Homomorphism of A,H equals
:Def2: g|(the carrier of A);
coherence
proof
A1:the carrier of A c= the carrier of G by GROUP_2:def 5;
then reconsider f=g|(the carrier of A) as
Function of the carrier of A,the carrier of H by FUNCT_2:38;
f is Homomorphism of A,H
proof
now let a,b be Element of A;
A2:a is Element of G &
b is Element of G by A1,TARSKI:def 3;
A3:(the mult of G).(a,b)=a*b
proof
reconsider a'=a as Element of G by A1,TARSKI:def 3;
reconsider b'=b as Element of G by A1,TARSKI:def 3;
thus (the mult of G).(a,b)=a'* b' by VECTSP_1:def 10
.=a*b by GROUP_2:52;
end;
A4:f.a=g.a & f.b=g.b by FUNCT_1:72;
A5: for a,b being Element of G holds
(the mult of H).(g.a , g.b)=g.((the mult of G).(a,b))
proof
let a,b be Element of G;
thus (the mult of H).(g.a , g.b)=g.a * g.b by VECTSP_1:def 10
.=g.(a*b) by GROUP_6:def 7
.=g.((the mult of G).(a,b)) by VECTSP_1:def 10
;
end;
thus f.a * f.b =
(the mult of H).((g|(the carrier of A)).a, (g|(the carrier of A)).b) by
VECTSP_1:def 10
.=g.((the mult of G).(a,b))by A2,A4,A5
.= f.(a * b) by A3,FUNCT_1:72;
end;
hence f is Homomorphism of A,H by GROUP_6:def 7;
end;
hence thesis;
end;
end;
definition let G,H be strict Group;
let g be Homomorphism of G,H;let A be Subgroup of G;
func g.:A -> strict Subgroup of H equals
:Def3: Image (g| A);
correctness;
end;
theorem
Th8: for G,H being strict Group, g being Homomorphism of G,H
for A being Subgroup of G holds
rng (g|A)=g.:(the carrier of A)
proof
let G,H be strict Group;let g be Homomorphism of G,H;
let A be Subgroup of G;
thus rng (g|A)= rng (g| (the carrier of A)) by Def2
.=g.:(the carrier of A) by RELAT_1:148;
end;
theorem
Th9: for G,H being strict Group, g being Homomorphism of G,H
for A being strict Subgroup of G holds
the carrier of (g.: A)=g.:(the carrier of A)
proof
let G,H be strict Group;let g be Homomorphism of G,H;
let A be strict Subgroup of G;
thus the carrier of (g.: A)=the carrier of Image (g| A) by Def3
.=rng (g|A) by GROUP_6:53
.=g.:(the carrier of A) by Th8;
end;
theorem
Th10: for G,H being strict Group, h being Homomorphism of G,H holds
for A being strict Subgroup of G holds
Image(h|A) is strict Subgroup of Image h
proof
let G,H be strict Group;
let h be Homomorphism of G,H;
let A be strict Subgroup of G;
A1:the carrier of A c= the carrier of G by GROUP_2:def 5;
A2:the carrier of Image (h|A)=rng (h|A) by GROUP_6:53
.=h.:(the carrier of A) by Th8;
h.:(the carrier of G) = the carrier of Image h by GROUP_6:def 11;
then the carrier of Image (h|A)c=the carrier of Image h by A1,A2,RELAT_1:
156;
hence thesis by GROUP_2:66;
end;
theorem
Th11: for G,H being strict Group, h being Homomorphism of G,H holds
for A being strict Subgroup of G holds h.:A is strict Subgroup of Image h
proof
let G,H be strict Group;
let h be Homomorphism of G,H;
let A be strict Subgroup of G;
Image(h|A) is strict Subgroup of Image h by Th10;
then A1:the carrier of Image (h|A)c=the carrier of Image h by GROUP_2:def 5
;
the carrier of h.:(A)=the carrier of Image (h| A) by Def3;
hence h.:(A) is strict Subgroup of Image h by A1,GROUP_2:66;
end;
theorem
Th12: for G,H being strict Group, h being Homomorphism of G,H holds
h.:((1).G)=(1).H & h.:((Omega).G)=(Omega).(Image h)
proof
let G,H be strict Group;
let h be Homomorphism of G,H;
A1: dom h=the carrier of G by FUNCT_2:def 1;
A2:the carrier of (1).G={1.G} by GROUP_2:def 7;
A3:the carrier of (1).H={1.H} by GROUP_2:def 7;
the carrier of h.:((1).G)=h.:({1.G}) by A2,Th9
.={h.(1.G)} by A1,FUNCT_1:117
.= the carrier of (1).H by A3,GROUP_6:40;
hence h.:((1).G)= (1).H by GROUP_2:68;
A4:(Omega).(Image h)=the HGrStr of Image h by GROUP_2:def 8;
the carrier of (Omega).G=the carrier of G by GROUP_2:def 8;
then the carrier of h.:((Omega).G)=h.:(the carrier of G) by Th9
.=the carrier of (Omega).(Image h) by A4,GROUP_6:def 11;
hence h.:((Omega).G)=(Omega).(Image h) by A4,GROUP_2:68;
end;
theorem
Th13:for G,H being strict Group, h being Homomorphism of G,H
for A,B being strict Subgroup of G holds
A is Subgroup of B implies
h.:A is Subgroup of h.:B
proof
let G,H be strict Group;let h be Homomorphism of G,H;
let A,B be strict Subgroup of G;
assume A is Subgroup of B;
then the carrier of A c= the carrier of B by GROUP_2:def 5;
then A1:h.:(the carrier of A)c= h.:(the carrier of B ) by RELAT_1:156;
the carrier of h.:B= h.:(the carrier of B) by Th9;
then the carrier of h.:A c= the carrier of h.:B by A1,Th9;
hence h.:A is Subgroup of h.:B by GROUP_2:66;
end;
theorem
Th14:for G,H being strict Group, h being Homomorphism of G,H
for A being strict Subgroup of G for a being Element of G
holds
h.a* h.:A=h.:(a*A) & h.:A * h.a=h.:(A*a)
proof
let G,H be strict Group;
let h be Homomorphism of G,H;
let A be strict Subgroup of G;
let a be Element of G;
now let x be set;
assume x in h.a *h.:A;
then consider b1 being Element of H such that
A1:x = h.a * b1 & b1 in h.:A
by GROUP_2:125;
b1 in Image(h |A) by A1,Def3;
then consider b being Element of A such that
A2: b1=(h|A).b by GROUP_6:54;
A3:b in A by RLVECT_1:def 1;
reconsider b as Element of G by GROUP_2:51;
b1=(h|(the carrier of A)).b by A2,Def2
.=h.b by FUNCT_1:72;
then A4:x=h.(a*b) by A1,GROUP_6:def 7;
a* b in a*A by A3,GROUP_2:125;
hence x in h.:(a*A) by A4,FUNCT_2:43;
end;
then A5:h.a *h.:A c= h.:(a * A) by TARSKI:def 3;
now let x be set;
assume x in h.:(a *A);
then consider y being set such that
A6:y in the carrier of G & y in a*A & x = h.y by FUNCT_2:115;
reconsider y as Element of G by A6;
consider b being Element of G such that
A7:y=a* b & b in A by A6,GROUP_2:125;
A8:b in the carrier of A by A7,RLVECT_1:def 1;
A9:x=h.a *h.b by A6,A7,GROUP_6:def 7;
h.b in h.:(the carrier of A) by A8,FUNCT_2:43;
then h.b in the carrier of h.: A by Th9;
then h.b in h.:A by RLVECT_1:def 1;
hence x in h.a * h.:A by A9,GROUP_2:125;
end;
then h.:(a * A) c= h.a *h.:A by TARSKI:def 3;
hence h.a *h.:A = h.:(a * A) by A5,XBOOLE_0:def 10;
now let x be set;
assume x in h.:A*h.a;
then consider b1 being Element of H such that
A10:x = b1*h.a & b1 in h.:A
by GROUP_2:126;
b1 in Image(h |A) by A10,Def3;
then consider b being Element of A such that
A11: b1=(h|A).b by GROUP_6:54;
A12:b in A by RLVECT_1:def 1;
reconsider b as Element of G by GROUP_2:51;
b1=(h|(the carrier of A)).b by A11,Def2
.=h.b by FUNCT_1:72;
then A13:x=h.(b*a) by A10,GROUP_6:def 7;
b* a in A*a by A12,GROUP_2:126;
hence x in h.:(A*a) by A13,FUNCT_2:43;
end;
then A14:h.:A*h.a c= h.:(A* a) by TARSKI:def 3;
now let x be set;
assume x in h.:(A* a);
then consider y being set such that
A15:y in the carrier of G & y in A* a & x = h.y by FUNCT_2:115;
reconsider y as Element of G by A15;
consider b being Element of G such that
A16:y=b* a & b in A by A15,GROUP_2:126;
A17:b in the carrier of A by A16,RLVECT_1:def 1;
A18:x=h.b *h.a by A15,A16,GROUP_6:def 7;
h.b in h.:(the carrier of A) by A17,FUNCT_2:43;
then h.b in the carrier of h.: A by Th9;
then h.b in h.:A by RLVECT_1:def 1;
hence x in h.:A*h.a by A18,GROUP_2:126;
end;
then h.:(A*a) c= h.:A*h.a by TARSKI:def 3;
hence h.:A*h.a = h.:(A * a) by A14,XBOOLE_0:def 10;
end;
theorem
Th15:for G,H being strict Group, h being Homomorphism of G,H
for A,B being Subset of G holds
h.:A* h.:B=h.:(A*B)
proof
let G,H be strict Group, h be Homomorphism of G,H;
let A,B be Subset of G;
now let z be set;
assume z in h.:(A)*h.:(B);
then consider z1,z2 being Element of H such that
A1: z=z1 *z2 &
z1 in h.:(A) & z2 in h.:(B) by GROUP_2:12;
consider z3 being set such that
A2:z3 in the carrier of G & z3 in A & z1=h.z3 by A1,FUNCT_2:115;
consider z4 being set such that
A3:z4 in the carrier of G & z4 in B & z2=h.z4 by A1,FUNCT_2:115;
reconsider z3 as Element of G by A2;
reconsider z4 as Element of G by A3;
A4:z=h.(z3* z4) by A1,A2,A3,GROUP_6:def 7;
z3 * z4 in (A) *(B) by A2,A3,GROUP_2:12;
hence z in h.:((A) *(B)) by A4,FUNCT_2:43;
end;
then A5: h.:(A)*h.:(B)c= h.:((A) *(B)) by TARSKI:def 3;
now let z be set;
assume z in h.:((A) *(B));
then consider x being set such that
A6:x in the carrier of G & x in (A)*(B) & z=h.x by FUNCT_2:115;
reconsider x as Element of G by A6;
consider z1,z2 being Element of G such that
A7: x=z1 *z2 & z1 in(A)& z2 in (B) by A6,GROUP_2:12;
A8:z=h.z1 * h.z2 by A6,A7,GROUP_6:def 7;
h.z1 in h.:(A)& h.z2 in h.:(B) by A7,FUNCT_2:43;
hence z in h.:(A)* h.:(B) by A8,GROUP_2:12;
end;
then h.:((A) *(B)) c=h.:(A)*h.:(B) by TARSKI:def 3;
hence h.:(A)*h.:(B) = h.:((A) *(B)) by A5,XBOOLE_0:def 10;
end;
theorem
Th16:for G,H being strict Group, h being Homomorphism of G,H
for A,B being strict Subgroup of G holds
A is strict normal Subgroup of B implies
h.:A is strict normal Subgroup of h.:B
proof
let G,H be strict Group;
let h be Homomorphism of G,H;
let A,B be strict Subgroup of G;
assume A is strict normal Subgroup of B;
then reconsider A1=A as strict normal Subgroup of B;
reconsider C=h.:A1 as strict Subgroup of h.:B by Th13;
for b2 being Element of h.:B holds b2* C c= C * b2
proof
let b2 be Element of h.:B;
b2 in h.:B by RLVECT_1:def 1;
then A1:b2 in Image(h |B) by Def3;
now let x be set;
assume A2:x in b2* C;
consider b1 being Element of B such that
A3: b2=(h|B).b1 by A1,GROUP_6:54;
reconsider b1 as Element of G by GROUP_2:51;
A4:b2=(h|(the carrier of B)).b1 by A3,Def2
.=h.b1 by FUNCT_1:72;
consider g being Element of h.:B such that
A5:x = b2 * g & g in C
by A2,GROUP_2:125;
g in Image (h|A1) by A5,Def3;
then consider g1 being Element of A1 such that
A6: g=(h|A1).g1 by GROUP_6:54;
reconsider g1 as Element of G by GROUP_2:51;
A7:g1 in A1 by RLVECT_1:def 1;
g=(h|(the carrier of A1)).g1 by A6,Def2
.=h.g1 by FUNCT_1:72;
then A8:x =h.b1 * h.g1 by A4,A5,GROUP_2:52
.=h.(b1 *g1) by GROUP_6:def 7;
A9:b1 * g1 in b1 * A1 by A7,GROUP_2:125;
reconsider b=b1 as Element of B;
b1 * A1=b * A1 by GROUP_6:2
.=A1 * b by GROUP_3:140
.=A1 * b1 by GROUP_6:2;
then A10:x in h.:(A1 *b1) by A8,A9,FUNCT_2:43;
h.:(A1 * b1) = h.:A1 * h.b1 by Th14;
hence x in C* b2 by A4,A10,GROUP_6:2;
end;
hence b2* C c= C * b2 by TARSKI:def 3;
end;
hence thesis by GROUP_3:141;
end;
theorem
for G,H being strict Group, h being Homomorphism of G,H holds
G is solvable Group implies Image h is solvable
proof
let G,H be strict Group;let h be Homomorphism of G,H;
assume G is solvable Group;
then consider F being FinSequence of Subgroups G such that
A1:len F>0 & F.1=(Omega).G & F.(len F)=(1).G &
for i st i in dom F & i+1 in dom F
for G1,G2 being strict Subgroup of G st G1=F.i & G2=F.(i+1) holds
G2 is strict normal Subgroup of G1 &
for N being normal Subgroup of G1 st N=G2 holds G1./.N is commutative
by Def1;
defpred P[set,set] means
ex J being strict Subgroup of G st J= F.$1 & $2 =h.:(J);
A2:for k st k in Seg len F
ex x being Element of Subgroups Image h st P[k,x]
proof
let k;
assume k in Seg len F;
then k in dom F by FINSEQ_1:def 3;
then F.k in Subgroups G by FINSEQ_2:13;
then F.k is strict Subgroup of G by GROUP_3:def 1;
then consider A being strict Subgroup of G
such that A3: A=F.k;
h.:(A) is strict Subgroup of Image h by Th11;
then h.:(A) in Subgroups Image h by GROUP_3:def 1;
then consider x being Element of Subgroups Image h such that
A4:x=h.:(A);
thus thesis by A3,A4;
end;
consider z being FinSequence of Subgroups Image h such that
A5:dom z = Seg len F & for j st j in Seg len F holds P[j,z.j]
from SeqDEx(A2);
A6: Seg len z=Seg len F by A5,FINSEQ_1:def 3;
A7:len z= len F by A5,FINSEQ_1:def 3;
A8:dom F=Seg len z by A6,FINSEQ_1:def 3
.=dom z by FINSEQ_1:def 3;
1<=1 &1 <= len F by A1,RLVECT_1:99;
then A9:1 in Seg len F by FINSEQ_1:3;
A10:z.1=(Omega).(Image h) & z.(len z)=(1).(Image h)
proof
consider A being strict Subgroup of G such that
A11:A=F.1 & z.1=h.:(A) by A5,A9;
thus z.1=(Omega).(Image h) by A1,A11,Th12;
len F in Seg len F by A1,FINSEQ_1:5;
then consider B being strict Subgroup of G such that
A12:B=F.(len F) & z.(len F)=h.:(B) by A5;
thus z.(len z)=(1).H by A1,A7,A12,Th12
.=(1).(Image h) by GROUP_2:75;
end;
A13:for i st i in dom z & i+1 in dom z
for G1,G2 being strict Subgroup of Image h st G1=z.i & G2=z.(i+1) holds
G2 is strict normal Subgroup of G1 &
for N being normal Subgroup of G1 st N=G2 holds G1./.N is commutative
proof
let i;
assume A14:i in dom z & i+1 in dom z;
let G1,G2 be strict Subgroup of Image h;
assume A15: G1=z.i & G2=z.(i+1);
then consider A being strict Subgroup of G such that A16:A=F.i & G1=h.:A
by A5,A14;
consider B being strict Subgroup of G such that A17:B=F.(i+1) & G2=h.:B
by A5,A14,A15;
A18:B is strict normal Subgroup of A by A1,A8,A14,A16,A17;
for N being normal Subgroup of G1 st N=G2 holds G1./.N is commutative
proof
let N be normal Subgroup of G1;
assume A19:N=G2;
now let x,y be Element of G1./.N;
A20:x in G1./.N & y in G1./.N by RLVECT_1:def 1;
x in the carrier of G1./.N & y in the carrier of G1./.N;
then A21:x in Cosets N & y in Cosets N by GROUP_6:22;
consider a being Element of G1 such that
A22:x= a* N & x=N* a by A20,GROUP_6:28;
consider b being Element of G1 such that
A23:y= b* N & y=N* b by A20,GROUP_6:28;
reconsider x1=x as Subset of G1 by A21,GROUP_6:17;
reconsider y1=y as Subset of G1 by A21,GROUP_6:17;
a in h.:A & b in h.:A by A16,RLVECT_1:def 1;
then A24:a in Image (h|A)& b in Image (h|A) by Def3;
then consider a1 being Element of A such that
A25: a=(h|A).a1 by GROUP_6:54;
consider b1 being Element of A such that
A26: b=(h|A).b1 by A24,GROUP_6:54;
reconsider a1 as Element of G by GROUP_2:51;
reconsider b1 as Element of G by GROUP_2:51;
A27:a=(h|(the carrier of A)).a1 by A25,Def2
.=h.a1 by FUNCT_1:72;
A28:b=(h|(the carrier of A)).b1 by A26,Def2
.=h.b1 by FUNCT_1:72;
A29:a * N= h.a1 * h.:B by A17,A19,A27,GROUP_6:2
.=h.:(a1*B) by Th14;
A30:b * N= h.b1 * h.:B by A17,A19,A28,GROUP_6:2
.=h .:(b1 *B ) by Th14;
reconsider x2=h.:(a1 *B) as Subset of G1 by A29;
reconsider y2=h.:(b1 *B) as Subset of G1 by A30;
A31:h.:(a1*B)*h.:(b1 * B)=h.:((a1 *B)*(b1 *B)) by Th15;
A32:x2*y2 =h.:(a1*B)* h.:(b1*B)
proof
now let z be set;
assume z in x2*y2;
then consider z1,z2 being Element of G1 such that
A33: z=z1 *z2 &
z1 in x2 & z2 in y2 by GROUP_2:12;
reconsider z11=z1 as Element of H by A33;
reconsider z22=z2 as Element of H by A33;
z=z11 * z22 by A33,GROUP_2:52;
hence z in h.:(a1 *B) *h.:(b1 * B) by A33,GROUP_2:12;
end;
then A34:x2 * y2 c= h.:(a1 *B) *h.:(b1 * B) by TARSKI:def 3;
now let z be set;
assume z in h.:(a1 *B) *h.:(b1 * B);
then consider x being set such that A35:x in the carrier of G
& x in (a1*B)*(b1*B) & z=h.x by A31,FUNCT_2:115;
reconsider x as Element of G by A35;
consider z1,z2 being Element of G such that
A36: x=z1 *z2 & z1 in(a1*B)& z2 in (b1*B) by A35,GROUP_2:12;
A37:h.z1 in x2 & h.z2 in y2 by A36,FUNCT_2:43;
then reconsider z11=h.z1 as Element of G1;
reconsider z22=h.z2 as Element of G1 by A37;
z=h.z1 * h.z2 by A35,A36,GROUP_6:def 7
.=z11 *z22 by GROUP_2:52;
hence z in x2* y2 by A37,GROUP_2:12;
end;
then h.:(a1 *B) *h.:(b1 * B) c= x2 * y2 by TARSKI:def 3;
hence x2 * y2 = h.:(a1 *B) *h.:(b1 * B) by A34,XBOOLE_0:def 10;
end;
A38:h.:(b1*B)*h.:(a1 * B)=h.:((b1 *B)*(a1 *B)) by Th15;
A39:y2*x2 =h.:(b1*B)* h.:(a1*B)
proof
now
let z be set;
assume z in y2*x2;
then consider z1,z2 being Element of G1 such that
A40: z=z1 *z2 &
z1 in y2 & z2 in x2 by GROUP_2:12;
reconsider z11=z1 as Element of H by A40;
reconsider z22=z2 as Element of H by A40;
z=z11 * z22 by A40,GROUP_2:52;
hence z in h.:(b1 *B) *h.:(a1 * B) by A40,GROUP_2:12;
end;
then A41:y2*x2 c= h.:(b1 *B) *h.:(a1 * B) by TARSKI:def 3;
now
let z be set;
assume z in h.:(b1 *B) *h.:(a1 * B);
then consider x being set such that A42:x in the carrier of G
& x in (b1*B)*(a1*B) & z=h.x by A38,FUNCT_2:115;
reconsider x as Element of G by A42;
consider z1,z2 being Element of G such that
A43: x=z1 *z2 & z1 in(b1*B)& z2 in (a1*B) by A42,GROUP_2:12;
A44:h.z1 in y2 & h.z2 in x2 by A43,FUNCT_2:43;
then reconsider z11=h.z1 as Element of G1;
reconsider z22=h.z2 as Element of G1 by A44;
z=h.z1 * h.z2 by A42,A43,GROUP_6:def 7
.=z11 *z22 by GROUP_2:52;
hence z in y2*x2 by A44,GROUP_2:12;
end;
then h.:(b1 *B) *h.:(a1 * B) c= y2*x2 by TARSKI:def 3;
hence y2*x2 = h.:(b1 *B) *h.:(a1 * B) by A41,XBOOLE_0:def 10;
end;
A45:(a1*B)*(b1*B)=(b1 *B)*(a1*B)
proof
reconsider K=B as normal Subgroup of A by A1,A8,A14,A16,A17;
reconsider a2=a1 ,b2=b1 as Element of A;
A46:A ./. K is commutative Group by A1,A8,A14,A16,A17;
A47:for a,b being Element of A./.K holds
(the mult of A./.K).(a,b)= (the mult of A./.K).(b,a)
proof
let a,b be Element of A./.K;
(the mult of A./.K) is commutative by A46,GROUP_3:2;
hence (the mult of A./.K).(a,b)= (the mult of A./.K).(b,a)
by BINOP_1:def 2;
end;
A48:a1*B=a2 *K & b1 *B=b2*K by GROUP_6:2;
A49: a2 * K is Element of A./.K by GROUP_6:27;
A50: b2 * K is Element of A./.K by GROUP_6:27;
reconsider a12=a1 * B,b12=b1 * B
as Element of Cosets K by A48,GROUP_6:16;
reconsider a11=a12 as Element of A./.K
by A49,GROUP_6:2;
reconsider b11=b12 as Element of A./.K
by A50,GROUP_6:2;
reconsider A1=a1 * B as Subset of A
by A48;
reconsider B1=b1 * B as Subset of A by A48;
A51: A1*B1=(CosOp K).(a11,b11) by GROUP_6:def 4
.=(the mult of A./.K).(a12,b12) by GROUP_6:23
.=(the mult of A./.K).(b11,a11) by A47
.=(CosOp K).(b12,a12) by GROUP_6:23
.=B1*A1 by GROUP_6:def 4;
A52:(a1*B)*(b1 *B)=A1*B1
proof
now
let x be set;
assume x in (a1 *B) *(b1 * B);
then consider z1,z2 being Element of G such that
A53: x=z1 *z2 & z1 in(a1*B)& z2 in (b1*B) by GROUP_2:12;
z1 in A1 & z2 in B1 by A53;
then reconsider z11=z1, z22=z2 as Element of A;
z1*z2=z11*z22 by GROUP_2:52;
hence x in A1* B1 by A53,GROUP_2:12;
end;
then A54:(a1*B)*(b1 *B) c= A1*B1 by TARSKI:def 3;
now
let x be set;
assume x in A1 * B1;
then consider z1,z2 being Element of A such that
A55: x=z1 *z2 & z1 in A1 & z2 in B1 by GROUP_2:12;
reconsider z11=z1, z22=z2 as Element of G by A55
;
z1*z2=z11*z22 by GROUP_2:52;
hence x in (a1*B)*(b1 *B)by A55,GROUP_2:12;
end;
then A1*B1 c=(a1*B)*(b1 *B) by TARSKI:def 3;
hence thesis by A54,XBOOLE_0:def 10;
end;
(b1*B)*(a1*B)=B1*A1
proof
now
let x be set;
assume x in (b1 *B) *(a1 * B);
then consider z1,z2 being Element of G such that
A56: x=z1 *z2 & z1 in(b1*B)& z2 in (a1*B) by GROUP_2:12;
z1 in B1 & z2 in A1 by A56;
then reconsider z11=z1, z22=z2 as Element of A;
z1*z2=z11*z22 by GROUP_2:52;
hence x in B1*A1 by A56,GROUP_2:12;
end;
then A57:(b1*B)*(a1*B) c= B1*A1 by TARSKI:def 3;
now
let x be set;
assume x in B1*A1;
then consider z1,z2 being Element of A such that
A58: x=z1 *z2 & z1 in B1 & z2 in A1 by GROUP_2:12;
reconsider z11=z1, z22=z2 as Element of G by A58
;
z1*z2=z11*z22 by GROUP_2:52;
hence x in (b1*B)*(a1*B)by A58,GROUP_2:12;
end;
then B1*A1 c=(b1*B)*(a1*B) by TARSKI:def 3;
hence thesis by A57,XBOOLE_0:def 10;
end;
hence thesis by A51,A52;
end;
thus x*y=(the mult of G1./.N).(x,y) by VECTSP_1:def 10
.=(CosOp N).(x,y) by GROUP_6:23
.=y1*x1 by A21,A22,A23,A29,A30,A31,A32,A38,A39,A45,GROUP_6:def
4
.=(CosOp N).(y,x) by A21,GROUP_6:def 4
.=(the mult of G1./.N).(y,x)by GROUP_6:23
.=y *x by VECTSP_1:def 10;
end;
hence thesis by VECTSP_1:def 17;
end;
hence thesis by A16,A17,A18,Th16;
end;
take z;
thus thesis by A1,A5,A10,A13,FINSEQ_1:def 3;
end;