let G be finite commutative Group; :: thesis: for h, k being Nat st card G = h * k & h,k are_coprime holds

ex H, K being finite strict Subgroup of G st

( the carrier of H = { x where x is Element of G : x |^ h = 1_ G } & the carrier of K = { x where x is Element of G : x |^ k = 1_ G } & H is normal & K is normal & ( for x being Element of G ex a, b being Element of G st

( a in H & b in K & x = a * b ) ) & the carrier of H /\ the carrier of K = {(1_ G)} )

let h, k be Nat; :: thesis: ( card G = h * k & h,k are_coprime implies ex H, K being finite strict Subgroup of G st

( the carrier of H = { x where x is Element of G : x |^ h = 1_ G } & the carrier of K = { x where x is Element of G : x |^ k = 1_ G } & H is normal & K is normal & ( for x being Element of G ex a, b being Element of G st

( a in H & b in K & x = a * b ) ) & the carrier of H /\ the carrier of K = {(1_ G)} ) )

assume A1: ( card G = h * k & h,k are_coprime ) ; :: thesis: ex H, K being finite strict Subgroup of G st

( the carrier of H = { x where x is Element of G : x |^ h = 1_ G } & the carrier of K = { x where x is Element of G : x |^ k = 1_ G } & H is normal & K is normal & ( for x being Element of G ex a, b being Element of G st

( a in H & b in K & x = a * b ) ) & the carrier of H /\ the carrier of K = {(1_ G)} )

set A = { x where x is Element of G : x |^ h = 1_ G } ;

set B = { x where x is Element of G : x |^ k = 1_ G } ;

{ x where x is Element of G : x |^ h = 1_ G } c= the carrier of G

{ x where x is Element of G : x |^ k = 1_ G } c= the carrier of G

consider H being finite strict Subgroup of G such that

A2: ( the carrier of H = A & H is commutative & H is normal ) by Th14;

consider K being finite strict Subgroup of G such that

A3: ( the carrier of K = B & K is commutative & K is normal ) by Th14;

(1_ G) |^ h = 1_ G by GROUP_1:31;

then A4: 1_ G in the carrier of H by A2;

(1_ G) |^ k = 1_ G by GROUP_1:31;

then 1_ G in the carrier of K by A3;

then 1_ G in the carrier of H /\ the carrier of K by A4, XBOOLE_0:def 4;

then A5: {(1_ G)} c= the carrier of H /\ the carrier of K by ZFMISC_1:31;

h gcd k = 1 by A1, INT_2:def 3;

then consider a, b being Integer such that

A6: (a * h) + (b * k) = 1 by NAT_D:68;

the carrier of H /\ the carrier of K c= {(1_ G)}

A12: for x being Element of G ex s, t being Element of G st

( s in H & t in K & x = s * t )

( the carrier of H = { x where x is Element of G : x |^ h = 1_ G } & the carrier of K = { x where x is Element of G : x |^ k = 1_ G } & H is normal & K is normal & ( for x being Element of G ex a, b being Element of G st

( a in H & b in K & x = a * b ) ) & the carrier of H /\ the carrier of K = {(1_ G)} )

take K ; :: thesis: ( the carrier of H = { x where x is Element of G : x |^ h = 1_ G } & the carrier of K = { x where x is Element of G : x |^ k = 1_ G } & H is normal & K is normal & ( for x being Element of G ex a, b being Element of G st

( a in H & b in K & x = a * b ) ) & the carrier of H /\ the carrier of K = {(1_ G)} )

thus ( the carrier of H = { x where x is Element of G : x |^ h = 1_ G } & the carrier of K = { x where x is Element of G : x |^ k = 1_ G } & H is normal & K is normal & ( for x being Element of G ex a, b being Element of G st

( a in H & b in K & x = a * b ) ) & the carrier of H /\ the carrier of K = {(1_ G)} ) by A2, A3, A11, A12, A5, XBOOLE_0:def 10; :: thesis: verum

ex H, K being finite strict Subgroup of G st

( the carrier of H = { x where x is Element of G : x |^ h = 1_ G } & the carrier of K = { x where x is Element of G : x |^ k = 1_ G } & H is normal & K is normal & ( for x being Element of G ex a, b being Element of G st

( a in H & b in K & x = a * b ) ) & the carrier of H /\ the carrier of K = {(1_ G)} )

let h, k be Nat; :: thesis: ( card G = h * k & h,k are_coprime implies ex H, K being finite strict Subgroup of G st

( the carrier of H = { x where x is Element of G : x |^ h = 1_ G } & the carrier of K = { x where x is Element of G : x |^ k = 1_ G } & H is normal & K is normal & ( for x being Element of G ex a, b being Element of G st

( a in H & b in K & x = a * b ) ) & the carrier of H /\ the carrier of K = {(1_ G)} ) )

