|
Dear Victor,
For the second question: " about the product of two subgroups H and K:
H*K is a subgroup iff H*K = K*H.", with Adam's suggestion
Roland
========
environ
vocabularies GROUP_1, STRUCT_0, GROUP_2,SUBSET_1, RELAT_1, TARSKI,EQREL_1,
GROUP_4;
notations TARSKI, STRUCT_0, ALGSTR_0, GROUP_2, GROUP_1, GROUP_4;
constructors NAT_1, FINSOP_1, GROUP_4;
registrations STRUCT_0, GROUP_2;
requirements BOOLE, SUBSET;
equalities GROUP_2, GROUP_4;
expansions TARSKI, XBOOLE_0;
theorems GROUP_1, GROUP_2,GROUP_4;
begin
theorem
for G being Group for H,K being Subgroup of G holds
(ex HK being Subgroup of G st the carrier of HK = H * K) iff
H * K = K * H
proof
let G be Group;
let H,K be Subgroup of G;
now
hereby
assume H * K = K * H;
then
A1: the carrier of (H "\/" K) = H * K & H "\/" K = gr(H * K)
by GROUP_4:50,51;
reconsider HK = gr(H * K) as Subgroup of G;
take HK;
thus the carrier of HK = H * K by A1;
end;
assume ex HK be Subgroup of G st the carrier of HK = H * K;
then consider HK be Subgroup of G such that
A2: the carrier of HK = H * K;
now
hereby
let x be object;
assume x in H * K;
then reconsider x9 = x as Element of HK by A2;
x9" in { h * k where h,k is Element of G : h in carr H &
k in carr K} by A2;
then consider h1,k1 be Element of G such that
A3: x9" = h1 * k1 and
A4: h1 in carr H and
A5: k1 in carr K;
A6: x9 = (x9") "
.= (h1 * k1) " by A3,GROUP_2:48
.= k1" * h1" by GROUP_1:17;
reconsider k2 = k1 as Element of K by A5;
reconsider h2 = h1 as Element of H by A4;
k2" = k1" & h2" = h1" by GROUP_2:48;
hence x in K * H by A6;
end;
hereby
let x be object;
assume
A7: x in K * H;
consider k,h be Element of G such that
A8: x = k * h and
A9: k in carr K and
A10: h in carr H by A7;
reconsider h9 = h as Element of H by A10;
reconsider h99 = h" as Element of G;
A11: h9" is Element of H;
reconsider k9 = k as Element of K by A9;
reconsider k99 = k" as Element of G;
k9" is Element of K;
then h99 is Element of H & k99 is Element of K by A11,GROUP_2:48;
then h99 * k99 in H * K;
then reconsider kh = (k * h)" as Element of HK by A2,GROUP_1:17;
kh" is Element of HK;
then (k * h)" " is Element of HK by GROUP_2:48;
hence x in H * K by A2,A8;
end;
end;
then H * K c= K * H & K * H c= H * K;
hence H * K = K * H;
end;
hence thesis;
end;
|