set X = {0,1,2};
set f = QLT_Ex2 ;
thus QLT_Ex2 is commutative :: thesis: ( QLT_Ex2 is associative & QLT_Ex2 is idempotent )

proof

let a, b be Element of {0,1,2}; :: according to BINOP_1:def 2 :: thesis: QLT_Ex2 . (a,b) = QLT_Ex2 . (b,a)

per cases ( a = 1 or b = 1 or ( a <> 1 & b <> 1 ) ) ;

suppose A1: ( a = 1 or b = 1 ) ; :: thesis: QLT_Ex2 . (a,b) = QLT_Ex2 . (b,a)

then QLT_Ex2 . (a,b) = 1 by QLTEx2Def
.= QLT_Ex2 . (b,a) by A1, QLTEx2Def ;
hence QLT_Ex2 . (a,b) = QLT_Ex2 . (b,a) ; :: thesis: verum

end;

suppose A2: ( a <> 1 & b <> 1 ) ; :: thesis: QLT_Ex2 . (a,b) = QLT_Ex2 . (b,a)

then QLT_Ex2 . (a,b) = min (a,b) by QLTEx2Def
.= QLT_Ex2 . (b,a) by A2, QLTEx2Def ;
hence QLT_Ex2 . (a,b) = QLT_Ex2 . (b,a) ; :: thesis: verum

end;

end;

end;

thus QLT_Ex2 is associative :: thesis: QLT_Ex2 is idempotent

proof

let a, b, c be Element of {0,1,2}; :: according to BINOP_1:def 3 :: thesis: QLT_Ex2 . (a,(QLT_Ex2 . (b,c))) = QLT_Ex2 . ((QLT_Ex2 . (a,b)),c)

per cases ( ( a = 1 & ( b = 1 or c = 1 ) ) or ( ( a = 1 or b = 1 ) & c = 1 ) or ( a <> 1 & b = 1 & c <> 1 ) or ( a = 1 & b <> 1 & c = 1 ) or ( a = 1 & b <> 1 & c <> 1 ) or ( a <> 1 & b = 1 & c <> 1 ) or ( a <> 1 & b <> 1 & c = 1 ) or ( a <> 1 & b <> 1 & c <> 1 ) ) ;

suppose A1: ( a = 1 & ( b = 1 or c = 1 ) ) ; :: thesis: QLT_Ex2 . (a,(QLT_Ex2 . (b,c))) = QLT_Ex2 . ((QLT_Ex2 . (a,b)),c)

then A2: QLT_Ex2 . (a,b) = 1 by QLTEx2Def;
A3: QLT_Ex2 . (b,c) = 1 by QLTEx2Def, A1;
QLT_Ex2 . ((QLT_Ex2 . (a,b)),c) = 1 by QLTEx2Def, A2;
hence QLT_Ex2 . (a,(QLT_Ex2 . (b,c))) = QLT_Ex2 . ((QLT_Ex2 . (a,b)),c) by QLTEx2Def, A3; :: thesis: verum

end;

suppose A1: ( ( a = 1 or b = 1 ) & c = 1 ) ; :: thesis: QLT_Ex2 . (a,(QLT_Ex2 . (b,c))) = QLT_Ex2 . ((QLT_Ex2 . (a,b)),c)

then A5: QLT_Ex2 . ((QLT_Ex2 . (a,b)),c) = 1 by QLTEx2Def;
QLT_Ex2 . (b,c) = 1 by QLTEx2Def, A1;
hence QLT_Ex2 . (a,(QLT_Ex2 . (b,c))) = QLT_Ex2 . ((QLT_Ex2 . (a,b)),c) by A5, QLTEx2Def; :: thesis: verum

end;

suppose A1: ( a <> 1 & b = 1 & c <> 1 ) ; :: thesis: QLT_Ex2 . (a,(QLT_Ex2 . (b,c))) = QLT_Ex2 . ((QLT_Ex2 . (a,b)),c)

then QLT_Ex2 . (a,b) = 1 by QLTEx2Def;
then A5: QLT_Ex2 . ((QLT_Ex2 . (a,b)),c) = 1 by QLTEx2Def;
QLT_Ex2 . (b,c) = 1 by QLTEx2Def, A1;
hence QLT_Ex2 . (a,(QLT_Ex2 . (b,c))) = QLT_Ex2 . ((QLT_Ex2 . (a,b)),c) by A5, QLTEx2Def; :: thesis: verum

end;

suppose A1: ( a = 1 & b <> 1 & c = 1 ) ; :: thesis: QLT_Ex2 . (a,(QLT_Ex2 . (b,c))) = QLT_Ex2 . ((QLT_Ex2 . (a,b)),c)

then QLT_Ex2 . (b,c) = 1 by QLTEx2Def;
hence QLT_Ex2 . (a,(QLT_Ex2 . (b,c))) = QLT_Ex2 . ((QLT_Ex2 . (a,b)),c) by QLTEx2Def, A1; :: thesis: verum

end;

