let x, y, z, a, b be Element of {0,1,2}; :: thesis: ( a = 0 & b = 1 implies ( x + y = y + x & (x + y) + z = x + (y + z) & x + a = x & x + (- x) = a & x * y = y * x & (x * y) * z = x * (y * z) & b * x = x & ( x <> a implies ex y being Element of {0,1,2} st x * y = b ) & a <> b & x * (y + z) = (x * y) + (x * z) ) )
assume that
A1: a = 0 and
A2: b = 1 ; :: thesis: ( x + y = y + x & (x + y) + z = x + (y + z) & x + a = x & x + (- x) = a & x * y = y * x & (x * y) * z = x * (y * z) & b * x = x & ( x <> a implies ex y being Element of {0,1,2} st x * y = b ) & a <> b & x * (y + z) = (x * y) + (x * z) )
thus x + y = y + x :: thesis: ( (x + y) + z = x + (y + z) & x + a = x & x + (- x) = a & x * y = y * x & (x * y) * z = x * (y * z) & b * x = x & ( x <> a implies ex y being Element of {0,1,2} st x * y = b ) & a <> b & x * (y + z) = (x * y) + (x * z) )

proof

now :: thesis: x + y = y + x

per cases ( x = 0 or y = 0 or ( x = 1 & y = 1 ) or ( x = 1 & y = 2 ) or ( x = 2 & y = 1 ) or ( x = 2 & y = 2 ) ) by ENUMSET1:def 1;

suppose A3: x = 0 ; :: thesis: x + y = y + x

hence x + y = y by Def13
.= y + x by A3, Def13 ;
:: thesis: verum

end;

suppose A4: y = 0 ; :: thesis: x + y = y + x

hence x + y = x by Def13
.= y + x by A4, Def13 ;
:: thesis: verum

end;

suppose ( x = 1 & y = 1 ) ; :: thesis: x + y = y + x

hence x + y = y + x ; :: thesis: verum

end;

suppose A5: ( x = 1 & y = 2 ) ; :: thesis: x + y = y + x

hence x + y = 0 by Def13
.= y + x by A5, Def13 ;
:: thesis: verum

end;

suppose A6: ( x = 2 & y = 1 ) ; :: thesis: x + y = y + x

hence x + y = 0 by Def13
.= y + x by A6, Def13 ;
:: thesis: verum

end;

suppose ( x = 2 & y = 2 ) ; :: thesis: x + y = y + x

hence x + y = y + x ; :: thesis: verum

end;

end;

end;

hence x + y = y + x ; :: thesis: verum

end;

thus (x + y) + z = x + (y + z) by A1, Lm7; :: thesis: ( x + a = x & x + (- x) = a & x * y = y * x & (x * y) * z = x * (y * z) & b * x = x & ( x <> a implies ex y being Element of {0,1,2} st x * y = b ) & a <> b & x * (y + z) = (x * y) + (x * z) )
thus x + a = x by A1, Def13; :: thesis: ( x + (- x) = a & x * y = y * x & (x * y) * z = x * (y * z) & b * x = x & ( x <> a implies ex y being Element of {0,1,2} st x * y = b ) & a <> b & x * (y + z) = (x * y) + (x * z) )
thus x + (- x) = a by A1, Lm7; :: thesis: ( x * y = y * x & (x * y) * z = x * (y * z) & b * x = x & ( x <> a implies ex y being Element of {0,1,2} st x * y = b ) & a <> b & x * (y + z) = (x * y) + (x * z) )
thus x * y = y * x :: thesis: ( (x * y) * z = x * (y * z) & b * x = x & ( x <> a implies ex y being Element of {0,1,2} st x * y = b ) & a <> b & x * (y + z) = (x * y) + (x * z) )

proof

now :: thesis: x * y = y * x

per cases ( y = 0 or x = 0 or y = 1 or x = 1 or ( x = 2 & y = 2 ) ) by ENUMSET1:def 1;

suppose A7: y = 0 ; :: thesis: x * y = y * x

hence x * y = 0 by Def14
.= y * x by A7, Def14 ;
:: thesis: verum

end;

suppose A8: x = 0 ; :: thesis: x * y = y * x

hence x * y = 0 by Def14
.= y * x by A8, Def14 ;
:: thesis: verum

end;

suppose A9: y = 1 ; :: thesis: x * y = y * x

hence x * y = x by Def14
.= y * x by A9, Def14 ;
:: thesis: verum

end;

suppose A10: x = 1 ; :: thesis: x * y = y * x

hence x * y = y by Def14
.= y * x by A10, Def14 ;
:: thesis: verum

end;

suppose ( x = 2 & y = 2 ) ; :: thesis: x * y = y * x

