Theorem un0mulcl 9530

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

Hypotheses

Ref	Expression
un0addcl.1	⊢ (𝜑 → 𝑆 ⊆ ℂ)
un0addcl.2	⊢ 𝑇 = (𝑆 ∪ {0})
un0mulcl.3	⊢ ((𝜑 ∧ (𝑀 ∈ 𝑆 ∧ 𝑁 ∈ 𝑆)) → (𝑀 · 𝑁) ∈ 𝑆)

Assertion

Ref	Expression
un0mulcl	⊢ ((𝜑 ∧ (𝑀 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇)) → (𝑀 · 𝑁) ∈ 𝑇)

Proof of Theorem un0mulcl

Step	Hyp	Ref	Expression
1		un0addcl.2	. . . . 5 ⊢ 𝑇 = (𝑆 ∪ {0})
2	1	eleq2i 2299	. . . 4 ⊢ (𝑁 ∈ 𝑇 ↔ 𝑁 ∈ (𝑆 ∪ {0}))
3		elun 3360	. . . 4 ⊢ (𝑁 ∈ (𝑆 ∪ {0}) ↔ (𝑁 ∈ 𝑆 ∨ 𝑁 ∈ {0}))
4	2, 3	bitri 184	. . 3 ⊢ (𝑁 ∈ 𝑇 ↔ (𝑁 ∈ 𝑆 ∨ 𝑁 ∈ {0}))
5	1	eleq2i 2299	. . . . . 6 ⊢ (𝑀 ∈ 𝑇 ↔ 𝑀 ∈ (𝑆 ∪ {0}))
6		elun 3360	. . . . . 6 ⊢ (𝑀 ∈ (𝑆 ∪ {0}) ↔ (𝑀 ∈ 𝑆 ∨ 𝑀 ∈ {0}))
7	5, 6	bitri 184	. . . . 5 ⊢ (𝑀 ∈ 𝑇 ↔ (𝑀 ∈ 𝑆 ∨ 𝑀 ∈ {0}))
8		ssun1 3382	. . . . . . . . 9 ⊢ 𝑆 ⊆ (𝑆 ∪ {0})
9	8, 1	sseqtrri 3273	. . . . . . . 8 ⊢ 𝑆 ⊆ 𝑇
10		un0mulcl.3	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑀 ∈ 𝑆 ∧ 𝑁 ∈ 𝑆)) → (𝑀 · 𝑁) ∈ 𝑆)
11	9, 10	sselid 3236	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑀 ∈ 𝑆 ∧ 𝑁 ∈ 𝑆)) → (𝑀 · 𝑁) ∈ 𝑇)
12	11	expr 375	. . . . . 6 ⊢ ((𝜑 ∧ 𝑀 ∈ 𝑆) → (𝑁 ∈ 𝑆 → (𝑀 · 𝑁) ∈ 𝑇))
13		un0addcl.1	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆 ⊆ ℂ)
14	13	sselda 3238	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑆) → 𝑁 ∈ ℂ)
15	14	mul02d 8665	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑆) → (0 · 𝑁) = 0)
16		ssun2 3383	. . . . . . . . . . 11 ⊢ {0} ⊆ (𝑆 ∪ {0})
17	16, 1	sseqtrri 3273	. . . . . . . . . 10 ⊢ {0} ⊆ 𝑇
18		c0ex 8268	. . . . . . . . . . 11 ⊢ 0 ∈ V
19	18	snss 3829	. . . . . . . . . 10 ⊢ (0 ∈ 𝑇 ↔ {0} ⊆ 𝑇)
20	17, 19	mpbir 146	. . . . . . . . 9 ⊢ 0 ∈ 𝑇
21	15, 20	eqeltrdi 2323	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑆) → (0 · 𝑁) ∈ 𝑇)
22		elsni 3707	. . . . . . . . . 10 ⊢ (𝑀 ∈ {0} → 𝑀 = 0)
23	22	oveq1d 6065	. . . . . . . . 9 ⊢ (𝑀 ∈ {0} → (𝑀 · 𝑁) = (0 · 𝑁))
24	23	eleq1d 2301	. . . . . . . 8 ⊢ (𝑀 ∈ {0} → ((𝑀 · 𝑁) ∈ 𝑇 ↔ (0 · 𝑁) ∈ 𝑇))
25	21, 24	syl5ibrcom 157	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑆) → (𝑀 ∈ {0} → (𝑀 · 𝑁) ∈ 𝑇))
26	25	impancom 260	. . . . . 6 ⊢ ((𝜑 ∧ 𝑀 ∈ {0}) → (𝑁 ∈ 𝑆 → (𝑀 · 𝑁) ∈ 𝑇))
27	12, 26	jaodan 805	. . . . 5 ⊢ ((𝜑 ∧ (𝑀 ∈ 𝑆 ∨ 𝑀 ∈ {0})) → (𝑁 ∈ 𝑆 → (𝑀 · 𝑁) ∈ 𝑇))
28	7, 27	sylan2b 287	. . . 4 ⊢ ((𝜑 ∧ 𝑀 ∈ 𝑇) → (𝑁 ∈ 𝑆 → (𝑀 · 𝑁) ∈ 𝑇))
29		0cnd 8267	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ∈ ℂ)
30	29	snssd 3839	. . . . . . . . . 10 ⊢ (𝜑 → {0} ⊆ ℂ)
31	13, 30	unssd 3395	. . . . . . . . 9 ⊢ (𝜑 → (𝑆 ∪ {0}) ⊆ ℂ)
32	1, 31	eqsstrid 3284	. . . . . . . 8 ⊢ (𝜑 → 𝑇 ⊆ ℂ)
33	32	sselda 3238	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑀 ∈ 𝑇) → 𝑀 ∈ ℂ)
34	33	mul01d 8666	. . . . . 6 ⊢ ((𝜑 ∧ 𝑀 ∈ 𝑇) → (𝑀 · 0) = 0)
35	34, 20	eqeltrdi 2323	. . . . 5 ⊢ ((𝜑 ∧ 𝑀 ∈ 𝑇) → (𝑀 · 0) ∈ 𝑇)
36		elsni 3707	. . . . . . 7 ⊢ (𝑁 ∈ {0} → 𝑁 = 0)
37	36	oveq2d 6066	. . . . . 6 ⊢ (𝑁 ∈ {0} → (𝑀 · 𝑁) = (𝑀 · 0))
38	37	eleq1d 2301	. . . . 5 ⊢ (𝑁 ∈ {0} → ((𝑀 · 𝑁) ∈ 𝑇 ↔ (𝑀 · 0) ∈ 𝑇))
39	35, 38	syl5ibrcom 157	. . . 4 ⊢ ((𝜑 ∧ 𝑀 ∈ 𝑇) → (𝑁 ∈ {0} → (𝑀 · 𝑁) ∈ 𝑇))
40	28, 39	jaod 725	. . 3 ⊢ ((𝜑 ∧ 𝑀 ∈ 𝑇) → ((𝑁 ∈ 𝑆 ∨ 𝑁 ∈ {0}) → (𝑀 · 𝑁) ∈ 𝑇))
41	4, 40	biimtrid 152	. 2 ⊢ ((𝜑 ∧ 𝑀 ∈ 𝑇) → (𝑁 ∈ 𝑇 → (𝑀 · 𝑁) ∈ 𝑇))
42	41	impr 379	1 ⊢ ((𝜑 ∧ (𝑀 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇)) → (𝑀 · 𝑁) ∈ 𝑇)

