This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rnghmresel

Description: An element of the non-unital ring homomorphisms restricted to a subset of non-unital rings is a non-unital ring homomorphisms. (Contributed by AV, 9-Mar-2020)

Ref Expression
Hypothesis rnghmresel.h 
|- ( ph -> H = ( RngHom |` ( B X. B ) ) )
Assertion rnghmresel 
|- ( ( ph /\ ( X e. B /\ Y e. B ) /\ F e. ( X H Y ) ) -> F e. ( X RngHom Y ) )

Proof

Step Hyp Ref Expression
1 rnghmresel.h 
 |-  ( ph -> H = ( RngHom |` ( B X. B ) ) )
2 1 adantr 
 |-  ( ( ph /\ ( X e. B /\ Y e. B ) ) -> H = ( RngHom |` ( B X. B ) ) )
3 2 oveqd 
 |-  ( ( ph /\ ( X e. B /\ Y e. B ) ) -> ( X H Y ) = ( X ( RngHom |` ( B X. B ) ) Y ) )
4 ovres 
 |-  ( ( X e. B /\ Y e. B ) -> ( X ( RngHom |` ( B X. B ) ) Y ) = ( X RngHom Y ) )
5 4 adantl 
 |-  ( ( ph /\ ( X e. B /\ Y e. B ) ) -> ( X ( RngHom |` ( B X. B ) ) Y ) = ( X RngHom Y ) )
6 3 5 eqtrd 
 |-  ( ( ph /\ ( X e. B /\ Y e. B ) ) -> ( X H Y ) = ( X RngHom Y ) )
7 6 eleq2d 
 |-  ( ( ph /\ ( X e. B /\ Y e. B ) ) -> ( F e. ( X H Y ) <-> F e. ( X RngHom Y ) ) )
8 7 biimp3a 
 |-  ( ( ph /\ ( X e. B /\ Y e. B ) /\ F e. ( X H Y ) ) -> F e. ( X RngHom Y ) )