Theorem rngohomval 37951

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) → (𝑅 RingOpsHom 𝑆) = {𝑓 ∈ (𝑌 ↑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 484	. . . . . . . 8 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → 𝑠 = 𝑆)
2	1	fveq2d 6911	. . . . . . 7 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (1st ‘𝑠) = (1st ‘𝑆))
3		rnghomval.5	. . . . . . 7 ⊢ 𝐽 = (1st ‘𝑆)
4	2, 3	eqtr4di 2793	. . . . . 6 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (1st ‘𝑠) = 𝐽)
5	4	rneqd 5952	. . . . 5 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → ran (1st ‘𝑠) = ran 𝐽)
6		rnghomval.7	. . . . 5 ⊢ 𝑌 = ran 𝐽
7	5, 6	eqtr4di 2793	. . . 4 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → ran (1st ‘𝑠) = 𝑌)
8		simpl 482	. . . . . . . 8 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → 𝑟 = 𝑅)
9	8	fveq2d 6911	. . . . . . 7 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (1st ‘𝑟) = (1st ‘𝑅))
10		rnghomval.1	. . . . . . 7 ⊢ 𝐺 = (1st ‘𝑅)
11	9, 10	eqtr4di 2793	. . . . . 6 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (1st ‘𝑟) = 𝐺)
12	11	rneqd 5952	. . . . 5 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → ran (1st ‘𝑟) = ran 𝐺)
13		rnghomval.3	. . . . 5 ⊢ 𝑋 = ran 𝐺
14	12, 13	eqtr4di 2793	. . . 4 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → ran (1st ‘𝑟) = 𝑋)
15	7, 14	oveq12d 7449	. . 3 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (ran (1st ‘𝑠) ↑m ran (1st ‘𝑟)) = (𝑌 ↑m 𝑋))
16	8	fveq2d 6911	. . . . . . . . 9 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (2nd ‘𝑟) = (2nd ‘𝑅))
17		rnghomval.2	. . . . . . . . 9 ⊢ 𝐻 = (2nd ‘𝑅)
18	16, 17	eqtr4di 2793	. . . . . . . 8 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (2nd ‘𝑟) = 𝐻)
19	18	fveq2d 6911	. . . . . . 7 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (GId‘(2nd ‘𝑟)) = (GId‘𝐻))
20		rnghomval.4	. . . . . . 7 ⊢ 𝑈 = (GId‘𝐻)
21	19, 20	eqtr4di 2793	. . . . . 6 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (GId‘(2nd ‘𝑟)) = 𝑈)
22	21	fveq2d 6911	. . . . 5 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (𝑓‘(GId‘(2nd ‘𝑟))) = (𝑓‘𝑈))
23	1	fveq2d 6911	. . . . . . . 8 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (2nd ‘𝑠) = (2nd ‘𝑆))
24		rnghomval.6	. . . . . . . 8 ⊢ 𝐾 = (2nd ‘𝑆)
25	23, 24	eqtr4di 2793	. . . . . . 7 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (2nd ‘𝑠) = 𝐾)
26	25	fveq2d 6911	. . . . . 6 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (GId‘(2nd ‘𝑠)) = (GId‘𝐾))
27		rnghomval.8	. . . . . 6 ⊢ 𝑉 = (GId‘𝐾)
28	26, 27	eqtr4di 2793	. . . . 5 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (GId‘(2nd ‘𝑠)) = 𝑉)
29	22, 28	eqeq12d 2751	. . . 4 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → ((𝑓‘(GId‘(2nd ‘𝑟))) = (GId‘(2nd ‘𝑠)) ↔ (𝑓‘𝑈) = 𝑉))
30	11	oveqd 7448	. . . . . . . . 9 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (𝑥(1st ‘𝑟)𝑦) = (𝑥𝐺𝑦))
31	30	fveq2d 6911	. . . . . . . 8 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (𝑓‘(𝑥(1st ‘𝑟)𝑦)) = (𝑓‘(𝑥𝐺𝑦)))
32	4	oveqd 7448	. . . . . . . 8 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → ((𝑓‘𝑥)(1st ‘𝑠)(𝑓‘𝑦)) = ((𝑓‘𝑥)𝐽(𝑓‘𝑦)))
33	31, 32	eqeq12d 2751	. . . . . . 7 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → ((𝑓‘(𝑥(1st ‘𝑟)𝑦)) = ((𝑓‘𝑥)(1st ‘𝑠)(𝑓‘𝑦)) ↔ (𝑓‘(𝑥𝐺𝑦)) = ((𝑓‘𝑥)𝐽(𝑓‘𝑦))))
34	18	oveqd 7448	. . . . . . . . 9 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (𝑥(2nd ‘𝑟)𝑦) = (𝑥𝐻𝑦))
35	34	fveq2d 6911	. . . . . . . 8 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (𝑓‘(𝑥(2nd ‘𝑟)𝑦)) = (𝑓‘(𝑥𝐻𝑦)))
36	25	oveqd 7448	. . . . . . . 8 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → ((𝑓‘𝑥)(2nd ‘𝑠)(𝑓‘𝑦)) = ((𝑓‘𝑥)𝐾(𝑓‘𝑦)))
37	35, 36	eqeq12d 2751	. . . . . . 7 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → ((𝑓‘(𝑥(2nd ‘𝑟)𝑦)) = ((𝑓‘𝑥)(2nd ‘𝑠)(𝑓‘𝑦)) ↔ (𝑓‘(𝑥𝐻𝑦)) = ((𝑓‘𝑥)𝐾(𝑓‘𝑦))))
38	33, 37	anbi12d 632	. . . . . 6 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (((𝑓‘(𝑥(1st ‘𝑟)𝑦)) = ((𝑓‘𝑥)(1st ‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(2nd ‘𝑟)𝑦)) = ((𝑓‘𝑥)(2nd ‘𝑠)(𝑓‘𝑦))) ↔ ((𝑓‘(𝑥𝐺𝑦)) = ((𝑓‘𝑥)𝐽(𝑓‘𝑦)) ∧ (𝑓‘(𝑥𝐻𝑦)) = ((𝑓‘𝑥)𝐾(𝑓‘𝑦)))))
39	14, 38	raleqbidv 3344	. . . . 5 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (∀𝑦 ∈ ran (1st ‘𝑟)((𝑓‘(𝑥(1st ‘𝑟)𝑦)) = ((𝑓‘𝑥)(1st ‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(2nd ‘𝑟)𝑦)) = ((𝑓‘𝑥)(2nd ‘𝑠)(𝑓‘𝑦))) ↔ ∀𝑦 ∈ 𝑋 ((𝑓‘(𝑥𝐺𝑦)) = ((𝑓‘𝑥)𝐽(𝑓‘𝑦)) ∧ (𝑓‘(𝑥𝐻𝑦)) = ((𝑓‘𝑥)𝐾(𝑓‘𝑦)))))
40	14, 39	raleqbidv 3344	. . . 4 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (∀𝑥 ∈ ran (1st ‘𝑟)∀𝑦 ∈ ran (1st ‘𝑟)((𝑓‘(𝑥(1st ‘𝑟)𝑦)) = ((𝑓‘𝑥)(1st ‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(2nd ‘𝑟)𝑦)) = ((𝑓‘𝑥)(2nd ‘𝑠)(𝑓‘𝑦))) ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑓‘(𝑥𝐺𝑦)) = ((𝑓‘𝑥)𝐽(𝑓‘𝑦)) ∧ (𝑓‘(𝑥𝐻𝑦)) = ((𝑓‘𝑥)𝐾(𝑓‘𝑦)))))
41	29, 40	anbi12d 632	. . 3 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (((𝑓‘(GId‘(2nd ‘𝑟))) = (GId‘(2nd ‘𝑠)) ∧ ∀𝑥 ∈ ran (1st ‘𝑟)∀𝑦 ∈ ran (1st ‘𝑟)((𝑓‘(𝑥(1st ‘𝑟)𝑦)) = ((𝑓‘𝑥)(1st ‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(2nd ‘𝑟)𝑦)) = ((𝑓‘𝑥)(2nd ‘𝑠)(𝑓‘𝑦)))) ↔ ((𝑓‘𝑈) = 𝑉 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑓‘(𝑥𝐺𝑦)) = ((𝑓‘𝑥)𝐽(𝑓‘𝑦)) ∧ (𝑓‘(𝑥𝐻𝑦)) = ((𝑓‘𝑥)𝐾(𝑓‘𝑦))))))
42	15, 41	rabeqbidv 3452	. 2 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → {𝑓 ∈ (ran (1st ‘𝑠) ↑m ran (1st ‘𝑟)) ∣ ((𝑓‘(GId‘(2nd ‘𝑟))) = (GId‘(2nd ‘𝑠)) ∧ ∀𝑥 ∈ ran (1st ‘𝑟)∀𝑦 ∈ ran (1st ‘𝑟)((𝑓‘(𝑥(1st ‘𝑟)𝑦)) = ((𝑓‘𝑥)(1st ‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(2nd ‘𝑟)𝑦)) = ((𝑓‘𝑥)(2nd ‘𝑠)(𝑓‘𝑦))))} = {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ((𝑓‘𝑈) = 𝑉 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑓‘(𝑥𝐺𝑦)) = ((𝑓‘𝑥)𝐽(𝑓‘𝑦)) ∧ (𝑓‘(𝑥𝐻𝑦)) = ((𝑓‘𝑥)𝐾(𝑓‘𝑦))))})
43		df-rngohom 37950	. 2 ⊢ RingOpsHom = (𝑟 ∈ RingOps, 𝑠 ∈ RingOps ↦ {𝑓 ∈ (ran (1st ‘𝑠) ↑m ran (1st ‘𝑟)) ∣ ((𝑓‘(GId‘(2nd ‘𝑟))) = (GId‘(2nd ‘𝑠)) ∧ ∀𝑥 ∈ ran (1st ‘𝑟)∀𝑦 ∈ ran (1st ‘𝑟)((𝑓‘(𝑥(1st ‘𝑟)𝑦)) = ((𝑓‘𝑥)(1st ‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(2nd ‘𝑟)𝑦)) = ((𝑓‘𝑥)(2nd ‘𝑠)(𝑓‘𝑦))))})
44		ovex 7464	. . 3 ⊢ (𝑌 ↑m 𝑋) ∈ V
45	44	rabex 5345	. 2 ⊢ {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ((𝑓‘𝑈) = 𝑉 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑓‘(𝑥𝐺𝑦)) = ((𝑓‘𝑥)𝐽(𝑓‘𝑦)) ∧ (𝑓‘(𝑥𝐻𝑦)) = ((𝑓‘𝑥)𝐾(𝑓‘𝑦))))} ∈ V
46	42, 43, 45	ovmpoa 7588	1 ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) → (𝑅 RingOpsHom 𝑆) = {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ((𝑓‘𝑈) = 𝑉 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑓‘(𝑥𝐺𝑦)) = ((𝑓‘𝑥)𝐽(𝑓‘𝑦)) ∧ (𝑓‘(𝑥𝐻𝑦)) = ((𝑓‘𝑥)𝐾(𝑓‘𝑦))))})

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ∈ wcel 2106  ∀wral 3059  {crab 3433  ran crn 5690  ‘cfv 6563  (class class class)co 7431  1^st c1st 8011  2^nd c2nd 8012   ↑_m cmap 8865  GIdcgi 30519  RingOpscrngo 37881   RingOpsHom crngohom 37947

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-sbc 3792  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-iota 6516  df-fun 6565  df-fv 6571  df-ov 7434  df-oprab 7435  df-mpo 7436  df-rngohom 37950

This theorem is referenced by:  isrngohom  37952