set K = RenField r;

thus C: RenField r is commutative :: thesis: ( RenField r is associative & RenField r is well-unital & RenField r is distributive & RenField r is almost_left_invertible )

thus C: RenField r is commutative :: thesis: ( RenField r is associative & RenField r is well-unital & RenField r is distributive & RenField r is almost_left_invertible )

proof

end;

thus
RenField r is associative
:: thesis: ( RenField r is well-unital & RenField r is distributive & RenField r is almost_left_invertible )now :: thesis: for a, b being Element of (RenField r) holds a * b = b * a

hence
RenField r is commutative
; :: 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_mult r) . (a,b) by defrf

.= r . (((r ") . a1) * ((r ") . b1)) by defrm

.= r . (((r ") . b1) * ((r ") . a1)) by GROUP_1:def 12

.= (ren_mult r) . (b,a) by defrm

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

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

thus a * b = (ren_mult r) . (a,b) by defrf

.= r . (((r ") . a1) * ((r ") . b1)) by defrm

.= r . (((r ") . b1) * ((r ") . a1)) by GROUP_1:def 12

.= (ren_mult r) . (b,a) by defrm

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

proof

end;

thus
RenField r is well-unital
:: thesis: ( RenField r is distributive & RenField r is almost_left_invertible )now :: thesis: for a, b, c being Element of (RenField r) holds (a * b) * c = a * (b * c)

hence
RenField r is 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;

H0: 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_mult r) . ((a * b),c) by defrf

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

.= (ren_mult r) . ((r . (((r ") . a1) * ((r ") . b1))),c) by defrm

.= r . (((r ") . ab) * ((r ") . c1)) by defrm

