let G be Group; :: thesis: for a being Element of G

for H being Subgroup of G holds

( a in H iff a * H = carr H )

let a be Element of G; :: thesis: for H being Subgroup of G holds

( a in H iff a * H = carr H )

let H be Subgroup of G; :: thesis: ( a in H iff a * H = carr H )

thus ( a in H implies a * H = carr H ) :: thesis: ( a * H = carr H implies a in H )

( a * (1_ G) = a & 1_ G in H ) by Th46, GROUP_1:def 4;

then a in carr H by A7, Th103;

hence a in H ; :: thesis: verum

for H being Subgroup of G holds

( a in H iff a * H = carr H )

let a be Element of G; :: thesis: for H being Subgroup of G holds

( a in H iff a * H = carr H )

let H be Subgroup of G; :: thesis: ( a in H iff a * H = carr H )

thus ( a in H implies a * H = carr H ) :: thesis: ( a * H = carr H implies a in H )

proof

assume A7:
a * H = carr H
; :: thesis: a in H
assume A1:
a in H
; :: thesis: a * H = carr H

thus a * H c= carr H :: according to XBOOLE_0:def 10 :: thesis: carr H c= a * H

assume A4: x in carr H ; :: thesis: x in a * H

then A5: x in H ;

reconsider b = x as Element of G by A4;

A6: a * ((a ") * b) = (a * (a ")) * b by GROUP_1:def 3

.= (1_ G) * b by GROUP_1:def 5

.= x by GROUP_1:def 4 ;

a " in H by A1, Th51;

then (a ") * b in H by A5, Th50;

hence x in a * H by A6, Th103; :: thesis: verum

end;thus a * H c= carr H :: according to XBOOLE_0:def 10 :: thesis: carr H c= a * H

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in carr H or x in a * H )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in a * H or x in carr H )

assume x in a * H ; :: thesis: x in carr H

then consider g being Element of G such that

A2: x = a * g and

A3: g in H by Th103;

a * g in H by A1, A3, Th50;

hence x in carr H by A2; :: thesis: verum

end;assume x in a * H ; :: thesis: x in carr H

then consider g being Element of G such that

A2: x = a * g and

A3: g in H by Th103;

a * g in H by A1, A3, Th50;

hence x in carr H by A2; :: thesis: verum

assume A4: x in carr H ; :: thesis: x in a * H

then A5: x in H ;

reconsider b = x as Element of G by A4;

A6: a * ((a ") * b) = (a * (a ")) * b by GROUP_1:def 3

.= (1_ G) * b by GROUP_1:def 5

.= x by GROUP_1:def 4 ;

a " in H by A1, Th51;

then (a ") * b in H by A5, Th50;

hence x in a * H by A6, Th103; :: thesis: verum

( a * (1_ G) = a & 1_ G in H ) by Th46, GROUP_1:def 4;

then a in carr H by A7, Th103;

hence a in H ; :: thesis: verum