let R1, R2 be Ring; ( 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:
now let x,
y,
z be
Element of
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 & ex x9 being Element of BiModStr(# 1,op2,op0,(pr2 ( the carrier of R1,1)),(pr1 (1, the carrier of R2)) #) st x + x9 = 0. BiModStr(# 1,op2,op0,(pr2 ( the carrier of R1,1)),(pr1 (1, the carrier of R2)) #) )A2:
x + (0. BiModStr(# 1,op2,op0,(pr2 ( the carrier of R1,1)),(pr1 (1, the carrier of R2)) #)) = {}
by CARD_1:49, TARSKI:def 1;
(
x + y = {} &
(x + y) + z = {} )
by CARD_1:49, 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
x9 being
Element of
BiModStr(# 1,
op2,
op0,
(pr2 ( the carrier of R1,1)),
(pr1 (1, the carrier of R2)) #) st
x + x9 = 0. BiModStr(# 1,
op2,
op0,
(pr2 ( the carrier of R1,1)),
(pr1 (1, the carrier of R2)) #) )
by A2, CARD_1:49, TARSKI:def 1;
verum end;
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)) #);
ALGSTR_0:def 16 x is right_complementable
take
x
;
ALGSTR_0:def 11 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:49, TARSKI:def 1;
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 2, RLVECT_1:def 3, RLVECT_1:def 4; verum