| Step | Hyp | Ref
| Expression |
| 1 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑥 = 0 → (𝑥 · 𝑋) = (0 · 𝑋)) |
| 2 | 1 | oveq1d 7446 |
. . . . . 6
⊢ (𝑥 = 0 → ((𝑥 · 𝑋) × 𝑌) = ((0 · 𝑋) × 𝑌)) |
| 3 | | oveq1 7438 |
. . . . . 6
⊢ (𝑥 = 0 → (𝑥 · (𝑋 × 𝑌)) = (0 · (𝑋 × 𝑌))) |
| 4 | 2, 3 | eqeq12d 2753 |
. . . . 5
⊢ (𝑥 = 0 → (((𝑥 · 𝑋) × 𝑌) = (𝑥 · (𝑋 × 𝑌)) ↔ ((0 · 𝑋) × 𝑌) = (0 · (𝑋 × 𝑌)))) |
| 5 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑥 · 𝑋) = (𝑦 · 𝑋)) |
| 6 | 5 | oveq1d 7446 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((𝑥 · 𝑋) × 𝑌) = ((𝑦 · 𝑋) × 𝑌)) |
| 7 | | oveq1 7438 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑥 · (𝑋 × 𝑌)) = (𝑦 · (𝑋 × 𝑌))) |
| 8 | 6, 7 | eqeq12d 2753 |
. . . . 5
⊢ (𝑥 = 𝑦 → (((𝑥 · 𝑋) × 𝑌) = (𝑥 · (𝑋 × 𝑌)) ↔ ((𝑦 · 𝑋) × 𝑌) = (𝑦 · (𝑋 × 𝑌)))) |
| 9 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑥 = (𝑦 + 1) → (𝑥 · 𝑋) = ((𝑦 + 1) · 𝑋)) |
| 10 | 9 | oveq1d 7446 |
. . . . . 6
⊢ (𝑥 = (𝑦 + 1) → ((𝑥 · 𝑋) × 𝑌) = (((𝑦 + 1) · 𝑋) × 𝑌)) |
| 11 | | oveq1 7438 |
. . . . . 6
⊢ (𝑥 = (𝑦 + 1) → (𝑥 · (𝑋 × 𝑌)) = ((𝑦 + 1) · (𝑋 × 𝑌))) |
| 12 | 10, 11 | eqeq12d 2753 |
. . . . 5
⊢ (𝑥 = (𝑦 + 1) → (((𝑥 · 𝑋) × 𝑌) = (𝑥 · (𝑋 × 𝑌)) ↔ (((𝑦 + 1) · 𝑋) × 𝑌) = ((𝑦 + 1) · (𝑋 × 𝑌)))) |
| 13 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑥 = -𝑦 → (𝑥 · 𝑋) = (-𝑦 · 𝑋)) |
| 14 | 13 | oveq1d 7446 |
. . . . . 6
⊢ (𝑥 = -𝑦 → ((𝑥 · 𝑋) × 𝑌) = ((-𝑦 · 𝑋) × 𝑌)) |
| 15 | | oveq1 7438 |
. . . . . 6
⊢ (𝑥 = -𝑦 → (𝑥 · (𝑋 × 𝑌)) = (-𝑦 · (𝑋 × 𝑌))) |
| 16 | 14, 15 | eqeq12d 2753 |
. . . . 5
⊢ (𝑥 = -𝑦 → (((𝑥 · 𝑋) × 𝑌) = (𝑥 · (𝑋 × 𝑌)) ↔ ((-𝑦 · 𝑋) × 𝑌) = (-𝑦 · (𝑋 × 𝑌)))) |
| 17 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑥 = 𝑁 → (𝑥 · 𝑋) = (𝑁 · 𝑋)) |
| 18 | 17 | oveq1d 7446 |
. . . . . 6
⊢ (𝑥 = 𝑁 → ((𝑥 · 𝑋) × 𝑌) = ((𝑁 · 𝑋) × 𝑌)) |
| 19 | | oveq1 7438 |
. . . . . 6
⊢ (𝑥 = 𝑁 → (𝑥 · (𝑋 × 𝑌)) = (𝑁 · (𝑋 × 𝑌))) |
| 20 | 18, 19 | eqeq12d 2753 |
. . . . 5
⊢ (𝑥 = 𝑁 → (((𝑥 · 𝑋) × 𝑌) = (𝑥 · (𝑋 × 𝑌)) ↔ ((𝑁 · 𝑋) × 𝑌) = (𝑁 · (𝑋 × 𝑌)))) |
| 21 | | mulgass2.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝑅) |
| 22 | | mulgass2.t |
. . . . . . . 8
⊢ × =
(.r‘𝑅) |
| 23 | | eqid 2737 |
. . . . . . . 8
⊢
(0g‘𝑅) = (0g‘𝑅) |
| 24 | 21, 22, 23 | ringlz 20290 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵) → ((0g‘𝑅) × 𝑌) = (0g‘𝑅)) |
| 25 | 24 | 3adant3 1133 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → ((0g‘𝑅) × 𝑌) = (0g‘𝑅)) |
| 26 | | simp3 1139 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → 𝑋 ∈ 𝐵) |
| 27 | | mulgass2.m |
. . . . . . . . 9
⊢ · =
(.g‘𝑅) |
| 28 | 21, 23, 27 | mulg0 19092 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝐵 → (0 · 𝑋) = (0g‘𝑅)) |
| 29 | 26, 28 | syl 17 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → (0 · 𝑋) = (0g‘𝑅)) |
| 30 | 29 | oveq1d 7446 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → ((0 · 𝑋) × 𝑌) = ((0g‘𝑅) × 𝑌)) |
| 31 | 21, 22 | ringcl 20247 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 × 𝑌) ∈ 𝐵) |
| 32 | 31 | 3com23 1127 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → (𝑋 × 𝑌) ∈ 𝐵) |
| 33 | 21, 23, 27 | mulg0 19092 |
. . . . . . 7
⊢ ((𝑋 × 𝑌) ∈ 𝐵 → (0 · (𝑋 × 𝑌)) = (0g‘𝑅)) |
| 34 | 32, 33 | syl 17 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → (0 · (𝑋 × 𝑌)) = (0g‘𝑅)) |
| 35 | 25, 30, 34 | 3eqtr4d 2787 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → ((0 · 𝑋) × 𝑌) = (0 · (𝑋 × 𝑌))) |
| 36 | | oveq1 7438 |
. . . . . . 7
⊢ (((𝑦 · 𝑋) × 𝑌) = (𝑦 · (𝑋 × 𝑌)) → (((𝑦 · 𝑋) × 𝑌)(+g‘𝑅)(𝑋 × 𝑌)) = ((𝑦 · (𝑋 × 𝑌))(+g‘𝑅)(𝑋 × 𝑌))) |
| 37 | | simpl1 1192 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑦 ∈ ℕ0) → 𝑅 ∈ Ring) |
| 38 | | ringgrp 20235 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) |
| 39 | 37, 38 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑦 ∈ ℕ0) → 𝑅 ∈ Grp) |
| 40 | | nn0z 12638 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ0
→ 𝑦 ∈
ℤ) |
| 41 | 40 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑦 ∈ ℕ0) → 𝑦 ∈
ℤ) |
| 42 | 26 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑦 ∈ ℕ0) → 𝑋 ∈ 𝐵) |
| 43 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(+g‘𝑅) = (+g‘𝑅) |
| 44 | 21, 27, 43 | mulgp1 19125 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → ((𝑦 + 1) · 𝑋) = ((𝑦 · 𝑋)(+g‘𝑅)𝑋)) |
| 45 | 39, 41, 42, 44 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑦 ∈ ℕ0) → ((𝑦 + 1) · 𝑋) = ((𝑦 · 𝑋)(+g‘𝑅)𝑋)) |
| 46 | 45 | oveq1d 7446 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑦 ∈ ℕ0) → (((𝑦 + 1) · 𝑋) × 𝑌) = (((𝑦 · 𝑋)(+g‘𝑅)𝑋) × 𝑌)) |
| 47 | 38 | 3ad2ant1 1134 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → 𝑅 ∈ Grp) |
| 48 | 47 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑦 ∈ ℕ0) → 𝑅 ∈ Grp) |
| 49 | 21, 27 | mulgcl 19109 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (𝑦 · 𝑋) ∈ 𝐵) |
| 50 | 48, 41, 42, 49 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑦 ∈ ℕ0) → (𝑦 · 𝑋) ∈ 𝐵) |
| 51 | | simpl2 1193 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑦 ∈ ℕ0) → 𝑌 ∈ 𝐵) |
| 52 | 21, 43, 22 | ringdir 20259 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ ((𝑦 · 𝑋) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (((𝑦 · 𝑋)(+g‘𝑅)𝑋) × 𝑌) = (((𝑦 · 𝑋) × 𝑌)(+g‘𝑅)(𝑋 × 𝑌))) |
| 53 | 37, 50, 42, 51, 52 | syl13anc 1374 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑦 ∈ ℕ0) → (((𝑦 · 𝑋)(+g‘𝑅)𝑋) × 𝑌) = (((𝑦 · 𝑋) × 𝑌)(+g‘𝑅)(𝑋 × 𝑌))) |
| 54 | 46, 53 | eqtrd 2777 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑦 ∈ ℕ0) → (((𝑦 + 1) · 𝑋) × 𝑌) = (((𝑦 · 𝑋) × 𝑌)(+g‘𝑅)(𝑋 × 𝑌))) |
| 55 | 32 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑦 ∈ ℕ0) → (𝑋 × 𝑌) ∈ 𝐵) |
| 56 | 21, 27, 43 | mulgp1 19125 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ (𝑋 × 𝑌) ∈ 𝐵) → ((𝑦 + 1) · (𝑋 × 𝑌)) = ((𝑦 · (𝑋 × 𝑌))(+g‘𝑅)(𝑋 × 𝑌))) |
| 57 | 39, 41, 55, 56 | syl3anc 1373 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑦 ∈ ℕ0) → ((𝑦 + 1) · (𝑋 × 𝑌)) = ((𝑦 · (𝑋 × 𝑌))(+g‘𝑅)(𝑋 × 𝑌))) |
| 58 | 54, 57 | eqeq12d 2753 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑦 ∈ ℕ0) → ((((𝑦 + 1) · 𝑋) × 𝑌) = ((𝑦 + 1) · (𝑋 × 𝑌)) ↔ (((𝑦 · 𝑋) × 𝑌)(+g‘𝑅)(𝑋 × 𝑌)) = ((𝑦 · (𝑋 × 𝑌))(+g‘𝑅)(𝑋 × 𝑌)))) |
| 59 | 36, 58 | imbitrrid 246 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑦 ∈ ℕ0) → (((𝑦 · 𝑋) × 𝑌) = (𝑦 · (𝑋 × 𝑌)) → (((𝑦 + 1) · 𝑋) × 𝑌) = ((𝑦 + 1) · (𝑋 × 𝑌)))) |
| 60 | 59 | ex 412 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → (𝑦 ∈ ℕ0 → (((𝑦 · 𝑋) × 𝑌) = (𝑦 · (𝑋 × 𝑌)) → (((𝑦 + 1) · 𝑋) × 𝑌) = ((𝑦 + 1) · (𝑋 × 𝑌))))) |
| 61 | | fveq2 6906 |
. . . . . . 7
⊢ (((𝑦 · 𝑋) × 𝑌) = (𝑦 · (𝑋 × 𝑌)) → ((invg‘𝑅)‘((𝑦 · 𝑋) × 𝑌)) = ((invg‘𝑅)‘(𝑦 · (𝑋 × 𝑌)))) |
| 62 | 47 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑦 ∈ ℕ) → 𝑅 ∈ Grp) |
| 63 | | nnz 12634 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℤ) |
| 64 | 63 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈ ℤ) |
| 65 | 26 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑦 ∈ ℕ) → 𝑋 ∈ 𝐵) |
| 66 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(invg‘𝑅) = (invg‘𝑅) |
| 67 | 21, 27, 66 | mulgneg 19110 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (-𝑦 · 𝑋) = ((invg‘𝑅)‘(𝑦 · 𝑋))) |
| 68 | 62, 64, 65, 67 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑦 ∈ ℕ) → (-𝑦 · 𝑋) = ((invg‘𝑅)‘(𝑦 · 𝑋))) |
| 69 | 68 | oveq1d 7446 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑦 ∈ ℕ) → ((-𝑦 · 𝑋) × 𝑌) = (((invg‘𝑅)‘(𝑦 · 𝑋)) × 𝑌)) |
| 70 | | simpl1 1192 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑦 ∈ ℕ) → 𝑅 ∈ Ring) |
| 71 | 62, 64, 65, 49 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑦 ∈ ℕ) → (𝑦 · 𝑋) ∈ 𝐵) |
| 72 | | simpl2 1193 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑦 ∈ ℕ) → 𝑌 ∈ 𝐵) |
| 73 | 21, 22, 66, 70, 71, 72 | ringmneg1 20301 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑦 ∈ ℕ) →
(((invg‘𝑅)‘(𝑦 · 𝑋)) × 𝑌) = ((invg‘𝑅)‘((𝑦 · 𝑋) × 𝑌))) |
| 74 | 69, 73 | eqtrd 2777 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑦 ∈ ℕ) → ((-𝑦 · 𝑋) × 𝑌) = ((invg‘𝑅)‘((𝑦 · 𝑋) × 𝑌))) |
| 75 | 32 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑦 ∈ ℕ) → (𝑋 × 𝑌) ∈ 𝐵) |
| 76 | 21, 27, 66 | mulgneg 19110 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ (𝑋 × 𝑌) ∈ 𝐵) → (-𝑦 · (𝑋 × 𝑌)) = ((invg‘𝑅)‘(𝑦 · (𝑋 × 𝑌)))) |
| 77 | 62, 64, 75, 76 | syl3anc 1373 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑦 ∈ ℕ) → (-𝑦 · (𝑋 × 𝑌)) = ((invg‘𝑅)‘(𝑦 · (𝑋 × 𝑌)))) |
| 78 | 74, 77 | eqeq12d 2753 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑦 ∈ ℕ) → (((-𝑦 · 𝑋) × 𝑌) = (-𝑦 · (𝑋 × 𝑌)) ↔ ((invg‘𝑅)‘((𝑦 · 𝑋) × 𝑌)) = ((invg‘𝑅)‘(𝑦 · (𝑋 × 𝑌))))) |
| 79 | 61, 78 | imbitrrid 246 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑦 ∈ ℕ) → (((𝑦 · 𝑋) × 𝑌) = (𝑦 · (𝑋 × 𝑌)) → ((-𝑦 · 𝑋) × 𝑌) = (-𝑦 · (𝑋 × 𝑌)))) |
| 80 | 79 | ex 412 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → (𝑦 ∈ ℕ → (((𝑦 · 𝑋) × 𝑌) = (𝑦 · (𝑋 × 𝑌)) → ((-𝑦 · 𝑋) × 𝑌) = (-𝑦 · (𝑋 × 𝑌))))) |
| 81 | 4, 8, 12, 16, 20, 35, 60, 80 | zindd 12719 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → (𝑁 ∈ ℤ → ((𝑁 · 𝑋) × 𝑌) = (𝑁 · (𝑋 × 𝑌)))) |
| 82 | 81 | 3exp 1120 |
. . 3
⊢ (𝑅 ∈ Ring → (𝑌 ∈ 𝐵 → (𝑋 ∈ 𝐵 → (𝑁 ∈ ℤ → ((𝑁 · 𝑋) × 𝑌) = (𝑁 · (𝑋 × 𝑌)))))) |
| 83 | 82 | com24 95 |
. 2
⊢ (𝑅 ∈ Ring → (𝑁 ∈ ℤ → (𝑋 ∈ 𝐵 → (𝑌 ∈ 𝐵 → ((𝑁 · 𝑋) × 𝑌) = (𝑁 · (𝑋 × 𝑌)))))) |
| 84 | 83 | 3imp2 1350 |
1
⊢ ((𝑅 ∈ Ring ∧ (𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((𝑁 · 𝑋) × 𝑌) = (𝑁 · (𝑋 × 𝑌))) |