Theorem rngogrphom

Description: A ring homomorphism is a group homomorphism. (Contributed by Jeff Madsen, 2-Jan-2011)

	Ref	Expression
Hypotheses	rnggrphom.1	$$⊢G=1^{st}\left(R\right)$$
	rnggrphom.2	$$⊢J=1^{st}\left(S\right)$$
Assertion	rngogrphom	Could not format assertion : No typesetting found for |- ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) -> F e. ( G GrpOpHom J ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		rnggrphom.1	$$⊢G=1^{st}\left(R\right)$$
2		rnggrphom.2	$$⊢J=1^{st}\left(S\right)$$
3		eqid	$$⊢\mathrm{ran}G=\mathrm{ran}G$$
4		eqid	$$⊢\mathrm{ran}J=\mathrm{ran}J$$
5	1 3 2 4	rngohomf	Could not format ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) -> F : ran G --> ran J ) : No typesetting found for |- ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) -> F : ran G --> ran J ) with typecode |-
6	1 3 2	rngohomadd	Could not format ( ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ ( x e. ran G /\ y e. ran G ) ) -> ( F ` ( x G y ) ) = ( ( F ` x ) J ( F ` y ) ) ) : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ ( x e. ran G /\ y e. ran G ) ) -> ( F ` ( x G y ) ) = ( ( F ` x ) J ( F ` y ) ) ) with typecode |-
7	6	eqcomd	Could not format ( ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ ( x e. ran G /\ y e. ran G ) ) -> ( ( F ` x ) J ( F ` y ) ) = ( F ` ( x G y ) ) ) : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ ( x e. ran G /\ y e. ran G ) ) -> ( ( F ` x ) J ( F ` y ) ) = ( F ` ( x G y ) ) ) with typecode |-
8	7	ralrimivva	Could not format ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) -> A. x e. ran G A. y e. ran G ( ( F ` x ) J ( F ` y ) ) = ( F ` ( x G y ) ) ) : No typesetting found for |- ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) -> A. x e. ran G A. y e. ran G ( ( F ` x ) J ( F ` y ) ) = ( F ` ( x G y ) ) ) with typecode |-
9	1	rngogrpo	$$⊢R\in \mathrm{RingOps}\to G\in \mathrm{GrpOp}$$
10	2	rngogrpo	$$⊢S\in \mathrm{RingOps}\to J\in \mathrm{GrpOp}$$
11	3 4	elghomOLD	$$⊢\left(G\in \mathrm{GrpOp}\wedge J\in \mathrm{GrpOp}\right)\to \left(F\in \left(G\mathrm{GrpOpHom}J\right)\leftrightarrow \left(F:\mathrm{ran}G⟶\mathrm{ran}J\wedge \forall x\in \mathrm{ran}G\forall y\in \mathrm{ran}GF\left(x\right)JF\left(y\right)=F\left(xGy\right)\right)\right)$$
12	9 10 11	syl2an	$$⊢\left(R\in \mathrm{RingOps}\wedge S\in \mathrm{RingOps}\right)\to \left(F\in \left(G\mathrm{GrpOpHom}J\right)\leftrightarrow \left(F:\mathrm{ran}G⟶\mathrm{ran}J\wedge \forall x\in \mathrm{ran}G\forall y\in \mathrm{ran}GF\left(x\right)JF\left(y\right)=F\left(xGy\right)\right)\right)$$
13	12	3adant3	Could not format ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) -> ( F e. ( G GrpOpHom J ) <-> ( F : ran G --> ran J /\ A. x e. ran G A. y e. ran G ( ( F ` x ) J ( F ` y ) ) = ( F ` ( x G y ) ) ) ) ) : No typesetting found for |- ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) -> ( F e. ( G GrpOpHom J ) <-> ( F : ran G --> ran J /\ A. x e. ran G A. y e. ran G ( ( F ` x ) J ( F ` y ) ) = ( F ` ( x G y ) ) ) ) ) with typecode |-
14	5 8 13	mpbir2and	Could not format ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) -> F e. ( G GrpOpHom J ) ) : No typesetting found for |- ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) -> F e. ( G GrpOpHom J ) ) with typecode |-