set X = {0,1,2};
XX: 0 in {0,1,2} by ENUMSET1:def 1;
set f = QLT_Ex1 ;
thus QLT_Ex1 is commutative :: thesis: ( QLT_Ex1 is associative & QLT_Ex1 is idempotent )
proof
let a, b be Element of {0,1,2}; :: according to BINOP_1:def 2 :: thesis: QLT_Ex1 . (a,b) = QLT_Ex1 . (b,a)
per cases ( a = b or a <> b ) ;
suppose a = b ; :: thesis: QLT_Ex1 . (a,b) = QLT_Ex1 . (b,a)
hence QLT_Ex1 . (a,b) = QLT_Ex1 . (b,a) ; :: thesis: verum
end;
suppose A2: a <> b ; :: thesis: QLT_Ex1 . (a,b) = QLT_Ex1 . (b,a)
then QLT_Ex1 . (a,b) = 0 by QLTEx1Def
.= QLT_Ex1 . (b,a) by A2, QLTEx1Def ;
hence QLT_Ex1 . (a,b) = QLT_Ex1 . (b,a) ; :: thesis: verum
end;
end;
end;
thus QLT_Ex1 is associative :: thesis: QLT_Ex1 is idempotent
proof
let a, b, c be Element of {0,1,2}; :: according to BINOP_1:def 3 :: thesis: QLT_Ex1 . (a,(QLT_Ex1 . (b,c))) = QLT_Ex1 . ((QLT_Ex1 . (a,b)),c)
per cases ( ( a = b & b = c ) or ( a <> b & b = c ) or ( a = b & b <> c ) or ( a <> b & b <> c ) ) ;
suppose A1: ( a = b & b = c ) ; :: thesis: QLT_Ex1 . (a,(QLT_Ex1 . (b,c))) = QLT_Ex1 . ((QLT_Ex1 . (a,b)),c)
then QLT_Ex1 . (a,b) = a by QLTEx1Def;
hence QLT_Ex1 . (a,(QLT_Ex1 . (b,c))) = QLT_Ex1 . ((QLT_Ex1 . (a,b)),c) by A1; :: thesis: verum
end;
suppose A1: ( a <> b & b = c ) ; :: thesis: QLT_Ex1 . (a,(QLT_Ex1 . (b,c))) = QLT_Ex1 . ((QLT_Ex1 . (a,b)),c)
then A2: QLT_Ex1 . (a,b) = 0 by QLTEx1Def;
D2: 0 in {0,1,2} by ENUMSET1:def 1;
QLT_Ex1 . ((QLT_Ex1 . (a,b)),c) = QLT_Ex1 . (0,c) by A1, QLTEx1Def
.= 0 by QLTEx1Def, D2 ;
hence QLT_Ex1 . (a,(QLT_Ex1 . (b,c))) = QLT_Ex1 . ((QLT_Ex1 . (a,b)),c) by A2, QLTEx1Def, A1; :: thesis: verum
end;
suppose A1: ( a = b & b <> c ) ; :: thesis: QLT_Ex1 . (a,(QLT_Ex1 . (b,c))) = QLT_Ex1 . ((QLT_Ex1 . (a,b)),c)
then A2: QLT_Ex1 . (a,b) = a by QLTEx1Def;
A3: QLT_Ex1 . (b,c) = 0 by QLTEx1Def, A1;
per cases ( a = 0 or a <> 0 ) ;
suppose a = 0 ; :: thesis: QLT_Ex1 . (a,(QLT_Ex1 . (b,c))) = QLT_Ex1 . ((QLT_Ex1 . (a,b)),c)
hence QLT_Ex1 . (a,(QLT_Ex1 . (b,c))) = QLT_Ex1 . ((QLT_Ex1 . (a,b)),c) by A3, A1, A2; :: thesis: verum
end;
suppose a <> 0 ; :: thesis: QLT_Ex1 . (a,(QLT_Ex1 . (b,c))) = QLT_Ex1 . ((QLT_Ex1 . (a,b)),c)
hence QLT_Ex1 . (a,(QLT_Ex1 . (b,c))) = QLT_Ex1 . ((QLT_Ex1 . (a,b)),c) by QLTEx1Def, A3, A1, A2; :: thesis: verum
end;
end;
end;
suppose A1: ( a <> b & b <> c ) ; :: thesis: QLT_Ex1 . (a,(QLT_Ex1 . (b,c))) = QLT_Ex1 . ((QLT_Ex1 . (a,b)),c)
then A3: QLT_Ex1 . (b,c) = 0 by QLTEx1Def;
per cases ( a = 0 or a <> 0 ) ;
suppose B1: a = 0 ; :: thesis: QLT_Ex1 . (a,(QLT_Ex1 . (b,c))) = QLT_Ex1 . ((QLT_Ex1 . (a,b)),c)
QLT_Ex1 . ((QLT_Ex1 . (a,b)),c) = QLT_Ex1 . (0,c) by A1, QLTEx1Def
.= 0 by B1, QLTEx1Def ;
hence QLT_Ex1 . (a,(QLT_Ex1 . (b,c))) = QLT_Ex1 . ((QLT_Ex1 . (a,b)),c) by B1, QLTEx1Def, A3; :: thesis: verum
end;
suppose b1: a <> 0 ; :: thesis: QLT_Ex1 . (a,(QLT_Ex1 . (b,c))) = QLT_Ex1 . ((QLT_Ex1 . (a,b)),c)
QLT_Ex1 . ((QLT_Ex1 . (a,b)),c) = QLT_Ex1 . (0,c) by A1, QLTEx1Def
.= 0 by QLTEx1Def, XX ;
hence QLT_Ex1 . (a,(QLT_Ex1 . (b,c))) = QLT_Ex1 . ((QLT_Ex1 . (a,b)),c) by b1, QLTEx1Def, A3; :: thesis: verum
end;
end;
end;
end;
end;
let a be Element of {0,1,2}; :: according to BINOP_1:def 4 :: thesis: QLT_Ex1 . (a,a) = a
thus QLT_Ex1 . (a,a) = a by QLTEx1Def; :: thesis: verum