Theorem rngohomval 35816

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

Hypotheses

Ref	Expression
rnghomval.1	⊢ 𝐺 = (1st ‘𝑅)
rnghomval.2	⊢ 𝐻 = (2nd ‘𝑅)
rnghomval.3	⊢ 𝑋 = ran 𝐺
rnghomval.4	⊢ 𝑈 = (GId‘𝐻)
rnghomval.5	⊢ 𝐽 = (1st ‘𝑆)
rnghomval.6	⊢ 𝐾 = (2nd ‘𝑆)
rnghomval.7	⊢ 𝑌 = ran 𝐽
rnghomval.8	⊢ 𝑉 = (GId‘𝐾)

Assertion

Ref	Expression
rngohomval	⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) → (𝑅 RngHom 𝑆) = {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ((𝑓‘𝑈) = 𝑉 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑓‘(𝑥𝐺𝑦)) = ((𝑓‘𝑥)𝐽(𝑓‘𝑦)) ∧ (𝑓‘(𝑥𝐻𝑦)) = ((𝑓‘𝑥)𝐾(𝑓‘𝑦))))})

Distinct variable groups:   𝑥,𝑓,𝑦   𝑓,𝐺   𝑓,𝐻   𝑓,𝐽   𝑓,𝑌,𝑦   𝑓,𝐾   𝑅,𝑓,𝑥,𝑦   𝑆,𝑓,𝑥,𝑦   𝑓,𝑋,𝑥,𝑦   𝑈,𝑓   𝑓,𝑉

Allowed substitution hints:   𝑈(𝑥,𝑦)   𝐺(𝑥,𝑦)   𝐻(𝑥,𝑦)   𝐽(𝑥,𝑦)   𝐾(𝑥,𝑦)   𝑉(𝑥,𝑦)   𝑌(𝑥)

Proof of Theorem rngohomval

Dummy variables 𝑟 𝑠 are mutually distinct and distinct from all other variables.

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1543   ∈ wcel 2110  ∀wral 3054  {crab 3058  ran crn 5541  ‘cfv 6369  (class class class)co 7202  1^st c1st 7748  2^nd c2nd 7749   ↑_m cmap 8497  GIdcgi 28543  RingOpscrngo 35746   RngHom crnghom 35812

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2706  ax-sep 5181  ax-nul 5188  ax-pr 5311

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2537  df-eu 2566  df-clab 2713  df-cleq 2726  df-clel 2812  df-nfc 2882  df-ral 3059  df-rex 3060  df-rab 3063  df-v 3403  df-sbc 3688  df-dif 3860  df-un 3862  df-in 3864  df-ss 3874  df-nul 4228  df-if 4430  df-sn 4532  df-pr 4534  df-op 4538  df-uni 4810  df-br 5044  df-opab 5106  df-id 5444  df-xp 5546  df-rel 5547  df-cnv 5548  df-co 5549  df-dm 5550  df-rn 5551  df-iota 6327  df-fun 6371  df-fv 6377  df-ov 7205  df-oprab 7206  df-mpo 7207  df-rngohom 35815

This theorem is referenced by:  isrngohom  35817