let G be Group; :: thesis: for a being Element of G
for H1, H2 being Subgroup of G holds (H1 /\ H2) |^ a = (H1 |^ a) /\ (H2 |^ a)
let a be Element of G; :: thesis: for H1, H2 being Subgroup of G holds (H1 /\ H2) |^ a = (H1 |^ a) /\ (H2 |^ a)
let H1, H2 be Subgroup of G; :: thesis: (H1 /\ H2) |^ a = (H1 |^ a) /\ (H2 |^ a)
let g be Element of G; :: according to GROUP_2:def 6 :: thesis: ( ( not g in (H1 /\ H2) |^ a or g in (H1 |^ a) /\ (H2 |^ a) ) & ( not g in (H1 |^ a) /\ (H2 |^ a) or g in (H1 /\ H2) |^ a ) )
thus ( g in (H1 /\ H2) |^ a implies g in (H1 |^ a) /\ (H2 |^ a) ) :: thesis: ( not g in (H1 |^ a) /\ (H2 |^ a) or g in (H1 /\ H2) |^ a )
proof
assume g in (H1 /\ H2) |^ a ; :: thesis: g in (H1 |^ a) /\ (H2 |^ a)
then consider h being Element of G such that
A1: g = h |^ a and
A2: h in H1 /\ H2 by Th58;
h in H2 by A2, GROUP_2:82;
then A3: g in H2 |^ a by A1, Th58;
h in H1 by A2, GROUP_2:82;
then g in H1 |^ a by A1, Th58;
hence g in (H1 |^ a) /\ (H2 |^ a) by A3, GROUP_2:82; :: thesis: verum
end;
assume A4: g in (H1 |^ a) /\ (H2 |^ a) ; :: thesis: g in (H1 /\ H2) |^ a
then g in H1 |^ a by GROUP_2:82;
then consider b being Element of G such that
A5: g = b |^ a and
A6: b in H1 by Th58;
g in H2 |^ a by A4, GROUP_2:82;
then consider c being Element of G such that
A7: g = c |^ a and
A8: c in H2 by Th58;
b = c by A5, A7, Th16;
then b in H1 /\ H2 by A6, A8, GROUP_2:82;
hence g in (H1 /\ H2) |^ a by A5, Th58; :: thesis: verum