let G be addGroup; :: thesis: for a, b being Element of G
for H being Subgroup of G holds
( H + a = H + b iff b + (- a) in H )
let a, b be Element of G; :: thesis: for H being Subgroup of G holds
( H + a = H + b iff b + (- a) in H )
let H be Subgroup of G; :: thesis: ( H + a = H + b iff b + (- a) in H )
thus ( H + a = H + b implies b + (- a) in H ) :: thesis: ( b + (- a) in H implies H + a = H + b )
proof
assume A1: H + a = H + b ; :: thesis: b + (- a) in H
carr H = H + (0_ G) by Th37
.= H + (a + (- a)) by Def5
.= (H + b) + (- a) by A1, ThB34
.= H + (b + (- a)) by ThB34 ;
hence b + (- a) in H by Th119; :: thesis: verum
end;
assume b + (- a) in H ; :: thesis: H + a = H + b
hence H + a = (H + (b + (- a))) + a by Th119
.= H + ((b + (- a)) + a) by ThB34
.= H + (b + ((- a) + a)) by RLVECT_1:def 3
.= H + (b + (0_ G)) by Def5
.= H + b by Def4 ;
:: thesis: verum