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 biimtrid ⊢φ∧M∈T→N∈T→ M⋅ N∈T
42 41 impr ⊢φ∧M∈T∧N∈T→ M⋅ N∈T