Metamath Proof Explorer

Theorem mgmhmrcl

Description: Reverse closure of a magma homomorphism. (Contributed by AV, 24-Feb-2020)

		Ref	Expression
	Assertion	mgmhmrcl	\|- ( F e. ( S MgmHom T ) -> ( S e. Mgm /\ T e. Mgm ) )

Proof

Step	Hyp	Ref	Expression
1		df-mgmhm	\|- MgmHom = ( s e. Mgm , t e. Mgm \|-> { f e. ( ( Base ` t ) ^m ( Base ` s ) ) \| A. x e. ( Base ` s ) A. y e. ( Base ` s ) ( f ` ( x ( +g ` s ) y ) ) = ( ( f ` x ) ( +g ` t ) ( f ` y ) ) } )
2	1	elmpocl	\|- ( F e. ( S MgmHom T ) -> ( S e. Mgm /\ T e. Mgm ) )

Step

Hyp

Ref

Expression

df-mgmhm

 |-  MgmHom = ( s e. Mgm , t e. Mgm |-> { f e. ( ( Base ` t ) ^m ( Base ` s ) ) | A. x e. ( Base ` s ) A. y e. ( Base ` s ) ( f ` ( x ( +g ` s ) y ) ) = ( ( f ` x ) ( +g ` t ) ( f ` y ) ) } )

elmpocl

 |-  ( F e. ( S MgmHom T ) -> ( S e. Mgm /\ T e. Mgm ) )