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	⊢ 𝐺 = ( 1^st ‘ 𝑅 )
	rnghomval.2	⊢ 𝐻 = ( 2^nd ‘ 𝑅 )
	rnghomval.3	⊢ 𝑋 = ran 𝐺
	rnghomval.4	⊢ 𝑈 = ( GId ‘ 𝐻 )
	rnghomval.5	⊢ 𝐽 = ( 1^st ‘ 𝑆 )
	rnghomval.6	⊢ 𝐾 = ( 2^nd ‘ 𝑆 )
	rnghomval.7	⊢ 𝑌 = ran 𝐽
	rnghomval.8	⊢ 𝑉 = ( GId ‘ 𝐾 )
Assertion	rngohomval	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) → ( 𝑅 RngHom 𝑆 ) = { 𝑓 ∈ ( 𝑌 ↑_m 𝑋 ) ∣ ( ( 𝑓 ‘ 𝑈 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑓 ‘ ( 𝑥 𝐺 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 𝐻 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) 𝐾 ( 𝑓 ‘ 𝑦 ) ) ) ) } )

Proof

Step	Hyp	Ref	Expression
1		rnghomval.1	⊢ 𝐺 = ( 1^st ‘ 𝑅 )
2		rnghomval.2	⊢ 𝐻 = ( 2^nd ‘ 𝑅 )
3		rnghomval.3	⊢ 𝑋 = ran 𝐺
4		rnghomval.4	⊢ 𝑈 = ( GId ‘ 𝐻 )
5		rnghomval.5	⊢ 𝐽 = ( 1^st ‘ 𝑆 )
6		rnghomval.6	⊢ 𝐾 = ( 2^nd ‘ 𝑆 )
7		rnghomval.7	⊢ 𝑌 = ran 𝐽
8		rnghomval.8	⊢ 𝑉 = ( GId ‘ 𝐾 )
9		simpr	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → 𝑠 = 𝑆 )
10	9	fveq2d	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( 1^st ‘ 𝑠 ) = ( 1^st ‘ 𝑆 ) )
11	10 5	eqtr4di	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( 1^st ‘ 𝑠 ) = 𝐽 )
12	11	rneqd	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ran ( 1^st ‘ 𝑠 ) = ran 𝐽 )
13	12 7	eqtr4di	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ran ( 1^st ‘ 𝑠 ) = 𝑌 )
14		simpl	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → 𝑟 = 𝑅 )
15	14	fveq2d	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( 1^st ‘ 𝑟 ) = ( 1^st ‘ 𝑅 ) )
16	15 1	eqtr4di	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( 1^st ‘ 𝑟 ) = 𝐺 )
17	16	rneqd	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ran ( 1^st ‘ 𝑟 ) = ran 𝐺 )
18	17 3	eqtr4di	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ran ( 1^st ‘ 𝑟 ) = 𝑋 )
19	13 18	oveq12d	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( ran ( 1^st ‘ 𝑠 ) ↑_m ran ( 1^st ‘ 𝑟 ) ) = ( 𝑌 ↑_m 𝑋 ) )
20	14	fveq2d	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( 2^nd ‘ 𝑟 ) = ( 2^nd ‘ 𝑅 ) )
21	20 2	eqtr4di	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( 2^nd ‘ 𝑟 ) = 𝐻 )
22	21	fveq2d	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( GId ‘ ( 2^nd ‘ 𝑟 ) ) = ( GId ‘ 𝐻 ) )
23	22 4	eqtr4di	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( GId ‘ ( 2^nd ‘ 𝑟 ) ) = 𝑈 )
24	23	fveq2d	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( 𝑓 ‘ ( GId ‘ ( 2^nd ‘ 𝑟 ) ) ) = ( 𝑓 ‘ 𝑈 ) )
25	9	fveq2d	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( 2^nd ‘ 𝑠 ) = ( 2^nd ‘ 𝑆 ) )
26	25 6	eqtr4di	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( 2^nd ‘ 𝑠 ) = 𝐾 )
27	26	fveq2d	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( GId ‘ ( 2^nd ‘ 𝑠 ) ) = ( GId ‘ 𝐾 ) )
28	27 8	eqtr4di	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( GId ‘ ( 2^nd ‘ 𝑠 ) ) = 𝑉 )
29	24 28	eqeq12d	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( ( 𝑓 ‘ ( GId ‘ ( 2^nd ‘ 𝑟 ) ) ) = ( GId ‘ ( 2^nd ‘ 𝑠 ) ) ↔ ( 𝑓 ‘ 𝑈 ) = 𝑉 ) )
30	16	oveqd	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( 𝑥 ( 1^st ‘ 𝑟 ) 𝑦 ) = ( 𝑥 𝐺 𝑦 ) )
31	30	fveq2d	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( 𝑓 ‘ ( 𝑥 ( 1^st ‘ 𝑟 ) 𝑦 ) ) = ( 𝑓 ‘ ( 𝑥 𝐺 𝑦 ) ) )
32	11	oveqd	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( ( 𝑓 ‘ 𝑥 ) ( 1^st ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) )
33	31 32	eqeq12d	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( ( 𝑓 ‘ ( 𝑥 ( 1^st ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( 1^st ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ↔ ( 𝑓 ‘ ( 𝑥 𝐺 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) ) )
34	21	oveqd	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( 𝑥 ( 2^nd ‘ 𝑟 ) 𝑦 ) = ( 𝑥 𝐻 𝑦 ) )
35	34	fveq2d	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( 𝑓 ‘ ( 𝑥 ( 2^nd ‘ 𝑟 ) 𝑦 ) ) = ( 𝑓 ‘ ( 𝑥 𝐻 𝑦 ) ) )
36	26	oveqd	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( ( 𝑓 ‘ 𝑥 ) ( 2^nd ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) 𝐾 ( 𝑓 ‘ 𝑦 ) ) )
37	35 36	eqeq12d	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( ( 𝑓 ‘ ( 𝑥 ( 2^nd ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( 2^nd ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ↔ ( 𝑓 ‘ ( 𝑥 𝐻 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) 𝐾 ( 𝑓 ‘ 𝑦 ) ) ) )
38	33 37	anbi12d	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( ( ( 𝑓 ‘ ( 𝑥 ( 1^st ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( 1^st ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( 2^nd ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( 2^nd ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) ↔ ( ( 𝑓 ‘ ( 𝑥 𝐺 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 𝐻 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) 𝐾 ( 𝑓 ‘ 𝑦 ) ) ) ) )
39	18 38	raleqbidv	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( ∀ 𝑦 ∈ ran ( 1^st ‘ 𝑟 ) ( ( 𝑓 ‘ ( 𝑥 ( 1^st ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( 1^st ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( 2^nd ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( 2^nd ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) ↔ ∀ 𝑦 ∈ 𝑋 ( ( 𝑓 ‘ ( 𝑥 𝐺 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 𝐻 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) 𝐾 ( 𝑓 ‘ 𝑦 ) ) ) ) )
40	18 39	raleqbidv	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( ∀ 𝑥 ∈ ran ( 1^st ‘ 𝑟 ) ∀ 𝑦 ∈ ran ( 1^st ‘ 𝑟 ) ( ( 𝑓 ‘ ( 𝑥 ( 1^st ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( 1^st ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( 2^nd ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( 2^nd ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑓 ‘ ( 𝑥 𝐺 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 𝐻 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) 𝐾 ( 𝑓 ‘ 𝑦 ) ) ) ) )
41	29 40	anbi12d	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( ( ( 𝑓 ‘ ( GId ‘ ( 2^nd ‘ 𝑟 ) ) ) = ( GId ‘ ( 2^nd ‘ 𝑠 ) ) ∧ ∀ 𝑥 ∈ ran ( 1^st ‘ 𝑟 ) ∀ 𝑦 ∈ ran ( 1^st ‘ 𝑟 ) ( ( 𝑓 ‘ ( 𝑥 ( 1^st ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( 1^st ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( 2^nd ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( 2^nd ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) ) ↔ ( ( 𝑓 ‘ 𝑈 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑓 ‘ ( 𝑥 𝐺 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 𝐻 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) 𝐾 ( 𝑓 ‘ 𝑦 ) ) ) ) ) )
42	19 41	rabeqbidv	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → { 𝑓 ∈ ( ran ( 1^st ‘ 𝑠 ) ↑_m ran ( 1^st ‘ 𝑟 ) ) ∣ ( ( 𝑓 ‘ ( GId ‘ ( 2^nd ‘ 𝑟 ) ) ) = ( GId ‘ ( 2^nd ‘ 𝑠 ) ) ∧ ∀ 𝑥 ∈ ran ( 1^st ‘ 𝑟 ) ∀ 𝑦 ∈ ran ( 1^st ‘ 𝑟 ) ( ( 𝑓 ‘ ( 𝑥 ( 1^st ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( 1^st ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( 2^nd ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( 2^nd ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) ) } = { 𝑓 ∈ ( 𝑌 ↑_m 𝑋 ) ∣ ( ( 𝑓 ‘ 𝑈 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑓 ‘ ( 𝑥 𝐺 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 𝐻 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) 𝐾 ( 𝑓 ‘ 𝑦 ) ) ) ) } )
43		df-rngohom	⊢ RngHom = ( 𝑟 ∈ RingOps , 𝑠 ∈ RingOps ↦ { 𝑓 ∈ ( ran ( 1^st ‘ 𝑠 ) ↑_m ran ( 1^st ‘ 𝑟 ) ) ∣ ( ( 𝑓 ‘ ( GId ‘ ( 2^nd ‘ 𝑟 ) ) ) = ( GId ‘ ( 2^nd ‘ 𝑠 ) ) ∧ ∀ 𝑥 ∈ ran ( 1^st ‘ 𝑟 ) ∀ 𝑦 ∈ ran ( 1^st ‘ 𝑟 ) ( ( 𝑓 ‘ ( 𝑥 ( 1^st ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( 1^st ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( 2^nd ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( 2^nd ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) ) } )
44		ovex	⊢ ( 𝑌 ↑_m 𝑋 ) ∈ V
45	44	rabex	⊢ { 𝑓 ∈ ( 𝑌 ↑_m 𝑋 ) ∣ ( ( 𝑓 ‘ 𝑈 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑓 ‘ ( 𝑥 𝐺 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 𝐻 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) 𝐾 ( 𝑓 ‘ 𝑦 ) ) ) ) } ∈ V
46	42 43 45	ovmpoa	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) → ( 𝑅 RngHom 𝑆 ) = { 𝑓 ∈ ( 𝑌 ↑_m 𝑋 ) ∣ ( ( 𝑓 ‘ 𝑈 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑓 ‘ ( 𝑥 𝐺 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 𝐻 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) 𝐾 ( 𝑓 ‘ 𝑦 ) ) ) ) } )

Metamath Proof Explorer

Theorem rngohomval

Proof