Syntax hints:   → wi 4   ∧ wa 104   ∨ wo 716   = wceq 1398   ∈ wcel 2203   ∪ cun 3209   ⊆ wss 3211  {csn 3689  (class class class)co 6050  ℂcc 8125  0cc0 8127   · cmul 8132

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-14 2206  ax-ext 2214  ax-sep 4228  ax-pow 4287  ax-pr 4322  ax-setind 4659  ax-resscn 8219  ax-1cn 8220  ax-icn 8222  ax-addcl 8223  ax-addrcl 8224  ax-mulcl 8225  ax-addcom 8227  ax-mulcom 8228  ax-addass 8229  ax-distr 8231  ax-i2m1 8232  ax-0id 8235  ax-rnegex 8236  ax-cnre 8238

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-fal 1404  df-nf 1510  df-sb 1812  df-eu 2083  df-mo 2084  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ne 2413  df-ral 2525  df-rex 2526  df-reu 2527  df-rab 2529  df-v 2815  df-sbc 3043  df-dif 3213  df-un 3215  df-in 3217  df-ss 3224  df-pw 3671  df-sn 3695  df-pr 3696  df-op 3698  df-uni 3915  df-br 4110  df-opab 4172  df-id 4414  df-xp 4755  df-rel 4756  df-cnv 4757  df-co 4758  df-dm 4759  df-iota 5312  df-fun 5354  df-fv 5360  df-riota 6003  df-ov 6053  df-oprab 6054  df-mpo 6055  df-sub 8446

This theorem is referenced by:  nn0mulcl  9532  plymullem  15615