Theorem rngohom1

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

	Ref	Expression
Hypotheses	rnghom1.1	$$⊢H=2^{nd}\left(R\right)$$
	rnghom1.2	$$⊢U=\mathrm{GId}\left(H\right)$$
	rnghom1.3	$$⊢K=2^{nd}\left(S\right)$$
	rnghom1.4	$$⊢V=\mathrm{GId}\left(K\right)$$
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}\left(R\right)$$
2		rnghom1.2	$$⊢U=\mathrm{GId}\left(H\right)$$
3		rnghom1.3	$$⊢K=2^{nd}\left(S\right)$$
4		rnghom1.4	$$⊢V=\mathrm{GId}\left(K\right)$$
5		eqid	$$⊢1^{st}\left(R\right)=1^{st}\left(R\right)$$
6		eqid	$$⊢\mathrm{ran}{1}^{st}\left(R\right)=\mathrm{ran}{1}^{st}\left(R\right)$$
7		eqid	$$⊢1^{st}\left(S\right)=1^{st}\left(S\right)$$
8		eqid	$$⊢\mathrm{ran}{1}^{st}\left(S\right)=\mathrm{ran}{1}^{st}\left(S\right)$$
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 |-