set P = PrimeField F;
A1: 0. (PrimeField F) = 0. F by Def10;
A2: the carrier of (PrimeField F) = carrier/\ F by Def10;
hereby :: according to RLVECT_1:def 2 :: thesis: ( PrimeField F is add-associative & PrimeField F is right_zeroed & PrimeField F is right_complementable )
let x, y be Element of (PrimeField F); :: thesis: x + y = y + x
reconsider a = x, b = y as Element of F by Lm10;
thus x + y = a + b by Lm11
.= y + x by Lm11 ; :: thesis: verum
end;
hereby :: according to RLVECT_1:def 3 :: thesis: ( PrimeField F is right_zeroed & PrimeField F is right_complementable )
let x, y, z be Element of (PrimeField F); :: thesis: (x + y) + z = x + (y + z)
reconsider a = x, b = y, c = z as Element of F by Lm10;
A3: y + z = b + c by Lm11;
x + y = a + b by Lm11;
hence (x + y) + z = (a + b) + c by Lm11
.= a + (b + c) by RLVECT_1:def 3
.= x + (y + z) by A3, Lm11 ;
:: thesis: verum
end;
hereby :: according to RLVECT_1:def 4 :: thesis: PrimeField F is right_complementable
let x be Element of (PrimeField F); :: thesis: x + (0. (PrimeField F)) = x
reconsider a = x as Element of F by Lm10;
thus x + (0. (PrimeField F)) = a + (0. F) by A1, Lm11
.= x ; :: thesis: verum
end;
let x be Element of (PrimeField F); :: according to ALGSTR_0:def 16 :: thesis: x is right_complementable
reconsider a = x as Element of F by Lm10;
x in carrier/\ F by A2;
then consider x1 being Element of F such that
A4: x = x1 and
A5: for K being Subfield of F holds x1 in K ;
now :: thesis: for K being Subfield of F holds - x1 in K
let K be Subfield of F; :: thesis: - x1 in K
x1 in K by A5;
then reconsider t = x1 as Element of K ;
- t = - x1 by GAUSSINT:19;
hence - x1 in K ; :: thesis: verum
end;
then - x1 in carrier/\ F ;
then reconsider y = - x1 as Element of (PrimeField F) by Def10;
take y ; :: according to ALGSTR_0:def 11 :: thesis: x + y = 0. (PrimeField F)
thus x + y = a + (- x1) by Lm11
.= 0. (PrimeField F) by A1, A4, RLVECT_1:5 ; :: thesis: verum