Theorem rngohommul

Description: Ring homomorphisms preserve multiplication. (Contributed by Jeff Madsen, 3-Jan-2011)

	Ref	Expression
Hypotheses	rnghommul.1	$$⊢G=1^{st}\left(R\right)$$
	rnghommul.2	$$⊢X=\mathrm{ran}G$$
	rnghommul.3	$$⊢H=2^{nd}\left(R\right)$$
	rnghommul.4	$$⊢K=2^{nd}\left(S\right)$$
Assertion	rngohommul	Could not format assertion : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ ( A e. X /\ B e. X ) ) -> ( F ` ( A H B ) ) = ( ( F ` A ) K ( F ` B ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		rnghommul.1	$$⊢G=1^{st}\left(R\right)$$
2		rnghommul.2	$$⊢X=\mathrm{ran}G$$
3		rnghommul.3	$$⊢H=2^{nd}\left(R\right)$$
4		rnghommul.4	$$⊢K=2^{nd}\left(S\right)$$
5		eqid	$$⊢\mathrm{GId}\left(H\right)=\mathrm{GId}\left(H\right)$$
6		eqid	$$⊢1^{st}\left(S\right)=1^{st}\left(S\right)$$
7		eqid	$$⊢\mathrm{ran}{1}^{st}\left(S\right)=\mathrm{ran}{1}^{st}\left(S\right)$$
8		eqid	$$⊢\mathrm{GId}\left(K\right)=\mathrm{GId}\left(K\right)$$
9	1 3 2 5 6 4 7 8	isrngohom	Could not format ( ( R e. RingOps /\ S e. RingOps ) -> ( F e. ( R RingOpsHom S ) <-> ( F : X --> ran ( 1st ` S ) /\ ( F ` ( GId ` H ) ) = ( GId ` K ) /\ A. x e. X A. y e. X ( ( F ` ( x G 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 : X --> ran ( 1st ` S ) /\ ( F ` ( GId ` H ) ) = ( GId ` K ) /\ A. x e. X A. y e. X ( ( F ` ( x G 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 : X --> ran ( 1st ` S ) /\ ( F ` ( GId ` H ) ) = ( GId ` K ) /\ A. x e. X A. y e. X ( ( F ` ( x G 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 : X --> ran ( 1st ` S ) /\ ( F ` ( GId ` H ) ) = ( GId ` K ) /\ A. x e. X A. y e. X ( ( F ` ( x G y ) ) = ( ( F ` x ) ( 1st ` S ) ( F ` y ) ) /\ ( F ` ( x H y ) ) = ( ( F ` x ) K ( F ` y ) ) ) ) ) with typecode |-
11	10	simp3d	Could not format ( ( ( R e. RingOps /\ S e. RingOps ) /\ F e. ( R RingOpsHom S ) ) -> A. x e. X A. y e. X ( ( F ` ( x G 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 ) ) -> A. x e. X A. y e. X ( ( F ` ( x G y ) ) = ( ( F ` x ) ( 1st ` S ) ( F ` y ) ) /\ ( F ` ( x H y ) ) = ( ( F ` x ) K ( F ` y ) ) ) ) with typecode |-
12	11	3impa	Could not format ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) -> A. x e. X A. y e. X ( ( F ` ( x G 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 ) ) -> A. x e. X A. y e. X ( ( F ` ( x G y ) ) = ( ( F ` x ) ( 1st ` S ) ( F ` y ) ) /\ ( F ` ( x H y ) ) = ( ( F ` x ) K ( F ` y ) ) ) ) with typecode |-
13		simpr	$$⊢\left(F\left(xGy\right)=F\left(x\right)1^{st}\left(S\right)F\left(y\right)\wedge F\left(xHy\right)=F\left(x\right)KF\left(y\right)\right)\to F\left(xHy\right)=F\left(x\right)KF\left(y\right)$$
14	13	2ralimi	$$⊢\forall x\in X\forall y\in X\left(F\left(xGy\right)=F\left(x\right)1^{st}\left(S\right)F\left(y\right)\wedge F\left(xHy\right)=F\left(x\right)KF\left(y\right)\right)\to \forall x\in X\forall y\in XF\left(xHy\right)=F\left(x\right)KF\left(y\right)$$
15	12 14	syl	Could not format ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) -> A. x e. X A. y e. X ( F ` ( x H y ) ) = ( ( F ` x ) K ( F ` y ) ) ) : No typesetting found for |- ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) -> A. x e. X A. y e. X ( F ` ( x H y ) ) = ( ( F ` x ) K ( F ` y ) ) ) with typecode |-
16		fvoveq1	$$⊢x=A\to F\left(xHy\right)=F\left(AHy\right)$$
17		fveq2	$$⊢x=A\to F\left(x\right)=F\left(A\right)$$
18	17	oveq1d	$$⊢x=A\to F\left(x\right)KF\left(y\right)=F\left(A\right)KF\left(y\right)$$
19	16 18	eqeq12d	$$⊢x=A\to \left(F\left(xHy\right)=F\left(x\right)KF\left(y\right)\leftrightarrow F\left(AHy\right)=F\left(A\right)KF\left(y\right)\right)$$
20		oveq2	$$⊢y=B\to AHy=AHB$$
21	20	fveq2d	$$⊢y=B\to F\left(AHy\right)=F\left(AHB\right)$$
22		fveq2	$$⊢y=B\to F\left(y\right)=F\left(B\right)$$
23	22	oveq2d	$$⊢y=B\to F\left(A\right)KF\left(y\right)=F\left(A\right)KF\left(B\right)$$
24	21 23	eqeq12d	$$⊢y=B\to \left(F\left(AHy\right)=F\left(A\right)KF\left(y\right)\leftrightarrow F\left(AHB\right)=F\left(A\right)KF\left(B\right)\right)$$
25	19 24	rspc2v	$$⊢\left(A\in X\wedge B\in X\right)\to \left(\forall x\in X\forall y\in XF\left(xHy\right)=F\left(x\right)KF\left(y\right)\to F\left(AHB\right)=F\left(A\right)KF\left(B\right)\right)$$
26	15 25	mpan9	Could not format ( ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ ( A e. X /\ B e. X ) ) -> ( F ` ( A H B ) ) = ( ( F ` A ) K ( F ` B ) ) ) : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ ( A e. X /\ B e. X ) ) -> ( F ` ( A H B ) ) = ( ( F ` A ) K ( F ` B ) ) ) with typecode |-