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 A1: ( a = 0 & 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 A2: x = 0 ; :: thesis: x + y = y + x
hence x + y = y by Def16
.= y + x by A2, Def16 ;
:: thesis: verum
end;
suppose A3: y = 0 ; :: thesis: x + y = y + x
hence x + y = x by Def16
.= y + x by A3, Def16 ;
:: thesis: verum
end;
suppose ( x = 1 & y = 1 ) ; :: thesis: x + y = y + x
hence x + y = y + x ; :: thesis: verum
end;
suppose A4: ( x = 1 & y = 2 ) ; :: thesis: x + y = y + x
hence x + y = 0 by Def16
.= y + x by A4, Def16 ;
:: thesis: verum
end;
suppose A5: ( x = 2 & y = 1 ) ; :: thesis: x + y = y + x
hence x + y = 0 by Def16
.= y + x by A5, 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 A6: y = 0 ; :: thesis: x * y = y * x
hence x * y = 0 by Def17
.= y * x by A6, Def17 ;
:: thesis: verum
end;
suppose A7: x = 0 ; :: thesis: x * y = y * x
hence x * y = 0 by Def17
.= y * x by A7, Def17 ;
:: thesis: verum
end;
suppose A8: y = 1 ; :: thesis: x * y = y * x
hence x * y = x by Def17
.= y * x by A8, Def17 ;
:: thesis: verum
end;
suppose A9: x = 1 ; :: thesis: x * y = y * x
hence x * y = y by Def17
.= y * x by A9, 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 A10: z = 0 ; :: thesis: (x * y) * z = x * (y * z)
then A11: y * z = 0 by Def17;
thus (x * y) * z = 0 by A10, Def17
.= x * (y * z) by A11, Def17 ; :: thesis: verum
end;
suppose y = 0 ; :: thesis: (x * y) * z = x * (y * z)
then A12: ( x * y = 0 & y * z = 0 ) by Def17;
hence (x * y) * z = 0 by Def17
.= x * (y * z) by A12, Def17 ;
:: thesis: verum
end;
suppose A13: 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 A13, Def17 ;
:: thesis: verum
end;
suppose A14: z = 1 ; :: thesis: (x * y) * z = x * (y * z)
then y * z = y by Def17;
hence (x * y) * z = x * (y * z) by A14, Def17; :: thesis: verum
end;
suppose y = 1 ; :: thesis: (x * y) * z = x * (y * z)
then ( x * y = x & y * z = z ) by Def17;
hence (x * y) * z = x * (y * z) ; :: thesis: verum
end;
suppose A15: x = 1 ; :: thesis: (x * y) * z = x * (y * z)
hence (x * y) * z = y * z by Def17
.= x * (y * z) by A15, Def17 ;
:: thesis: verum
end;
suppose A16: ( x = 2 & y = 2 & z = 2 ) ; :: thesis: (x * y) * z = x * (y * z)
then A17: ( x * y = 1 & y * z = 1 ) by Def17;
hence (x * y) * z = x by A16, Def17
.= x * (y * z) by A17, Def17 ;
:: thesis: verum
end;
end;
end;
hence (x * y) * z = x * (y * z) ; :: thesis: verum
end;
thus b * x = x by A1, 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 A18: 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 A18, Def17;
hence ( x <> a implies ex y being Element of {0 ,1,2} st x * y = b ) by A1; :: thesis: verum
end;
case A19: 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 A19, Def17;
hence ( x <> a implies ex y being Element of {0 ,1,2} st x * y = b ) by A1; :: 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; :: 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 A20: x = 0 ; :: thesis: x * (y + z) = (x * y) + (x * z)
then A21: ( x * y = 0 & x * z = 0 ) by Def17;
thus x * (y + z) = 0 by A20, Def17
.= (x * y) + (x * z) by A21, 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 A22: ( x = 1 & y = 1 & z = 1 ) ; :: thesis: x * (y + z) = (x * y) + (x * z)
then ( y + z = 2 & x * y = 1 & x * z = 1 ) by Def16, Def17;
hence x * (y + z) = (x * y) + (x * z) by A22, Def17; :: thesis: verum
end;
suppose ( x = 1 & y = 1 & z = 2 ) ; :: thesis: x * (y + z) = (x * y) + (x * z)
then A23: ( y + z = 0 & x * y = 1 & x * z = 2 ) by Def16, Def17;
hence x * (y + z) = 0 by Def17
.= (x * y) + (x * z) by A23, Def16 ;
:: thesis: verum
end;
suppose ( x = 1 & y = 2 & z = 1 ) ; :: thesis: x * (y + z) = (x * y) + (x * z)
then A24: ( y + z = 0 & x * y = 2 & x * z = 1 ) by Def16, Def17;
hence x * (y + z) = 0 by Def17
.= (x * y) + (x * z) by A24, Def16 ;
:: thesis: verum
end;
suppose A25: ( x = 1 & y = 2 & z = 2 ) ; :: thesis: x * (y + z) = (x * y) + (x * z)
then ( y + z = 1 & x * y = 2 & x * z = 2 ) by Def16, Def17;
hence x * (y + z) = (x * y) + (x * z) by A25, Def17; :: thesis: verum
end;
suppose A26: ( x = 2 & y = 1 & z = 1 ) ; :: thesis: x * (y + z) = (x * y) + (x * z)
then A27: ( y + z = 2 & x * y = 2 & x * z = 2 ) by Def16, Def17;
hence x * (y + z) = 1 by A26, Def17
.= (x * y) + (x * z) by A27, Def16 ;
:: thesis: verum
end;
suppose ( x = 2 & y = 1 & z = 2 ) ; :: thesis: x * (y + z) = (x * y) + (x * z)
then A28: ( y + z = 0 & x * y = 2 & x * z = 1 ) by Def16, Def17;
hence x * (y + z) = 0 by Def17
.= (x * y) + (x * z) by A28, Def16 ;
:: thesis: verum
end;
suppose ( x = 2 & y = 2 & z = 1 ) ; :: thesis: x * (y + z) = (x * y) + (x * z)
then A29: ( y + z = 0 & x * y = 1 & x * z = 2 ) by Def16, Def17;
hence x * (y + z) = 0 by Def17
.= (x * y) + (x * z) by A29, Def16 ;
:: thesis: verum
end;
suppose A30: ( x = 2 & y = 2 & z = 2 ) ; :: thesis: x * (y + z) = (x * y) + (x * z)
then A31: ( y + z = 1 & x * y = 1 & x * z = 1 ) by Def16, Def17;
hence x * (y + z) = 2 by A30, Def17
.= (x * y) + (x * z) by A31, Def16 ;
:: thesis: verum
end;
end;
end;
hence x * (y + z) = (x * y) + (x * z) ; :: thesis: verum
end;