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

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 Def16
.= y + x by A3, Def16 ;
:: thesis: verum

end;

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

hence x + y = x by Def16
.= y + x by A4, Def16 ;
:: 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 Def16
.= y + x by A5, Def16 ;
:: thesis: verum

end;

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

hence x + y = 0 by Def16
.= y + x by A6, Def16 ;
:: 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, Def16; :: 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

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 Def17
.= y * x by A7, Def17 ;
:: thesis: verum

end;

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

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

end;

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

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

end;

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

hence x * y = y by Def17
.= y * x by A10, Def17 ;
:: 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

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 Def17;
thus (x * y) * z = 0 by A11, Def17
.= x * (y * z) by A12, Def17 ; :: thesis: verum

end;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

end;

end;

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

end;

thus b * x = x by A2, Def17; :: 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

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, Def17;
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, Def17;
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

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 Def17;
thus x * (y + z) = 0 by A23, Def17
.= (x * y) + (x * z) by A24, Def16 ; :: thesis: verum

end;

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

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

end;

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

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

end;

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

then x * y = 1 by Def17;
hence x * (y + z) = (x * y) + (x * z) by A25, Def17; :: 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 Def17;
y + z = 0 by A26, Def16;
hence x * (y + z) = 0 by Def17
.= (x * y) + (x * z) by A27, Def16 ;
:: 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 Def17;
y + z = 0 by A28, Def16;
hence x * (y + z) = 0 by Def17
.= (x * y) + (x * z) by A29, Def16 ;
:: thesis: verum

end;

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

then x * y = 2 by Def17;
hence x * (y + z) = (x * y) + (x * z) by A30, Def17; :: 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 Def17;
y + z = 2 by A31, Def16;
hence x * (y + z) = 1 by A31, Def17
.= (x * y) + (x * z) by A31, A32, Def16 ;
:: 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 Def17;
y + z = 0 by A33, Def16;
hence x * (y + z) = 0 by Def17
.= (x * y) + (x * z) by A34, Def16 ;
:: 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 Def17;
y + z = 0 by A35, Def16;
hence x * (y + z) = 0 by Def17
.= (x * y) + (x * z) by A36, Def16 ;
:: 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 Def17;
y + z = 1 by A37, Def16;
hence x * (y + z) = 2 by A37, Def17
.= (x * y) + (x * z) by A37, A38, Def16 ;
:: thesis: verum

end;

end;

end;

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

end;