Theorem rngohomval

Description: The set of ring homomorphisms. (Contributed by Jeff Madsen, 19-Jun-2010) (Revised by Mario Carneiro, 22-Sep-2015)

	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	rngohomval	Could not format assertion : 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 |-

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		simpr	$$⊢\left(r=R\wedge s=S\right)\to s=S$$
10	9	fveq2d	$$⊢\left(r=R\wedge s=S\right)\to 1^{st}\left(s\right)=1^{st}\left(S\right)$$
11	10 5	eqtr4di	$$⊢\left(r=R\wedge s=S\right)\to 1^{st}\left(s\right)=J$$
12	11	rneqd	$$⊢\left(r=R\wedge s=S\right)\to \mathrm{ran}{1}^{st}\left(s\right)=\mathrm{ran}J$$
13	12 7	eqtr4di	$$⊢\left(r=R\wedge s=S\right)\to \mathrm{ran}{1}^{st}\left(s\right)=Y$$
14		simpl	$$⊢\left(r=R\wedge s=S\right)\to r=R$$
15	14	fveq2d	$$⊢\left(r=R\wedge s=S\right)\to 1^{st}\left(r\right)=1^{st}\left(R\right)$$
16	15 1	eqtr4di	$$⊢\left(r=R\wedge s=S\right)\to 1^{st}\left(r\right)=G$$
17	16	rneqd	$$⊢\left(r=R\wedge s=S\right)\to \mathrm{ran}{1}^{st}\left(r\right)=\mathrm{ran}G$$
18	17 3	eqtr4di	$$⊢\left(r=R\wedge s=S\right)\to \mathrm{ran}{1}^{st}\left(r\right)=X$$
19	13 18	oveq12d	$$⊢\left(r=R\wedge s=S\right)\to {\mathrm{ran}{1}^{st}\left(s\right)}^{\mathrm{ran}{1}^{st}\left(r\right)}=Y^X$$
20	14	fveq2d	$$⊢\left(r=R\wedge s=S\right)\to 2^{nd}\left(r\right)=2^{nd}\left(R\right)$$
21	20 2	eqtr4di	$$⊢\left(r=R\wedge s=S\right)\to 2^{nd}\left(r\right)=H$$
22	21	fveq2d	$$⊢\left(r=R\wedge s=S\right)\to \mathrm{GId}\left(2^{nd}\left(r\right)\right)=\mathrm{GId}\left(H\right)$$
23	22 4	eqtr4di	$$⊢\left(r=R\wedge s=S\right)\to \mathrm{GId}\left(2^{nd}\left(r\right)\right)=U$$
24	23	fveq2d	$$⊢\left(r=R\wedge s=S\right)\to f\left(\mathrm{GId}\left(2^{nd}\left(r\right)\right)\right)=f\left(U\right)$$
25	9	fveq2d	$$⊢\left(r=R\wedge s=S\right)\to 2^{nd}\left(s\right)=2^{nd}\left(S\right)$$
26	25 6	eqtr4di	$$⊢\left(r=R\wedge s=S\right)\to 2^{nd}\left(s\right)=K$$
27	26	fveq2d	$$⊢\left(r=R\wedge s=S\right)\to \mathrm{GId}\left(2^{nd}\left(s\right)\right)=\mathrm{GId}\left(K\right)$$
28	27 8	eqtr4di	$$⊢\left(r=R\wedge s=S\right)\to \mathrm{GId}\left(2^{nd}\left(s\right)\right)=V$$
29	24 28	eqeq12d	$$⊢\left(r=R\wedge s=S\right)\to \left(f\left(\mathrm{GId}\left(2^{nd}\left(r\right)\right)\right)=\mathrm{GId}\left(2^{nd}\left(s\right)\right)\leftrightarrow f\left(U\right)=V\right)$$
30	16	oveqd	$$⊢\left(r=R\wedge s=S\right)\to x{1}^{st}\left(r\right)y=xGy$$
31	30	fveq2d	$$⊢\left(r=R\wedge s=S\right)\to f\left(x{1}^{st}\left(r\right)y\right)=f\left(xGy\right)$$
32	11	oveqd	$$⊢\left(r=R\wedge s=S\right)\to f\left(x\right)1^{st}\left(s\right)f\left(y\right)=f\left(x\right)Jf\left(y\right)$$
33	31 32	eqeq12d	$$⊢\left(r=R\wedge s=S\right)\to \left(f\left(x{1}^{st}\left(r\right)y\right)=f\left(x\right)1^{st}\left(s\right)f\left(y\right)\leftrightarrow f\left(xGy\right)=f\left(x\right)Jf\left(y\right)\right)$$
34	21	oveqd	$$⊢\left(r=R\wedge s=S\right)\to x{2}^{nd}\left(r\right)y=xHy$$
35	34	fveq2d	$$⊢\left(r=R\wedge s=S\right)\to f\left(x{2}^{nd}\left(r\right)y\right)=f\left(xHy\right)$$
36	26	oveqd	$$⊢\left(r=R\wedge s=S\right)\to f\left(x\right)2^{nd}\left(s\right)f\left(y\right)=f\left(x\right)Kf\left(y\right)$$
37	35 36	eqeq12d	$$⊢\left(r=R\wedge s=S\right)\to \left(f\left(x{2}^{nd}\left(r\right)y\right)=f\left(x\right)2^{nd}\left(s\right)f\left(y\right)\leftrightarrow f\left(xHy\right)=f\left(x\right)Kf\left(y\right)\right)$$
38	33 37	anbi12d	$$⊢\left(r=R\wedge s=S\right)\to \left(\left(f\left(x{1}^{st}\left(r\right)y\right)=f\left(x\right)1^{st}\left(s\right)f\left(y\right)\wedge f\left(x{2}^{nd}\left(r\right)y\right)=f\left(x\right)2^{nd}\left(s\right)f\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)$$
39	18 38	raleqbidv	$$⊢\left(r=R\wedge s=S\right)\to \left(\forall y\in \mathrm{ran}{1}^{st}\left(r\right)\left(f\left(x{1}^{st}\left(r\right)y\right)=f\left(x\right)1^{st}\left(s\right)f\left(y\right)\wedge f\left(x{2}^{nd}\left(r\right)y\right)=f\left(x\right)2^{nd}\left(s\right)f\left(y\right)\right)\leftrightarrow \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)$$
40	18 39	raleqbidv	$$⊢\left(r=R\wedge s=S\right)\to \left(\forall x\in \mathrm{ran}{1}^{st}\left(r\right)\forall y\in \mathrm{ran}{1}^{st}\left(r\right)\left(f\left(x{1}^{st}\left(r\right)y\right)=f\left(x\right)1^{st}\left(s\right)f\left(y\right)\wedge f\left(x{2}^{nd}\left(r\right)y\right)=f\left(x\right)2^{nd}\left(s\right)f\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)$$
41	29 40	anbi12d	$$⊢\left(r=R\wedge s=S\right)\to \left(\left(f\left(\mathrm{GId}\left(2^{nd}\left(r\right)\right)\right)=\mathrm{GId}\left(2^{nd}\left(s\right)\right)\wedge \forall x\in \mathrm{ran}{1}^{st}\left(r\right)\forall y\in \mathrm{ran}{1}^{st}\left(r\right)\left(f\left(x{1}^{st}\left(r\right)y\right)=f\left(x\right)1^{st}\left(s\right)f\left(y\right)\wedge f\left(x{2}^{nd}\left(r\right)y\right)=f\left(x\right)2^{nd}\left(s\right)f\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)$$
42	19 41	rabeqbidv	$$⊢\left(r=R\wedge s=S\right)\to \left\{f\in \left({\mathrm{ran}{1}^{st}\left(s\right)}^{\mathrm{ran}{1}^{st}\left(r\right)}\right)|\left(f\left(\mathrm{GId}\left(2^{nd}\left(r\right)\right)\right)=\mathrm{GId}\left(2^{nd}\left(s\right)\right)\wedge \forall x\in \mathrm{ran}{1}^{st}\left(r\right)\forall y\in \mathrm{ran}{1}^{st}\left(r\right)\left(f\left(x{1}^{st}\left(r\right)y\right)=f\left(x\right)1^{st}\left(s\right)f\left(y\right)\wedge f\left(x{2}^{nd}\left(r\right)y\right)=f\left(x\right)2^{nd}\left(s\right)f\left(y\right)\right)\right)\right\}=\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\}$$
43		df-rngohom	Could not format RingOpsHom = ( r e. RingOps , s e. RingOps |-> { f e. ( ran ( 1st ` s ) ^m ran ( 1st ` r ) ) | ( ( f ` ( GId ` ( 2nd ` r ) ) ) = ( GId ` ( 2nd ` s ) ) /\ 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 ( 2nd ` r ) y ) ) = ( ( f ` x ) ( 2nd ` s ) ( f ` y ) ) ) ) } ) : No typesetting found for |- RingOpsHom = ( r e. RingOps , s e. RingOps |-> { f e. ( ran ( 1st ` s ) ^m ran ( 1st ` r ) ) | ( ( f ` ( GId ` ( 2nd ` r ) ) ) = ( GId ` ( 2nd ` s ) ) /\ 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 ( 2nd ` r ) y ) ) = ( ( f ` x ) ( 2nd ` s ) ( f ` y ) ) ) ) } ) with typecode |-
44		ovex	$$⊢Y^X\in \mathrm{V}$$
45	44	rabex	$$⊢\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\}\in \mathrm{V}$$
46	42 43 45	ovmpoa	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 |-