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 for a being Element of G st a in gr ((carr H1) * (carr H2)) holds
a in H1 "\/" H2let 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 Th28;
rng (F |^ I) c= carr (H1 "\/" H2)
proof
set f =
F |^ I;
let x be
object ;
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
object such that A5:
y in dom (F |^ I)
and A6:
(F |^ I) . y = x
by FUNCT_1:def 3;
reconsider y =
y as
Element of
NAT by A5;
A7:
len (F |^ I) = len F
by Def3;
then A8:
y in dom I
by A1, A5, FINSEQ_3:29;
then A9:
I /. y = I . y
by PARTFUN1:def 6;
I . y in rng I
by A8, FUNCT_1:def 3;
then reconsider i =
I . y as
Integer by A4;
A10:
@ (I /. y) = I /. y
;
y in dom F
by A5, A7, FINSEQ_3:29;
then
(
F /. y = F . y &
F . y in rng F )
by FUNCT_1:def 3, PARTFUN1:def 6;
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:8;
y in dom F
by A5, A7, FINSEQ_3:29;
then A14:
x = (F /. y) |^ i
by A6, A9, A10, Def3;
now x in carr (H1 "\/" H2)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:3;
defpred S1[
Nat,
object ]
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
object st
S1[
k,
x]
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 Def4;
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 Product F1 = (F /. y) |^ (k div 2)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:9;
then reconsider m =
k - 2 as
Element of
NAT by INT_1:3;
reconsider q =
p | (Seg m) as
FinSequence of the
carrier of
G by FINSEQ_1:18;
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:53;
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:53;
A43:
m < k
by A35, NAT_1:16;
then A44:
Product q = (F /. y) |^ (m div 2)
by A26, A36, A34;
A45:
now for l being Nat st l in dom <*b,c*> holds
F1 . ((len q) + l) = <*b,c*> . llet l be
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:2, FINSEQ_1:89;
now F1 . ((len q) + l) = <*b,c*> . lper 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
;
A49:
(
(m + 1) mod 2
= 1 &
dom F1 c= dom p )
by A29, A34, NAT_D:16, RELAT_1:60;
(
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:25;
then
F1 . ((len q) + l) = p . (m + 1)
by A29, A37, A47, FUNCT_1:47;
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
;
A53:
dom F1 c= dom p
by A29, RELAT_1:60;
1
<= m + (1 + 1)
by NAT_1:12;
then A54:
m + 2
in dom F1
by A39, FINSEQ_3:25;
then
F1 . ((len q) + l) = p . (m + 2)
by A29, A37, A51, FUNCT_1:47;
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:53
.=
(len q) + (len <*b,c*>)
by A37, FINSEQ_1:44
;
then
F1 = q ^ <*b,c*>
by A40, A45, FINSEQ_3:38;
then Product F1 =
(Product q) * (Product <*b,c*>)
by FINSOP_1:5
.=
(Product q) * (F /. y)
by A11, FINSOP_1:12
.=
(F /. y) |^ ((m div 2) + 1)
by A44, GROUP_1:34
;
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:32;
then A57:
rng p c= (carr H1) \/ (carr H2)
by A21;
len p = 2
* n
by A18, FINSEQ_1:def 3;
then A58:
p = p | (Seg (2 * n))
by FINSEQ_3:49;
(
(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, Th18, 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,
object ]
means ( ( $1
mod 2
= 1 implies $2
= c " ) & ( $1
mod 2
= 0 implies $2
= b " ) );
set n =
|.i.|;
A60:
(
(2 * |.i.|) mod 2
= 0 &
(2 * |.i.|) div 2
= |.i.| )
by NAT_D:13, NAT_D:18;
A61:
for
k being
Nat st
k in Seg (2 * |.i.|) holds
ex
x being
object st
S1[
k,
x]
consider p being
FinSequence such that A64:
dom p = Seg (2 * |.i.|)
and A65:
for
k being
Nat st
k in Seg (2 * |.i.|) holds
S1[
k,
p . k]
from FINSEQ_1:sch 1(A61);
A66:
len p = 2
* |.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 Def4;
defpred S2[
Nat]
means ( $1
<= 2
* |.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
* |.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 Product F1 = ((F /. y) |^ (k div 2)) " 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:9;
then reconsider m =
k - 2 as
Element of
NAT by INT_1:3;
reconsider q =
p | (Seg m) as
FinSequence of the
carrier of
G by FINSEQ_1:18;
1
* 2
= 2
;
then A80:
m mod 2
= 0
by A74, NAT_D:15;
A81:
m + 2
= k
;
then A82:
m <= 2
* |.i.|
by A73, NAT_1:16, XXREAL_0:2;
then
ex
o being
Nat st 2
* |.i.| = m + o
by NAT_1:10;
then A83:
len q = m
by A66, FINSEQ_3:53;
A84:
ex
j being
Nat st 2
* |.i.| = k + j
by A73, NAT_1:10;
then A85:
len F1 = k
by A66, A75, FINSEQ_3:53;
A89:
m < k
by A81, NAT_1:16;
then A90:
Product q = ((F /. y) |^ (m div 2)) "
by A72, A82, A80;
A91:
now for l being Nat st l in dom <*(c "),(b ")*> holds
F1 . ((len q) + l) = <*(c "),(b ")*> . llet l be
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:2, FINSEQ_1:89;
now F1 . ((len q) + l) = <*(c "),(b ")*> . lper 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 "
;
A95:
(
(m + 1) mod 2
= 1 &
dom F1 c= dom p )
by A75, A80, NAT_D:16, RELAT_1:60;
(
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:25;
then
F1 . ((len q) + l) = p . (m + 1)
by A75, A83, A93, FUNCT_1:47;
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 "
;
A99:
dom F1 c= dom p
by A75, RELAT_1:60;
1
<= m + (1 + 1)
by NAT_1:12;
then A100:
m + 2
in dom F1
by A85, FINSEQ_3:25;
then
F1 . ((len q) + l) = p . (m + 2)
by A75, A83, A97, FUNCT_1:47;
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:53
.=
(len q) + (len <*(c "),(b ")*>)
by A83, FINSEQ_1:44
;
then
F1 = q ^ <*(c "),(b ")*>
by A86, A91, FINSEQ_3:38;
then Product F1 =
(Product q) * (Product <*(c "),(b ")*>)
by FINSOP_1:5
.=
(Product q) * ((c ") * (b "))
by FINSOP_1:12
.=
(Product q) * ((F /. y) ")
by A11, GROUP_1:17
.=
((F /. y) * ((F /. y) |^ (m div 2))) "
by A90, GROUP_1:17
.=
((F /. y) |^ ((m div 2) + 1)) "
by GROUP_1:34
;
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:75;
then A103:
c " in (carr H1) \/ (carr H2)
by XBOOLE_0:def 3;
len p = 2
* |.i.|
by A64, FINSEQ_1:def 3;
then A104:
p = p | (Seg (2 * |.i.|))
by FINSEQ_3:49;
b " in carr H1
by A12, GROUP_2:75;
then
b " in (carr H1) \/ (carr H2)
by XBOOLE_0:def 3;
then
{(b "),(c ")} c= (carr H1) \/ (carr H2)
by A103, ZFMISC_1:32;
then A105:
rng p c= (carr H1) \/ (carr H2)
by A67;
x = ((F /. y) |^ |.i.|) "
by A14, A59, GROUP_1:30;
then
x = Product p
by A102, A60, A104;
then
x in gr ((carr H1) \/ (carr H2))
by A105, A70, Th18, 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, Th18;
verum end;
then A106:
gr ((carr H1) * (carr H2)) is Subgroup of H1 "\/" H2
by GROUP_2:58;
(carr H1) \/ (carr H2) c= (carr H1) * (carr H2)
then
H1 "\/" H2 is Subgroup of gr ((carr H1) * (carr H2))
by Th32;
hence
gr (H1 * H2) = H1 "\/" H2
by A106, GROUP_2:55; verum