thus
not GroupHomography3 is empty
; :: thesis: ( GroupHomography3 is associative & GroupHomography3 is Group-like )

thus GroupHomography3 is associative :: thesis: GroupHomography3 is Group-like_{1} being Element of the carrier of GroupHomography3 holds

( b_{1} * e = b_{1} & e * b_{1} = b_{1} & ex b_{2} being Element of the carrier of GroupHomography3 st

( b_{1} * b_{2} = e & b_{2} * b_{1} = e ) )

let h be Element of GroupHomography3; :: thesis: ( h * e = h & e * h = h & ex b_{1} being Element of the carrier of GroupHomography3 st

( h * b_{1} = e & b_{1} * h = e ) )

thus ( h * e = h & e * h = h ) by Lm1; :: thesis: ex b_{1} being Element of the carrier of GroupHomography3 st

( h * b_{1} = e & b_{1} * h = e )

h in EnsHomography3 ;

then consider N being invertible Matrix of 3,F_Real such that

A9: h = homography N ;

reconsider Ng = N ~ as invertible Matrix of 3,F_Real ;

homography Ng in EnsHomography3 ;

then reconsider g = homography Ng as Element of GroupHomography3 ;

take g ; :: thesis: ( h * g = e & g * h = e )

thus ( h * g = e & g * h = e ) by A9, Lm2; :: thesis: verum

thus GroupHomography3 is associative :: thesis: GroupHomography3 is Group-like

proof

take
e
; :: according to GROUP_1:def 2 :: thesis: for b
let x, y, z be Element of GroupHomography3; :: according to GROUP_1:def 3 :: thesis: (x * y) * z = x * (y * z)

reconsider xf = x, yf = y, zf = z as Element of EnsHomography3 ;

A7: x * y = xf (*) yf by Def02;

A8: (x * y) * z = (xf (*) yf) (*) zf by Def02, A7;

y * z = yf (*) zf by Def02;

then x * (y * z) = xf (*) (yf (*) zf) by Def02;

hence (x * y) * z = x * (y * z) by A8, Ta1; :: thesis: verum

end;reconsider xf = x, yf = y, zf = z as Element of EnsHomography3 ;

A7: x * y = xf (*) yf by Def02;

A8: (x * y) * z = (xf (*) yf) (*) zf by Def02, A7;

y * z = yf (*) zf by Def02;

then x * (y * z) = xf (*) (yf (*) zf) by Def02;

hence (x * y) * z = x * (y * z) by A8, Ta1; :: thesis: verum

( b

( b

let h be Element of GroupHomography3; :: thesis: ( h * e = h & e * h = h & ex b

( h * b

thus ( h * e = h & e * h = h ) by Lm1; :: thesis: ex b

( h * b

h in EnsHomography3 ;

then consider N being invertible Matrix of 3,F_Real such that

A9: h = homography N ;

reconsider Ng = N ~ as invertible Matrix of 3,F_Real ;

homography Ng in EnsHomography3 ;

then reconsider g = homography Ng as Element of GroupHomography3 ;

take g ; :: thesis: ( h * g = e & g * h = e )

thus ( h * g = e & g * h = e ) by A9, Lm2; :: thesis: verum