.= r . ((((r ") . a1) * ((r ") . b1)) * ((r ") . c1)) by H0, FUNCT_1:34

.= r . (((r ") . a1) * (((r ") . b1) * ((r ") . c1))) by GROUP_1:def 3

.= r . (((r ") . a1) * ((r ") . bc)) by H0, FUNCT_1:34

.= (ren_mult r) . (a,(r . (((r ") . b1) * ((r ") . c1)))) by defrm

.= (ren_mult r) . (a,((ren_mult r) . (b,c))) by defrm

.= (ren_mult 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;

H0: 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_mult r) . ((a * b),c) by defrf

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

.= (ren_mult r) . ((r . (((r ") . a1) * ((r ") . b1))),c) by defrm

.= r . (((r ") . ab) * ((r ") . c1)) by defrm

.= r . ((((r ") . a1) * ((r ") . b1)) * ((r ") . c1)) by H0, FUNCT_1:34

.= r . (((r ") . a1) * (((r ") . b1) * ((r ") . c1))) by GROUP_1:def 3

.= r . (((r ") . a1) * ((r ") . bc)) by H0, FUNCT_1:34

.= (ren_mult r) . (a,(r . (((r ") . b1) * ((r ") . c1)))) by defrm

.= (ren_mult r) . (a,((ren_mult r) . (b,c))) by defrm

.= (ren_mult r) . (a,(b * c)) by defrf

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

proof

end;

thus
RenField r is distributive
:: thesis: RenField r is almost_left_invertible now :: thesis: for a being Element of (RenField r) holds

( a * (1. (RenField r)) = a & (1. (RenField r)) * a = a )

hence
RenField r is well-unital
; :: thesis: verum( a * (1. (RenField r)) = a & (1. (RenField r)) * a = a )

let a be Element of (RenField r); :: thesis: ( a * (1. (RenField r)) = a & (1. (RenField r)) * a = a )

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

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

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

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

thus a * (1. (RenField r)) = (ren_mult r) . (a,(1. (RenField r))) by defrf

.= (ren_mult r) . (a,(r . (1. F))) by defrf

.= r . (((r ") . a1) * ((r ") . o)) by defrm

.= a by H1, FUNCT_1:35 ; :: thesis: (1. (RenField r)) * a = a

thus (1. (RenField r)) * a = (ren_mult r) . ((1. (RenField r)),a) by defrf

.= (ren_mult r) . ((r . (1. F)),a) by defrf

.= r . (((r ") . o) * ((r ") . a1)) by defrm

.= 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 . (1. F) as Element of rng r by FUNCT_1:3;

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

thus a * (1. (RenField r)) = (ren_mult r) . (a,(1. (RenField r))) by defrf

.= (ren_mult r) . (a,(r . (1. F))) by defrf

.= r . (((r ") . a1) * ((r ") . o)) by defrm

.= a by H1, FUNCT_1:35 ; :: thesis: (1. (RenField r)) * a = a

thus (1. (RenField r)) * a = (ren_mult r) . ((1. (RenField r)),a) by defrf

.= (ren_mult r) . ((r . (1. F)),a) by defrf

.= r . (((r ") . o) * ((r ") . a1)) by defrm

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

proof

end;

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

let a, b, c be Element of (RenField r); :: thesis: (a + b) * c = (a * c) + (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)), ac = r . (((r ") . a1) * ((r ") . c1)), bc = r . (((r ") . b1) * ((r ") . c1)) as Element of rng r by FUNCT_1:3;

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

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

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

.= r . (((r ") . ab) * ((r ") . c1)) by defrm

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

.= r . ((((r ") . a1) * ((r ") . c1)) + (((r ") . b1) * ((r ") . c1))) by VECTSP_1:def 7

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

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

.= (ren_add r) . (ac,bc) by defra

.= (ren_add r) . ((r . (((r ") . a1) * ((r ") . c1))),((ren_mult r) . (b,c))) by defrm

.= (ren_add r) . (((ren_mult r) . (a,c)),((ren_mult r) . (b,c))) by defrm

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

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

.= (a * c) + (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)), ac = r . (((r ") . a1) * ((r ") . c1)), bc = r . (((r ") . b1) * ((r ") . c1)) as Element of rng r by FUNCT_1:3;

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

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

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

.= r . (((r ") . ab) * ((r ") . c1)) by defrm

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

.= r . ((((r ") . a1) * ((r ") . c1)) + (((r ") . b1) * ((r ") . c1))) by VECTSP_1:def 7

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

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

.= (ren_add r) . (ac,bc) by defra

.= (ren_add r) . ((r . (((r ") . a1) * ((r ") . c1))),((ren_mult r) . (b,c))) by defrm

.= (ren_add r) . (((ren_mult r) . (a,c)),((ren_mult r) . (b,c))) by defrm

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

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

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

now :: thesis: for a, b, c being Element of (RenField r) holds

( (a + b) * c = (a * c) + (b * c) & a * (b + c) = (a * b) + (a * c) )

hence
RenField r is distributive
; :: thesis: verum( (a + b) * c = (a * c) + (b * c) & a * (b + c) = (a * b) + (a * c) )

let a, b, c be Element of (RenField r); :: thesis: ( (a + b) * c = (a * c) + (b * c) & a * (b + c) = (a * b) + (a * c) )

thus (a + b) * c = (a * c) + (b * c) by D; :: thesis: a * (b + c) = (a * b) + (a * c)

thus a * (b + c) = (b + c) * a by C

.= (b * a) + (c * a) by D

.= (a * b) + (c * a) by C

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

end;thus (a + b) * c = (a * c) + (b * c) by D; :: thesis: a * (b + c) = (a * b) + (a * c)

thus a * (b + c) = (b + c) * a by C

.= (b * a) + (c * a) by D

.= (a * b) + (c * a) by C

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

proof

end;

now :: thesis: for a being Element of (RenField r) st a <> 0. (RenField r) holds

a is left_invertible

hence
RenField r is almost_left_invertible
; :: thesis: veruma is left_invertible

let a be Element of (RenField r); :: thesis: ( a <> 0. (RenField r) implies a is left_invertible )

assume AS: a <> 0. (RenField r) ; :: thesis: a is left_invertible

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

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

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

I2: dom (r ") = rng r by FUNCT_1:33;

0. (RenField r) = r . (0. F) by defrf;

then (r ") . a1 <> (r ") . (r . (0. F)) by I1, I2, AS, FUNCT_1:def 4;

then (r ") . a1 <> 0. F by I0, FUNCT_1:34;

then (r ") . a1 is left_invertible by ALGSTR_0:def 39;

then consider b1 being Element of F such that

H0: b1 * ((r ") . a1) = 1. 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;

b * a = (ren_mult r) . (b,a) by defrf

.= r . (((r ") . o) * ((r ") . a1)) by defrm

.= r . (1. F) by I0, H0, FUNCT_1:34

.= 1. (RenField r) by defrf ;

hence a is left_invertible ; :: thesis: verum

end;assume AS: a <> 0. (RenField r) ; :: thesis: a is left_invertible

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

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

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

I2: dom (r ") = rng r by FUNCT_1:33;

0. (RenField r) = r . (0. F) by defrf;

then (r ") . a1 <> (r ") . (r . (0. F)) by I1, I2, AS, FUNCT_1:def 4;

then (r ") . a1 <> 0. F by I0, FUNCT_1:34;

then (r ") . a1 is left_invertible by ALGSTR_0:def 39;

then consider b1 being Element of F such that

H0: b1 * ((r ") . a1) = 1. 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;

b * a = (ren_mult r) . (b,a) by defrf

.= r . (((r ") . o) * ((r ") . a1)) by defrm

.= r . (1. F) by I0, H0, FUNCT_1:34

.= 1. (RenField r) by defrf ;

hence a is left_invertible ; :: thesis: verum