let G be Group; :: thesis: for H1, H2 being Subgroup of G holds H1 "\/" H2 = gr (H1 * H2)
let H1, H2 be Subgroup of G; :: thesis: H1 "\/" H2 = gr (H1 * H2)
set H = gr ((carr H1) * (carr H2));
(carr H1) \/ (carr H2) c= (carr H1) * (carr H2)
then A4:
H1 "\/" H2 is Subgroup of gr ((carr H1) * (carr H2))
by Th41;
now let a be
Element of
G;
:: thesis: ( a in gr ((carr H1) * (carr H2)) implies a in H1 "\/" H2 )assume
a in gr ((carr H1) * (carr H2))
;
:: thesis: a in H1 "\/" H2then consider F being
FinSequence of the
carrier of
G,
I being
FinSequence of
INT such that A5:
len F = len I
and A6:
rng F c= (carr H1) * (carr H2)
and A7:
a = Product (F |^ I)
by Th37;
rng (F |^ I) c= carr (H1 "\/" H2)
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in rng (F |^ I) or x in carr (H1 "\/" H2) )
set f =
F |^ I;
assume
x in rng (F |^ I)
;
:: thesis: x in carr (H1 "\/" H2)
then consider y being
set such that A8:
y in dom (F |^ I)
and A9:
(F |^ I) . y = x
by FUNCT_1:def 5;
reconsider y =
y as
Element of
NAT by A8;
A10:
len (F |^ I) = len F
by Def4;
then A11:
y in dom I
by A5, A8, FINSEQ_3:31;
then
(
I . y in rng I &
rng I c= INT )
by FINSEQ_1:def 4, FUNCT_1:def 5;
then reconsider i =
I . y as
Integer ;
A12:
y in dom F
by A8, A10, FINSEQ_3:31;
(
I /. y = I . y &
@ (I /. y) = I /. y )
by A11, PARTFUN1:def 8;
then A13:
x = (F /. y) |^ i
by A9, A12, Def4;
y in dom F
by A8, A10, FINSEQ_3:31;
then
(
F /. y = F . y &
F . y in rng F )
by FUNCT_1:def 5, PARTFUN1:def 8;
then consider b,
c being
Element of
G such that A14:
F /. y = b * c
and A15:
b in carr H1
and A16:
c in carr H2
by A6, GROUP_2:12;
now per cases
( i >= 0 or i < 0 )
;
suppose
i >= 0
;
:: thesis: x in carr (H1 "\/" H2)then reconsider n =
i as
Element of
NAT by INT_1:16;
defpred S1[
Nat,
set ]
means ( ( $1
mod 2
= 1 implies $2
= b ) & ( $1
mod 2
= 0 implies $2
= c ) );
A18:
for
k being
Nat st
k in Seg (2 * n) holds
ex
x being
set st
S1[
k,
x]
consider p being
FinSequence such that A21:
dom p = Seg (2 * n)
and A22:
for
k being
Nat st
k in Seg (2 * n) holds
S1[
k,
p . k]
from FINSEQ_1:sch 1(A18);
A23:
len p = 2
* n
by A21, FINSEQ_1:def 3;
A24:
rng p c= {b,c}
then
rng p c= the
carrier of
G
by XBOOLE_1:1;
then reconsider p =
p as
FinSequence of the
carrier of
G by FINSEQ_1:def 4;
defpred S2[
Nat]
means ( $1
<= 2
* n & $1
mod 2
= 0 implies for
F1 being
FinSequence of the
carrier of
G st
F1 = p | (Seg $1) holds
Product F1 = (F /. y) |^ ($1 div 2) );
A27:
for
k being
Nat st ( for
l being
Nat st
l < k holds
S2[
l] ) holds
S2[
k]
proof
let k be
Nat;
:: thesis: ( ( for l being Nat st l < k holds
S2[l] ) implies S2[k] )
assume A28:
for
l being
Nat st
l < k holds
S2[
l]
;
:: thesis: S2[k]
assume that A29:
k <= 2
* n
and A30:
k mod 2
= 0
;
:: thesis: for F1 being FinSequence of the carrier of G st F1 = p | (Seg k) holds
Product F1 = (F /. y) |^ (k div 2)
let F1 be
FinSequence of the
carrier of
G;
:: thesis: ( F1 = p | (Seg k) implies Product F1 = (F /. y) |^ (k div 2) )
assume A31:
F1 = p | (Seg k)
;
:: thesis: Product F1 = (F /. y) |^ (k div 2)
now per cases
( k = 0 or k <> 0 )
;
suppose
k <> 0
;
:: thesis: Product F1 = (F /. y) |^ (k div 2)then A34:
k >= 1
by NAT_1:14;
k <> 1
by A30, NAT_D:14;
then
k > 1
by A34, XXREAL_0:1;
then
k >= 1
+ 1
by NAT_1:13;
then
k - 2
>= 2
- 2
by XREAL_1:11;
then reconsider m =
k - 2 as
Element of
NAT by INT_1:16;
A35:
m + 2
= k
;
then A36:
m < k
by NAT_1:16;
A37:
m <= 2
* n
by A29, A35, NAT_1:16, XXREAL_0:2;
1
* 2
= 2
;
then A38:
m mod 2
= 0
by A30, NAT_D:15;
reconsider q =
p | (Seg m) as
FinSequence of the
carrier of
G by FINSEQ_1:23;
A39:
Product q = (F /. y) |^ (m div 2)
by A28, A36, A37, A38;
A40:
ex
j being
Nat st 2
* n = k + j
by A29, NAT_1:10;
ex
o being
Nat st 2
* n = m + o
by A37, NAT_1:10;
then A41:
(
len F1 = k &
len q = m )
by A23, A31, A40, FINSEQ_3:59;
A42:
len F1 =
m + 2
by A23, A31, A40, FINSEQ_3:59
.=
(len q) + (len <*b,c*>)
by A41, FINSEQ_1:61
;
now let l be
Element of
NAT ;
:: thesis: ( l in dom <*b,c*> implies F1 . ((len q) + l) = <*b,c*> . l )assume
l in dom <*b,c*>
;
:: thesis: F1 . ((len q) + l) = <*b,c*> . lthen A45:
l in {1,2}
by FINSEQ_1:4, FINSEQ_3:29;
now per cases
( l = 1 or l = 2 )
by A45, TARSKI:def 2;
suppose A46:
l = 1
;
:: thesis: F1 . ((len q) + l) = <*b,c*> . lthen A47:
<*b,c*> . l = b
by FINSEQ_1:61;
(
m + 1
<= k & 1
<= m + 1 )
by A36, NAT_1:12, NAT_1:13;
then A48:
m + 1
in dom F1
by A41, FINSEQ_3:27;
then A49:
F1 . ((len q) + l) = p . (m + 1)
by A31, A41, A46, FUNCT_1:70;
A50:
(m + 1) mod 2
= 1
by A38, NAT_D:16;
dom F1 c= dom p
by A31, RELAT_1:89;
hence
F1 . ((len q) + l) = <*b,c*> . l
by A21, A22, A47, A48, A49, A50;
:: thesis: verum end; suppose A51:
l = 2
;
:: thesis: F1 . ((len q) + l) = <*b,c*> . lthen A52:
<*b,c*> . l = c
by FINSEQ_1:61;
1
<= m + (1 + 1)
by NAT_1:12;
then A53:
m + 2
in dom F1
by A41, FINSEQ_3:27;
then A54:
F1 . ((len q) + l) = p . (m + 2)
by A31, A41, A51, FUNCT_1:70;
dom F1 c= dom p
by A31, RELAT_1:89;
hence
F1 . ((len q) + l) = <*b,c*> . l
by A21, A22, A30, A52, A53, A54;
:: thesis: verum end; hence
F1 . ((len q) + l) = <*b,c*> . l
;
:: thesis: verum end; then
F1 = q ^ <*b,c*>
by A42, A43, FINSEQ_3:43;
then A55:
Product F1 =
(Product q) * (Product <*b,c*>)
by Th8
.=
(Product q) * (F /. y)
by A14, FINSOP_1:13
.=
(F /. y) |^ ((m div 2) + 1)
by A39, GROUP_1:49
;
(m div (2 * 1)) + 1 =
(m div 2) + (2 div 2)
by NAT_D:18
.=
k div 2
by A35, A38, NAT_D:19
;
hence
Product F1 = (F /. y) |^ (k div 2)
by A55;
:: thesis: verum end;
hence
Product F1 = (F /. y) |^ (k div 2)
;
:: thesis: verum
end; A56:
for
k being
Nat holds
S2[
k]
from NAT_1:sch 4(A27);
A57:
(2 * n) mod 2
= 0
by NAT_D:13;
A58:
(2 * n) div 2
= n
by NAT_D:18;
len p = 2
* n
by A21, FINSEQ_1:def 3;
then
p = p | (Seg (2 * n))
by FINSEQ_3:55;
then A59:
x = Product p
by A13, A56, A57, A58;
(
b in (carr H1) \/ (carr H2) &
c in (carr H1) \/ (carr H2) )
by A15, A16, XBOOLE_0:def 3;
then
{b,c} c= (carr H1) \/ (carr H2)
by ZFMISC_1:38;
then A60:
rng p c= (carr H1) \/ (carr H2)
by A24, XBOOLE_1:1;
(
(carr H1) \/ (carr H2) c= the
carrier of
(gr ((carr H1) \/ (carr H2))) &
carr (gr ((carr H1) \/ (carr H2))) = the
carrier of
(gr ((carr H1) \/ (carr H2))) )
by Def5;
then
x in gr ((carr H1) \/ (carr H2))
by A59, A60, Th21, XBOOLE_1:1;
hence
x in carr (H1 "\/" H2)
by STRUCT_0:def 5;
:: thesis: verum end; suppose A61:
i < 0
;
:: thesis: x in carr (H1 "\/" H2)set n =
abs i;
defpred S1[
Nat,
set ]
means ( ( $1
mod 2
= 1 implies $2
= c " ) & ( $1
mod 2
= 0 implies $2
= b " ) );
A63:
for
k being
Nat st
k in Seg (2 * (abs i)) holds
ex
x being
set st
S1[
k,
x]
consider p being
FinSequence such that A66:
dom p = Seg (2 * (abs i))
and A67:
for
k being
Nat st
k in Seg (2 * (abs i)) holds
S1[
k,
p . k]
from FINSEQ_1:sch 1(A63);
A68:
len p = 2
* (abs i)
by A66, FINSEQ_1:def 3;
A69:
rng p c= {(b " ),(c " )}
then
rng p c= the
carrier of
G
by XBOOLE_1:1;
then reconsider p =
p as
FinSequence of the
carrier of
G by FINSEQ_1:def 4;
defpred S2[
Nat]
means ( $1
<= 2
* (abs i) & $1
mod 2
= 0 implies for
F1 being
FinSequence of the
carrier of
G st
F1 = p | (Seg $1) holds
Product F1 = ((F /. y) |^ ($1 div 2)) " );
A72:
for
k being
Nat st ( for
l being
Nat st
l < k holds
S2[
l] ) holds
S2[
k]
proof
let k be
Nat;
:: thesis: ( ( for l being Nat st l < k holds
S2[l] ) implies S2[k] )
assume A73:
for
l being
Nat st
l < k holds
S2[
l]
;
:: thesis: S2[k]
assume that A74:
k <= 2
* (abs i)
and A75:
k mod 2
= 0
;
:: thesis: for F1 being FinSequence of the carrier of G st F1 = p | (Seg k) holds
Product F1 = ((F /. y) |^ (k div 2)) "
let F1 be
FinSequence of the
carrier of
G;
:: thesis: ( F1 = p | (Seg k) implies Product F1 = ((F /. y) |^ (k div 2)) " )
assume A76:
F1 = p | (Seg k)
;
:: thesis: Product F1 = ((F /. y) |^ (k div 2)) "
now per cases
( k = 0 or k <> 0 )
;
suppose
k <> 0
;
:: thesis: Product F1 = ((F /. y) |^ (k div 2)) " then A79:
k >= 1
by NAT_1:14;
k <> 1
by A75, NAT_D:14;
then
k > 1
by A79, XXREAL_0:1;
then
k >= 1
+ 1
by NAT_1:13;
then
k - 2
>= 2
- 2
by XREAL_1:11;
then reconsider m =
k - 2 as
Element of
NAT by INT_1:16;
A80:
m + 2
= k
;
then A81:
m < k
by NAT_1:16;
A82:
m <= 2
* (abs i)
by A74, A80, NAT_1:16, XXREAL_0:2;
1
* 2
= 2
;
then A83:
m mod 2
= 0
by A75, NAT_D:15;
reconsider q =
p | (Seg m) as
FinSequence of the
carrier of
G by FINSEQ_1:23;
A84:
Product q = ((F /. y) |^ (m div 2)) "
by A73, A81, A82, A83;
A85:
ex
j being
Nat st 2
* (abs i) = k + j
by A74, NAT_1:10;
ex
o being
Nat st 2
* (abs i) = m + o
by A82, NAT_1:10;
then A86:
(
len F1 = k &
len q = m )
by A68, A76, A85, FINSEQ_3:59;
A87:
len F1 =
m + 2
by A68, A76, A85, FINSEQ_3:59
.=
(len q) + (len <*(c " ),(b " )*>)
by A86, FINSEQ_1:61
;
now let l be
Element of
NAT ;
:: thesis: ( l in dom <*(c " ),(b " )*> implies F1 . ((len q) + l) = <*(c " ),(b " )*> . l )assume
l in dom <*(c " ),(b " )*>
;
:: thesis: F1 . ((len q) + l) = <*(c " ),(b " )*> . lthen A90:
l in {1,2}
by FINSEQ_1:4, FINSEQ_3:29;
now per cases
( l = 1 or l = 2 )
by A90, TARSKI:def 2;
suppose A91:
l = 1
;
:: thesis: F1 . ((len q) + l) = <*(c " ),(b " )*> . lthen A92:
<*(c " ),(b " )*> . l = c "
by FINSEQ_1:61;
(
m + 1
<= k & 1
<= m + 1 )
by A81, NAT_1:12, NAT_1:13;
then A93:
m + 1
in dom F1
by A86, FINSEQ_3:27;
then A94:
F1 . ((len q) + l) = p . (m + 1)
by A76, A86, A91, FUNCT_1:70;
A95:
(m + 1) mod 2
= 1
by A83, NAT_D:16;
dom F1 c= dom p
by A76, RELAT_1:89;
hence
F1 . ((len q) + l) = <*(c " ),(b " )*> . l
by A66, A67, A92, A93, A94, A95;
:: thesis: verum end; suppose A96:
l = 2
;
:: thesis: F1 . ((len q) + l) = <*(c " ),(b " )*> . lthen A97:
<*(c " ),(b " )*> . l = b "
by FINSEQ_1:61;
1
<= m + (1 + 1)
by NAT_1:12;
then A98:
m + 2
in dom F1
by A86, FINSEQ_3:27;
then A99:
F1 . ((len q) + l) = p . (m + 2)
by A76, A86, A96, FUNCT_1:70;
dom F1 c= dom p
by A76, RELAT_1:89;
hence
F1 . ((len q) + l) = <*(c " ),(b " )*> . l
by A66, A67, A75, A97, A98, A99;
:: thesis: verum end; hence
F1 . ((len q) + l) = <*(c " ),(b " )*> . l
;
:: thesis: verum end; then
F1 = q ^ <*(c " ),(b " )*>
by A87, A88, FINSEQ_3:43;
then A100:
Product F1 =
(Product q) * (Product <*(c " ),(b " )*>)
by Th8
.=
(Product q) * ((c " ) * (b " ))
by FINSOP_1:13
.=
(Product q) * ((F /. y) " )
by A14, GROUP_1:25
.=
((F /. y) * ((F /. y) |^ (m div 2))) "
by A84, GROUP_1:25
.=
((F /. y) |^ ((m div 2) + 1)) "
by GROUP_1:49
;
(m div (2 * 1)) + 1 =
(m div 2) + (2 div 2)
by NAT_D:18
.=
k div 2
by A80, A83, NAT_D:19
;
hence
Product F1 = ((F /. y) |^ (k div 2)) "
by A100;
:: thesis: verum end;
hence
Product F1 = ((F /. y) |^ (k div 2)) "
;
:: thesis: verum
end; A101:
for
k being
Nat holds
S2[
k]
from NAT_1:sch 4(A72);
A102:
(2 * (abs i)) mod 2
= 0
by NAT_D:13;
A103:
(2 * (abs i)) div 2
= abs i
by NAT_D:18;
len p = 2
* (abs i)
by A66, FINSEQ_1:def 3;
then A104:
p = p | (Seg (2 * (abs i)))
by FINSEQ_3:55;
x = ((F /. y) |^ (abs i)) "
by A13, A61, GROUP_1:56;
then A105:
x = Product p
by A101, A102, A103, A104;
(
b " in carr H1 &
c " in carr H2 )
by A15, A16, GROUP_2:90;
then
(
b " in (carr H1) \/ (carr H2) &
c " in (carr H1) \/ (carr H2) )
by XBOOLE_0:def 3;
then
{(b " ),(c " )} c= (carr H1) \/ (carr H2)
by ZFMISC_1:38;
then A106:
rng p c= (carr H1) \/ (carr H2)
by A69, XBOOLE_1:1;
(
(carr H1) \/ (carr H2) c= the
carrier of
(gr ((carr H1) \/ (carr H2))) &
carr (gr ((carr H1) \/ (carr H2))) = the
carrier of
(gr ((carr H1) \/ (carr H2))) )
by Def5;
then
x in gr ((carr H1) \/ (carr H2))
by A105, A106, Th21, XBOOLE_1:1;
hence
x in carr (H1 "\/" H2)
by STRUCT_0:def 5;
:: thesis: verum end;
hence
x in carr (H1 "\/" H2)
;
:: thesis: verum
end; hence
a in H1 "\/" H2
by A7, Th21;
:: thesis: verum end;
then
gr ((carr H1) * (carr H2)) is Subgroup of H1 "\/" H2
by GROUP_2:67;
hence
gr (H1 * H2) = H1 "\/" H2
by A4, GROUP_2:64; :: thesis: verum