Metamath Proof Explorer


Theorem rngohom1

Description: A ring homomorphism preserves 1 . (Contributed by Jeff Madsen, 24-Jun-2011)

Ref Expression
Hypotheses rnghom1.1 H = 2 nd R
rnghom1.2 U = GId H
rnghom1.3 K = 2 nd S
rnghom1.4 V = GId K
Assertion rngohom1 Could not format assertion : No typesetting found for |- ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) -> ( F ` U ) = V ) with typecode |-

Proof

Step Hyp Ref Expression
1 rnghom1.1 H = 2 nd R
2 rnghom1.2 U = GId H
3 rnghom1.3 K = 2 nd S
4 rnghom1.4 V = GId K
5 eqid 1 st R = 1 st R
6 eqid ran 1 st R = ran 1 st R
7 eqid 1 st S = 1 st S
8 eqid ran 1 st S = ran 1 st S
9 5 1 6 2 7 3 8 4 isrngohom Could not format ( ( R e. RingOps /\ S e. RingOps ) -> ( F e. ( R RingOpsHom S ) <-> ( F : ran ( 1st ` R ) --> ran ( 1st ` S ) /\ ( F ` U ) = V /\ A. x e. ran ( 1st ` R ) A. y e. ran ( 1st ` R ) ( ( F ` ( x ( 1st ` R ) y ) ) = ( ( F ` x ) ( 1st ` S ) ( F ` y ) ) /\ ( F ` ( x H y ) ) = ( ( F ` x ) K ( F ` y ) ) ) ) ) ) : No typesetting found for |- ( ( R e. RingOps /\ S e. RingOps ) -> ( F e. ( R RingOpsHom S ) <-> ( F : ran ( 1st ` R ) --> ran ( 1st ` S ) /\ ( F ` U ) = V /\ A. x e. ran ( 1st ` R ) A. y e. ran ( 1st ` R ) ( ( F ` ( x ( 1st ` R ) y ) ) = ( ( F ` x ) ( 1st ` S ) ( F ` y ) ) /\ ( F ` ( x H y ) ) = ( ( F ` x ) K ( F ` y ) ) ) ) ) ) with typecode |-
10 9 biimpa Could not format ( ( ( R e. RingOps /\ S e. RingOps ) /\ F e. ( R RingOpsHom S ) ) -> ( F : ran ( 1st ` R ) --> ran ( 1st ` S ) /\ ( F ` U ) = V /\ A. x e. ran ( 1st ` R ) A. y e. ran ( 1st ` R ) ( ( F ` ( x ( 1st ` R ) y ) ) = ( ( F ` x ) ( 1st ` S ) ( F ` y ) ) /\ ( F ` ( x H y ) ) = ( ( F ` x ) K ( F ` y ) ) ) ) ) : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps ) /\ F e. ( R RingOpsHom S ) ) -> ( F : ran ( 1st ` R ) --> ran ( 1st ` S ) /\ ( F ` U ) = V /\ A. x e. ran ( 1st ` R ) A. y e. ran ( 1st ` R ) ( ( F ` ( x ( 1st ` R ) y ) ) = ( ( F ` x ) ( 1st ` S ) ( F ` y ) ) /\ ( F ` ( x H y ) ) = ( ( F ` x ) K ( F ` y ) ) ) ) ) with typecode |-
11 10 simp2d Could not format ( ( ( R e. RingOps /\ S e. RingOps ) /\ F e. ( R RingOpsHom S ) ) -> ( F ` U ) = V ) : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps ) /\ F e. ( R RingOpsHom S ) ) -> ( F ` U ) = V ) with typecode |-
12 11 3impa Could not format ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) -> ( F ` U ) = V ) : No typesetting found for |- ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) -> ( F ` U ) = V ) with typecode |-