let n be non zero Nat; :: thesis: ( not addLoopStr(# the carrier of (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #) is empty & addLoopStr(# the carrier of (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #) is Abelian & addLoopStr(# the carrier of (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #) is right_complementable & addLoopStr(# the carrier of (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #) is add-associative & addLoopStr(# the carrier of (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #) is right_zeroed )
A1: 1 <= n by NAT_1:14;
now :: thesis: INT.Ring n is Ring
per cases ( n = 1 or n <> 1 ) ;
end;
end;
then reconsider R = INT.Ring n as Ring ;
set S = addLoopStr(# the carrier of (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #);
A2: for v, w being Element of addLoopStr(# the carrier of (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #) holds v + w = w + v
proof
let v, w be Element of addLoopStr(# the carrier of (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #); :: thesis: v + w = w + v
reconsider v1 = v, w1 = w as Element of R ;
thus v + w = v1 + w1
.= w1 + v1
.= w + v ; :: thesis: verum
end;
A3: for x being Element of addLoopStr(# the carrier of (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #) holds x is right_complementable
proof
let v be Element of addLoopStr(# the carrier of (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #); :: thesis: v is right_complementable
reconsider v1 = v as Element of R ;
consider w1 being Element of R such that
A4: v1 + w1 = 0. R by ALGSTR_0:def 11;
reconsider w = w1 as Element of addLoopStr(# the carrier of (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #) ;
v + w = 0. addLoopStr(# the carrier of (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #) by A4;
hence v is right_complementable ; :: thesis: verum
end;
A5: for u, v, w being Element of addLoopStr(# the carrier of (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #) holds (u + v) + w = u + (v + w)
proof
let u, v, w be Element of addLoopStr(# the carrier of (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #); :: thesis: (u + v) + w = u + (v + w)
reconsider u1 = u, v1 = v, w1 = w as Element of R ;
thus (u + v) + w = (u1 + v1) + w1
.= u1 + (v1 + w1) by RLVECT_1:def 3
.= u + (v + w) ; :: thesis: verum
end;
A6: for v being Element of addLoopStr(# the carrier of (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #) holds v + (0. addLoopStr(# the carrier of (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #)) = v
proof
let v be Element of addLoopStr(# the carrier of (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #); :: thesis: v + (0. addLoopStr(# the carrier of (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #)) = v
reconsider v1 = v as Element of R ;
thus v + (0. addLoopStr(# the carrier of (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #)) = v1 + (0. R)
.= v ; :: thesis: verum
end;
thus ( not addLoopStr(# the carrier of (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #) is empty & addLoopStr(# the carrier of (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #) is Abelian & addLoopStr(# the carrier of (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #) is right_complementable & addLoopStr(# the carrier of (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #) is add-associative & addLoopStr(# the carrier of (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #) is right_zeroed ) by A2, A3, A5, A6, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4; :: thesis: verum