let R1, R2 be Ring; :: thesis: ( H3(R1,R2) is Abelian & H3(R1,R2) is add-associative & H3(R1,R2) is right_zeroed & H3(R1,R2) is right_complementable )
set G = BiModStr(# 1,op2 ,op0 ,(pr2 the carrier of R1,1),(pr1 1,the carrier of R2) #);
A1:
BiModStr(# 1,op2 ,op0 ,(pr2 the carrier of R1,1),(pr1 1,the carrier of R2) #) is right_complementable
proof
let x be
Element of
BiModStr(# 1,
op2 ,
op0 ,
(pr2 the carrier of R1,1),
(pr1 1,the carrier of R2) #);
:: according to ALGSTR_0:def 16 :: thesis: x is right_complementable
take
x
;
:: according to ALGSTR_0:def 11 :: thesis: x + x = 0. BiModStr(# 1,op2 ,op0 ,(pr2 the carrier of R1,1),(pr1 1,the carrier of R2) #)
thus
x + x = 0. BiModStr(# 1,
op2 ,
op0 ,
(pr2 the carrier of R1,1),
(pr1 1,the carrier of R2) #)
by CARD_1:87, TARSKI:def 1;
:: thesis: verum
end;
now let x,
y,
z be
Element of
BiModStr(# 1,
op2 ,
op0 ,
(pr2 the carrier of R1,1),
(pr1 1,the carrier of R2) #);
:: thesis: ( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. BiModStr(# 1,op2 ,op0 ,(pr2 the carrier of R1,1),(pr1 1,the carrier of R2) #)) = x & ex x' being Element of BiModStr(# 1,op2 ,op0 ,(pr2 the carrier of R1,1),(pr1 1,the carrier of R2) #) st x + x' = 0. BiModStr(# 1,op2 ,op0 ,(pr2 the carrier of R1,1),(pr1 1,the carrier of R2) #) )
(
x + y = {} &
y + x = {} &
(x + y) + z = {} &
x + (y + z) = {} &
x + (0. BiModStr(# 1,op2 ,op0 ,(pr2 the carrier of R1,1),(pr1 1,the carrier of R2) #)) = {} &
x = {} &
x + (- x) = {} &
0. BiModStr(# 1,
op2 ,
op0 ,
(pr2 the carrier of R1,1),
(pr1 1,the carrier of R2) #)
= {} )
by CARD_1:87, TARSKI:def 1;
hence
(
x + y = y + x &
(x + y) + z = x + (y + z) &
x + (0. BiModStr(# 1,op2 ,op0 ,(pr2 the carrier of R1,1),(pr1 1,the carrier of R2) #)) = x & ex
x' being
Element of
BiModStr(# 1,
op2 ,
op0 ,
(pr2 the carrier of R1,1),
(pr1 1,the carrier of R2) #) st
x + x' = 0. BiModStr(# 1,
op2 ,
op0 ,
(pr2 the carrier of R1,1),
(pr1 1,the carrier of R2) #) )
;
:: thesis: verum end;
hence
( H3(R1,R2) is Abelian & H3(R1,R2) is add-associative & H3(R1,R2) is right_zeroed & H3(R1,R2) is right_complementable )
by A1, RLVECT_1:def 5, RLVECT_1:def 6, RLVECT_1:def 7; :: thesis: verum