let A be Abelian addGroup; :: thesis: ( addLoopStr(# the carrier of A, the addF of A,(0_ A) #) is Abelian & addLoopStr(# the carrier of A, the addF of A,(0_ A) #) is add-associative & addLoopStr(# the carrier of A, the addF of A,(0_ A) #) is right_zeroed & addLoopStr(# the carrier of A, the addF of A,(0_ A) #) is right_complementable )
set G = addLoopStr(# the carrier of A, the addF of A,(0_ A) #);
thus addLoopStr(# the carrier of A, the addF of A,(0_ A) #) is Abelian :: thesis: ( addLoopStr(# the carrier of A, the addF of A,(0_ A) #) is add-associative & addLoopStr(# the carrier of A, the addF of A,(0_ A) #) is right_zeroed & addLoopStr(# the carrier of A, the addF of A,(0_ A) #) is right_complementable )
proof
let a, b be Element of addLoopStr(# the carrier of A, the addF of A,(0_ A) #); :: according to RLVECT_1:def 2 :: thesis: a + b = b + a
reconsider x = a, y = b as Element of A ;
A1: for a, b being Element of addLoopStr(# the carrier of A, the addF of A,(0_ A) #)
for x, y being Element of A st a = x & b = y holds
a + b = x + y ;
thus a + b = x + y
.= b + a by A1 ; :: thesis: verum
end;
hereby :: according to RLVECT_1:def 3 :: thesis: ( addLoopStr(# the carrier of A, the addF of A,(0_ A) #) is right_zeroed & addLoopStr(# the carrier of A, the addF of A,(0_ A) #) is right_complementable )
let a, b, c be Element of addLoopStr(# the carrier of A, the addF of A,(0_ A) #); :: thesis: (a + b) + c = a + (b + c)
reconsider x = a, y = b, z = c as Element of A ;
thus (a + b) + c = (x + y) + z
.= x + (y + z) by RLVECT_1:def 3
.= a + (b + c) ; :: thesis: verum
end;
hereby :: according to RLVECT_1:def 4 :: thesis: addLoopStr(# the carrier of A, the addF of A,(0_ A) #) is right_complementable
let a be Element of addLoopStr(# the carrier of A, the addF of A,(0_ A) #); :: thesis: a + (0. addLoopStr(# the carrier of A, the addF of A,(0_ A) #)) = a
reconsider x = a as Element of A ;
thus a + (0. addLoopStr(# the carrier of A, the addF of A,(0_ A) #)) = x + (0_ A)
.= a by Def4 ; :: thesis: verum
end;
let a be Element of addLoopStr(# the carrier of A, the addF of A,(0_ A) #); :: according to ALGSTR_0:def 16 :: thesis: a is right_complementable
reconsider x = a as Element of A ;
reconsider b = (add_inverse A) . x as Element of addLoopStr(# the carrier of A, the addF of A,(0_ A) #) ;
take b ; :: according to ALGSTR_0:def 11 :: thesis: a + b = 0. addLoopStr(# the carrier of A, the addF of A,(0_ A) #)
thus a + b = x + (- x) by Def6
.= 0. addLoopStr(# the carrier of A, the addF of A,(0_ A) #) by Def5 ; :: thesis: verum