Theorem rngohomval 37993

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∀wral 3052  {crab 3420  ran crn 5660  ‘cfv 6536  (class class class)co 7410  1^st c1st 7991  2^nd c2nd 7992   ↑_m cmap 8845  GIdcgi 30476  RingOpscrngo 37923   RingOpsHom crngohom 37989

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pr 5407

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-sbc 3771  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-opab 5187  df-id 5553  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-iota 6489  df-fun 6538  df-fv 6544  df-ov 7413  df-oprab 7414  df-mpo 7415  df-rngohom 37992

This theorem is referenced by:  isrngohom  37994