Step | Hyp | Ref
| Expression |
1 | | rnghommul.1 |
. . . . . . 7
⊢ 𝐺 = (1st ‘𝑅) |
2 | | rnghommul.3 |
. . . . . . 7
⊢ 𝐻 = (2nd ‘𝑅) |
3 | | rnghommul.2 |
. . . . . . 7
⊢ 𝑋 = ran 𝐺 |
4 | | eqid 2622 |
. . . . . . 7
⊢
(GId‘𝐻) =
(GId‘𝐻) |
5 | | eqid 2622 |
. . . . . . 7
⊢
(1st ‘𝑆) = (1st ‘𝑆) |
6 | | rnghommul.4 |
. . . . . . 7
⊢ 𝐾 = (2nd ‘𝑆) |
7 | | eqid 2622 |
. . . . . . 7
⊢ ran
(1st ‘𝑆) =
ran (1st ‘𝑆) |
8 | | eqid 2622 |
. . . . . . 7
⊢
(GId‘𝐾) =
(GId‘𝐾) |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | isrngohom 33764 |
. . . . . 6
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) → (𝐹 ∈ (𝑅 RngHom 𝑆) ↔ (𝐹:𝑋⟶ran (1st ‘𝑆) ∧ (𝐹‘(GId‘𝐻)) = (GId‘𝐾) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝐹‘(𝑥𝐺𝑦)) = ((𝐹‘𝑥)(1st ‘𝑆)(𝐹‘𝑦)) ∧ (𝐹‘(𝑥𝐻𝑦)) = ((𝐹‘𝑥)𝐾(𝐹‘𝑦)))))) |
10 | 9 | biimpa 501 |
. . . . 5
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (𝐹:𝑋⟶ran (1st ‘𝑆) ∧ (𝐹‘(GId‘𝐻)) = (GId‘𝐾) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝐹‘(𝑥𝐺𝑦)) = ((𝐹‘𝑥)(1st ‘𝑆)(𝐹‘𝑦)) ∧ (𝐹‘(𝑥𝐻𝑦)) = ((𝐹‘𝑥)𝐾(𝐹‘𝑦))))) |
11 | 10 | simp3d 1075 |
. . . 4
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝐹‘(𝑥𝐺𝑦)) = ((𝐹‘𝑥)(1st ‘𝑆)(𝐹‘𝑦)) ∧ (𝐹‘(𝑥𝐻𝑦)) = ((𝐹‘𝑥)𝐾(𝐹‘𝑦)))) |
12 | 11 | 3impa 1259 |
. . 3
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝐹‘(𝑥𝐺𝑦)) = ((𝐹‘𝑥)(1st ‘𝑆)(𝐹‘𝑦)) ∧ (𝐹‘(𝑥𝐻𝑦)) = ((𝐹‘𝑥)𝐾(𝐹‘𝑦)))) |
13 | | simpr 477 |
. . . 4
⊢ (((𝐹‘(𝑥𝐺𝑦)) = ((𝐹‘𝑥)(1st ‘𝑆)(𝐹‘𝑦)) ∧ (𝐹‘(𝑥𝐻𝑦)) = ((𝐹‘𝑥)𝐾(𝐹‘𝑦))) → (𝐹‘(𝑥𝐻𝑦)) = ((𝐹‘𝑥)𝐾(𝐹‘𝑦))) |
14 | 13 | 2ralimi 2953 |
. . 3
⊢
(∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑋 ((𝐹‘(𝑥𝐺𝑦)) = ((𝐹‘𝑥)(1st ‘𝑆)(𝐹‘𝑦)) ∧ (𝐹‘(𝑥𝐻𝑦)) = ((𝐹‘𝑥)𝐾(𝐹‘𝑦))) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝐹‘(𝑥𝐻𝑦)) = ((𝐹‘𝑥)𝐾(𝐹‘𝑦))) |
15 | 12, 14 | syl 17 |
. 2
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝐹‘(𝑥𝐻𝑦)) = ((𝐹‘𝑥)𝐾(𝐹‘𝑦))) |
16 | | oveq1 6657 |
. . . . 5
⊢ (𝑥 = 𝐴 → (𝑥𝐻𝑦) = (𝐴𝐻𝑦)) |
17 | 16 | fveq2d 6195 |
. . . 4
⊢ (𝑥 = 𝐴 → (𝐹‘(𝑥𝐻𝑦)) = (𝐹‘(𝐴𝐻𝑦))) |
18 | | fveq2 6191 |
. . . . 5
⊢ (𝑥 = 𝐴 → (𝐹‘𝑥) = (𝐹‘𝐴)) |
19 | 18 | oveq1d 6665 |
. . . 4
⊢ (𝑥 = 𝐴 → ((𝐹‘𝑥)𝐾(𝐹‘𝑦)) = ((𝐹‘𝐴)𝐾(𝐹‘𝑦))) |
20 | 17, 19 | eqeq12d 2637 |
. . 3
⊢ (𝑥 = 𝐴 → ((𝐹‘(𝑥𝐻𝑦)) = ((𝐹‘𝑥)𝐾(𝐹‘𝑦)) ↔ (𝐹‘(𝐴𝐻𝑦)) = ((𝐹‘𝐴)𝐾(𝐹‘𝑦)))) |
21 | | oveq2 6658 |
. . . . 5
⊢ (𝑦 = 𝐵 → (𝐴𝐻𝑦) = (𝐴𝐻𝐵)) |
22 | 21 | fveq2d 6195 |
. . . 4
⊢ (𝑦 = 𝐵 → (𝐹‘(𝐴𝐻𝑦)) = (𝐹‘(𝐴𝐻𝐵))) |
23 | | fveq2 6191 |
. . . . 5
⊢ (𝑦 = 𝐵 → (𝐹‘𝑦) = (𝐹‘𝐵)) |
24 | 23 | oveq2d 6666 |
. . . 4
⊢ (𝑦 = 𝐵 → ((𝐹‘𝐴)𝐾(𝐹‘𝑦)) = ((𝐹‘𝐴)𝐾(𝐹‘𝐵))) |
25 | 22, 24 | eqeq12d 2637 |
. . 3
⊢ (𝑦 = 𝐵 → ((𝐹‘(𝐴𝐻𝑦)) = ((𝐹‘𝐴)𝐾(𝐹‘𝑦)) ↔ (𝐹‘(𝐴𝐻𝐵)) = ((𝐹‘𝐴)𝐾(𝐹‘𝐵)))) |
26 | 20, 25 | rspc2v 3322 |
. 2
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝐹‘(𝑥𝐻𝑦)) = ((𝐹‘𝑥)𝐾(𝐹‘𝑦)) → (𝐹‘(𝐴𝐻𝐵)) = ((𝐹‘𝐴)𝐾(𝐹‘𝐵)))) |
27 | 15, 26 | mpan9 486 |
1
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐹‘(𝐴𝐻𝐵)) = ((𝐹‘𝐴)𝐾(𝐹‘𝐵))) |