Step | Hyp | Ref
| Expression |
1 | | eqid 2177 |
. . . . . 6
⊢
(oppr‘𝑅) = (oppr‘𝑅) |
2 | 1 | opprring 13061 |
. . . . 5
⊢ (𝑅 ∈ Ring →
(oppr‘𝑅) ∈ Ring) |
3 | 2 | adantr 276 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ (𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) →
(oppr‘𝑅) ∈ Ring) |
4 | | simpr1 1003 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ (𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑁 ∈ ℤ) |
5 | | simpr3 1005 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ (𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑌 ∈ 𝐵) |
6 | | mulgass3.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑅) |
7 | 1, 6 | opprbasg 13059 |
. . . . . 6
⊢ (𝑅 ∈ Ring → 𝐵 =
(Base‘(oppr‘𝑅))) |
8 | 7 | adantr 276 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ (𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝐵 =
(Base‘(oppr‘𝑅))) |
9 | 5, 8 | eleqtrd 2256 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ (𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑌 ∈
(Base‘(oppr‘𝑅))) |
10 | | simpr2 1004 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ (𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑋 ∈ 𝐵) |
11 | 10, 8 | eleqtrd 2256 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ (𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑋 ∈
(Base‘(oppr‘𝑅))) |
12 | | eqid 2177 |
. . . . 5
⊢
(Base‘(oppr‘𝑅)) =
(Base‘(oppr‘𝑅)) |
13 | | eqid 2177 |
. . . . 5
⊢
(.g‘(oppr‘𝑅)) =
(.g‘(oppr‘𝑅)) |
14 | | eqid 2177 |
. . . . 5
⊢
(.r‘(oppr‘𝑅)) =
(.r‘(oppr‘𝑅)) |
15 | 12, 13, 14 | mulgass2 13048 |
. . . 4
⊢
(((oppr‘𝑅) ∈ Ring ∧ (𝑁 ∈ ℤ ∧ 𝑌 ∈
(Base‘(oppr‘𝑅)) ∧ 𝑋 ∈
(Base‘(oppr‘𝑅)))) → ((𝑁(.g‘(oppr‘𝑅))𝑌)(.r‘(oppr‘𝑅))𝑋) = (𝑁(.g‘(oppr‘𝑅))(𝑌(.r‘(oppr‘𝑅))𝑋))) |
16 | 3, 4, 9, 11, 15 | syl13anc 1240 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ (𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((𝑁(.g‘(oppr‘𝑅))𝑌)(.r‘(oppr‘𝑅))𝑋) = (𝑁(.g‘(oppr‘𝑅))(𝑌(.r‘(oppr‘𝑅))𝑋))) |
17 | | simpl 109 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ (𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑅 ∈ Ring) |
18 | 3 | ringgrpd 13001 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ (𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) →
(oppr‘𝑅) ∈ Grp) |
19 | 12, 13, 18, 4, 9 | mulgcld 12880 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ (𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑁(.g‘(oppr‘𝑅))𝑌) ∈ (Base‘(oppr‘𝑅))) |
20 | 19, 8 | eleqtrrd 2257 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ (𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑁(.g‘(oppr‘𝑅))𝑌) ∈ 𝐵) |
21 | | mulgass3.t |
. . . . 5
⊢ × =
(.r‘𝑅) |
22 | 6, 21, 1, 14 | opprmulg 13055 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ (𝑁(.g‘(oppr‘𝑅))𝑌) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → ((𝑁(.g‘(oppr‘𝑅))𝑌)(.r‘(oppr‘𝑅))𝑋) = (𝑋 × (𝑁(.g‘(oppr‘𝑅))𝑌))) |
23 | 17, 20, 10, 22 | syl3anc 1238 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ (𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((𝑁(.g‘(oppr‘𝑅))𝑌)(.r‘(oppr‘𝑅))𝑋) = (𝑋 × (𝑁(.g‘(oppr‘𝑅))𝑌))) |
24 | 6, 21, 1, 14 | opprmulg 13055 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → (𝑌(.r‘(oppr‘𝑅))𝑋) = (𝑋 × 𝑌)) |
25 | 17, 5, 10, 24 | syl3anc 1238 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ (𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑌(.r‘(oppr‘𝑅))𝑋) = (𝑋 × 𝑌)) |
26 | 25 | oveq2d 5884 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ (𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑁(.g‘(oppr‘𝑅))(𝑌(.r‘(oppr‘𝑅))𝑋)) = (𝑁(.g‘(oppr‘𝑅))(𝑋 × 𝑌))) |
27 | 16, 23, 26 | 3eqtr3d 2218 |
. 2
⊢ ((𝑅 ∈ Ring ∧ (𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋 × (𝑁(.g‘(oppr‘𝑅))𝑌)) = (𝑁(.g‘(oppr‘𝑅))(𝑋 × 𝑌))) |
28 | | mulgass3.m |
. . . . . 6
⊢ · =
(.g‘𝑅) |
29 | 28 | a1i 9 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ (𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → · =
(.g‘𝑅)) |
30 | | eqidd 2178 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ (𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) →
(.g‘(oppr‘𝑅)) =
(.g‘(oppr‘𝑅))) |
31 | 6 | a1i 9 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ (𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝐵 = (Base‘𝑅)) |
32 | | ssidd 3176 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ (𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝐵 ⊆ 𝐵) |
33 | | eqid 2177 |
. . . . . . . 8
⊢
(+g‘𝑅) = (+g‘𝑅) |
34 | 6, 33 | ringacl 13026 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥(+g‘𝑅)𝑦) ∈ 𝐵) |
35 | 34 | 3expb 1204 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝑅)𝑦) ∈ 𝐵) |
36 | 35 | adantlr 477 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ (𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝑅)𝑦) ∈ 𝐵) |
37 | 1, 33 | oppraddg 13060 |
. . . . . . 7
⊢ (𝑅 ∈ Ring →
(+g‘𝑅) =
(+g‘(oppr‘𝑅))) |
38 | 37 | oveqdr 5896 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ (𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑥(+g‘𝑅)𝑦) = (𝑥(+g‘(oppr‘𝑅))𝑦)) |
39 | 38 | adantr 276 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ (𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝑅)𝑦) = (𝑥(+g‘(oppr‘𝑅))𝑦)) |
40 | 29, 30, 17, 3, 31, 8, 32, 36, 39 | mulgpropdg 12900 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ (𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → · =
(.g‘(oppr‘𝑅))) |
41 | 40 | oveqd 5885 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ (𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑁 · 𝑌) = (𝑁(.g‘(oppr‘𝑅))𝑌)) |
42 | 41 | oveq2d 5884 |
. 2
⊢ ((𝑅 ∈ Ring ∧ (𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋 × (𝑁 · 𝑌)) = (𝑋 × (𝑁(.g‘(oppr‘𝑅))𝑌))) |
43 | 40 | oveqd 5885 |
. 2
⊢ ((𝑅 ∈ Ring ∧ (𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑁 · (𝑋 × 𝑌)) = (𝑁(.g‘(oppr‘𝑅))(𝑋 × 𝑌))) |
44 | 27, 42, 43 | 3eqtr4d 2220 |
1
⊢ ((𝑅 ∈ Ring ∧ (𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋 × (𝑁 · 𝑌)) = (𝑁 · (𝑋 × 𝑌))) |