suppose A1: ( a = 1 & b <> 1 & c <> 1 ) ; :: thesis: QLT_Ex2 . (a,(QLT_Ex2 . (b,c))) = QLT_Ex2 . ((QLT_Ex2 . (a,b)),c)

then A2: QLT_Ex2 . (a,b) = 1 by QLTEx2Def;
A3: QLT_Ex2 . (b,c) = min (b,c) by QLTEx2Def, A1;

per cases ( min (b,c) = b or min (b,c) = c ) by XXREAL_0:15;

suppose min (b,c) = b ; :: thesis: QLT_Ex2 . (a,(QLT_Ex2 . (b,c))) = QLT_Ex2 . ((QLT_Ex2 . (a,b)),c)

hence QLT_Ex2 . ((QLT_Ex2 . (a,b)),c) = QLT_Ex2 . (a,(QLT_Ex2 . (b,c))) by A2, A3, QLTEx2Def; :: thesis: verum

end;

suppose min (b,c) = c ; :: thesis: QLT_Ex2 . (a,(QLT_Ex2 . (b,c))) = QLT_Ex2 . ((QLT_Ex2 . (a,b)),c)

hence QLT_Ex2 . ((QLT_Ex2 . (a,b)),c) = QLT_Ex2 . (a,(QLT_Ex2 . (b,c))) by A1, QLTEx2Def, A2; :: thesis: verum

end;

end;

end;

suppose A1: ( a <> 1 & b = 1 & c <> 1 ) ; :: thesis: QLT_Ex2 . (a,(QLT_Ex2 . (b,c))) = QLT_Ex2 . ((QLT_Ex2 . (a,b)),c)

then A2: QLT_Ex2 . (a,b) = 1 by QLTEx2Def;
A3: QLT_Ex2 . (b,c) = 1 by QLTEx2Def, A1;
QLT_Ex2 . ((QLT_Ex2 . (a,b)),c) = 1 by QLTEx2Def, A2;
hence QLT_Ex2 . (a,(QLT_Ex2 . (b,c))) = QLT_Ex2 . ((QLT_Ex2 . (a,b)),c) by QLTEx2Def, A3; :: thesis: verum

end;

suppose A1: ( a <> 1 & b <> 1 & c = 1 ) ; :: thesis: QLT_Ex2 . (a,(QLT_Ex2 . (b,c))) = QLT_Ex2 . ((QLT_Ex2 . (a,b)),c)

then A2: QLT_Ex2 . (a,b) = min (a,b) by QLTEx2Def;
A3: QLT_Ex2 . (b,c) = 1 by QLTEx2Def, A1;

per cases ( min (a,b) = a or min (a,b) = b ) by XXREAL_0:15;

suppose min (a,b) = a ; :: thesis: QLT_Ex2 . (a,(QLT_Ex2 . (b,c))) = QLT_Ex2 . ((QLT_Ex2 . (a,b)),c)

QLT_Ex2 . (a,(QLT_Ex2 . (b,c))) = QLT_Ex2 . (a,1) by QLTEx2Def, A1
.= 1 by QLTEx2Def, A1 ;
hence QLT_Ex2 . ((QLT_Ex2 . (a,b)),c) = QLT_Ex2 . (a,(QLT_Ex2 . (b,c))) by QLTEx2Def, A1; :: thesis: verum

end;

suppose min (a,b) = b ; :: thesis: QLT_Ex2 . (a,(QLT_Ex2 . (b,c))) = QLT_Ex2 . ((QLT_Ex2 . (a,b)),c)

hence QLT_Ex2 . ((QLT_Ex2 . (a,b)),c) = QLT_Ex2 . (a,(QLT_Ex2 . (b,c))) by QLTEx2Def, A3, A2; :: thesis: verum

end;

end;

end;

suppose A1: ( a <> 1 & b <> 1 & c <> 1 ) ; :: thesis: QLT_Ex2 . (a,(QLT_Ex2 . (b,c))) = QLT_Ex2 . ((QLT_Ex2 . (a,b)),c)

then A2: QLT_Ex2 . (a,b) = min (a,b) by QLTEx2Def;
A3: QLT_Ex2 . (b,c) = min (b,c) by QLTEx2Def, A1;

per cases ( min (a,c) = a or min (a,c) = c ) by XXREAL_0:15;

suppose C1: min (a,c) = a ; :: thesis: QLT_Ex2 . (a,(QLT_Ex2 . (b,c))) = QLT_Ex2 . ((QLT_Ex2 . (a,b)),c)

per cases ( ( min (a,b) = a & min (b,c) = b ) or ( min (a,b) = a & min (b,c) = c ) or ( min (a,b) = b & min (b,c) = b ) or ( min (a,b) = b & min (b,c) = c ) ) by XXREAL_0:15;

suppose ( min (a,b) = a & min (b,c) = b ) ; :: thesis: QLT_Ex2 . (a,(QLT_Ex2 . (b,c))) = QLT_Ex2 . ((QLT_Ex2 . (a,b)),c)

