let x be set ; :: thesis: for f being BinOp of {x} holds
( f = (x,x) .--> x & f is having_a_unity & f is commutative & f is associative & f is idempotent & f is invertible & f is cancelable & f is uniquely-decomposable )
let f be BinOp of {x}; :: thesis: ( f = (x,x) .--> x & f is having_a_unity & f is commutative & f is associative & f is idempotent & f is invertible & f is cancelable & f is uniquely-decomposable )
reconsider a = x as Element of {x} by TARSKI:def 1;
A1: [:{x},{x}:] = {[x,x]} by ZFMISC_1:29;
A2: now :: thesis: for y being object st y in {[x,x]} holds
f . y = ((x,x) .--> x) . y
let y be object ; :: thesis: ( y in {[x,x]} implies f . y = ((x,x) .--> x) . y )
assume A3: y in {[x,x]} ; :: thesis: f . y = ((x,x) .--> x) . y
then reconsider b = y as Element of [:{x},{x}:] by ZFMISC_1:29;
thus f . y = f . b
.= x by TARSKI:def 1
.= ((x,x) .--> x) . y by A3, FUNCOP_1:7 ; :: thesis: verum
end;
( dom f = [:{x},{x}:] & dom ((x,x) .--> x) = {[x,x]} ) by FUNCT_2:def 1;
hence f = (x,x) .--> x by A1, A2, FUNCT_1:2; :: thesis: ( f is having_a_unity & f is commutative & f is associative & f is idempotent & f is invertible & f is cancelable & f is uniquely-decomposable )
A4: now :: thesis: for a, b being Element of {x} holds a = b
let a, b be Element of {x}; :: thesis: a = b
a = x by TARSKI:def 1;
hence a = b by TARSKI:def 1; :: thesis: verum
end;
then for b being Element of {x} holds
( f . (a,b) = b & f . (b,a) = b ) ;
then A5: a is_a_unity_wrt f by BINOP_1:3;
hence ex a being Element of {x} st a is_a_unity_wrt f ; :: according to SETWISEO:def 2 :: thesis: ( f is commutative & f is associative & f is idempotent & f is invertible & f is cancelable & f is uniquely-decomposable )
thus for a, b being Element of {x} holds f . (a,b) = f . (b,a) by A4; :: according to BINOP_1:def 2 :: thesis: ( f is associative & f is idempotent & f is invertible & f is cancelable & f is uniquely-decomposable )
thus for a, b, c being Element of {x} holds f . (a,(f . (b,c))) = f . ((f . (a,b)),c) by A4; :: according to BINOP_1:def 3 :: thesis: ( f is idempotent & f is invertible & f is cancelable & f is uniquely-decomposable )
thus for a being Element of {x} holds f . (a,a) = a by A4; :: according to BINOP_1:def 4 :: thesis: ( f is invertible & f is cancelable & f is uniquely-decomposable )
thus for a, b being Element of {x} ex r, l being Element of {x} st
( f . (a,r) = b & f . (l,a) = b ) :: according to MONOID_0:def 5 :: thesis: ( f is cancelable & f is uniquely-decomposable )
proof
let a, b be Element of {x}; :: thesis: ex r, l being Element of {x} st
( f . (a,r) = b & f . (l,a) = b )
take a ; :: thesis: ex l being Element of {x} st
( f . (a,a) = b & f . (l,a) = b )
take a ; :: thesis: ( f . (a,a) = b & f . (a,a) = b )
thus ( f . (a,a) = b & f . (a,a) = b ) by A4; :: thesis: verum
end;
thus for a, b, c being Element of {x} st ( f . (a,b) = f . (a,c) or f . (b,a) = f . (c,a) ) holds
b = c by A4; :: according to MONOID_0:def 8 :: thesis: f is uniquely-decomposable
thus ex a being Element of {x} st a is_a_unity_wrt f by A5; :: according to SETWISEO:def 2,MONOID_0:def 9 :: thesis: for a, b being Element of {x} st f . (a,b) = the_unity_wrt f holds
( a = b & b = the_unity_wrt f )
let a, b be Element of {x}; :: thesis: ( f . (a,b) = the_unity_wrt f implies ( a = b & b = the_unity_wrt f ) )
thus ( f . (a,b) = the_unity_wrt f implies ( a = b & b = the_unity_wrt f ) ) by A4; :: thesis: verum