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 ) );
A17:
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 A20:
dom p = Seg (2 * n)
and A21:
for
k being
Nat st
k in Seg (2 * n) holds
S1[
k,
p . k]
from FINSEQ_1:sch 1(A17);
A22:
len p = 2
* n
by A20, FINSEQ_1:def 3;
A23:
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) );
A26:
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 A27:
for
l being
Nat st
l < k holds
S2[
l]
;
:: thesis: S2[k]
assume that A28:
k <= 2
* n
and A29:
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 A30:
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 A33:
k >= 1
by NAT_1:14;
k <> 1
by A29, NAT_D:14;
then
k > 1
by A33, 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;
A34:
m + 2
= k
;
then A35:
m < k
by NAT_1:16;
A36:
m <= 2
* n
by A28, A34, NAT_1:16, XXREAL_0:2;
1
* 2
= 2
;
then A37:
m mod 2
= 0
by A29, NAT_D:15;
reconsider q =
p | (Seg m) as
FinSequence of the
carrier of
G by FINSEQ_1:23;
A38:
Product q = (F /. y) |^ (m div 2)
by A27, A35, A36, A37;
A39:
ex
j being
Nat st 2
* n = k + j
by A28, NAT_1:10;
ex
o being
Nat st 2
* n = m + o
by A36, NAT_1:10;
then A40:
(
len F1 = k &
len q = m )
by A22, A30, A39, FINSEQ_3:59;
A41:
len F1 =
m + 2
by A22, A30, A39, FINSEQ_3:59
.=
(len q) + (len <*b,c*>)
by A40, 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 A44:
l in {1,2}
by FINSEQ_1:4, FINSEQ_3:29;
now per cases
( l = 1 or l = 2 )
by A44, TARSKI:def 2;
suppose A45:
l = 1
;
:: thesis: F1 . ((len q) + l) = <*b,c*> . lthen A46:
<*b,c*> . l = b
by FINSEQ_1:61;
(
m + 1
<= k & 1
<= m + 1 )
by A35, NAT_1:12, NAT_1:13;
then A47:
m + 1
in dom F1
by A40, FINSEQ_3:27;
then A48:
F1 . ((len q) + l) = p . (m + 1)
by A30, A40, A45, FUNCT_1:70;
A49:
(m + 1) mod 2
= 1
by A37, NAT_D:16;
dom F1 c= dom p
by A30, RELAT_1:89;
hence
F1 . ((len q) + l) = <*b,c*> . l
by A20, A21, A46, A47, A48, A49;
:: thesis: verum end; suppose A50:
l = 2
;
:: thesis: F1 . ((len q) + l) = <*b,c*> . lthen A51:
<*b,c*> . l = c
by FINSEQ_1:61;
1
<= m + (1 + 1)
by NAT_1:12;
then A52:
m + 2
in dom F1
by A40, FINSEQ_3:27;
then A53:
F1 . ((len q) + l) = p . (m + 2)
by A30, A40, A50, FUNCT_1:70;
dom F1 c= dom p
by A30, RELAT_1:89;
hence
F1 . ((len q) + l) = <*b,c*> . l
by A20, A21, A29, A51, A52, A53;
:: thesis: verum end; hence
F1 . ((len q) + l) = <*b,c*> . l
;
:: thesis: verum end; then
F1 = q ^ <*b,c*>
by A41, A42, FINSEQ_3:43;
then A54:
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 A38, GROUP_1:66
;
(m div (2 * 1)) + 1 =
(m div 2) + (2 div 2)
by NAT_D:18
.=
k div 2
by A34, A37, NAT_D:19
;
hence
Product F1 = (F /. y) |^ (k div 2)
by A54;
:: thesis: verum end;
hence
Product F1 = (F /. y) |^ (k div 2)
;
:: thesis: verum
end; A55:
for
k being
Nat holds
S2[
k]
from NAT_1:sch 4(A26);
A56:
(2 * n) mod 2
= 0
by NAT_D:13;
A57:
(2 * n) div 2
= n
by NAT_D:18;
len p = 2
* n
by A20, FINSEQ_1:def 3;
then
p = p | (Seg (2 * n))
by FINSEQ_3:55;
then A58:
x = Product p
by A13, A55, A56, A57;
(
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 A59:
rng p c= (carr H1) \/ (carr H2)
by A23, 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 A58, A59, Th21, XBOOLE_1:1;
hence
x in carr (H1 "\/" H2)
by STRUCT_0:def 5;
:: thesis: verum end; suppose A60:
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 " ) );
A61:
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 A64:
dom p = Seg (2 * (abs i))
and A65:
for
k being
Nat st
k in Seg (2 * (abs i)) holds
S1[
k,
p . k]
from FINSEQ_1:sch 1(A61);
A66:
len p = 2
* (abs i)
by A64, FINSEQ_1:def 3;
A67:
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)) " );
A70:
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 A71:
for
l being
Nat st
l < k holds
S2[
l]
;
:: thesis: S2[k]
assume that A72:
k <= 2
* (abs i)
and A73:
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 A74:
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 A77:
k >= 1
by NAT_1:14;
k <> 1
by A73, NAT_D:14;
then
k > 1
by A77, 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;
A78:
m + 2
= k
;
then A79:
m < k
by NAT_1:16;
A80:
m <= 2
* (abs i)
by A72, A78, NAT_1:16, XXREAL_0:2;
1
* 2
= 2
;
then A81:
m mod 2
= 0
by A73, NAT_D:15;
reconsider q =
p | (Seg m) as
FinSequence of the
carrier of
G by FINSEQ_1:23;
A82:
Product q = ((F /. y) |^ (m div 2)) "
by A71, A79, A80, A81;
A83:
ex
j being
Nat st 2
* (abs i) = k + j
by A72, NAT_1:10;
ex
o being
Nat st 2
* (abs i) = m + o
by A80, NAT_1:10;
then A84:
(
len F1 = k &
len q = m )
by A66, A74, A83, FINSEQ_3:59;
A85:
len F1 =
m + 2
by A66, A74, A83, FINSEQ_3:59
.=
(len q) + (len <*(c " ),(b " )*>)
by A84, 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 A88:
l in {1,2}
by FINSEQ_1:4, FINSEQ_3:29;
now per cases
( l = 1 or l = 2 )
by A88, TARSKI:def 2;
suppose A89:
l = 1
;
:: thesis: F1 . ((len q) + l) = <*(c " ),(b " )*> . lthen A90:
<*(c " ),(b " )*> . l = c "
by FINSEQ_1:61;
(
m + 1
<= k & 1
<= m + 1 )
by A79, NAT_1:12, NAT_1:13;
then A91:
m + 1
in dom F1
by A84, FINSEQ_3:27;
then A92:
F1 . ((len q) + l) = p . (m + 1)
by A74, A84, A89, FUNCT_1:70;
A93:
(m + 1) mod 2
= 1
by A81, NAT_D:16;
dom F1 c= dom p
by A74, RELAT_1:89;
hence
F1 . ((len q) + l) = <*(c " ),(b " )*> . l
by A64, A65, A90, A91, A92, A93;
:: thesis: verum end; suppose A94:
l = 2
;
:: thesis: F1 . ((len q) + l) = <*(c " ),(b " )*> . lthen A95:
<*(c " ),(b " )*> . l = b "
by FINSEQ_1:61;
1
<= m + (1 + 1)
by NAT_1:12;
then A96:
m + 2
in dom F1
by A84, FINSEQ_3:27;
then A97:
F1 . ((len q) + l) = p . (m + 2)
by A74, A84, A94, FUNCT_1:70;
dom F1 c= dom p
by A74, RELAT_1:89;
hence
F1 . ((len q) + l) = <*(c " ),(b " )*> . l
by A64, A65, A73, A95, A96, A97;
:: thesis: verum end; hence
F1 . ((len q) + l) = <*(c " ),(b " )*> . l
;
:: thesis: verum end; then
F1 = q ^ <*(c " ),(b " )*>
by A85, A86, FINSEQ_3:43;
then A98:
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 A82, GROUP_1:25
.=
((F /. y) |^ ((m div 2) + 1)) "
by GROUP_1:66
;
(m div (2 * 1)) + 1 =
(m div 2) + (2 div 2)
by NAT_D:18
.=
k div 2
by A78, A81, NAT_D:19
;
hence
Product F1 = ((F /. y) |^ (k div 2)) "
by A98;
:: thesis: verum end;
hence
Product F1 = ((F /. y) |^ (k div 2)) "
;
:: thesis: verum
end; A99:
for
k being
Nat holds
S2[
k]
from NAT_1:sch 4(A70);
A100:
(2 * (abs i)) mod 2
= 0
by NAT_D:13;
A101:
(2 * (abs i)) div 2
= abs i
by NAT_D:18;
len p = 2
* (abs i)
by A64, FINSEQ_1:def 3;
then A102:
p = p | (Seg (2 * (abs i)))
by FINSEQ_3:55;
x = ((F /. y) |^ (abs i)) "
by A13, A60, GROUP_1:60;
then A103:
x = Product p
by A99, A100, A101, A102;
(
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 A104:
rng p c= (carr H1) \/ (carr H2)
by A67, 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 A103, A104, 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