let G be Group; :: thesis: for H, K being Subgroup of G
for phi being Function of (product <*H,K*>),G st ( for h, k being Element of G st h in H & k in K holds
phi . <*h,k*> = h * k ) holds
( phi is one-to-one iff H /\ K = (1). G )
let H, K be Subgroup of G; :: thesis: for phi being Function of (product <*H,K*>),G st ( for h, k being Element of G st h in H & k in K holds
phi . <*h,k*> = h * k ) holds
( phi is one-to-one iff H /\ K = (1). G )
let phi be Function of (product <*H,K*>),G; :: thesis: ( ( for h, k being Element of G st h in H & k in K holds
phi . <*h,k*> = h * k ) implies ( phi is one-to-one iff H /\ K = (1). G ) )
assume A1: for h, k being Element of G st h in H & k in K holds
phi . <*h,k*> = h * k ; :: thesis: ( phi is one-to-one iff H /\ K = (1). G )
A2: ( 1_ G in H & 1_ G in K ) by GROUP_2:46;
thus ( phi is one-to-one implies H /\ K = (1). G ) :: thesis: ( H /\ K = (1). G implies phi is one-to-one )

proof

assume B1: phi is one-to-one ; :: thesis: H /\ K = (1). G
B2: for h1, h2, k1, k2 being Element of G st h1 in H & h2 in H & k1 in K & k2 in K & phi . <*h1,k1*> = phi . <*h2,k2*> holds
<*h1,k1*> = <*h2,k2*>

proof

let h1, h2, k1, k2 be Element of G; :: thesis: ( h1 in H & h2 in H & k1 in K & k2 in K & phi . <*h1,k1*> = phi . <*h2,k2*> implies <*h1,k1*> = <*h2,k2*> )
assume Z1: h1 in H ; :: thesis: ( not h2 in H or not k1 in K or not k2 in K or not phi . <*h1,k1*> = phi . <*h2,k2*> or <*h1,k1*> = <*h2,k2*> )
assume Z2: h2 in H ; :: thesis: ( not k1 in K or not k2 in K or not phi . <*h1,k1*> = phi . <*h2,k2*> or <*h1,k1*> = <*h2,k2*> )
assume Z3: k1 in K ; :: thesis: ( not k2 in K or not phi . <*h1,k1*> = phi . <*h2,k2*> or <*h1,k1*> = <*h2,k2*> )
assume Z4: k2 in K ; :: thesis: ( not phi . <*h1,k1*> = phi . <*h2,k2*> or <*h1,k1*> = <*h2,k2*> )
assume Z5: phi . <*h1,k1*> = phi . <*h2,k2*> ; :: thesis: <*h1,k1*> = <*h2,k2*>
<*h1,k1*> in product <*H,K*> by Z1, Z3, Th7;
then reconsider x1 = <*h1,k1*> as Element of (product <*H,K*>) ;
<*h2,k2*> in product <*H,K*> by Z2, Z4, Th7;
then reconsider x2 = <*h2,k2*> as Element of (product <*H,K*>) ;
phi . x1 = phi . x2 by Z5;
hence <*h1,k1*> = <*h2,k2*> by B1, GROUP_6:1; :: thesis: verum

end;

H /\ K = (1). G

proof

assume Z1: H /\ K <> (1). G ; :: thesis: contradiction
(1). G is Subgroup of H /\ K by GROUP_2:65;
then consider h1 being Element of G such that
Z2: ( h1 in H /\ K & not h1 in (1). G ) by Z1, Th8;
Z3: h1 <> 1_ G by Z2, GROUP_5:1;
( h1 in H & h1 in K ) by Z2, GROUP_2:82;
then Z4: ( h1 in H & h1 " in K ) by GROUP_2:51;
then phi . <*h1,(h1 ")*> = h1 * (h1 ") by A1
.= 1_ G by GROUP_1:def 5
.= (1_ G) * (1_ G) by GROUP_1:def 4
.= phi . <*(1_ G),(1_ G)*> by A1, A2 ;
then <*h1,(h1 ")*> = <*(1_ G),(1_ G)*> by A2, B2, Z4;
hence contradiction by Z3, FINSEQ_1:77; :: thesis: verum

end;

hence H /\ K = (1). G ; :: thesis: verum

end;

thus ( H /\ K = (1). G implies phi is one-to-one ) :: thesis: verum

proof

assume B1: H /\ K = (1). G ; :: thesis: phi is one-to-one
for x, y being Element of (product <*H,K*>) st phi . x = phi . y holds
x = y

proof

let x, y be Element of (product <*H,K*>); :: thesis: ( phi . x = phi . y implies x = y )
assume B2: phi . x = phi . y ; :: thesis: x = y
( x . 1 in H & x . 2 in K & dom x = {1,2} ) by Th6;
then ( x . 1 in H & x . 1 in G & x . 2 in K & x . 2 in G & dom x = {1,2} ) by GROUP_2:41;
then consider h1, k1 being Element of G such that
B3: ( x . 1 = h1 & x . 2 = k1 & h1 in H & k1 in K ) ;
dom x = {1,2} by Th6;
then len x = 2 by FINSEQ_1:2, FINSEQ_1:def 3;
then B4: ( x . 1 = h1 & x . 2 = k1 & h1 in H & k1 in K & x = <*h1,k1*> ) by B3, FINSEQ_1:44;
( y . 1 in H & y . 2 in K & dom y = {1,2} ) by Th6;
then ( y . 1 in G & y . 1 in H & y . 2 in G & y . 2 in K & dom y = {1,2} ) by GROUP_2:41;
then consider h2, k2 being Element of G such that
B5: ( y . 1 = h2 & y . 2 = k2 & h2 in H & k2 in K ) ;
dom y = {1,2} by Th6;
then len y = 2 by FINSEQ_1:2, FINSEQ_1:def 3;
then B6: ( y . 1 = h2 & y . 2 = k2 & h2 in H & k2 in K & y = <*h2,k2*> ) by B5, FINSEQ_1:44;
h1 * k1 = phi . x by A1, B4
.= h2 * k2 by A1, B2, B6 ;
then (h2 ") * (h1 * k1) = ((h2 ") * h2) * k2 by GROUP_1:def 3
.= (1_ G) * k2 by GROUP_1:def 5
.= k2 by GROUP_1:def 4 ;
then B7: k2 * (k1 ") = (((h2 ") * h1) * k1) * (k1 ") by GROUP_1:def 3
.= ((h2 ") * h1) * (k1 * (k1 ")) by GROUP_1:def 3
.= ((h2 ") * h1) * (1_ G) by GROUP_1:def 5
.= (h2 ") * h1 by GROUP_1:def 4 ;
( k2 in K & k1 " in K ) by B4, B6, GROUP_2:51;
then B8: k2 * (k1 ") in K by GROUP_2:50;
( h1 in H & h2 " in H ) by B4, B6, GROUP_2:51;
then B9: (h2 ") * h1 in H by GROUP_2:50;
(h2 ") * h1 = 1_ G by B1, B7, B8, B9, GROUP_2:82, GROUP_5:1;
then B10: h1 = (h2 ") " by GROUP_1:12
.= h2 ;
k2 * (k1 ") = 1_ G by B1, B7, B8, B9, GROUP_2:82, GROUP_5:1;
then k2 = (k1 ") " by GROUP_1:12
.= k1 ;
hence x = y by B4, B6, B10; :: thesis: verum

end;

hence phi is one-to-one by GROUP_6:1; :: thesis: verum

end;