Theorem isrngohom

Description: The predicate "is a ring homomorphism from R to S ". (Contributed by Jeff Madsen, 19-Jun-2010)

	Ref	Expression
Hypotheses	rnghomval.1	$$⊢G=1^{st}\left(R\right)$$
	rnghomval.2	$$⊢H=2^{nd}\left(R\right)$$
	rnghomval.3	$$⊢X=\mathrm{ran}G$$
	rnghomval.4	$$⊢U=\mathrm{GId}\left(H\right)$$
	rnghomval.5	$$⊢J=1^{st}\left(S\right)$$
	rnghomval.6	$$⊢K=2^{nd}\left(S\right)$$
	rnghomval.7	$$⊢Y=\mathrm{ran}J$$
	rnghomval.8	$$⊢V=\mathrm{GId}\left(K\right)$$
Assertion	isrngohom	Could not format assertion : No typesetting found for |- ( ( R e. RingOps /\ S e. RingOps ) -> ( F e. ( R RingOpsHom S ) <-> ( F : X --> Y /\ ( F ` U ) = V /\ A. x e. X A. y e. X ( ( F ` ( x G y ) ) = ( ( F ` x ) J ( F ` y ) ) /\ ( F ` ( x H y ) ) = ( ( F ` x ) K ( F ` y ) ) ) ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		rnghomval.1	$$⊢G=1^{st}\left(R\right)$$
2		rnghomval.2	$$⊢H=2^{nd}\left(R\right)$$
3		rnghomval.3	$$⊢X=\mathrm{ran}G$$
4		rnghomval.4	$$⊢U=\mathrm{GId}\left(H\right)$$
5		rnghomval.5	$$⊢J=1^{st}\left(S\right)$$
6		rnghomval.6	$$⊢K=2^{nd}\left(S\right)$$
7		rnghomval.7	$$⊢Y=\mathrm{ran}J$$
8		rnghomval.8	$$⊢V=\mathrm{GId}\left(K\right)$$
9	1 2 3 4 5 6 7 8	rngohomval	Could not format ( ( R e. RingOps /\ S e. RingOps ) -> ( R RingOpsHom S ) = { f e. ( Y ^m X ) | ( ( f ` U ) = V /\ A. x e. X A. y e. X ( ( f ` ( x G y ) ) = ( ( f ` x ) J ( f ` y ) ) /\ ( f ` ( x H y ) ) = ( ( f ` x ) K ( f ` y ) ) ) ) } ) : No typesetting found for |- ( ( R e. RingOps /\ S e. RingOps ) -> ( R RingOpsHom S ) = { f e. ( Y ^m X ) | ( ( f ` U ) = V /\ A. x e. X A. y e. X ( ( f ` ( x G y ) ) = ( ( f ` x ) J ( f ` y ) ) /\ ( f ` ( x H y ) ) = ( ( f ` x ) K ( f ` y ) ) ) ) } ) with typecode |-
10	9	eleq2d	Could not format ( ( R e. RingOps /\ S e. RingOps ) -> ( F e. ( R RingOpsHom S ) <-> F e. { f e. ( Y ^m X ) | ( ( f ` U ) = V /\ A. x e. X A. y e. X ( ( f ` ( x G y ) ) = ( ( f ` x ) J ( 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 e. { f e. ( Y ^m X ) | ( ( f ` U ) = V /\ A. x e. X A. y e. X ( ( f ` ( x G y ) ) = ( ( f ` x ) J ( f ` y ) ) /\ ( f ` ( x H y ) ) = ( ( f ` x ) K ( f ` y ) ) ) ) } ) ) with typecode |-
11	5	fvexi	$$⊢J\in \mathrm{V}$$
12	11	rnex	$$⊢\mathrm{ran}J\in \mathrm{V}$$
13	7 12	eqeltri	$$⊢Y\in \mathrm{V}$$
14	1	fvexi	$$⊢G\in \mathrm{V}$$
15	14	rnex	$$⊢\mathrm{ran}G\in \mathrm{V}$$
16	3 15	eqeltri	$$⊢X\in \mathrm{V}$$
17	13 16	elmap	$$⊢F\in \left(Y^X\right)\leftrightarrow F:X⟶Y$$
18	17	anbi1i	$$⊢\left(F\in \left(Y^X\right)\wedge \left(F\left(U\right)=V\wedge \forall x\in X\forall y\in X\left(F\left(xGy\right)=F\left(x\right)JF\left(y\right)\wedge F\left(xHy\right)=F\left(x\right)KF\left(y\right)\right)\right)\right)\leftrightarrow \left(F:X⟶Y\wedge \left(F\left(U\right)=V\wedge \forall x\in X\forall y\in X\left(F\left(xGy\right)=F\left(x\right)JF\left(y\right)\wedge F\left(xHy\right)=F\left(x\right)KF\left(y\right)\right)\right)\right)$$
19		fveq1	$$⊢f=F\to f\left(U\right)=F\left(U\right)$$
20	19	eqeq1d	$$⊢f=F\to \left(f\left(U\right)=V\leftrightarrow F\left(U\right)=V\right)$$
21		fveq1	$$⊢f=F\to f\left(xGy\right)=F\left(xGy\right)$$
22		fveq1	$$⊢f=F\to f\left(x\right)=F\left(x\right)$$
23		fveq1	$$⊢f=F\to f\left(y\right)=F\left(y\right)$$
24	22 23	oveq12d	$$⊢f=F\to f\left(x\right)Jf\left(y\right)=F\left(x\right)JF\left(y\right)$$
25	21 24	eqeq12d	$$⊢f=F\to \left(f\left(xGy\right)=f\left(x\right)Jf\left(y\right)\leftrightarrow F\left(xGy\right)=F\left(x\right)JF\left(y\right)\right)$$
26		fveq1	$$⊢f=F\to f\left(xHy\right)=F\left(xHy\right)$$
27	22 23	oveq12d	$$⊢f=F\to f\left(x\right)Kf\left(y\right)=F\left(x\right)KF\left(y\right)$$
28	26 27	eqeq12d	$$⊢f=F\to \left(f\left(xHy\right)=f\left(x\right)Kf\left(y\right)\leftrightarrow F\left(xHy\right)=F\left(x\right)KF\left(y\right)\right)$$
29	25 28	anbi12d	$$⊢f=F\to \left(\left(f\left(xGy\right)=f\left(x\right)Jf\left(y\right)\wedge f\left(xHy\right)=f\left(x\right)Kf\left(y\right)\right)\leftrightarrow \left(F\left(xGy\right)=F\left(x\right)JF\left(y\right)\wedge F\left(xHy\right)=F\left(x\right)KF\left(y\right)\right)\right)$$
30	29	2ralbidv	$$⊢f=F\to \left(\forall x\in X\forall y\in X\left(f\left(xGy\right)=f\left(x\right)Jf\left(y\right)\wedge f\left(xHy\right)=f\left(x\right)Kf\left(y\right)\right)\leftrightarrow \forall x\in X\forall y\in X\left(F\left(xGy\right)=F\left(x\right)JF\left(y\right)\wedge F\left(xHy\right)=F\left(x\right)KF\left(y\right)\right)\right)$$
31	20 30	anbi12d	$$⊢f=F\to \left(\left(f\left(U\right)=V\wedge \forall x\in X\forall y\in X\left(f\left(xGy\right)=f\left(x\right)Jf\left(y\right)\wedge f\left(xHy\right)=f\left(x\right)Kf\left(y\right)\right)\right)\leftrightarrow \left(F\left(U\right)=V\wedge \forall x\in X\forall y\in X\left(F\left(xGy\right)=F\left(x\right)JF\left(y\right)\wedge F\left(xHy\right)=F\left(x\right)KF\left(y\right)\right)\right)\right)$$
32	31	elrab	$$⊢F\in \left\{f\in \left(Y^X\right)|\left(f\left(U\right)=V\wedge \forall x\in X\forall y\in X\left(f\left(xGy\right)=f\left(x\right)Jf\left(y\right)\wedge f\left(xHy\right)=f\left(x\right)Kf\left(y\right)\right)\right)\right\}\leftrightarrow \left(F\in \left(Y^X\right)\wedge \left(F\left(U\right)=V\wedge \forall x\in X\forall y\in X\left(F\left(xGy\right)=F\left(x\right)JF\left(y\right)\wedge F\left(xHy\right)=F\left(x\right)KF\left(y\right)\right)\right)\right)$$
33		3anass	$$⊢\left(F:X⟶Y\wedge F\left(U\right)=V\wedge \forall x\in X\forall y\in X\left(F\left(xGy\right)=F\left(x\right)JF\left(y\right)\wedge F\left(xHy\right)=F\left(x\right)KF\left(y\right)\right)\right)\leftrightarrow \left(F:X⟶Y\wedge \left(F\left(U\right)=V\wedge \forall x\in X\forall y\in X\left(F\left(xGy\right)=F\left(x\right)JF\left(y\right)\wedge F\left(xHy\right)=F\left(x\right)KF\left(y\right)\right)\right)\right)$$
34	18 32 33	3bitr4i	$$⊢F\in \left\{f\in \left(Y^X\right)|\left(f\left(U\right)=V\wedge \forall x\in X\forall y\in X\left(f\left(xGy\right)=f\left(x\right)Jf\left(y\right)\wedge f\left(xHy\right)=f\left(x\right)Kf\left(y\right)\right)\right)\right\}\leftrightarrow \left(F:X⟶Y\wedge F\left(U\right)=V\wedge \forall x\in X\forall y\in X\left(F\left(xGy\right)=F\left(x\right)JF\left(y\right)\wedge F\left(xHy\right)=F\left(x\right)KF\left(y\right)\right)\right)$$
35	10 34	bitrdi	Could not format ( ( R e. RingOps /\ S e. RingOps ) -> ( F e. ( R RingOpsHom S ) <-> ( F : X --> Y /\ ( F ` U ) = V /\ A. x e. X A. y e. X ( ( F ` ( x G y ) ) = ( ( F ` x ) J ( 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 --> Y /\ ( F ` U ) = V /\ A. x e. X A. y e. X ( ( F ` ( x G y ) ) = ( ( F ` x ) J ( F ` y ) ) /\ ( F ` ( x H y ) ) = ( ( F ` x ) K ( F ` y ) ) ) ) ) ) with typecode |-