assume A1: ( card G = h * k & h,k are_coprime ) ; :: thesis: ex H, K being finite strict Subgroup of G st

( the carrier of H = { x where x is Element of G : x |^ h = 1_ G } & the carrier of K = { x where x is Element of G : x |^ k = 1_ G } & H is normal & K is normal & ( for x being Element of G ex a, b being Element of G st

( a in H & b in K & x = a * b ) ) & the carrier of H /\ the carrier of K = {(1_ G)} )

set A = { x where x is Element of G : x |^ h = 1_ G } ;

set B = { x where x is Element of G : x |^ k = 1_ G } ;

{ x where x is Element of G : x |^ h = 1_ G } c= the carrier of G

proof

then reconsider A = { x where x is Element of G : x |^ h = 1_ G } as Subset of G ;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { x where x is Element of G : x |^ h = 1_ G } or y in the carrier of G )

assume y in { x where x is Element of G : x |^ h = 1_ G } ; :: thesis: y in the carrier of G

then ex x being Element of G st

( y = x & x |^ h = 1_ G ) ;

hence y in the carrier of G ; :: thesis: verum

end;assume y in { x where x is Element of G : x |^ h = 1_ G } ; :: thesis: y in the carrier of G

then ex x being Element of G st

( y = x & x |^ h = 1_ G ) ;

hence y in the carrier of G ; :: thesis: verum

{ x where x is Element of G : x |^ k = 1_ G } c= the carrier of G

proof

then reconsider B = { x where x is Element of G : x |^ k = 1_ G } as Subset of G ;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { x where x is Element of G : x |^ k = 1_ G } or y in the carrier of G )

assume y in { x where x is Element of G : x |^ k = 1_ G } ; :: thesis: y in the carrier of G

then ex x being Element of G st

( y = x & x |^ k = 1_ G ) ;

hence y in the carrier of G ; :: thesis: verum

end;assume y in { x where x is Element of G : x |^ k = 1_ G } ; :: thesis: y in the carrier of G

then ex x being Element of G st

( y = x & x |^ k = 1_ G ) ;

hence y in the carrier of G ; :: thesis: verum

consider H being finite strict Subgroup of G such that

A2: ( the carrier of H = A & H is commutative & H is normal ) by Th14;

consider K being finite strict Subgroup of G such that

A3: ( the carrier of K = B & K is commutative & K is normal ) by Th14;

(1_ G) |^ h = 1_ G by GROUP_1:31;

then A4: 1_ G in the carrier of H by A2;

(1_ G) |^ k = 1_ G by GROUP_1:31;

then 1_ G in the carrier of K by A3;

then 1_ G in the carrier of H /\ the carrier of K by A4, XBOOLE_0:def 4;

then A5: {(1_ G)} c= the carrier of H /\ the carrier of K by ZFMISC_1:31;

h gcd k = 1 by A1, INT_2:def 3;

then consider a, b being Integer such that

A6: (a * h) + (b * k) = 1 by NAT_D:68;

the carrier of H /\ the carrier of K c= {(1_ G)}

proof

then A11:
the carrier of H /\ the carrier of K c= {(1_ G)}
;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in the carrier of H /\ the carrier of K or z in {(1_ G)} )

assume A7: z in the carrier of H /\ the carrier of K ; :: thesis: z in {(1_ G)}

then z in the carrier of H by XBOOLE_0:def 4;

then z in G by STRUCT_0:def 5, GROUP_2:40;

then reconsider w = z as Element of G ;

A8: ( w in A & w in B ) by A2, A3, A7, XBOOLE_0:def 4;

then A9: ex x being Element of G st

( w = x & x |^ h = 1_ G ) ;

A10: ex x being Element of G st

( w = x & x |^ k = 1_ G ) by A8;

w = w |^ 1 by GROUP_1:26

.= (w |^ (a * h)) * (w |^ (b * k)) by GROUP_1:33, A6

.= ((w |^ h) |^ a) * (w |^ (b * k)) by GROUP_1:35

.= ((w |^ h) |^ a) * ((w |^ k) |^ b) by GROUP_1:35

.= (1_ G) * ((1_ G) |^ b) by GROUP_1:31, A10, A9

.= (1_ G) * (1_ G) by GROUP_1:31

.= 1_ G by GROUP_1:def 4 ;

hence z in {(1_ G)} by TARSKI:def 1; :: thesis: verum

end;assume A7: z in the carrier of H /\ the carrier of K ; :: thesis: z in {(1_ G)}

then z in the carrier of H by XBOOLE_0:def 4;

