Metamath Proof Explorer

Theorem rnghmrcl

Description: Reverse closure of a non-unital ring homomorphism. (Contributed by AV, 22-Feb-2020)

		Ref	Expression
	Assertion	rnghmrcl	\|- ( F e. ( R RngHomo S ) -> ( R e. Rng /\ S e. Rng ) )

Proof

Step	Hyp	Ref	Expression
1		df-rnghomo	\|- RngHomo = ( r e. Rng , s e. Rng \|-> [_ ( Base ` r ) / v ]_ [_ ( Base ` s ) / w ]_ { f e. ( w ^m v ) \| A. x e. v A. y e. v ( ( f ` ( x ( +g ` r ) y ) ) = ( ( f ` x ) ( +g ` s ) ( f ` y ) ) /\ ( f ` ( x ( .r ` r ) y ) ) = ( ( f ` x ) ( .r ` s ) ( f ` y ) ) ) } )
2	1	elmpocl	\|- ( F e. ( R RngHomo S ) -> ( R e. Rng /\ S e. Rng ) )

Step

Hyp

Ref

Expression

df-rnghomo

 |-  RngHomo = ( r e. Rng , s e. Rng |-> [_ ( Base ` r ) / v ]_ [_ ( Base ` s ) / w ]_ { f e. ( w ^m v ) | A. x e. v A. y e. v ( ( f ` ( x ( +g ` r ) y ) ) = ( ( f ` x ) ( +g ` s ) ( f ` y ) ) /\ ( f ` ( x ( .r ` r ) y ) ) = ( ( f ` x ) ( .r ` s ) ( f ` y ) ) ) } )

elmpocl

 |-  ( F e. ( R RngHomo S ) -> ( R e. Rng /\ S e. Rng ) )