let D be non empty set ; for f being BinOp of D holds
( f is invertible iff ( f is left-invertible & f is right-invertible ) )
let f be BinOp of D; ( f is invertible iff ( f is left-invertible & f is right-invertible ) )
thus
( f is invertible implies ( f is left-invertible & f is right-invertible ) )
( f is left-invertible & f is right-invertible implies f is invertible )proof
assume A1:
for
a,
b being
Element of
D ex
r,
l being
Element of
D st
(
f . (
a,
r)
= b &
f . (
l,
a)
= b )
;
MONOID_0:def 5 ( f is left-invertible & f is right-invertible )
now for a, b being Element of D ex l being Element of D st f . (l,a) = blet a,
b be
Element of
D;
ex l being Element of D st f . (l,a) = bconsider r,
l being
Element of
D such that
f . (
a,
r)
= b
and A2:
f . (
l,
a)
= b
by A1;
take l =
l;
f . (l,a) = bthus
f . (
l,
a)
= b
by A2;
verum end;
hence
for
a,
b being
Element of
D ex
l being
Element of
D st
f . (
l,
a)
= b
;
MONOID_0:def 3 f is right-invertible
let a,
b be
Element of
D;
MONOID_0:def 4 ex r being Element of D st f . (a,r) = b
consider r,
l being
Element of
D such that A3:
f . (
a,
r)
= b
and
f . (
l,
a)
= b
by A1;
take
r
;
f . (a,r) = b
thus
f . (
a,
r)
= b
by A3;
verum
end;
assume that
A4:
for a, b being Element of D ex l being Element of D st f . (l,a) = b
and
A5:
for a, b being Element of D ex r being Element of D st f . (a,r) = b
; MONOID_0:def 3,MONOID_0:def 4 f is invertible
let a, b be Element of D; MONOID_0:def 5 ex r, l being Element of D st
( f . (a,r) = b & f . (l,a) = b )
consider l being Element of D such that
A6:
f . (l,a) = b
by A4;
consider r being Element of D such that
A7:
f . (a,r) = b
by A5;
take
r
; ex l being Element of D st
( f . (a,r) = b & f . (l,a) = b )
take
l
; ( f . (a,r) = b & f . (l,a) = b )
thus
( f . (a,r) = b & f . (l,a) = b )
by A6, A7; verum