| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simpr 484 | . . . . . . . 8
⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → 𝑠 = 𝑆) | 
| 2 | 1 | fveq2d 6909 | . . . . . . 7
⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (1st ‘𝑠) = (1st ‘𝑆)) | 
| 3 |  | rnghomval.5 | . . . . . . 7
⊢ 𝐽 = (1st ‘𝑆) | 
| 4 | 2, 3 | eqtr4di 2794 | . . . . . 6
⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (1st ‘𝑠) = 𝐽) | 
| 5 | 4 | rneqd 5948 | . . . . 5
⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → ran (1st ‘𝑠) = ran 𝐽) | 
| 6 |  | rnghomval.7 | . . . . 5
⊢ 𝑌 = ran 𝐽 | 
| 7 | 5, 6 | eqtr4di 2794 | . . . 4
⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → ran (1st ‘𝑠) = 𝑌) | 
| 8 |  | simpl 482 | . . . . . . . 8
⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → 𝑟 = 𝑅) | 
| 9 | 8 | fveq2d 6909 | . . . . . . 7
⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (1st ‘𝑟) = (1st ‘𝑅)) | 
| 10 |  | rnghomval.1 | . . . . . . 7
⊢ 𝐺 = (1st ‘𝑅) | 
| 11 | 9, 10 | eqtr4di 2794 | . . . . . 6
⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (1st ‘𝑟) = 𝐺) | 
| 12 | 11 | rneqd 5948 | . . . . 5
⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → ran (1st ‘𝑟) = ran 𝐺) | 
| 13 |  | rnghomval.3 | . . . . 5
⊢ 𝑋 = ran 𝐺 | 
| 14 | 12, 13 | eqtr4di 2794 | . . . 4
⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → ran (1st ‘𝑟) = 𝑋) | 
| 15 | 7, 14 | oveq12d 7450 | . . 3
⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (ran (1st ‘𝑠) ↑m ran
(1st ‘𝑟))
= (𝑌 ↑m
𝑋)) | 
| 16 | 8 | fveq2d 6909 | . . . . . . . . 9
⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (2nd ‘𝑟) = (2nd ‘𝑅)) | 
| 17 |  | rnghomval.2 | . . . . . . . . 9
⊢ 𝐻 = (2nd ‘𝑅) | 
| 18 | 16, 17 | eqtr4di 2794 | . . . . . . . 8
⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (2nd ‘𝑟) = 𝐻) | 
| 19 | 18 | fveq2d 6909 | . . . . . . 7
⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (GId‘(2nd
‘𝑟)) =
(GId‘𝐻)) | 
| 20 |  | rnghomval.4 | . . . . . . 7
⊢ 𝑈 = (GId‘𝐻) | 
| 21 | 19, 20 | eqtr4di 2794 | . . . . . 6
⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (GId‘(2nd
‘𝑟)) = 𝑈) | 
| 22 | 21 | fveq2d 6909 | . . . . 5
⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (𝑓‘(GId‘(2nd
‘𝑟))) = (𝑓‘𝑈)) | 
| 23 | 1 | fveq2d 6909 | . . . . . . . 8
⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (2nd ‘𝑠) = (2nd ‘𝑆)) | 
| 24 |  | rnghomval.6 | . . . . . . . 8
⊢ 𝐾 = (2nd ‘𝑆) | 
| 25 | 23, 24 | eqtr4di 2794 | . . . . . . 7
⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (2nd ‘𝑠) = 𝐾) | 
| 26 | 25 | fveq2d 6909 | . . . . . 6
⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (GId‘(2nd
‘𝑠)) =
(GId‘𝐾)) | 
| 27 |  | rnghomval.8 | . . . . . 6
⊢ 𝑉 = (GId‘𝐾) | 
| 28 | 26, 27 | eqtr4di 2794 | . . . . 5
⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (GId‘(2nd
‘𝑠)) = 𝑉) | 
| 29 | 22, 28 | eqeq12d 2752 | . . . 4
⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → ((𝑓‘(GId‘(2nd
‘𝑟))) =
(GId‘(2nd ‘𝑠)) ↔ (𝑓‘𝑈) = 𝑉)) | 
| 30 | 11 | oveqd 7449 | . . . . . . . . 9
⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (𝑥(1st ‘𝑟)𝑦) = (𝑥𝐺𝑦)) | 
| 31 | 30 | fveq2d 6909 | . . . . . . . 8
⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (𝑓‘(𝑥(1st ‘𝑟)𝑦)) = (𝑓‘(𝑥𝐺𝑦))) | 
| 32 | 4 | oveqd 7449 | . . . . . . . 8
⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → ((𝑓‘𝑥)(1st ‘𝑠)(𝑓‘𝑦)) = ((𝑓‘𝑥)𝐽(𝑓‘𝑦))) | 
| 33 | 31, 32 | eqeq12d 2752 | . . . . . . 7
⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → ((𝑓‘(𝑥(1st ‘𝑟)𝑦)) = ((𝑓‘𝑥)(1st ‘𝑠)(𝑓‘𝑦)) ↔ (𝑓‘(𝑥𝐺𝑦)) = ((𝑓‘𝑥)𝐽(𝑓‘𝑦)))) | 
| 34 | 18 | oveqd 7449 | . . . . . . . . 9
⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (𝑥(2nd ‘𝑟)𝑦) = (𝑥𝐻𝑦)) | 
| 35 | 34 | fveq2d 6909 | . . . . . . . 8
⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (𝑓‘(𝑥(2nd ‘𝑟)𝑦)) = (𝑓‘(𝑥𝐻𝑦))) | 
| 36 | 25 | oveqd 7449 | . . . . . . . 8
⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → ((𝑓‘𝑥)(2nd ‘𝑠)(𝑓‘𝑦)) = ((𝑓‘𝑥)𝐾(𝑓‘𝑦))) | 
| 37 | 35, 36 | eqeq12d 2752 | . . . . . . 7
⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → ((𝑓‘(𝑥(2nd ‘𝑟)𝑦)) = ((𝑓‘𝑥)(2nd ‘𝑠)(𝑓‘𝑦)) ↔ (𝑓‘(𝑥𝐻𝑦)) = ((𝑓‘𝑥)𝐾(𝑓‘𝑦)))) | 
| 38 | 33, 37 | anbi12d 632 | . . . . . 6
⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (((𝑓‘(𝑥(1st ‘𝑟)𝑦)) = ((𝑓‘𝑥)(1st ‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(2nd ‘𝑟)𝑦)) = ((𝑓‘𝑥)(2nd ‘𝑠)(𝑓‘𝑦))) ↔ ((𝑓‘(𝑥𝐺𝑦)) = ((𝑓‘𝑥)𝐽(𝑓‘𝑦)) ∧ (𝑓‘(𝑥𝐻𝑦)) = ((𝑓‘𝑥)𝐾(𝑓‘𝑦))))) | 
| 39 | 14, 38 | raleqbidv 3345 | . . . . 5
⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (∀𝑦 ∈ ran (1st ‘𝑟)((𝑓‘(𝑥(1st ‘𝑟)𝑦)) = ((𝑓‘𝑥)(1st ‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(2nd ‘𝑟)𝑦)) = ((𝑓‘𝑥)(2nd ‘𝑠)(𝑓‘𝑦))) ↔ ∀𝑦 ∈ 𝑋 ((𝑓‘(𝑥𝐺𝑦)) = ((𝑓‘𝑥)𝐽(𝑓‘𝑦)) ∧ (𝑓‘(𝑥𝐻𝑦)) = ((𝑓‘𝑥)𝐾(𝑓‘𝑦))))) | 
| 40 | 14, 39 | raleqbidv 3345 | . . . 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 3454 | . 2
⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → {𝑓 ∈ (ran (1st ‘𝑠) ↑m ran
(1st ‘𝑟))
∣ ((𝑓‘(GId‘(2nd
‘𝑟))) =
(GId‘(2nd ‘𝑠)) ∧ ∀𝑥 ∈ ran (1st ‘𝑟)∀𝑦 ∈ ran (1st ‘𝑟)((𝑓‘(𝑥(1st ‘𝑟)𝑦)) = ((𝑓‘𝑥)(1st ‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(2nd ‘𝑟)𝑦)) = ((𝑓‘𝑥)(2nd ‘𝑠)(𝑓‘𝑦))))} = {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ((𝑓‘𝑈) = 𝑉 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑓‘(𝑥𝐺𝑦)) = ((𝑓‘𝑥)𝐽(𝑓‘𝑦)) ∧ (𝑓‘(𝑥𝐻𝑦)) = ((𝑓‘𝑥)𝐾(𝑓‘𝑦))))}) | 
| 43 |  | df-rngohom 37971 | . 2
⊢ 
RingOpsHom = (𝑟 ∈
RingOps, 𝑠 ∈ RingOps
↦ {𝑓 ∈ (ran
(1st ‘𝑠)
↑m ran (1st ‘𝑟)) ∣ ((𝑓‘(GId‘(2nd
‘𝑟))) =
(GId‘(2nd ‘𝑠)) ∧ ∀𝑥 ∈ ran (1st ‘𝑟)∀𝑦 ∈ ran (1st ‘𝑟)((𝑓‘(𝑥(1st ‘𝑟)𝑦)) = ((𝑓‘𝑥)(1st ‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(2nd ‘𝑟)𝑦)) = ((𝑓‘𝑥)(2nd ‘𝑠)(𝑓‘𝑦))))}) | 
| 44 |  | ovex 7465 | . . 3
⊢ (𝑌 ↑m 𝑋) ∈ V | 
| 45 | 44 | rabex 5338 | . 2
⊢ {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ((𝑓‘𝑈) = 𝑉 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑓‘(𝑥𝐺𝑦)) = ((𝑓‘𝑥)𝐽(𝑓‘𝑦)) ∧ (𝑓‘(𝑥𝐻𝑦)) = ((𝑓‘𝑥)𝐾(𝑓‘𝑦))))} ∈ V | 
| 46 | 42, 43, 45 | ovmpoa 7589 | 1
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) → (𝑅 RingOpsHom 𝑆) = {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ((𝑓‘𝑈) = 𝑉 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑓‘(𝑥𝐺𝑦)) = ((𝑓‘𝑥)𝐽(𝑓‘𝑦)) ∧ (𝑓‘(𝑥𝐻𝑦)) = ((𝑓‘𝑥)𝐾(𝑓‘𝑦))))}) |