Metamath Proof Explorer

Theorem un0mulcl

Description: If S is closed under multiplication, then so is S u. { 0 } . (Contributed by Mario Carneiro, 17-Jul-2014)

Ref Expression
Hypotheses un0addcl.1 ⊢ φ → S ⊆ ℂ
un0addcl.2 ⊢ T = S ∪ 0
un0mulcl.3 ⊢ φ ∧ M ∈ S ∧ N ∈ S → M ⋅ N ∈ S
Assertion un0mulcl ⊢ φ ∧ M ∈ T ∧ N ∈ T → M ⋅ N ∈ T

Proof

Step Hyp Ref Expression
1 un0addcl.1 ⊢ φ → S ⊆ ℂ
2 un0addcl.2 ⊢ T = S ∪ 0
3 un0mulcl.3 ⊢ φ ∧ M ∈ S ∧ N ∈ S → M ⋅ N ∈ S
4 2 eleq2i ⊢ N ∈ T ↔ N ∈ S ∪ 0
5 elun ⊢ N ∈ S ∪ 0 ↔ N ∈ S ∨ N ∈ 0
6 4 5 bitri ⊢ N ∈ T ↔ N ∈ S ∨ N ∈ 0
7 2 eleq2i ⊢ M ∈ T ↔ M ∈ S ∪ 0
8 elun ⊢ M ∈ S ∪ 0 ↔ M ∈ S ∨ M ∈ 0
9 7 8 bitri ⊢ M ∈ T ↔ M ∈ S ∨ M ∈ 0
10 ssun1 ⊢ S ⊆ S ∪ 0
11 10 2 sseqtrri ⊢ S ⊆ T
12 11 3 sselid ⊢ φ ∧ M ∈ S ∧ N ∈ S → M ⋅ N ∈ T
13 12 expr ⊢ φ ∧ M ∈ S → N ∈ S → M ⋅ N ∈ T
14 1 sselda ⊢ φ ∧ N ∈ S → N ∈ ℂ
15 14 mul02d ⊢ φ ∧ N ∈ S → 0 ⋅ N = 0
16 ssun2 ⊢ 0 ⊆ S ∪ 0
17 16 2 sseqtrri ⊢ 0 ⊆ T
18 c0ex ⊢ 0 ∈ V
19 18 snss ⊢ 0 ∈ T ↔ 0 ⊆ T
20 17 19 mpbir ⊢ 0 ∈ T
21 15 20 eqeltrdi ⊢ φ ∧ N ∈ S → 0 ⋅ N ∈ T
22 elsni ⊢ M ∈ 0 → M = 0
23 22 oveq1d ⊢ M ∈ 0 → M ⋅ N = 0 ⋅ N
24 23 eleq1d ⊢ M ∈ 0 → M ⋅ N ∈ T ↔ 0 ⋅ N ∈ T
25 21 24 syl5ibrcom ⊢ φ ∧ N ∈ S → M ∈ 0 → M ⋅ N ∈ T
26 25 impancom ⊢ φ ∧ M ∈ 0 → N ∈ S → M ⋅ N ∈ T
27 13 26 jaodan ⊢ φ ∧ M ∈ S ∨ M ∈ 0 → N ∈ S → M ⋅ N ∈ T
28 9 27 sylan2b ⊢ φ ∧ M ∈ T → N ∈ S → M ⋅ N ∈ T
29 0cnd ⊢ φ → 0 ∈ ℂ
30 29 snssd ⊢ φ → 0 ⊆ ℂ
31 1 30 unssd ⊢ φ → S ∪ 0 ⊆ ℂ
32 2 31 eqsstrid ⊢ φ → T ⊆ ℂ
33 32 sselda ⊢ φ ∧ M ∈ T → M ∈ ℂ
34 33 mul01d ⊢ φ ∧ M ∈ T → M ⋅ 0 = 0
35 34 20 eqeltrdi ⊢ φ ∧ M ∈ T → M ⋅ 0 ∈ T
36 elsni ⊢ N ∈ 0 → N = 0
37 36 oveq2d ⊢ N ∈ 0 → M ⋅ N = M ⋅ 0
38 37 eleq1d ⊢ N ∈ 0 → M ⋅ N ∈ T ↔ M ⋅ 0 ∈ T
39 35 38 syl5ibrcom ⊢ φ ∧ M ∈ T → N ∈ 0 → M ⋅ N ∈ T
40 28 39 jaod ⊢ φ ∧ M ∈ T → N ∈ S ∨ N ∈ 0 → M ⋅ N ∈ T
41 6 40 syl5bi ⊢ φ ∧ M ∈ T → N ∈ T → M ⋅ N ∈ T
42 41 impr ⊢ φ ∧ M ∈ T ∧ N ∈ T → M ⋅ N ∈ T