Step | Hyp | Ref
| Expression |
1 | | ringi.1 |
. . . . . 6
⊢ 𝐺 = (1st ‘𝑅) |
2 | | ringi.2 |
. . . . . 6
⊢ 𝐻 = (2nd ‘𝑅) |
3 | | ringi.3 |
. . . . . 6
⊢ 𝑋 = ran 𝐺 |
4 | 1, 2, 3 | rngoi 35794 |
. . . . 5
⊢ (𝑅 ∈ RingOps → ((𝐺 ∈ AbelOp ∧ 𝐻:(𝑋 × 𝑋)⟶𝑋) ∧ (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧)) ∧ (𝑥𝐻(𝑦𝐺𝑧)) = ((𝑥𝐻𝑦)𝐺(𝑥𝐻𝑧)) ∧ ((𝑥𝐺𝑦)𝐻𝑧) = ((𝑥𝐻𝑧)𝐺(𝑦𝐻𝑧))) ∧ ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥𝐻𝑦) = 𝑦 ∧ (𝑦𝐻𝑥) = 𝑦)))) |
5 | 4 | simprd 499 |
. . . 4
⊢ (𝑅 ∈ RingOps →
(∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧)) ∧ (𝑥𝐻(𝑦𝐺𝑧)) = ((𝑥𝐻𝑦)𝐺(𝑥𝐻𝑧)) ∧ ((𝑥𝐺𝑦)𝐻𝑧) = ((𝑥𝐻𝑧)𝐺(𝑦𝐻𝑧))) ∧ ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥𝐻𝑦) = 𝑦 ∧ (𝑦𝐻𝑥) = 𝑦))) |
6 | 5 | simpld 498 |
. . 3
⊢ (𝑅 ∈ RingOps →
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧)) ∧ (𝑥𝐻(𝑦𝐺𝑧)) = ((𝑥𝐻𝑦)𝐺(𝑥𝐻𝑧)) ∧ ((𝑥𝐺𝑦)𝐻𝑧) = ((𝑥𝐻𝑧)𝐺(𝑦𝐻𝑧)))) |
7 | | simp1 1138 |
. . . . 5
⊢ ((((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧)) ∧ (𝑥𝐻(𝑦𝐺𝑧)) = ((𝑥𝐻𝑦)𝐺(𝑥𝐻𝑧)) ∧ ((𝑥𝐺𝑦)𝐻𝑧) = ((𝑥𝐻𝑧)𝐺(𝑦𝐻𝑧))) → ((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧))) |
8 | 7 | ralimi 3083 |
. . . 4
⊢
(∀𝑧 ∈
𝑋 (((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧)) ∧ (𝑥𝐻(𝑦𝐺𝑧)) = ((𝑥𝐻𝑦)𝐺(𝑥𝐻𝑧)) ∧ ((𝑥𝐺𝑦)𝐻𝑧) = ((𝑥𝐻𝑧)𝐺(𝑦𝐻𝑧))) → ∀𝑧 ∈ 𝑋 ((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧))) |
9 | 8 | 2ralimi 3084 |
. . 3
⊢
(∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧)) ∧ (𝑥𝐻(𝑦𝐺𝑧)) = ((𝑥𝐻𝑦)𝐺(𝑥𝐻𝑧)) ∧ ((𝑥𝐺𝑦)𝐻𝑧) = ((𝑥𝐻𝑧)𝐺(𝑦𝐻𝑧))) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧))) |
10 | 6, 9 | syl 17 |
. 2
⊢ (𝑅 ∈ RingOps →
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧))) |
11 | | oveq1 7220 |
. . . . 5
⊢ (𝑥 = 𝐴 → (𝑥𝐻𝑦) = (𝐴𝐻𝑦)) |
12 | 11 | oveq1d 7228 |
. . . 4
⊢ (𝑥 = 𝐴 → ((𝑥𝐻𝑦)𝐻𝑧) = ((𝐴𝐻𝑦)𝐻𝑧)) |
13 | | oveq1 7220 |
. . . 4
⊢ (𝑥 = 𝐴 → (𝑥𝐻(𝑦𝐻𝑧)) = (𝐴𝐻(𝑦𝐻𝑧))) |
14 | 12, 13 | eqeq12d 2753 |
. . 3
⊢ (𝑥 = 𝐴 → (((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧)) ↔ ((𝐴𝐻𝑦)𝐻𝑧) = (𝐴𝐻(𝑦𝐻𝑧)))) |
15 | | oveq2 7221 |
. . . . 5
⊢ (𝑦 = 𝐵 → (𝐴𝐻𝑦) = (𝐴𝐻𝐵)) |
16 | 15 | oveq1d 7228 |
. . . 4
⊢ (𝑦 = 𝐵 → ((𝐴𝐻𝑦)𝐻𝑧) = ((𝐴𝐻𝐵)𝐻𝑧)) |
17 | | oveq1 7220 |
. . . . 5
⊢ (𝑦 = 𝐵 → (𝑦𝐻𝑧) = (𝐵𝐻𝑧)) |
18 | 17 | oveq2d 7229 |
. . . 4
⊢ (𝑦 = 𝐵 → (𝐴𝐻(𝑦𝐻𝑧)) = (𝐴𝐻(𝐵𝐻𝑧))) |
19 | 16, 18 | eqeq12d 2753 |
. . 3
⊢ (𝑦 = 𝐵 → (((𝐴𝐻𝑦)𝐻𝑧) = (𝐴𝐻(𝑦𝐻𝑧)) ↔ ((𝐴𝐻𝐵)𝐻𝑧) = (𝐴𝐻(𝐵𝐻𝑧)))) |
20 | | oveq2 7221 |
. . . 4
⊢ (𝑧 = 𝐶 → ((𝐴𝐻𝐵)𝐻𝑧) = ((𝐴𝐻𝐵)𝐻𝐶)) |
21 | | oveq2 7221 |
. . . . 5
⊢ (𝑧 = 𝐶 → (𝐵𝐻𝑧) = (𝐵𝐻𝐶)) |
22 | 21 | oveq2d 7229 |
. . . 4
⊢ (𝑧 = 𝐶 → (𝐴𝐻(𝐵𝐻𝑧)) = (𝐴𝐻(𝐵𝐻𝐶))) |
23 | 20, 22 | eqeq12d 2753 |
. . 3
⊢ (𝑧 = 𝐶 → (((𝐴𝐻𝐵)𝐻𝑧) = (𝐴𝐻(𝐵𝐻𝑧)) ↔ ((𝐴𝐻𝐵)𝐻𝐶) = (𝐴𝐻(𝐵𝐻𝐶)))) |
24 | 14, 19, 23 | rspc3v 3550 |
. 2
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧)) → ((𝐴𝐻𝐵)𝐻𝐶) = (𝐴𝐻(𝐵𝐻𝐶)))) |
25 | 10, 24 | mpan9 510 |
1
⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐻𝐵)𝐻𝐶) = (𝐴𝐻(𝐵𝐻𝐶))) |