Theorem rngohomval 39038

Description: Obsolete theorem, use rhmval0 20717 instead. The set of ring homomorphisms. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 22-Sep-2015.) (Proof modification is discouraged.) (New usage is discouraged.)

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 490	. . . . . . . 8 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → 𝑠 = 𝑆)
2	1	fveq2d 6897	. . . . . . 7 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (1st ‘𝑠) = (1st ‘𝑆))
3		rnghomval.5	. . . . . . 7 ⊢ 𝐽 = (1st ‘𝑆)
4	2, 3	eqtr4di 2816	. . . . . 6 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (1st ‘𝑠) = 𝐽)
5	4	rneqd 5924	. . . . 5 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → ran (1st ‘𝑠) = ran 𝐽)
6		rnghomval.7	. . . . 5 ⊢ 𝑌 = ran 𝐽
7	5, 6	eqtr4di 2816	. . . 4 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → ran (1st ‘𝑠) = 𝑌)
8		simpl 488	. . . . . . . 8 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → 𝑟 = 𝑅)
9	8	fveq2d 6897	. . . . . . 7 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (1st ‘𝑟) = (1st ‘𝑅))
10		rnghomval.1	. . . . . . 7 ⊢ 𝐺 = (1st ‘𝑅)
11	9, 10	eqtr4di 2816	. . . . . 6 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (1st ‘𝑟) = 𝐺)
12	11	rneqd 5924	. . . . 5 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → ran (1st ‘𝑟) = ran 𝐺)
13		rnghomval.3	. . . . 5 ⊢ 𝑋 = ran 𝐺
14	12, 13	eqtr4di 2816	. . . 4 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → ran (1st ‘𝑟) = 𝑋)
15	7, 14	oveq12d 7445	. . 3 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (ran (1st ‘𝑠) ↑m ran (1st ‘𝑟)) = (𝑌 ↑m 𝑋))
16	8	fveq2d 6897	. . . . . . . . 9 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (2nd ‘𝑟) = (2nd ‘𝑅))
17		rnghomval.2	. . . . . . . . 9 ⊢ 𝐻 = (2nd ‘𝑅)
18	16, 17	eqtr4di 2816	. . . . . . . 8 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (2nd ‘𝑟) = 𝐻)
19	18	fveq2d 6897	. . . . . . 7 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (GId‘(2nd ‘𝑟)) = (GId‘𝐻))
20		rnghomval.4	. . . . . . 7 ⊢ 𝑈 = (GId‘𝐻)
21	19, 20	eqtr4di 2816	. . . . . 6 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (GId‘(2nd ‘𝑟)) = 𝑈)
22	21	fveq2d 6897	. . . . 5 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (𝑓‘(GId‘(2nd ‘𝑟))) = (𝑓‘𝑈))
23	1	fveq2d 6897	. . . . . . . 8 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (2nd ‘𝑠) = (2nd ‘𝑆))
24		rnghomval.6	. . . . . . . 8 ⊢ 𝐾 = (2nd ‘𝑆)
25	23, 24	eqtr4di 2816	. . . . . . 7 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (2nd ‘𝑠) = 𝐾)
26	25	fveq2d 6897	. . . . . 6 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (GId‘(2nd ‘𝑠)) = (GId‘𝐾))
27		rnghomval.8	. . . . . 6 ⊢ 𝑉 = (GId‘𝐾)
28	26, 27	eqtr4di 2816	. . . . 5 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (GId‘(2nd ‘𝑠)) = 𝑉)
29	22, 28	eqeq12d 2779	. . . 4 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → ((𝑓‘(GId‘(2nd ‘𝑟))) = (GId‘(2nd ‘𝑠)) ↔ (𝑓‘𝑈) = 𝑉))
30	11	oveqd 7444	. . . . . . . . 9 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (𝑥(1st ‘𝑟)𝑦) = (𝑥𝐺𝑦))
31	30	fveq2d 6897	. . . . . . . 8 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (𝑓‘(𝑥(1st ‘𝑟)𝑦)) = (𝑓‘(𝑥𝐺𝑦)))
32	4	oveqd 7444	. . . . . . . 8 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → ((𝑓‘𝑥)(1st ‘𝑠)(𝑓‘𝑦)) = ((𝑓‘𝑥)𝐽(𝑓‘𝑦)))
33	31, 32	eqeq12d 2779	. . . . . . 7 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → ((𝑓‘(𝑥(1st ‘𝑟)𝑦)) = ((𝑓‘𝑥)(1st ‘𝑠)(𝑓‘𝑦)) ↔ (𝑓‘(𝑥𝐺𝑦)) = ((𝑓‘𝑥)𝐽(𝑓‘𝑦))))
34	18	oveqd 7444	. . . . . . . . 9 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (𝑥(2nd ‘𝑟)𝑦) = (𝑥𝐻𝑦))
35	34	fveq2d 6897	. . . . . . . 8 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (𝑓‘(𝑥(2nd ‘𝑟)𝑦)) = (𝑓‘(𝑥𝐻𝑦)))
36	25	oveqd 7444	. . . . . . . 8 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → ((𝑓‘𝑥)(2nd ‘𝑠)(𝑓‘𝑦)) = ((𝑓‘𝑥)𝐾(𝑓‘𝑦)))
37	35, 36	eqeq12d 2779	. . . . . . 7 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → ((𝑓‘(𝑥(2nd ‘𝑟)𝑦)) = ((𝑓‘𝑥)(2nd ‘𝑠)(𝑓‘𝑦)) ↔ (𝑓‘(𝑥𝐻𝑦)) = ((𝑓‘𝑥)𝐾(𝑓‘𝑦))))
38	33, 37	anbi12d 644	. . . . . 6 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (((𝑓‘(𝑥(1st ‘𝑟)𝑦)) = ((𝑓‘𝑥)(1st ‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(2nd ‘𝑟)𝑦)) = ((𝑓‘𝑥)(2nd ‘𝑠)(𝑓‘𝑦))) ↔ ((𝑓‘(𝑥𝐺𝑦)) = ((𝑓‘𝑥)𝐽(𝑓‘𝑦)) ∧ (𝑓‘(𝑥𝐻𝑦)) = ((𝑓‘𝑥)𝐾(𝑓‘𝑦)))))
39	14, 38	raleqbidv 3337	. . . . 5 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (∀𝑦 ∈ ran (1st ‘𝑟)((𝑓‘(𝑥(1st ‘𝑟)𝑦)) = ((𝑓‘𝑥)(1st ‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(2nd ‘𝑟)𝑦)) = ((𝑓‘𝑥)(2nd ‘𝑠)(𝑓‘𝑦))) ↔ ∀𝑦 ∈ 𝑋 ((𝑓‘(𝑥𝐺𝑦)) = ((𝑓‘𝑥)𝐽(𝑓‘𝑦)) ∧ (𝑓‘(𝑥𝐻𝑦)) = ((𝑓‘𝑥)𝐾(𝑓‘𝑦)))))
40	14, 39	raleqbidv 3337	. . . 4 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (∀𝑥 ∈ ran (1st ‘𝑟)∀𝑦 ∈ ran (1st ‘𝑟)((𝑓‘(𝑥(1st ‘𝑟)𝑦)) = ((𝑓‘𝑥)(1st ‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(2nd ‘𝑟)𝑦)) = ((𝑓‘𝑥)(2nd ‘𝑠)(𝑓‘𝑦))) ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑓‘(𝑥𝐺𝑦)) = ((𝑓‘𝑥)𝐽(𝑓‘𝑦)) ∧ (𝑓‘(𝑥𝐻𝑦)) = ((𝑓‘𝑥)𝐾(𝑓‘𝑦)))))
41	29, 40	anbi12d 644	. . 3 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (((𝑓‘(GId‘(2nd ‘𝑟))) = (GId‘(2nd ‘𝑠)) ∧ ∀𝑥 ∈ ran (1st ‘𝑟)∀𝑦 ∈ ran (1st ‘𝑟)((𝑓‘(𝑥(1st ‘𝑟)𝑦)) = ((𝑓‘𝑥)(1st ‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(2nd ‘𝑟)𝑦)) = ((𝑓‘𝑥)(2nd ‘𝑠)(𝑓‘𝑦)))) ↔ ((𝑓‘𝑈) = 𝑉 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑓‘(𝑥𝐺𝑦)) = ((𝑓‘𝑥)𝐽(𝑓‘𝑦)) ∧ (𝑓‘(𝑥𝐻𝑦)) = ((𝑓‘𝑥)𝐾(𝑓‘𝑦))))))
42	15, 41	rabeqbidv 3432	. 2 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → {𝑓 ∈ (ran (1st ‘𝑠) ↑m ran (1st ‘𝑟)) ∣ ((𝑓‘(GId‘(2nd ‘𝑟))) = (GId‘(2nd ‘𝑠)) ∧ ∀𝑥 ∈ ran (1st ‘𝑟)∀𝑦 ∈ ran (1st ‘𝑟)((𝑓‘(𝑥(1st ‘𝑟)𝑦)) = ((𝑓‘𝑥)(1st ‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(2nd ‘𝑟)𝑦)) = ((𝑓‘𝑥)(2nd ‘𝑠)(𝑓‘𝑦))))} = {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ((𝑓‘𝑈) = 𝑉 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑓‘(𝑥𝐺𝑦)) = ((𝑓‘𝑥)𝐽(𝑓‘𝑦)) ∧ (𝑓‘(𝑥𝐻𝑦)) = ((𝑓‘𝑥)𝐾(𝑓‘𝑦))))})
43		df-rngohom 39037	. 2 ⊢ RingOpsHom = (𝑟 ∈ RingOps, 𝑠 ∈ RingOps ↦ {𝑓 ∈ (ran (1st ‘𝑠) ↑m ran (1st ‘𝑟)) ∣ ((𝑓‘(GId‘(2nd ‘𝑟))) = (GId‘(2nd ‘𝑠)) ∧ ∀𝑥 ∈ ran (1st ‘𝑟)∀𝑦 ∈ ran (1st ‘𝑟)((𝑓‘(𝑥(1st ‘𝑟)𝑦)) = ((𝑓‘𝑥)(1st ‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(2nd ‘𝑟)𝑦)) = ((𝑓‘𝑥)(2nd ‘𝑠)(𝑓‘𝑦))))})
44		ovex 7460	. . 3 ⊢ (𝑌 ↑m 𝑋) ∈ V
45	44	rabex 5303	. 2 ⊢ {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ((𝑓‘𝑈) = 𝑉 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑓‘(𝑥𝐺𝑦)) = ((𝑓‘𝑥)𝐽(𝑓‘𝑦)) ∧ (𝑓‘(𝑥𝐻𝑦)) = ((𝑓‘𝑥)𝐾(𝑓‘𝑦))))} ∈ V
46	42, 43, 45	ovmpoa 7582	1 ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) → (𝑅 RingOpsHom 𝑆) = {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ((𝑓‘𝑈) = 𝑉 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑓‘(𝑥𝐺𝑦)) = ((𝑓‘𝑥)𝐽(𝑓‘𝑦)) ∧ (𝑓‘(𝑥𝐻𝑦)) = ((𝑓‘𝑥)𝐾(𝑓‘𝑦))))})

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ∈ wcel 2146  ∀wral 3079  {crab 3415  ran crn 5655  ‘cfv 6546  (class class class)co 7427  1^st c1st 8006  2^nd c2nd 8007   ↑_m cmap 8858  GIdcgi 31104  RingOpscrngo 38968   RingOpsHom crngohom 39034

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735  ax-sep 5251  ax-nul 5262  ax-pr 5394

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2101  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3416  df-v 3455  df-sbc 3742  df-ss 3900  df-dif 4049  df-in 4093  df-un 4153  df-nul 4281  df-if 4485  df-pw 4561  df-sn 4588  df-pr 4590  df-op 4838  df-uni 4870  df-br 5106  df-opab 5170  df-id 5549  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-iota 6500  df-fun 6548  df-fv 6554  df-ov 7430  df-oprab 7431  df-mpo 7432  df-rngohom 39037

This theorem is used by:  isrngohom  39039