set K = RenField r;

thus RenField r is Abelian :: thesis: ( RenField r is add-associative & RenField r is right_zeroed & RenField r is right_complementable )

thus RenField r is Abelian :: thesis: ( RenField r is add-associative & RenField r is right_zeroed & RenField r is right_complementable )

proof

end;

thus
RenField r is add-associative
:: thesis: ( RenField r is right_zeroed & RenField r is right_complementable )now :: thesis: for a, b being Element of (RenField r) holds a + b = b + a

hence
RenField r is Abelian
; :: thesis: verumlet a, b be Element of (RenField r); :: thesis: a + b = b + a

reconsider a1 = a, b1 = b as Element of rng r by defrf;

thus a + b = (ren_add r) . (a,b) by defrf

.= r . (((r ") . a1) + ((r ") . b1)) by defra

.= (ren_add r) . (b,a) by defra

.= b + a by defrf ; :: thesis: verum

end;reconsider a1 = a, b1 = b as Element of rng r by defrf;

thus a + b = (ren_add r) . (a,b) by defrf

.= r . (((r ") . a1) + ((r ") . b1)) by defra

.= (ren_add r) . (b,a) by defra

.= b + a by defrf ; :: thesis: verum

proof

end;

thus
RenField r is right_zeroed
:: thesis: RenField r is right_complementable now :: thesis: for a, b, c being Element of (RenField r) holds (a + b) + c = a + (b + c)

hence
RenField r is add-associative
; :: thesis: verumlet a, b, c be Element of (RenField r); :: thesis: (a + b) + c = a + (b + c)

reconsider a1 = a, b1 = b, c1 = c as Element of rng r by defrf;

H: dom r = the carrier of F by defr;

then reconsider ab = r . (((r ") . a1) + ((r ") . b1)), bc = r . (((r ") . b1) + ((r ") . c1)) as Element of rng r by FUNCT_1:3;

thus (a + b) + c = (ren_add r) . ((a + b),c) by defrf

.= (ren_add r) . (((ren_add r) . (a,b)),c) by defrf

.= (ren_add r) . ((r . (((r ") . a1) + ((r ") . b1))),c) by defra

.= r . (((r ") . ab) + ((r ") . c1)) by defra

.= r . ((((r ") . a1) + ((r ") . b1)) + ((r ") . c1)) by H, FUNCT_1:34

.= r . (((r ") . a1) + (((r ") . b1) + ((r ") . c1))) by RLVECT_1:def 3

.= r . (((r ") . a1) + ((r ") . bc)) by H, FUNCT_1:34

.= (ren_add r) . (a,(r . (((r ") . b1) + ((r ") . c1)))) by defra

.= (ren_add r) . (a,((ren_add r) . (b,c))) by defra

.= (ren_add r) . (a,(b + c)) by defrf

.= a + (b + c) by defrf ; :: thesis: verum

end;reconsider a1 = a, b1 = b, c1 = c as Element of rng r by defrf;

H: dom r = the carrier of F by defr;

then reconsider ab = r . (((r ") . a1) + ((r ") . b1)), bc = r . (((r ") . b1) + ((r ") . c1)) as Element of rng r by FUNCT_1:3;

thus (a + b) + c = (ren_add r) . ((a + b),c) by defrf

.= (ren_add r) . (((ren_add r) . (a,b)),c) by defrf

.= (ren_add r) . ((r . (((r ") . a1) + ((r ") . b1))),c) by defra

.= r . (((r ") . ab) + ((r ") . c1)) by defra

.= r . ((((r ") . a1) + ((r ") . b1)) + ((r ") . c1)) by H, FUNCT_1:34

.= r . (((r ") . a1) + (((r ") . b1) + ((r ") . c1))) by RLVECT_1:def 3

.= r . (((r ") . a1) + ((r ") . bc)) by H, FUNCT_1:34

.= (ren_add r) . (a,(r . (((r ") . b1) + ((r ") . c1)))) by defra

.= (ren_add r) . (a,((ren_add r) . (b,c))) by defra

.= (ren_add r) . (a,(b + c)) by defrf

.= a + (b + c) by defrf ; :: thesis: verum

proof

end;

thus
RenField r is right_complementable
:: thesis: verumnow :: thesis: for a being Element of (RenField r) holds a + (0. (RenField r)) = a

hence
RenField r is right_zeroed
; :: thesis: verumlet a be Element of (RenField r); :: thesis: a + (0. (RenField r)) = a

reconsider a1 = a as Element of rng r by defrf;

H0: dom r = the carrier of F by defr;

then reconsider o = r . (0. F) as Element of rng r by FUNCT_1:3;

H1: (r ") . (r . (0. F)) = 0. F by H0, FUNCT_1:34;

thus a + (0. (RenField r)) = (ren_add r) . (a,(0. (RenField r))) by defrf

.= (ren_add r) . (a,(r . (0. F))) by defrf

.= r . (((r ") . a1) + ((r ") . o)) by defra

.= a by H1, FUNCT_1:35 ; :: thesis: verum

end;reconsider a1 = a as Element of rng r by defrf;

H0: dom r = the carrier of F by defr;

then reconsider o = r . (0. F) as Element of rng r by FUNCT_1:3;

H1: (r ") . (r . (0. F)) = 0. F by H0, FUNCT_1:34;

thus a + (0. (RenField r)) = (ren_add r) . (a,(0. (RenField r))) by defrf

.= (ren_add r) . (a,(r . (0. F))) by defrf

.= r . (((r ") . a1) + ((r ") . o)) by defra

.= a by H1, FUNCT_1:35 ; :: thesis: verum

proof

end;

now :: thesis: for a being Element of (RenField r) holds a is right_complementable

hence
RenField r is right_complementable
; :: thesis: verumlet a be Element of (RenField r); :: thesis: a is right_complementable

reconsider a1 = a as Element of rng r by defrf;

(r ") . a1 is right_complementable ;

then consider b1 being Element of F such that

H0: ((r ") . a1) + b1 = 0. F ;

H1: rng r = the carrier of (RenField r) by defrf;

H2: dom r = the carrier of F by defr;

then reconsider b = r . b1 as Element of (RenField r) by H1, FUNCT_1:3;

reconsider o = r . b1 as Element of rng r by H2, FUNCT_1:3;

a + b = (ren_add r) . (a,b) by defrf

.= r . (((r ") . a1) + ((r ") . o)) by defra

.= r . (0. F) by H0, H2, FUNCT_1:34

.= 0. (RenField r) by defrf ;

hence a is right_complementable ; :: thesis: verum

end;reconsider a1 = a as Element of rng r by defrf;

(r ") . a1 is right_complementable ;

then consider b1 being Element of F such that

H0: ((r ") . a1) + b1 = 0. F ;

H1: rng r = the carrier of (RenField r) by defrf;

H2: dom r = the carrier of F by defr;

then reconsider b = r . b1 as Element of (RenField r) by H1, FUNCT_1:3;

reconsider o = r . b1 as Element of rng r by H2, FUNCT_1:3;

a + b = (ren_add r) . (a,b) by defrf

.= r . (((r ") . a1) + ((r ") . o)) by defra

.= r . (0. F) by H0, H2, FUNCT_1:34

.= 0. (RenField r) by defrf ;

hence a is right_complementable ; :: thesis: verum