hence x * y = y * x ; :: thesis: verum

end;

end;

end;

hence x * y = y * x ; :: thesis: verum

end;

thus (x * y) * z = x * (y * z) :: thesis: ( b * x = x & ( x <> a implies ex y being Element of {0,1,2} st x * y = b ) & a <> b & x * (y + z) = (x * y) + (x * z) )

proof

now :: thesis: (x * y) * z = x * (y * z)

per cases ( z = 0 or y = 0 or x = 0 or z = 1 or y = 1 or x = 1 or ( x = 2 & y = 2 & z = 2 ) ) by ENUMSET1:def 1;

suppose A11: z = 0 ; :: thesis: (x * y) * z = x * (y * z)

then A12: y * z = 0 by Def14;
thus (x * y) * z = 0 by A11, Def14
.= x * (y * z) by A12, Def14 ; :: thesis: verum

end;

suppose A13: y = 0 ; :: thesis: (x * y) * z = x * (y * z)

then A14: y * z = 0 by Def14;
x * y = 0 by A13, Def14;
hence (x * y) * z = 0 by Def14
.= x * (y * z) by A14, Def14 ;
:: thesis: verum

end;

suppose A15: x = 0 ; :: thesis: (x * y) * z = x * (y * z)

then x * y = 0 by Def14;
hence (x * y) * z = 0 by Def14
.= x * (y * z) by A15, Def14 ;
:: thesis: verum

end;

suppose A16: z = 1 ; :: thesis: (x * y) * z = x * (y * z)

then y * z = y by Def14;
hence (x * y) * z = x * (y * z) by A16, Def14; :: thesis: verum

end;

suppose A17: y = 1 ; :: thesis: (x * y) * z = x * (y * z)

then x * y = x by Def14;
hence (x * y) * z = x * (y * z) by A17, Def14; :: thesis: verum

end;

suppose A18: x = 1 ; :: thesis: (x * y) * z = x * (y * z)

hence (x * y) * z = y * z by Def14
.= x * (y * z) by A18, Def14 ;
:: thesis: verum

end;

suppose A19: ( x = 2 & y = 2 & z = 2 ) ; :: thesis: (x * y) * z = x * (y * z)

then A20: y * z = 1 by Def14;
x * y = 1 by A19, Def14;
hence (x * y) * z = x by A19, Def14
.= x * (y * z) by A20, Def14 ;
:: thesis: verum

end;

end;

end;

hence (x * y) * z = x * (y * z) ; :: thesis: verum

end;

thus b * x = x by A2, Def14; :: thesis: ( ( x <> a implies ex y being Element of {0,1,2} st x * y = b ) & a <> b & x * (y + z) = (x * y) + (x * z) )
thus ( x <> a implies ex y being Element of {0,1,2} st x * y = b ) :: thesis: ( a <> b & x * (y + z) = (x * y) + (x * z) )

proof

now :: thesis: ( ( x = 0 & ( x <> a implies ex y being Element of {0,1,2} st x * y = b ) ) or ( x = 1 & ex y being Element of {0,1,2} st
( x <> a implies ex y being Element of {0,1,2} st x * y = b ) ) or ( x = 2 & ex y being Element of {0,1,2} st
( x <> a implies ex y being Element of {0,1,2} st x * y = b ) ) )

per cases ( x = 0 or x = 1 or x = 2 ) by ENUMSET1:def 1;

case x = 0 ; :: thesis: ( x <> a implies ex y being Element of {0,1,2} st x * y = b )

hence ( x <> a implies ex y being Element of {0,1,2} st x * y = b ) by A1; :: thesis: verum

end;

case A21: x = 1 ; :: thesis: ex y being Element of {0,1,2} st
( x <> a implies ex y being Element of {0,1,2} st x * y = b )

reconsider y = 1 as Element of {0,1,2} by ENUMSET1:def 1;
take y = y; :: thesis: ( x <> a implies ex y being Element of {0,1,2} st x * y = b )
x * y = 1 by A21, Def14;
hence ( x <> a implies ex y being Element of {0,1,2} st x * y = b ) by A2; :: thesis: verum

end;

case A22: x = 2 ; :: thesis: ex y being Element of {0,1,2} st
( x <> a implies ex y being Element of {0,1,2} st x * y = b )

reconsider y = 2 as Element of {0,1,2} by ENUMSET1:def 1;
take y = y; :: thesis: ( x <> a implies ex y being Element of {0,1,2} st x * y = b )
x * y = 1 by A22, Def14;
hence ( x <> a implies ex y being Element of {0,1,2} st x * y = b ) by A2; :: thesis: verum

end;

end;

end;

