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	⊢ ( ( 𝜑 ∧ ( 𝑀 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ) ) → ( 𝑀 · 𝑁 ) ∈ 𝑇 )