set F = Z_3 ;
reconsider a = 0. Z_3, b = 1. Z_3 as Element of {0,1,2} ;
now :: thesis: for x, y, z being Scalar of Z_3 holds
( x + y = y + x & (x + y) + z = x + (y + z) & x + () = x & x + (- x) = 0. Z_3 & x * y = y * x & (x * y) * z = x * (y * z) & () * x = x & x * () = x & ( x <> 0. Z_3 implies ex y being Scalar of Z_3 st x * y = 1. Z_3 ) & 0. Z_3 <> 1. Z_3 & x * (y + z) = (x * y) + (x * z) )
let x, y, z be Scalar of Z_3; :: thesis: ( x + y = y + x & (x + y) + z = x + (y + z) & x + () = x & x + (- x) = 0. Z_3 & x * y = y * x & (x * y) * z = x * (y * z) & () * x = x & x * () = x & ( x <> 0. Z_3 implies ex y being Scalar of Z_3 st x * y = 1. Z_3 ) & 0. Z_3 <> 1. Z_3 & x * (y + z) = (x * y) + (x * z) )
thus ( x + y = y + x & (x + y) + z = x + (y + z) & x + () = x & x + (- x) = 0. Z_3 & x * y = y * x & (x * y) * z = x * (y * z) & () * x = x & x * () = x & ( x <> 0. Z_3 implies ex y being Scalar of Z_3 st x * y = 1. Z_3 ) & 0. Z_3 <> 1. Z_3 & x * (y + z) = (x * y) + (x * z) ) :: thesis: verum
proof
reconsider X = x, Y = y, Z = z as Element of {0,1,2} ;
A1: ( x * y = X * Y & x * z = X * Z ) by Th23;
thus x + y = X + Y by Th23
.= Y + X by Th25
.= y + x by Th23 ; :: thesis: ( (x + y) + z = x + (y + z) & x + () = x & x + (- x) = 0. Z_3 & x * y = y * x & (x * y) * z = x * (y * z) & () * x = x & x * () = x & ( x <> 0. Z_3 implies ex y being Scalar of Z_3 st x * y = 1. Z_3 ) & 0. Z_3 <> 1. Z_3 & x * (y + z) = (x * y) + (x * z) )
thus (x + y) + z = (X + Y) + Z by Th24
.= X + (Y + Z) by Th25
.= x + (y + z) by Th24 ; :: thesis: ( x + () = x & x + (- x) = 0. Z_3 & x * y = y * x & (x * y) * z = x * (y * z) & () * x = x & x * () = x & ( x <> 0. Z_3 implies ex y being Scalar of Z_3 st x * y = 1. Z_3 ) & 0. Z_3 <> 1. Z_3 & x * (y + z) = (x * y) + (x * z) )
thus x + () = X + a by Th23
.= x by Th25 ; :: thesis: ( x + (- x) = 0. Z_3 & x * y = y * x & (x * y) * z = x * (y * z) & () * x = x & x * () = x & ( x <> 0. Z_3 implies ex y being Scalar of Z_3 st x * y = 1. Z_3 ) & 0. Z_3 <> 1. Z_3 & x * (y + z) = (x * y) + (x * z) )
- x = - X by Th23;
hence x + (- x) = X + (- X) by Th23
.= 0. Z_3 by Th25 ;
:: thesis: ( x * y = y * x & (x * y) * z = x * (y * z) & () * x = x & x * () = x & ( x <> 0. Z_3 implies ex y being Scalar of Z_3 st x * y = 1. Z_3 ) & 0. Z_3 <> 1. Z_3 & x * (y + z) = (x * y) + (x * z) )
thus x * y = X * Y by Th23
.= Y * X by Th25
.= y * x by Th23 ; :: thesis: ( (x * y) * z = x * (y * z) & () * x = x & x * () = x & ( x <> 0. Z_3 implies ex y being Scalar of Z_3 st x * y = 1. Z_3 ) & 0. Z_3 <> 1. Z_3 & x * (y + z) = (x * y) + (x * z) )
thus (x * y) * z = (X * Y) * Z by Th24
.= X * (Y * Z) by Th25
.= x * (y * z) by Th24 ; :: thesis: ( () * x = x & x * () = x & ( x <> 0. Z_3 implies ex y being Scalar of Z_3 st x * y = 1. Z_3 ) & 0. Z_3 <> 1. Z_3 & x * (y + z) = (x * y) + (x * z) )
thus () * x = b * X by Th23
.= x by Th25 ; :: thesis: ( x * () = x & ( x <> 0. Z_3 implies ex y being Scalar of Z_3 st x * y = 1. Z_3 ) & 0. Z_3 <> 1. Z_3 & x * (y + z) = (x * y) + (x * z) )
thus x * () = X * b by Th23
.= b * X by Th25
.= x by Th25 ; :: thesis: ( ( x <> 0. Z_3 implies ex y being Scalar of Z_3 st x * y = 1. Z_3 ) & 0. Z_3 <> 1. Z_3 & x * (y + z) = (x * y) + (x * z) )
thus ( x <> 0. Z_3 implies ex y being Scalar of Z_3 st x * y = 1. Z_3 ) :: thesis: ( 0. Z_3 <> 1. Z_3 & x * (y + z) = (x * y) + (x * z) )
proof
assume x <> 0. Z_3 ; :: thesis: ex y being Scalar of Z_3 st x * y = 1. Z_3
then consider Y being Element of {0,1,2} such that
A2: X * Y = b by Th25;
reconsider y = Y as Scalar of Z_3 ;
take y ; :: thesis: x * y = 1. Z_3
thus x * y = 1. Z_3 by ; :: thesis: verum
end;
thus 0. Z_3 <> 1. Z_3 ; :: thesis: x * (y + z) = (x * y) + (x * z)
y + z = Y + Z by Th23;
hence x * (y + z) = X * (Y + Z) by Th23
.= (X * Y) + (X * Z) by Th25
.= (x * y) + (x * z) by ;
:: thesis: verum
end;
end;
then reconsider F = Z_3 as Field by Th26;
(1. F) + (1. F) = b + b by Def15
.= 2 by Def13 ;
hence Z_3 is Fanoian Field by ; :: thesis: verum