hence ( x <> a implies ex y being Element of {0,1,2} st x * y = b ) ; :: thesis: verum

end;

thus a <> b by A1, A2; :: thesis: x * (y + z) = (x * y) + (x * z)
thus x * (y + z) = (x * y) + (x * z) :: thesis: verum

proof

now :: thesis: x * (y + z) = (x * y) + (x * z)

per cases ( x = 0 or y = 0 or z = 0 or ( x = 1 & y = 1 & z = 1 ) or ( x = 1 & y = 1 & z = 2 ) or ( x = 1 & y = 2 & z = 1 ) or ( x = 1 & y = 2 & z = 2 ) or ( x = 2 & y = 1 & z = 1 ) or ( x = 2 & y = 1 & z = 2 ) or ( x = 2 & y = 2 & z = 1 ) or ( x = 2 & y = 2 & z = 2 ) ) by ENUMSET1:def 1;

suppose A23: x = 0 ; :: thesis: x * (y + z) = (x * y) + (x * z)

then A24: ( x * y = 0 & x * z = 0 ) by Def14;
thus x * (y + z) = 0 by A23, Def14
.= (x * y) + (x * z) by A24, Def13 ; :: thesis: verum

end;

suppose y = 0 ; :: thesis: x * (y + z) = (x * y) + (x * z)

then ( y + z = z & x * y = 0 ) by Def13, Def14;
hence x * (y + z) = (x * y) + (x * z) by Def13; :: thesis: verum

end;

suppose z = 0 ; :: thesis: x * (y + z) = (x * y) + (x * z)

then ( y + z = y & x * z = 0 ) by Def13, Def14;
hence x * (y + z) = (x * y) + (x * z) by Def13; :: thesis: verum

end;

suppose A25: ( x = 1 & y = 1 & z = 1 ) ; :: thesis: x * (y + z) = (x * y) + (x * z)

then x * y = 1 by Def14;
hence x * (y + z) = (x * y) + (x * z) by A25, Def14; :: thesis: verum

end;

suppose A26: ( x = 1 & y = 1 & z = 2 ) ; :: thesis: x * (y + z) = (x * y) + (x * z)

then A27: ( x * y = 1 & x * z = 2 ) by Def14;
y + z = 0 by A26, Def13;
hence x * (y + z) = 0 by Def14
.= (x * y) + (x * z) by A27, Def13 ;
:: thesis: verum

end;

suppose A28: ( x = 1 & y = 2 & z = 1 ) ; :: thesis: x * (y + z) = (x * y) + (x * z)

then A29: ( x * y = 2 & x * z = 1 ) by Def14;
y + z = 0 by A28, Def13;
hence x * (y + z) = 0 by Def14
.= (x * y) + (x * z) by A29, Def13 ;
:: thesis: verum

end;

suppose A30: ( x = 1 & y = 2 & z = 2 ) ; :: thesis: x * (y + z) = (x * y) + (x * z)

then x * y = 2 by Def14;
hence x * (y + z) = (x * y) + (x * z) by A30, Def14; :: thesis: verum

end;

suppose A31: ( x = 2 & y = 1 & z = 1 ) ; :: thesis: x * (y + z) = (x * y) + (x * z)

then A32: x * y = 2 by Def14;
y + z = 2 by A31, Def13;
hence x * (y + z) = 1 by A31, Def14
.= (x * y) + (x * z) by A31, A32, Def13 ;
:: thesis: verum

end;

suppose A33: ( x = 2 & y = 1 & z = 2 ) ; :: thesis: x * (y + z) = (x * y) + (x * z)

then A34: ( x * y = 2 & x * z = 1 ) by Def14;
y + z = 0 by A33, Def13;
hence x * (y + z) = 0 by Def14
.= (x * y) + (x * z) by A34, Def13 ;
:: thesis: verum

end;

suppose A35: ( x = 2 & y = 2 & z = 1 ) ; :: thesis: x * (y + z) = (x * y) + (x * z)

then A36: ( x * y = 1 & x * z = 2 ) by Def14;
y + z = 0 by A35, Def13;
hence x * (y + z) = 0 by Def14
.= (x * y) + (x * z) by A36, Def13 ;
:: thesis: verum

end;

suppose A37: ( x = 2 & y = 2 & z = 2 ) ; :: thesis: x * (y + z) = (x * y) + (x * z)

then A38: x * y = 1 by Def14;
y + z = 1 by A37, Def13;
hence x * (y + z) = 2 by A37, Def14
.= (x * y) + (x * z) by A37, A38, Def13 ;
:: thesis: verum

end;

end;

end;

hence x * (y + z) = (x * y) + (x * z) ; :: thesis: verum

end;