Metamath Proof Explorer

Theorem rngohomf

Description: A ring homomorphism is a function. (Contributed by Jeff Madsen, 19-Jun-2010)

Ref Expression
Hypotheses rnghomf.1 
|- G = ( 1st ` R )
rnghomf.2 
|- X = ran G
rnghomf.3 
|- J = ( 1st ` S )
rnghomf.4 
|- Y = ran J
Assertion rngohomf 
|- ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RngHom S ) ) -> F : X --> Y )

Proof

Step Hyp Ref Expression
1 rnghomf.1 
 |-  G = ( 1st ` R )
2 rnghomf.2 
 |-  X = ran G
3 rnghomf.3 
 |-  J = ( 1st ` S )
4 rnghomf.4 
 |-  Y = ran J
5 eqid 
 |-  ( 2nd ` R ) = ( 2nd ` R )
6 eqid 
 |-  ( GId ` ( 2nd ` R ) ) = ( GId ` ( 2nd ` R ) )
7 eqid 
 |-  ( 2nd ` S ) = ( 2nd ` S )
8 eqid 
 |-  ( GId ` ( 2nd ` S ) ) = ( GId ` ( 2nd ` S ) )
9 1 5 2 6 3 7 4 8 isrngohom 
 |-  ( ( R e. RingOps /\ S e. RingOps ) -> ( F e. ( R RngHom S ) <-> ( F : X --> Y /\ ( F ` ( GId ` ( 2nd ` R ) ) ) = ( GId ` ( 2nd ` S ) ) /\ A. x e. X A. y e. X ( ( F ` ( x G y ) ) = ( ( F ` x ) J ( F ` y ) ) /\ ( F ` ( x ( 2nd ` R ) y ) ) = ( ( F ` x ) ( 2nd ` S ) ( F ` y ) ) ) ) ) )
10 9 biimpa 
 |-  ( ( ( R e. RingOps /\ S e. RingOps ) /\ F e. ( R RngHom S ) ) -> ( F : X --> Y /\ ( F ` ( GId ` ( 2nd ` R ) ) ) = ( GId ` ( 2nd ` S ) ) /\ A. x e. X A. y e. X ( ( F ` ( x G y ) ) = ( ( F ` x ) J ( F ` y ) ) /\ ( F ` ( x ( 2nd ` R ) y ) ) = ( ( F ` x ) ( 2nd ` S ) ( F ` y ) ) ) ) )
11 10 simp1d 
 |-  ( ( ( R e. RingOps /\ S e. RingOps ) /\ F e. ( R RngHom S ) ) -> F : X --> Y )
12 11 3impa 
 |-  ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RngHom S ) ) -> F : X --> Y )