| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | rnghomadd.1 | . . . . . . 7
⊢ 𝐺 = (1st ‘𝑅) | 
| 2 |  | eqid 2737 | . . . . . . 7
⊢
(2nd ‘𝑅) = (2nd ‘𝑅) | 
| 3 |  | rnghomadd.2 | . . . . . . 7
⊢ 𝑋 = ran 𝐺 | 
| 4 |  | eqid 2737 | . . . . . . 7
⊢
(GId‘(2nd ‘𝑅)) = (GId‘(2nd ‘𝑅)) | 
| 5 |  | rnghomadd.3 | . . . . . . 7
⊢ 𝐽 = (1st ‘𝑆) | 
| 6 |  | eqid 2737 | . . . . . . 7
⊢
(2nd ‘𝑆) = (2nd ‘𝑆) | 
| 7 |  | eqid 2737 | . . . . . . 7
⊢ ran 𝐽 = ran 𝐽 | 
| 8 |  | eqid 2737 | . . . . . . 7
⊢
(GId‘(2nd ‘𝑆)) = (GId‘(2nd ‘𝑆)) | 
| 9 | 1, 2, 3, 4, 5, 6, 7, 8 | isrngohom 37972 | . . . . . 6
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) → (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ↔ (𝐹:𝑋⟶ran 𝐽 ∧ (𝐹‘(GId‘(2nd
‘𝑅))) =
(GId‘(2nd ‘𝑆)) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝐹‘(𝑥𝐺𝑦)) = ((𝐹‘𝑥)𝐽(𝐹‘𝑦)) ∧ (𝐹‘(𝑥(2nd ‘𝑅)𝑦)) = ((𝐹‘𝑥)(2nd ‘𝑆)(𝐹‘𝑦)))))) | 
| 10 | 9 | biimpa 476 | . . . . 5
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) → (𝐹:𝑋⟶ran 𝐽 ∧ (𝐹‘(GId‘(2nd
‘𝑅))) =
(GId‘(2nd ‘𝑆)) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝐹‘(𝑥𝐺𝑦)) = ((𝐹‘𝑥)𝐽(𝐹‘𝑦)) ∧ (𝐹‘(𝑥(2nd ‘𝑅)𝑦)) = ((𝐹‘𝑥)(2nd ‘𝑆)(𝐹‘𝑦))))) | 
| 11 | 10 | simp3d 1145 | . . . 4
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝐹‘(𝑥𝐺𝑦)) = ((𝐹‘𝑥)𝐽(𝐹‘𝑦)) ∧ (𝐹‘(𝑥(2nd ‘𝑅)𝑦)) = ((𝐹‘𝑥)(2nd ‘𝑆)(𝐹‘𝑦)))) | 
| 12 | 11 | 3impa 1110 | . . 3
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝐹‘(𝑥𝐺𝑦)) = ((𝐹‘𝑥)𝐽(𝐹‘𝑦)) ∧ (𝐹‘(𝑥(2nd ‘𝑅)𝑦)) = ((𝐹‘𝑥)(2nd ‘𝑆)(𝐹‘𝑦)))) | 
| 13 |  | simpl 482 | . . . 4
⊢ (((𝐹‘(𝑥𝐺𝑦)) = ((𝐹‘𝑥)𝐽(𝐹‘𝑦)) ∧ (𝐹‘(𝑥(2nd ‘𝑅)𝑦)) = ((𝐹‘𝑥)(2nd ‘𝑆)(𝐹‘𝑦))) → (𝐹‘(𝑥𝐺𝑦)) = ((𝐹‘𝑥)𝐽(𝐹‘𝑦))) | 
| 14 | 13 | 2ralimi 3123 | . . 3
⊢
(∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑋 ((𝐹‘(𝑥𝐺𝑦)) = ((𝐹‘𝑥)𝐽(𝐹‘𝑦)) ∧ (𝐹‘(𝑥(2nd ‘𝑅)𝑦)) = ((𝐹‘𝑥)(2nd ‘𝑆)(𝐹‘𝑦))) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝐹‘(𝑥𝐺𝑦)) = ((𝐹‘𝑥)𝐽(𝐹‘𝑦))) | 
| 15 | 12, 14 | syl 17 | . 2
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝐹‘(𝑥𝐺𝑦)) = ((𝐹‘𝑥)𝐽(𝐹‘𝑦))) | 
| 16 |  | fvoveq1 7454 | . . . 4
⊢ (𝑥 = 𝐴 → (𝐹‘(𝑥𝐺𝑦)) = (𝐹‘(𝐴𝐺𝑦))) | 
| 17 |  | fveq2 6906 | . . . . 5
⊢ (𝑥 = 𝐴 → (𝐹‘𝑥) = (𝐹‘𝐴)) | 
| 18 | 17 | oveq1d 7446 | . . . 4
⊢ (𝑥 = 𝐴 → ((𝐹‘𝑥)𝐽(𝐹‘𝑦)) = ((𝐹‘𝐴)𝐽(𝐹‘𝑦))) | 
| 19 | 16, 18 | eqeq12d 2753 | . . 3
⊢ (𝑥 = 𝐴 → ((𝐹‘(𝑥𝐺𝑦)) = ((𝐹‘𝑥)𝐽(𝐹‘𝑦)) ↔ (𝐹‘(𝐴𝐺𝑦)) = ((𝐹‘𝐴)𝐽(𝐹‘𝑦)))) | 
| 20 |  | oveq2 7439 | . . . . 5
⊢ (𝑦 = 𝐵 → (𝐴𝐺𝑦) = (𝐴𝐺𝐵)) | 
| 21 | 20 | fveq2d 6910 | . . . 4
⊢ (𝑦 = 𝐵 → (𝐹‘(𝐴𝐺𝑦)) = (𝐹‘(𝐴𝐺𝐵))) | 
| 22 |  | fveq2 6906 | . . . . 5
⊢ (𝑦 = 𝐵 → (𝐹‘𝑦) = (𝐹‘𝐵)) | 
| 23 | 22 | oveq2d 7447 | . . . 4
⊢ (𝑦 = 𝐵 → ((𝐹‘𝐴)𝐽(𝐹‘𝑦)) = ((𝐹‘𝐴)𝐽(𝐹‘𝐵))) | 
| 24 | 21, 23 | eqeq12d 2753 | . . 3
⊢ (𝑦 = 𝐵 → ((𝐹‘(𝐴𝐺𝑦)) = ((𝐹‘𝐴)𝐽(𝐹‘𝑦)) ↔ (𝐹‘(𝐴𝐺𝐵)) = ((𝐹‘𝐴)𝐽(𝐹‘𝐵)))) | 
| 25 | 19, 24 | rspc2v 3633 | . 2
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝐹‘(𝑥𝐺𝑦)) = ((𝐹‘𝑥)𝐽(𝐹‘𝑦)) → (𝐹‘(𝐴𝐺𝐵)) = ((𝐹‘𝐴)𝐽(𝐹‘𝐵)))) | 
| 26 | 15, 25 | mpan9 506 | 1
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐹‘(𝐴𝐺𝐵)) = ((𝐹‘𝐴)𝐽(𝐹‘𝐵))) |