then z in G by STRUCT_0:def 5, GROUP_2:40;

then reconsider w = z as Element of G ;

A8: ( w in A & w in B ) by A2, A3, A7, XBOOLE_0:def 4;

then A9: ex x being Element of G st

( w = x & x |^ h = 1_ G ) ;

A10: ex x being Element of G st

( w = x & x |^ k = 1_ G ) by A8;

w = w |^ 1 by GROUP_1:26

.= (w |^ (a * h)) * (w |^ (b * k)) by GROUP_1:33, A6

.= ((w |^ h) |^ a) * (w |^ (b * k)) by GROUP_1:35

.= ((w |^ h) |^ a) * ((w |^ k) |^ b) by GROUP_1:35

.= (1_ G) * ((1_ G) |^ b) by GROUP_1:31, A10, A9

.= (1_ G) * (1_ G) by GROUP_1:31

.= 1_ G by GROUP_1:def 4 ;

hence z in {(1_ G)} by TARSKI:def 1; :: thesis: verum

A12: for x being Element of G ex s, t being Element of G st

( s in H & t in K & x = s * t )

proof

take
H
; :: thesis: ex K being finite strict Subgroup of G st
let x be Element of G; :: thesis: ex s, t being Element of G st

( s in H & t in K & x = s * t )

A13: x = x |^ 1 by GROUP_1:26

.= (x |^ (b * k)) * (x |^ (a * h)) by GROUP_1:33, A6 ;

set t = x |^ (a * h);

set s = x |^ (b * k);

(x |^ (b * k)) |^ h = x |^ ((b * k) * h) by GROUP_1:35

.= x |^ ((k * h) * b)

.= (x |^ (k * h)) |^ b by GROUP_1:35

.= (1_ G) |^ b by A1, GR_CY_1:9

.= 1_ G by GROUP_1:31 ;

then A14: x |^ (b * k) in H by A2;

(x |^ (a * h)) |^ k = x |^ ((a * h) * k) by GROUP_1:35

.= x |^ ((h * k) * a)

.= (x |^ (h * k)) |^ a by GROUP_1:35

.= (1_ G) |^ a by A1, GR_CY_1:9

.= 1_ G by GROUP_1:31 ;

then x |^ (a * h) in K by A3;

hence ex s, t being Element of G st

( s in H & t in K & x = s * t ) by A13, A14; :: thesis: verum

end;( s in H & t in K & x = s * t )

A13: x = x |^ 1 by GROUP_1:26

.= (x |^ (b * k)) * (x |^ (a * h)) by GROUP_1:33, A6 ;

set t = x |^ (a * h);

set s = x |^ (b * k);

(x |^ (b * k)) |^ h = x |^ ((b * k) * h) by GROUP_1:35

.= x |^ ((k * h) * b)

.= (x |^ (k * h)) |^ b by GROUP_1:35

.= (1_ G) |^ b by A1, GR_CY_1:9

.= 1_ G by GROUP_1:31 ;

then A14: x |^ (b * k) in H by A2;

(x |^ (a * h)) |^ k = x |^ ((a * h) * k) by GROUP_1:35

.= x |^ ((h * k) * a)

.= (x |^ (h * k)) |^ a by GROUP_1:35

.= (1_ G) |^ a by A1, GR_CY_1:9

.= 1_ G by GROUP_1:31 ;

then x |^ (a * h) in K by A3;

hence ex s, t being Element of G st

( s in H & t in K & x = s * t ) by A13, A14; :: thesis: verum

( the carrier of H = { x where x is Element of G : x |^ h = 1_ G } & the carrier of K = { x where x is Element of G : x |^ k = 1_ G } & H is normal & K is normal & ( for x being Element of G ex a, b being Element of G st

( a in H & b in K & x = a * b ) ) & the carrier of H /\ the carrier of K = {(1_ G)} )

take K ; :: thesis: ( the carrier of H = { x where x is Element of G : x |^ h = 1_ G } & the carrier of K = { x where x is Element of G : x |^ k = 1_ G } & H is normal & K is normal & ( for x being Element of G ex a, b being Element of G st

( a in H & b in K & x = a * b ) ) & the carrier of H /\ the carrier of K = {(1_ G)} )

thus ( the carrier of H = { x where x is Element of G : x |^ h = 1_ G } & the carrier of K = { x where x is Element of G : x |^ k = 1_ G } & H is normal & K is normal & ( for x being Element of G ex a, b being Element of G st

( a in H & b in K & x = a * b ) ) & the carrier of H /\ the carrier of K = {(1_ G)} ) by A2, A3, A11, A12, A5, XBOOLE_0:def 10; :: thesis: verum