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