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)

thus (H1 /\ H2) * a c= (H1 * a) /\ (H2 * a) :: according to XBOOLE_0:def 10 :: thesis: (H1 * a) /\ (H2 * a) c= (H1 /\ H2) * a

assume A4: x in (H1 * a) /\ (H2 * a) ; :: thesis: x in (H1 /\ H2) * a

then x in H1 * a by XBOOLE_0:def 4;

then consider g being Element of G such that

A5: x = g * a and

A6: g in H1 by Th104;

x in H2 * a by A4, XBOOLE_0:def 4;

then consider g1 being Element of G such that

A7: x = g1 * a and

A8: g1 in H2 by Th104;

g = g1 by A5, A7, GROUP_1:6;

then g in H1 /\ H2 by A6, A8, Th82;

hence x in (H1 /\ H2) * a by A5, Th104; :: thesis: verum

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)

thus (H1 /\ H2) * a c= (H1 * a) /\ (H2 * a) :: according to XBOOLE_0:def 10 :: thesis: (H1 * a) /\ (H2 * a) c= (H1 /\ H2) * a

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (H1 * a) /\ (H2 * a) or x in (H1 /\ H2) * a )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (H1 /\ H2) * a or x in (H1 * a) /\ (H2 * a) )

assume x in (H1 /\ H2) * a ; :: thesis: x in (H1 * a) /\ (H2 * a)

then consider g being Element of G such that

A1: x = g * a and

A2: g in H1 /\ H2 by Th104;

g in H2 by A2, Th82;

then A3: x in H2 * a by A1, Th104;

g in H1 by A2, Th82;

then x in H1 * a by A1, Th104;

hence x in (H1 * a) /\ (H2 * a) by A3, XBOOLE_0:def 4; :: thesis: verum

end;assume x in (H1 /\ H2) * a ; :: thesis: x in (H1 * a) /\ (H2 * a)

then consider g being Element of G such that

A1: x = g * a and

A2: g in H1 /\ H2 by Th104;

g in H2 by A2, Th82;

then A3: x in H2 * a by A1, Th104;

g in H1 by A2, Th82;

then x in H1 * a by A1, Th104;

hence x in (H1 * a) /\ (H2 * a) by A3, XBOOLE_0:def 4; :: thesis: verum

assume A4: x in (H1 * a) /\ (H2 * a) ; :: thesis: x in (H1 /\ H2) * a

then x in H1 * a by XBOOLE_0:def 4;

then consider g being Element of G such that

A5: x = g * a and

A6: g in H1 by Th104;

x in H2 * a by A4, XBOOLE_0:def 4;

then consider g1 being Element of G such that

A7: x = g1 * a and

A8: g1 in H2 by Th104;

g = g1 by A5, A7, GROUP_1:6;

then g in H1 /\ H2 by A6, A8, Th82;

hence x in (H1 /\ H2) * a by A5, Th104; :: thesis: verum