hence QLT_Ex2 . ((QLT_Ex2 . (a,b)),c) = QLT_Ex2 . (a,(QLT_Ex2 . (b,c))) by A2, A3, C1, QLTEx2Def, A1; :: thesis: verum

end;

suppose ( min (a,b) = a & min (b,c) = c ) ; :: thesis: QLT_Ex2 . (a,(QLT_Ex2 . (b,c))) = QLT_Ex2 . ((QLT_Ex2 . (a,b)),c)

hence QLT_Ex2 . ((QLT_Ex2 . (a,b)),c) = QLT_Ex2 . (a,(QLT_Ex2 . (b,c))) by QLTEx2Def, A1, A2; :: thesis: verum

end;

suppose ( min (a,b) = b & min (b,c) = b ) ; :: thesis: QLT_Ex2 . (a,(QLT_Ex2 . (b,c))) = QLT_Ex2 . ((QLT_Ex2 . (a,b)),c)

hence QLT_Ex2 . ((QLT_Ex2 . (a,b)),c) = QLT_Ex2 . (a,(QLT_Ex2 . (b,c))) by A3, A2; :: thesis: verum

end;

suppose B1: ( min (a,b) = b & min (b,c) = c ) ; :: thesis: QLT_Ex2 . (a,(QLT_Ex2 . (b,c))) = QLT_Ex2 . ((QLT_Ex2 . (a,b)),c)

then ( a <= c & b <= a & c <= b ) by C1, XXREAL_0:def 9;
then ( a <= c & c <= a ) by XXREAL_0:2;
then a = c by XXREAL_0:1;
hence QLT_Ex2 . ((QLT_Ex2 . (a,b)),c) = QLT_Ex2 . (a,(QLT_Ex2 . (b,c))) by B1, A3; :: thesis: verum

end;

end;

end;

suppose C1: min (a,c) = c ; :: thesis: QLT_Ex2 . (a,(QLT_Ex2 . (b,c))) = QLT_Ex2 . ((QLT_Ex2 . (a,b)),c)

per cases ( ( min (a,b) = a & min (b,c) = b ) or ( min (a,b) = a & min (b,c) = c ) or ( min (a,b) = b & min (b,c) = b ) or ( min (a,b) = b & min (b,c) = c ) ) by XXREAL_0:15;

suppose B1: ( min (a,b) = a & min (b,c) = b ) ; :: thesis: QLT_Ex2 . (a,(QLT_Ex2 . (b,c))) = QLT_Ex2 . ((QLT_Ex2 . (a,b)),c)

then ( c <= a & a <= b & b <= c ) by C1, XXREAL_0:def 9;
then ( a <= c & c <= a ) by XXREAL_0:2;
then a = c by XXREAL_0:1;
hence QLT_Ex2 . ((QLT_Ex2 . (a,b)),c) = QLT_Ex2 . (a,(QLT_Ex2 . (b,c))) by A2, B1; :: thesis: verum

end;

suppose ( min (a,b) = a & min (b,c) = c ) ; :: thesis: QLT_Ex2 . (a,(QLT_Ex2 . (b,c))) = QLT_Ex2 . ((QLT_Ex2 . (a,b)),c)

hence QLT_Ex2 . ((QLT_Ex2 . (a,b)),c) = QLT_Ex2 . (a,(QLT_Ex2 . (b,c))) by QLTEx2Def, A1, A2; :: thesis: verum

end;

suppose ( min (a,b) = b & min (b,c) = b ) ; :: thesis: QLT_Ex2 . (a,(QLT_Ex2 . (b,c))) = QLT_Ex2 . ((QLT_Ex2 . (a,b)),c)

hence QLT_Ex2 . ((QLT_Ex2 . (a,b)),c) = QLT_Ex2 . (a,(QLT_Ex2 . (b,c))) by A2, A3; :: thesis: verum

end;

suppose ( min (a,b) = b & min (b,c) = c ) ; :: thesis: QLT_Ex2 . (a,(QLT_Ex2 . (b,c))) = QLT_Ex2 . ((QLT_Ex2 . (a,b)),c)

hence QLT_Ex2 . ((QLT_Ex2 . (a,b)),c) = QLT_Ex2 . (a,(QLT_Ex2 . (b,c))) by C1, QLTEx2Def, A1, A3, A2; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

let a be Element of {0,1,2}; :: according to BINOP_1:def 4 :: thesis: QLT_Ex2 . (a,a) = a

per cases ( a = 1 or a <> 1 ) ;

suppose a = 1 ; :: thesis: QLT_Ex2 . (a,a) = a

hence QLT_Ex2 . (a,a) = a by QLTEx2Def; :: thesis: verum

end;

suppose a <> 1 ; :: thesis: QLT_Ex2 . (a,a) = a

then QLT_Ex2 . (a,a) = min (a,a) by QLTEx2Def
.= a ;
hence QLT_Ex2 . (a,a) = a ; :: thesis: verum

end;

end;