ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  un0mulcl Structured version   GIF version

Theorem un0mulcl 7952
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
StepHypRef Expression
1 un0addcl.2 . . . . 5 𝑇 = (𝑆 ∪ {0})
21eleq2i 2101 . . . 4 (𝑁 𝑇𝑁 (𝑆 ∪ {0}))
3 elun 3078 . . . 4 (𝑁 (𝑆 ∪ {0}) ↔ (𝑁 𝑆 𝑁 {0}))
42, 3bitri 173 . . 3 (𝑁 𝑇 ↔ (𝑁 𝑆 𝑁 {0}))
51eleq2i 2101 . . . . . 6 (𝑀 𝑇𝑀 (𝑆 ∪ {0}))
6 elun 3078 . . . . . 6 (𝑀 (𝑆 ∪ {0}) ↔ (𝑀 𝑆 𝑀 {0}))
75, 6bitri 173 . . . . 5 (𝑀 𝑇 ↔ (𝑀 𝑆 𝑀 {0}))
8 ssun1 3100 . . . . . . . . 9 𝑆 ⊆ (𝑆 ∪ {0})
98, 1sseqtr4i 2972 . . . . . . . 8 𝑆𝑇
10 un0mulcl.3 . . . . . . . 8 ((φ (𝑀 𝑆 𝑁 𝑆)) → (𝑀 · 𝑁) 𝑆)
119, 10sseldi 2937 . . . . . . 7 ((φ (𝑀 𝑆 𝑁 𝑆)) → (𝑀 · 𝑁) 𝑇)
1211expr 357 . . . . . 6 ((φ 𝑀 𝑆) → (𝑁 𝑆 → (𝑀 · 𝑁) 𝑇))
13 un0addcl.1 . . . . . . . . . . 11 (φ𝑆 ⊆ ℂ)
1413sselda 2939 . . . . . . . . . 10 ((φ 𝑁 𝑆) → 𝑁 ℂ)
1514mul02d 7145 . . . . . . . . 9 ((φ 𝑁 𝑆) → (0 · 𝑁) = 0)
16 ssun2 3101 . . . . . . . . . . 11 {0} ⊆ (𝑆 ∪ {0})
1716, 1sseqtr4i 2972 . . . . . . . . . 10 {0} ⊆ 𝑇
18 c0ex 6779 . . . . . . . . . . 11 0 V
1918snss 3485 . . . . . . . . . 10 (0 𝑇 ↔ {0} ⊆ 𝑇)
2017, 19mpbir 134 . . . . . . . . 9 0 𝑇
2115, 20syl6eqel 2125 . . . . . . . 8 ((φ 𝑁 𝑆) → (0 · 𝑁) 𝑇)
22 elsni 3391 . . . . . . . . . 10 (𝑀 {0} → 𝑀 = 0)
2322oveq1d 5470 . . . . . . . . 9 (𝑀 {0} → (𝑀 · 𝑁) = (0 · 𝑁))
2423eleq1d 2103 . . . . . . . 8 (𝑀 {0} → ((𝑀 · 𝑁) 𝑇 ↔ (0 · 𝑁) 𝑇))
2521, 24syl5ibrcom 146 . . . . . . 7 ((φ 𝑁 𝑆) → (𝑀 {0} → (𝑀 · 𝑁) 𝑇))
2625impancom 247 . . . . . 6 ((φ 𝑀 {0}) → (𝑁 𝑆 → (𝑀 · 𝑁) 𝑇))
2712, 26jaodan 709 . . . . 5 ((φ (𝑀 𝑆 𝑀 {0})) → (𝑁 𝑆 → (𝑀 · 𝑁) 𝑇))
287, 27sylan2b 271 . . . 4 ((φ 𝑀 𝑇) → (𝑁 𝑆 → (𝑀 · 𝑁) 𝑇))
29 0cnd 6778 . . . . . . . . . . 11 (φ → 0 ℂ)
3029snssd 3500 . . . . . . . . . 10 (φ → {0} ⊆ ℂ)
3113, 30unssd 3113 . . . . . . . . 9 (φ → (𝑆 ∪ {0}) ⊆ ℂ)
321, 31syl5eqss 2983 . . . . . . . 8 (φ𝑇 ⊆ ℂ)
3332sselda 2939 . . . . . . 7 ((φ 𝑀 𝑇) → 𝑀 ℂ)
3433mul01d 7146 . . . . . 6 ((φ 𝑀 𝑇) → (𝑀 · 0) = 0)
3534, 20syl6eqel 2125 . . . . 5 ((φ 𝑀 𝑇) → (𝑀 · 0) 𝑇)
36 elsni 3391 . . . . . . 7 (𝑁 {0} → 𝑁 = 0)
3736oveq2d 5471 . . . . . 6 (𝑁 {0} → (𝑀 · 𝑁) = (𝑀 · 0))
3837eleq1d 2103 . . . . 5 (𝑁 {0} → ((𝑀 · 𝑁) 𝑇 ↔ (𝑀 · 0) 𝑇))
3935, 38syl5ibrcom 146 . . . 4 ((φ 𝑀 𝑇) → (𝑁 {0} → (𝑀 · 𝑁) 𝑇))
4028, 39jaod 636 . . 3 ((φ 𝑀 𝑇) → ((𝑁 𝑆 𝑁 {0}) → (𝑀 · 𝑁) 𝑇))
414, 40syl5bi 141 . 2 ((φ 𝑀 𝑇) → (𝑁 𝑇 → (𝑀 · 𝑁) 𝑇))
4241impr 361 1 ((φ (𝑀 𝑇 𝑁 𝑇)) → (𝑀 · 𝑁) 𝑇)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97   wo 628   = wceq 1242   wcel 1390  cun 2909  wss 2911  {csn 3367  (class class class)co 5455  cc 6669  0cc0 6671   · cmul 6676
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935  ax-setind 4220  ax-resscn 6735  ax-1cn 6736  ax-icn 6738  ax-addcl 6739  ax-addrcl 6740  ax-mulcl 6741  ax-addcom 6743  ax-mulcom 6744  ax-addass 6745  ax-distr 6747  ax-i2m1 6748  ax-0id 6751  ax-rnegex 6752  ax-cnre 6754
This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-fal 1248  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ne 2203  df-ral 2305  df-rex 2306  df-reu 2307  df-rab 2309  df-v 2553  df-sbc 2759  df-dif 2914  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-br 3756  df-opab 3810  df-id 4021  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-iota 4810  df-fun 4847  df-fv 4853  df-riota 5411  df-ov 5458  df-oprab 5459  df-mpt2 5460  df-sub 6941
This theorem is referenced by:  nn0mulcl  7954
  Copyright terms: Public domain W3C validator