Step | Hyp | Ref
| Expression |
1 | | rngdi.b |
. . . 4
⊢ 𝐵 = (Base‘𝑅) |
2 | | eqid 2739 |
. . . 4
⊢
(mulGrp‘𝑅) =
(mulGrp‘𝑅) |
3 | | rngdi.p |
. . . 4
⊢ + =
(+g‘𝑅) |
4 | | rngdi.t |
. . . 4
⊢ · =
(.r‘𝑅) |
5 | 1, 2, 3, 4 | isrng 45153 |
. . 3
⊢ (𝑅 ∈ Rng ↔ (𝑅 ∈ Abel ∧
(mulGrp‘𝑅) ∈
Smgrp ∧ ∀𝑎
∈ 𝐵 ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ((𝑎 · (𝑏 + 𝑐)) = ((𝑎 · 𝑏) + (𝑎 · 𝑐)) ∧ ((𝑎 + 𝑏) · 𝑐) = ((𝑎 · 𝑐) + (𝑏 · 𝑐))))) |
6 | | oveq1 7242 |
. . . . . . . 8
⊢ (𝑎 = 𝑋 → (𝑎 · (𝑏 + 𝑐)) = (𝑋 · (𝑏 + 𝑐))) |
7 | | oveq1 7242 |
. . . . . . . . 9
⊢ (𝑎 = 𝑋 → (𝑎 · 𝑏) = (𝑋 · 𝑏)) |
8 | | oveq1 7242 |
. . . . . . . . 9
⊢ (𝑎 = 𝑋 → (𝑎 · 𝑐) = (𝑋 · 𝑐)) |
9 | 7, 8 | oveq12d 7253 |
. . . . . . . 8
⊢ (𝑎 = 𝑋 → ((𝑎 · 𝑏) + (𝑎 · 𝑐)) = ((𝑋 · 𝑏) + (𝑋 · 𝑐))) |
10 | 6, 9 | eqeq12d 2755 |
. . . . . . 7
⊢ (𝑎 = 𝑋 → ((𝑎 · (𝑏 + 𝑐)) = ((𝑎 · 𝑏) + (𝑎 · 𝑐)) ↔ (𝑋 · (𝑏 + 𝑐)) = ((𝑋 · 𝑏) + (𝑋 · 𝑐)))) |
11 | | oveq1 7242 |
. . . . . . . . 9
⊢ (𝑎 = 𝑋 → (𝑎 + 𝑏) = (𝑋 + 𝑏)) |
12 | 11 | oveq1d 7250 |
. . . . . . . 8
⊢ (𝑎 = 𝑋 → ((𝑎 + 𝑏) · 𝑐) = ((𝑋 + 𝑏) · 𝑐)) |
13 | 8 | oveq1d 7250 |
. . . . . . . 8
⊢ (𝑎 = 𝑋 → ((𝑎 · 𝑐) + (𝑏 · 𝑐)) = ((𝑋 · 𝑐) + (𝑏 · 𝑐))) |
14 | 12, 13 | eqeq12d 2755 |
. . . . . . 7
⊢ (𝑎 = 𝑋 → (((𝑎 + 𝑏) · 𝑐) = ((𝑎 · 𝑐) + (𝑏 · 𝑐)) ↔ ((𝑋 + 𝑏) · 𝑐) = ((𝑋 · 𝑐) + (𝑏 · 𝑐)))) |
15 | 10, 14 | anbi12d 634 |
. . . . . 6
⊢ (𝑎 = 𝑋 → (((𝑎 · (𝑏 + 𝑐)) = ((𝑎 · 𝑏) + (𝑎 · 𝑐)) ∧ ((𝑎 + 𝑏) · 𝑐) = ((𝑎 · 𝑐) + (𝑏 · 𝑐))) ↔ ((𝑋 · (𝑏 + 𝑐)) = ((𝑋 · 𝑏) + (𝑋 · 𝑐)) ∧ ((𝑋 + 𝑏) · 𝑐) = ((𝑋 · 𝑐) + (𝑏 · 𝑐))))) |
16 | | oveq1 7242 |
. . . . . . . . 9
⊢ (𝑏 = 𝑌 → (𝑏 + 𝑐) = (𝑌 + 𝑐)) |
17 | 16 | oveq2d 7251 |
. . . . . . . 8
⊢ (𝑏 = 𝑌 → (𝑋 · (𝑏 + 𝑐)) = (𝑋 · (𝑌 + 𝑐))) |
18 | | oveq2 7243 |
. . . . . . . . 9
⊢ (𝑏 = 𝑌 → (𝑋 · 𝑏) = (𝑋 · 𝑌)) |
19 | 18 | oveq1d 7250 |
. . . . . . . 8
⊢ (𝑏 = 𝑌 → ((𝑋 · 𝑏) + (𝑋 · 𝑐)) = ((𝑋 · 𝑌) + (𝑋 · 𝑐))) |
20 | 17, 19 | eqeq12d 2755 |
. . . . . . 7
⊢ (𝑏 = 𝑌 → ((𝑋 · (𝑏 + 𝑐)) = ((𝑋 · 𝑏) + (𝑋 · 𝑐)) ↔ (𝑋 · (𝑌 + 𝑐)) = ((𝑋 · 𝑌) + (𝑋 · 𝑐)))) |
21 | | oveq2 7243 |
. . . . . . . . 9
⊢ (𝑏 = 𝑌 → (𝑋 + 𝑏) = (𝑋 + 𝑌)) |
22 | 21 | oveq1d 7250 |
. . . . . . . 8
⊢ (𝑏 = 𝑌 → ((𝑋 + 𝑏) · 𝑐) = ((𝑋 + 𝑌) · 𝑐)) |
23 | | oveq1 7242 |
. . . . . . . . 9
⊢ (𝑏 = 𝑌 → (𝑏 · 𝑐) = (𝑌 · 𝑐)) |
24 | 23 | oveq2d 7251 |
. . . . . . . 8
⊢ (𝑏 = 𝑌 → ((𝑋 · 𝑐) + (𝑏 · 𝑐)) = ((𝑋 · 𝑐) + (𝑌 · 𝑐))) |
25 | 22, 24 | eqeq12d 2755 |
. . . . . . 7
⊢ (𝑏 = 𝑌 → (((𝑋 + 𝑏) · 𝑐) = ((𝑋 · 𝑐) + (𝑏 · 𝑐)) ↔ ((𝑋 + 𝑌) · 𝑐) = ((𝑋 · 𝑐) + (𝑌 · 𝑐)))) |
26 | 20, 25 | anbi12d 634 |
. . . . . 6
⊢ (𝑏 = 𝑌 → (((𝑋 · (𝑏 + 𝑐)) = ((𝑋 · 𝑏) + (𝑋 · 𝑐)) ∧ ((𝑋 + 𝑏) · 𝑐) = ((𝑋 · 𝑐) + (𝑏 · 𝑐))) ↔ ((𝑋 · (𝑌 + 𝑐)) = ((𝑋 · 𝑌) + (𝑋 · 𝑐)) ∧ ((𝑋 + 𝑌) · 𝑐) = ((𝑋 · 𝑐) + (𝑌 · 𝑐))))) |
27 | | oveq2 7243 |
. . . . . . . . 9
⊢ (𝑐 = 𝑍 → (𝑌 + 𝑐) = (𝑌 + 𝑍)) |
28 | 27 | oveq2d 7251 |
. . . . . . . 8
⊢ (𝑐 = 𝑍 → (𝑋 · (𝑌 + 𝑐)) = (𝑋 · (𝑌 + 𝑍))) |
29 | | oveq2 7243 |
. . . . . . . . 9
⊢ (𝑐 = 𝑍 → (𝑋 · 𝑐) = (𝑋 · 𝑍)) |
30 | 29 | oveq2d 7251 |
. . . . . . . 8
⊢ (𝑐 = 𝑍 → ((𝑋 · 𝑌) + (𝑋 · 𝑐)) = ((𝑋 · 𝑌) + (𝑋 · 𝑍))) |
31 | 28, 30 | eqeq12d 2755 |
. . . . . . 7
⊢ (𝑐 = 𝑍 → ((𝑋 · (𝑌 + 𝑐)) = ((𝑋 · 𝑌) + (𝑋 · 𝑐)) ↔ (𝑋 · (𝑌 + 𝑍)) = ((𝑋 · 𝑌) + (𝑋 · 𝑍)))) |
32 | | oveq2 7243 |
. . . . . . . 8
⊢ (𝑐 = 𝑍 → ((𝑋 + 𝑌) · 𝑐) = ((𝑋 + 𝑌) · 𝑍)) |
33 | | oveq2 7243 |
. . . . . . . . 9
⊢ (𝑐 = 𝑍 → (𝑌 · 𝑐) = (𝑌 · 𝑍)) |
34 | 29, 33 | oveq12d 7253 |
. . . . . . . 8
⊢ (𝑐 = 𝑍 → ((𝑋 · 𝑐) + (𝑌 · 𝑐)) = ((𝑋 · 𝑍) + (𝑌 · 𝑍))) |
35 | 32, 34 | eqeq12d 2755 |
. . . . . . 7
⊢ (𝑐 = 𝑍 → (((𝑋 + 𝑌) · 𝑐) = ((𝑋 · 𝑐) + (𝑌 · 𝑐)) ↔ ((𝑋 + 𝑌) · 𝑍) = ((𝑋 · 𝑍) + (𝑌 · 𝑍)))) |
36 | 31, 35 | anbi12d 634 |
. . . . . 6
⊢ (𝑐 = 𝑍 → (((𝑋 · (𝑌 + 𝑐)) = ((𝑋 · 𝑌) + (𝑋 · 𝑐)) ∧ ((𝑋 + 𝑌) · 𝑐) = ((𝑋 · 𝑐) + (𝑌 · 𝑐))) ↔ ((𝑋 · (𝑌 + 𝑍)) = ((𝑋 · 𝑌) + (𝑋 · 𝑍)) ∧ ((𝑋 + 𝑌) · 𝑍) = ((𝑋 · 𝑍) + (𝑌 · 𝑍))))) |
37 | 15, 26, 36 | rspc3v 3565 |
. . . . 5
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ((𝑎 · (𝑏 + 𝑐)) = ((𝑎 · 𝑏) + (𝑎 · 𝑐)) ∧ ((𝑎 + 𝑏) · 𝑐) = ((𝑎 · 𝑐) + (𝑏 · 𝑐))) → ((𝑋 · (𝑌 + 𝑍)) = ((𝑋 · 𝑌) + (𝑋 · 𝑍)) ∧ ((𝑋 + 𝑌) · 𝑍) = ((𝑋 · 𝑍) + (𝑌 · 𝑍))))) |
38 | | simpr 488 |
. . . . 5
⊢ (((𝑋 · (𝑌 + 𝑍)) = ((𝑋 · 𝑌) + (𝑋 · 𝑍)) ∧ ((𝑋 + 𝑌) · 𝑍) = ((𝑋 · 𝑍) + (𝑌 · 𝑍))) → ((𝑋 + 𝑌) · 𝑍) = ((𝑋 · 𝑍) + (𝑌 · 𝑍))) |
39 | 37, 38 | syl6com 37 |
. . . 4
⊢
(∀𝑎 ∈
𝐵 ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ((𝑎 · (𝑏 + 𝑐)) = ((𝑎 · 𝑏) + (𝑎 · 𝑐)) ∧ ((𝑎 + 𝑏) · 𝑐) = ((𝑎 · 𝑐) + (𝑏 · 𝑐))) → ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → ((𝑋 + 𝑌) · 𝑍) = ((𝑋 · 𝑍) + (𝑌 · 𝑍)))) |
40 | 39 | 3ad2ant3 1137 |
. . 3
⊢ ((𝑅 ∈ Abel ∧
(mulGrp‘𝑅) ∈
Smgrp ∧ ∀𝑎
∈ 𝐵 ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ((𝑎 · (𝑏 + 𝑐)) = ((𝑎 · 𝑏) + (𝑎 · 𝑐)) ∧ ((𝑎 + 𝑏) · 𝑐) = ((𝑎 · 𝑐) + (𝑏 · 𝑐)))) → ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → ((𝑋 + 𝑌) · 𝑍) = ((𝑋 · 𝑍) + (𝑌 · 𝑍)))) |
41 | 5, 40 | sylbi 220 |
. 2
⊢ (𝑅 ∈ Rng → ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → ((𝑋 + 𝑌) · 𝑍) = ((𝑋 · 𝑍) + (𝑌 · 𝑍)))) |
42 | 41 | imp 410 |
1
⊢ ((𝑅 ∈ Rng ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) · 𝑍) = ((𝑋 · 𝑍) + (𝑌 · 𝑍))) |