Proof of Theorem un0mulcl
Step | Hyp | Ref
| Expression |
1 | | un0addcl.2 |
. . . . 5
⊢ 𝑇 = (𝑆 ∪ {0}) |
2 | 1 | eleq2i 2237 |
. . . 4
⊢ (𝑁 ∈ 𝑇 ↔ 𝑁 ∈ (𝑆 ∪ {0})) |
3 | | elun 3268 |
. . . 4
⊢ (𝑁 ∈ (𝑆 ∪ {0}) ↔ (𝑁 ∈ 𝑆 ∨ 𝑁 ∈ {0})) |
4 | 2, 3 | bitri 183 |
. . 3
⊢ (𝑁 ∈ 𝑇 ↔ (𝑁 ∈ 𝑆 ∨ 𝑁 ∈ {0})) |
5 | 1 | eleq2i 2237 |
. . . . . 6
⊢ (𝑀 ∈ 𝑇 ↔ 𝑀 ∈ (𝑆 ∪ {0})) |
6 | | elun 3268 |
. . . . . 6
⊢ (𝑀 ∈ (𝑆 ∪ {0}) ↔ (𝑀 ∈ 𝑆 ∨ 𝑀 ∈ {0})) |
7 | 5, 6 | bitri 183 |
. . . . 5
⊢ (𝑀 ∈ 𝑇 ↔ (𝑀 ∈ 𝑆 ∨ 𝑀 ∈ {0})) |
8 | | ssun1 3290 |
. . . . . . . . 9
⊢ 𝑆 ⊆ (𝑆 ∪ {0}) |
9 | 8, 1 | sseqtrri 3182 |
. . . . . . . 8
⊢ 𝑆 ⊆ 𝑇 |
10 | | un0mulcl.3 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑀 ∈ 𝑆 ∧ 𝑁 ∈ 𝑆)) → (𝑀 · 𝑁) ∈ 𝑆) |
11 | 9, 10 | sselid 3145 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑀 ∈ 𝑆 ∧ 𝑁 ∈ 𝑆)) → (𝑀 · 𝑁) ∈ 𝑇) |
12 | 11 | expr 373 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑀 ∈ 𝑆) → (𝑁 ∈ 𝑆 → (𝑀 · 𝑁) ∈ 𝑇)) |
13 | | un0addcl.1 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑆 ⊆ ℂ) |
14 | 13 | sselda 3147 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑆) → 𝑁 ∈ ℂ) |
15 | 14 | mul02d 8311 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑆) → (0 · 𝑁) = 0) |
16 | | ssun2 3291 |
. . . . . . . . . . 11
⊢ {0}
⊆ (𝑆 ∪
{0}) |
17 | 16, 1 | sseqtrri 3182 |
. . . . . . . . . 10
⊢ {0}
⊆ 𝑇 |
18 | | c0ex 7914 |
. . . . . . . . . . 11
⊢ 0 ∈
V |
19 | 18 | snss 3709 |
. . . . . . . . . 10
⊢ (0 ∈
𝑇 ↔ {0} ⊆ 𝑇) |
20 | 17, 19 | mpbir 145 |
. . . . . . . . 9
⊢ 0 ∈
𝑇 |
21 | 15, 20 | eqeltrdi 2261 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑆) → (0 · 𝑁) ∈ 𝑇) |
22 | | elsni 3601 |
. . . . . . . . . 10
⊢ (𝑀 ∈ {0} → 𝑀 = 0) |
23 | 22 | oveq1d 5868 |
. . . . . . . . 9
⊢ (𝑀 ∈ {0} → (𝑀 · 𝑁) = (0 · 𝑁)) |
24 | 23 | eleq1d 2239 |
. . . . . . . 8
⊢ (𝑀 ∈ {0} → ((𝑀 · 𝑁) ∈ 𝑇 ↔ (0 · 𝑁) ∈ 𝑇)) |
25 | 21, 24 | syl5ibrcom 156 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑆) → (𝑀 ∈ {0} → (𝑀 · 𝑁) ∈ 𝑇)) |
26 | 25 | impancom 258 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑀 ∈ {0}) → (𝑁 ∈ 𝑆 → (𝑀 · 𝑁) ∈ 𝑇)) |
27 | 12, 26 | jaodan 792 |
. . . . 5
⊢ ((𝜑 ∧ (𝑀 ∈ 𝑆 ∨ 𝑀 ∈ {0})) → (𝑁 ∈ 𝑆 → (𝑀 · 𝑁) ∈ 𝑇)) |
28 | 7, 27 | sylan2b 285 |
. . . 4
⊢ ((𝜑 ∧ 𝑀 ∈ 𝑇) → (𝑁 ∈ 𝑆 → (𝑀 · 𝑁) ∈ 𝑇)) |
29 | | 0cnd 7913 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ∈
ℂ) |
30 | 29 | snssd 3725 |
. . . . . . . . . 10
⊢ (𝜑 → {0} ⊆
ℂ) |
31 | 13, 30 | unssd 3303 |
. . . . . . . . 9
⊢ (𝜑 → (𝑆 ∪ {0}) ⊆
ℂ) |
32 | 1, 31 | eqsstrid 3193 |
. . . . . . . 8
⊢ (𝜑 → 𝑇 ⊆ ℂ) |
33 | 32 | sselda 3147 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑀 ∈ 𝑇) → 𝑀 ∈ ℂ) |
34 | 33 | mul01d 8312 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑀 ∈ 𝑇) → (𝑀 · 0) = 0) |
35 | 34, 20 | eqeltrdi 2261 |
. . . . 5
⊢ ((𝜑 ∧ 𝑀 ∈ 𝑇) → (𝑀 · 0) ∈ 𝑇) |
36 | | elsni 3601 |
. . . . . . 7
⊢ (𝑁 ∈ {0} → 𝑁 = 0) |
37 | 36 | oveq2d 5869 |
. . . . . 6
⊢ (𝑁 ∈ {0} → (𝑀 · 𝑁) = (𝑀 · 0)) |
38 | 37 | eleq1d 2239 |
. . . . 5
⊢ (𝑁 ∈ {0} → ((𝑀 · 𝑁) ∈ 𝑇 ↔ (𝑀 · 0) ∈ 𝑇)) |
39 | 35, 38 | syl5ibrcom 156 |
. . . 4
⊢ ((𝜑 ∧ 𝑀 ∈ 𝑇) → (𝑁 ∈ {0} → (𝑀 · 𝑁) ∈ 𝑇)) |
40 | 28, 39 | jaod 712 |
. . 3
⊢ ((𝜑 ∧ 𝑀 ∈ 𝑇) → ((𝑁 ∈ 𝑆 ∨ 𝑁 ∈ {0}) → (𝑀 · 𝑁) ∈ 𝑇)) |
41 | 4, 40 | syl5bi 151 |
. 2
⊢ ((𝜑 ∧ 𝑀 ∈ 𝑇) → (𝑁 ∈ 𝑇 → (𝑀 · 𝑁) ∈ 𝑇)) |
42 | 41 | impr 377 |
1
⊢ ((𝜑 ∧ (𝑀 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇)) → (𝑀 · 𝑁) ∈ 𝑇) |