Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  signsw0glem Structured version   Visualization version   GIF version

Theorem signsw0glem 32044
 Description: Neutral element property of ⨣. (Contributed by Thierry Arnoux, 9-Sep-2018.)
Hypothesis
Ref Expression
signsw.p = (𝑎 ∈ {-1, 0, 1}, 𝑏 ∈ {-1, 0, 1} ↦ if(𝑏 = 0, 𝑎, 𝑏))
Assertion
Ref Expression
signsw0glem 𝑢 ∈ {-1, 0, 1} ((0 𝑢) = 𝑢 ∧ (𝑢 0) = 𝑢)
Distinct variable group:   𝑎,𝑏,𝑢
Allowed substitution hints:   (𝑢,𝑎,𝑏)

Proof of Theorem signsw0glem
StepHypRef Expression
1 c0ex 10666 . . . . . 6 0 ∈ V
21tpid2 4664 . . . . 5 0 ∈ {-1, 0, 1}
3 signsw.p . . . . . 6 = (𝑎 ∈ {-1, 0, 1}, 𝑏 ∈ {-1, 0, 1} ↦ if(𝑏 = 0, 𝑎, 𝑏))
43signspval 32043 . . . . 5 ((0 ∈ {-1, 0, 1} ∧ 𝑢 ∈ {-1, 0, 1}) → (0 𝑢) = if(𝑢 = 0, 0, 𝑢))
52, 4mpan 690 . . . 4 (𝑢 ∈ {-1, 0, 1} → (0 𝑢) = if(𝑢 = 0, 0, 𝑢))
6 iftrue 4427 . . . . . 6 (𝑢 = 0 → if(𝑢 = 0, 0, 𝑢) = 0)
7 id 22 . . . . . 6 (𝑢 = 0 → 𝑢 = 0)
86, 7eqtr4d 2797 . . . . 5 (𝑢 = 0 → if(𝑢 = 0, 0, 𝑢) = 𝑢)
9 iffalse 4430 . . . . 5 𝑢 = 0 → if(𝑢 = 0, 0, 𝑢) = 𝑢)
108, 9pm2.61i 185 . . . 4 if(𝑢 = 0, 0, 𝑢) = 𝑢
115, 10eqtrdi 2810 . . 3 (𝑢 ∈ {-1, 0, 1} → (0 𝑢) = 𝑢)
123signspval 32043 . . . . 5 ((𝑢 ∈ {-1, 0, 1} ∧ 0 ∈ {-1, 0, 1}) → (𝑢 0) = if(0 = 0, 𝑢, 0))
132, 12mpan2 691 . . . 4 (𝑢 ∈ {-1, 0, 1} → (𝑢 0) = if(0 = 0, 𝑢, 0))
14 eqid 2759 . . . . 5 0 = 0
1514iftruei 4428 . . . 4 if(0 = 0, 𝑢, 0) = 𝑢
1613, 15eqtrdi 2810 . . 3 (𝑢 ∈ {-1, 0, 1} → (𝑢 0) = 𝑢)
1711, 16jca 516 . 2 (𝑢 ∈ {-1, 0, 1} → ((0 𝑢) = 𝑢 ∧ (𝑢 0) = 𝑢))
1817rgen 3081 1 𝑢 ∈ {-1, 0, 1} ((0 𝑢) = 𝑢 ∧ (𝑢 0) = 𝑢)
 Colors of variables: wff setvar class Syntax hints:   ∧ wa 400   = wceq 1539   ∈ wcel 2112  ∀wral 3071  ifcif 4421  {ctp 4527  (class class class)co 7151   ∈ cmpo 7153  0cc0 10568  1c1 10569  -cneg 10902 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-sep 5170  ax-nul 5177  ax-pr 5299  ax-1cn 10626  ax-icn 10627  ax-addcl 10628  ax-mulcl 10630  ax-i2m1 10636 This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ral 3076  df-rex 3077  df-rab 3080  df-v 3412  df-sbc 3698  df-dif 3862  df-un 3864  df-in 3866  df-ss 3876  df-nul 4227  df-if 4422  df-sn 4524  df-pr 4526  df-tp 4528  df-op 4530  df-uni 4800  df-br 5034  df-opab 5096  df-id 5431  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-iota 6295  df-fun 6338  df-fv 6344  df-ov 7154  df-oprab 7155  df-mpo 7156 This theorem is referenced by:  signsw0g  32047  signswmnd  32048
 Copyright terms: Public domain W3C validator