Step | Hyp | Ref
| Expression |
1 | | oveq1 7282 |
. . . . . . 7
⊢ (𝑥 = 0 → (𝑥 · 𝑋) = (0 · 𝑋)) |
2 | 1 | oveq1d 7290 |
. . . . . 6
⊢ (𝑥 = 0 → ((𝑥 · 𝑋) × 𝑌) = ((0 · 𝑋) × 𝑌)) |
3 | | oveq1 7282 |
. . . . . 6
⊢ (𝑥 = 0 → (𝑥 · (𝑋 × 𝑌)) = (0 · (𝑋 × 𝑌))) |
4 | 2, 3 | eqeq12d 2754 |
. . . . 5
⊢ (𝑥 = 0 → (((𝑥 · 𝑋) × 𝑌) = (𝑥 · (𝑋 × 𝑌)) ↔ ((0 · 𝑋) × 𝑌) = (0 · (𝑋 × 𝑌)))) |
5 | | oveq1 7282 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑥 · 𝑋) = (𝑦 · 𝑋)) |
6 | 5 | oveq1d 7290 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((𝑥 · 𝑋) × 𝑌) = ((𝑦 · 𝑋) × 𝑌)) |
7 | | oveq1 7282 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑥 · (𝑋 × 𝑌)) = (𝑦 · (𝑋 × 𝑌))) |
8 | 6, 7 | eqeq12d 2754 |
. . . . 5
⊢ (𝑥 = 𝑦 → (((𝑥 · 𝑋) × 𝑌) = (𝑥 · (𝑋 × 𝑌)) ↔ ((𝑦 · 𝑋) × 𝑌) = (𝑦 · (𝑋 × 𝑌)))) |
9 | | oveq1 7282 |
. . . . . . 7
⊢ (𝑥 = (𝑦 + 1) → (𝑥 · 𝑋) = ((𝑦 + 1) · 𝑋)) |
10 | 9 | oveq1d 7290 |
. . . . . 6
⊢ (𝑥 = (𝑦 + 1) → ((𝑥 · 𝑋) × 𝑌) = (((𝑦 + 1) · 𝑋) × 𝑌)) |
11 | | oveq1 7282 |
. . . . . 6
⊢ (𝑥 = (𝑦 + 1) → (𝑥 · (𝑋 × 𝑌)) = ((𝑦 + 1) · (𝑋 × 𝑌))) |
12 | 10, 11 | eqeq12d 2754 |
. . . . 5
⊢ (𝑥 = (𝑦 + 1) → (((𝑥 · 𝑋) × 𝑌) = (𝑥 · (𝑋 × 𝑌)) ↔ (((𝑦 + 1) · 𝑋) × 𝑌) = ((𝑦 + 1) · (𝑋 × 𝑌)))) |
13 | | oveq1 7282 |
. . . . . . 7
⊢ (𝑥 = -𝑦 → (𝑥 · 𝑋) = (-𝑦 · 𝑋)) |
14 | 13 | oveq1d 7290 |
. . . . . 6
⊢ (𝑥 = -𝑦 → ((𝑥 · 𝑋) × 𝑌) = ((-𝑦 · 𝑋) × 𝑌)) |
15 | | oveq1 7282 |
. . . . . 6
⊢ (𝑥 = -𝑦 → (𝑥 · (𝑋 × 𝑌)) = (-𝑦 · (𝑋 × 𝑌))) |
16 | 14, 15 | eqeq12d 2754 |
. . . . 5
⊢ (𝑥 = -𝑦 → (((𝑥 · 𝑋) × 𝑌) = (𝑥 · (𝑋 × 𝑌)) ↔ ((-𝑦 · 𝑋) × 𝑌) = (-𝑦 · (𝑋 × 𝑌)))) |
17 | | oveq1 7282 |
. . . . . . 7
⊢ (𝑥 = 𝑁 → (𝑥 · 𝑋) = (𝑁 · 𝑋)) |
18 | 17 | oveq1d 7290 |
. . . . . 6
⊢ (𝑥 = 𝑁 → ((𝑥 · 𝑋) × 𝑌) = ((𝑁 · 𝑋) × 𝑌)) |
19 | | oveq1 7282 |
. . . . . 6
⊢ (𝑥 = 𝑁 → (𝑥 · (𝑋 × 𝑌)) = (𝑁 · (𝑋 × 𝑌))) |
20 | 18, 19 | eqeq12d 2754 |
. . . . 5
⊢ (𝑥 = 𝑁 → (((𝑥 · 𝑋) × 𝑌) = (𝑥 · (𝑋 × 𝑌)) ↔ ((𝑁 · 𝑋) × 𝑌) = (𝑁 · (𝑋 × 𝑌)))) |
21 | | mulgass2.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝑅) |
22 | | mulgass2.t |
. . . . . . . 8
⊢ × =
(.r‘𝑅) |
23 | | eqid 2738 |
. . . . . . . 8
⊢
(0g‘𝑅) = (0g‘𝑅) |
24 | 21, 22, 23 | ringlz 19826 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵) → ((0g‘𝑅) × 𝑌) = (0g‘𝑅)) |
25 | 24 | 3adant3 1131 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → ((0g‘𝑅) × 𝑌) = (0g‘𝑅)) |
26 | | simp3 1137 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → 𝑋 ∈ 𝐵) |
27 | | mulgass2.m |
. . . . . . . . 9
⊢ · =
(.g‘𝑅) |
28 | 21, 23, 27 | mulg0 18707 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝐵 → (0 · 𝑋) = (0g‘𝑅)) |
29 | 26, 28 | syl 17 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → (0 · 𝑋) = (0g‘𝑅)) |
30 | 29 | oveq1d 7290 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → ((0 · 𝑋) × 𝑌) = ((0g‘𝑅) × 𝑌)) |
31 | 21, 22 | ringcl 19800 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 × 𝑌) ∈ 𝐵) |
32 | 31 | 3com23 1125 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → (𝑋 × 𝑌) ∈ 𝐵) |
33 | 21, 23, 27 | mulg0 18707 |
. . . . . . 7
⊢ ((𝑋 × 𝑌) ∈ 𝐵 → (0 · (𝑋 × 𝑌)) = (0g‘𝑅)) |
34 | 32, 33 | syl 17 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → (0 · (𝑋 × 𝑌)) = (0g‘𝑅)) |
35 | 25, 30, 34 | 3eqtr4d 2788 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → ((0 · 𝑋) × 𝑌) = (0 · (𝑋 × 𝑌))) |
36 | | oveq1 7282 |
. . . . . . 7
⊢ (((𝑦 · 𝑋) × 𝑌) = (𝑦 · (𝑋 × 𝑌)) → (((𝑦 · 𝑋) × 𝑌)(+g‘𝑅)(𝑋 × 𝑌)) = ((𝑦 · (𝑋 × 𝑌))(+g‘𝑅)(𝑋 × 𝑌))) |
37 | | simpl1 1190 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑦 ∈ ℕ0) → 𝑅 ∈ Ring) |
38 | | ringgrp 19788 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) |
39 | 37, 38 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑦 ∈ ℕ0) → 𝑅 ∈ Grp) |
40 | | nn0z 12343 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ0
→ 𝑦 ∈
ℤ) |
41 | 40 | adantl 482 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑦 ∈ ℕ0) → 𝑦 ∈
ℤ) |
42 | 26 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑦 ∈ ℕ0) → 𝑋 ∈ 𝐵) |
43 | | eqid 2738 |
. . . . . . . . . . . 12
⊢
(+g‘𝑅) = (+g‘𝑅) |
44 | 21, 27, 43 | mulgp1 18736 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → ((𝑦 + 1) · 𝑋) = ((𝑦 · 𝑋)(+g‘𝑅)𝑋)) |
45 | 39, 41, 42, 44 | syl3anc 1370 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑦 ∈ ℕ0) → ((𝑦 + 1) · 𝑋) = ((𝑦 · 𝑋)(+g‘𝑅)𝑋)) |
46 | 45 | oveq1d 7290 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑦 ∈ ℕ0) → (((𝑦 + 1) · 𝑋) × 𝑌) = (((𝑦 · 𝑋)(+g‘𝑅)𝑋) × 𝑌)) |
47 | 38 | 3ad2ant1 1132 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → 𝑅 ∈ Grp) |
48 | 47 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑦 ∈ ℕ0) → 𝑅 ∈ Grp) |
49 | 21, 27 | mulgcl 18721 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (𝑦 · 𝑋) ∈ 𝐵) |
50 | 48, 41, 42, 49 | syl3anc 1370 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑦 ∈ ℕ0) → (𝑦 · 𝑋) ∈ 𝐵) |
51 | | simpl2 1191 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑦 ∈ ℕ0) → 𝑌 ∈ 𝐵) |
52 | 21, 43, 22 | ringdir 19806 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ ((𝑦 · 𝑋) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (((𝑦 · 𝑋)(+g‘𝑅)𝑋) × 𝑌) = (((𝑦 · 𝑋) × 𝑌)(+g‘𝑅)(𝑋 × 𝑌))) |
53 | 37, 50, 42, 51, 52 | syl13anc 1371 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑦 ∈ ℕ0) → (((𝑦 · 𝑋)(+g‘𝑅)𝑋) × 𝑌) = (((𝑦 · 𝑋) × 𝑌)(+g‘𝑅)(𝑋 × 𝑌))) |
54 | 46, 53 | eqtrd 2778 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑦 ∈ ℕ0) → (((𝑦 + 1) · 𝑋) × 𝑌) = (((𝑦 · 𝑋) × 𝑌)(+g‘𝑅)(𝑋 × 𝑌))) |
55 | 32 | adantr 481 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑦 ∈ ℕ0) → (𝑋 × 𝑌) ∈ 𝐵) |
56 | 21, 27, 43 | mulgp1 18736 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ (𝑋 × 𝑌) ∈ 𝐵) → ((𝑦 + 1) · (𝑋 × 𝑌)) = ((𝑦 · (𝑋 × 𝑌))(+g‘𝑅)(𝑋 × 𝑌))) |
57 | 39, 41, 55, 56 | syl3anc 1370 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑦 ∈ ℕ0) → ((𝑦 + 1) · (𝑋 × 𝑌)) = ((𝑦 · (𝑋 × 𝑌))(+g‘𝑅)(𝑋 × 𝑌))) |
58 | 54, 57 | eqeq12d 2754 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑦 ∈ ℕ0) → ((((𝑦 + 1) · 𝑋) × 𝑌) = ((𝑦 + 1) · (𝑋 × 𝑌)) ↔ (((𝑦 · 𝑋) × 𝑌)(+g‘𝑅)(𝑋 × 𝑌)) = ((𝑦 · (𝑋 × 𝑌))(+g‘𝑅)(𝑋 × 𝑌)))) |
59 | 36, 58 | syl5ibr 245 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑦 ∈ ℕ0) → (((𝑦 · 𝑋) × 𝑌) = (𝑦 · (𝑋 × 𝑌)) → (((𝑦 + 1) · 𝑋) × 𝑌) = ((𝑦 + 1) · (𝑋 × 𝑌)))) |
60 | 59 | ex 413 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → (𝑦 ∈ ℕ0 → (((𝑦 · 𝑋) × 𝑌) = (𝑦 · (𝑋 × 𝑌)) → (((𝑦 + 1) · 𝑋) × 𝑌) = ((𝑦 + 1) · (𝑋 × 𝑌))))) |
61 | | fveq2 6774 |
. . . . . . 7
⊢ (((𝑦 · 𝑋) × 𝑌) = (𝑦 · (𝑋 × 𝑌)) → ((invg‘𝑅)‘((𝑦 · 𝑋) × 𝑌)) = ((invg‘𝑅)‘(𝑦 · (𝑋 × 𝑌)))) |
62 | 47 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑦 ∈ ℕ) → 𝑅 ∈ Grp) |
63 | | nnz 12342 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℤ) |
64 | 63 | adantl 482 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈ ℤ) |
65 | 26 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑦 ∈ ℕ) → 𝑋 ∈ 𝐵) |
66 | | eqid 2738 |
. . . . . . . . . . . 12
⊢
(invg‘𝑅) = (invg‘𝑅) |
67 | 21, 27, 66 | mulgneg 18722 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (-𝑦 · 𝑋) = ((invg‘𝑅)‘(𝑦 · 𝑋))) |
68 | 62, 64, 65, 67 | syl3anc 1370 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑦 ∈ ℕ) → (-𝑦 · 𝑋) = ((invg‘𝑅)‘(𝑦 · 𝑋))) |
69 | 68 | oveq1d 7290 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑦 ∈ ℕ) → ((-𝑦 · 𝑋) × 𝑌) = (((invg‘𝑅)‘(𝑦 · 𝑋)) × 𝑌)) |
70 | | simpl1 1190 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑦 ∈ ℕ) → 𝑅 ∈ Ring) |
71 | 62, 64, 65, 49 | syl3anc 1370 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑦 ∈ ℕ) → (𝑦 · 𝑋) ∈ 𝐵) |
72 | | simpl2 1191 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑦 ∈ ℕ) → 𝑌 ∈ 𝐵) |
73 | 21, 22, 66, 70, 71, 72 | ringmneg1 19835 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑦 ∈ ℕ) →
(((invg‘𝑅)‘(𝑦 · 𝑋)) × 𝑌) = ((invg‘𝑅)‘((𝑦 · 𝑋) × 𝑌))) |
74 | 69, 73 | eqtrd 2778 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑦 ∈ ℕ) → ((-𝑦 · 𝑋) × 𝑌) = ((invg‘𝑅)‘((𝑦 · 𝑋) × 𝑌))) |
75 | 32 | adantr 481 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑦 ∈ ℕ) → (𝑋 × 𝑌) ∈ 𝐵) |
76 | 21, 27, 66 | mulgneg 18722 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ (𝑋 × 𝑌) ∈ 𝐵) → (-𝑦 · (𝑋 × 𝑌)) = ((invg‘𝑅)‘(𝑦 · (𝑋 × 𝑌)))) |
77 | 62, 64, 75, 76 | syl3anc 1370 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑦 ∈ ℕ) → (-𝑦 · (𝑋 × 𝑌)) = ((invg‘𝑅)‘(𝑦 · (𝑋 × 𝑌)))) |
78 | 74, 77 | eqeq12d 2754 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑦 ∈ ℕ) → (((-𝑦 · 𝑋) × 𝑌) = (-𝑦 · (𝑋 × 𝑌)) ↔ ((invg‘𝑅)‘((𝑦 · 𝑋) × 𝑌)) = ((invg‘𝑅)‘(𝑦 · (𝑋 × 𝑌))))) |
79 | 61, 78 | syl5ibr 245 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑦 ∈ ℕ) → (((𝑦 · 𝑋) × 𝑌) = (𝑦 · (𝑋 × 𝑌)) → ((-𝑦 · 𝑋) × 𝑌) = (-𝑦 · (𝑋 × 𝑌)))) |
80 | 79 | ex 413 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → (𝑦 ∈ ℕ → (((𝑦 · 𝑋) × 𝑌) = (𝑦 · (𝑋 × 𝑌)) → ((-𝑦 · 𝑋) × 𝑌) = (-𝑦 · (𝑋 × 𝑌))))) |
81 | 4, 8, 12, 16, 20, 35, 60, 80 | zindd 12421 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → (𝑁 ∈ ℤ → ((𝑁 · 𝑋) × 𝑌) = (𝑁 · (𝑋 × 𝑌)))) |
82 | 81 | 3exp 1118 |
. . 3
⊢ (𝑅 ∈ Ring → (𝑌 ∈ 𝐵 → (𝑋 ∈ 𝐵 → (𝑁 ∈ ℤ → ((𝑁 · 𝑋) × 𝑌) = (𝑁 · (𝑋 × 𝑌)))))) |
83 | 82 | com24 95 |
. 2
⊢ (𝑅 ∈ Ring → (𝑁 ∈ ℤ → (𝑋 ∈ 𝐵 → (𝑌 ∈ 𝐵 → ((𝑁 · 𝑋) × 𝑌) = (𝑁 · (𝑋 × 𝑌)))))) |
84 | 83 | 3imp2 1348 |
1
⊢ ((𝑅 ∈ Ring ∧ (𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((𝑁 · 𝑋) × 𝑌) = (𝑁 · (𝑋 × 𝑌))) |