let G be non empty multMagma ; :: thesis: ( G is associative implies ( G is invertible iff ( G is unital & the multF of G is having_an_inverseOp ) ) )
assume A1: G is associative ; :: thesis: ( G is invertible iff ( G is unital & the multF of G is having_an_inverseOp ) )
thus ( G is invertible implies ( G is unital & H2(G) is having_an_inverseOp ) ) :: thesis: ( G is unital & the multF of G is having_an_inverseOp implies G is invertible )
proof
set e = the Element of G;
assume A2: G is invertible ; :: thesis: ( G is unital & H2(G) is having_an_inverseOp )
then consider x, y being Element of G such that
A3: the Element of G * x = the Element of G and
A4: y * the Element of G = the Element of G by Th10;
A5: now :: thesis: for a being Element of G holds
( y * a = a & a * x = a )
let a be Element of G; :: thesis: ( y * a = a & a * x = a )
A6: ex b, c being Element of G st
( the Element of G * b = a & c * the Element of G = a ) by A2, Th10;
hence y * a = a by A1, A4; :: thesis: a * x = a
thus a * x = a by A1, A3, A6; :: thesis: verum
end;
then A7: ( y * x = x & y * x = y ) ;
hence G is unital by A5; :: thesis: H2(G) is having_an_inverseOp
defpred S1[ Element of G, Element of G] means ( $1 * $2 = x & $2 * $1 = x );
A8: for a being Element of G ex b being Element of G st S1[a,b]
proof
let a be Element of G; :: thesis: ex b being Element of G st S1[a,b]
consider b, c being Element of G such that
A9: ( a * b = x & c * a = x ) by A2, Th10;
take b ; :: thesis: S1[a,b]
( c * (a * b) = (c * a) * b & x * b = b ) by A1, A5, A7;
hence S1[a,b] by A5, A9; :: thesis: verum
end;
ex f being Function of the carrier of G, the carrier of G st
for x being Element of G holds S1[x,f . x] from FUNCT_2:sch 3(A8);
 then consider u being UnOp of H1(G) such that
A10: for a being Element of G holds S1[a,u . a] ;
now :: thesis: for b being Element of G holds
( H2(G) . (x,b) = b & H2(G) . (b,x) = b )
let b be Element of G; :: thesis: ( H2(G) . (x,b) = b & H2(G) . (b,x) = b )
( x * b = H2(G) . (x,b) & b * x = H2(G) . (b,x) ) ;
hence ( H2(G) . (x,b) = b & H2(G) . (b,x) = b ) by A5, A7; :: thesis: verum
end;
then x is_a_unity_wrt H2(G) by BINOP_1:3;
then A11: x = the_unity_wrt H2(G) by BINOP_1:def 8;
take u ; :: according to FINSEQOP:def 2 :: thesis: u is_an_inverseOp_wrt H2(G)
let a be Element of G; :: according to FINSEQOP:def 1 :: thesis: ( H2(G) . (a,(u . a)) = the_unity_wrt H2(G) & H2(G) . ((u . a),a) = the_unity_wrt H2(G) )
( H2(G) . (a,(u . a)) = a * (u . a) & H2(G) . ((u . a),a) = (u . a) * a ) ;
hence ( H2(G) . (a,(u . a)) = the_unity_wrt H2(G) & H2(G) . ((u . a),a) = the_unity_wrt H2(G) ) by A10, A11; :: thesis: verum
end;
assume A12: H2(G) is having_a_unity ; :: according to MONOID_0:def 10 :: thesis: ( not the multF of G is having_an_inverseOp or G is invertible )
given u being UnOp of H1(G) such that A13: u is_an_inverseOp_wrt H2(G) ; :: according to FINSEQOP:def 2 :: thesis: G is invertible
let a be Element of G; :: according to MONOID_0:def 5,MONOID_0:def 16 :: thesis: for b being Element of the carrier of G ex r, l being Element of the carrier of G st
( the multF of G . (a,r) = b & the multF of G . (l,a) = b )
let c be Element of G; :: thesis: ex r, l being Element of the carrier of G st
( the multF of G . (a,r) = c & the multF of G . (l,a) = c )
take l = (u . a) * c; :: thesis: ex l being Element of the carrier of G st
( the multF of G . (a,l) = c & the multF of G . (l,a) = c )
take r = c * (u . a); :: thesis: ( the multF of G . (a,l) = c & the multF of G . (r,a) = c )
thus H2(G) . (a,l) = a * l
.= (a * (u . a)) * c by A1
.= H2(G) . ((the_unity_wrt H2(G)),c) by A13
.= c by A12, SETWISEO:15 ; :: thesis: the multF of G . (r,a) = c
thus H2(G) . (r,a) = r * a
.= c * ((u . a) * a) by A1
.= H2(G) . (c,(the_unity_wrt H2(G))) by A13
.= c by A12, SETWISEO:15 ; :: thesis: verum