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