set X = {0,1,2};
XX:
0 in {0,1,2}
by ENUMSET1:def 1;
set f = QLT_Ex1 ;
thus
QLT_Ex1 is commutative
( QLT_Ex1 is associative & QLT_Ex1 is idempotent )
thus
QLT_Ex1 is associative
QLT_Ex1 is idempotent proof
let a,
b,
c be
Element of
{0,1,2};
BINOP_1:def 3 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 )
;
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;
verum end; suppose A1:
(
a <> b &
b <> c )
;
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
;
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;
verum end; suppose b1:
a <> 0
;
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;
verum end; end; end; end;
end;
let a be Element of {0,1,2}; BINOP_1:def 4 QLT_Ex1 . (a,a) = a
thus
QLT_Ex1 . (a,a) = a
by QLTEx1Def; verum