This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
un0addcl.2 ⊢ 𝑇 = ( 𝑆 ∪ { 0 } )
un0mulcl.3 ⊢ ( ( 𝜑 ∧ ( 𝑀 ∈ 𝑆 ∧ 𝑁 ∈ 𝑆 ) ) → ( 𝑀 · 𝑁 ) ∈ 𝑆 )
Assertion un0mulcl ( ( 𝜑 ∧ ( 𝑀 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ) ) → ( 𝑀 · 𝑁 ) ∈ 𝑇 )

Proof

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