Metamath Proof Explorer

Theorem signswmnd

Description: W is a monoid structure on { -u 1 , 0 , 1 } which operation retains the right side, but skips zeroes. This will be used for skipping zeroes when counting sign changes. (Contributed by Thierry Arnoux, 9-Sep-2018)

Ref Expression
Hypotheses signsw.p ⊢ ⨣ ˙ = a ∈ − 1 0 1 , b ∈ − 1 0 1 ⟼ if b = 0 a b
signsw.w ⊢ W = Base ndx − 1 0 1 + ndx ⨣ ˙
Assertion signswmnd ⊢ W ∈ Mnd

Proof

Step Hyp Ref Expression
1 signsw.p ⊢ ⨣ ˙ = a ∈ − 1 0 1 , b ∈ − 1 0 1 ⟼ if b = 0 a b
2 signsw.w ⊢ W = Base ndx − 1 0 1 + ndx ⨣ ˙
3 1 signspval ⊢ u ∈ − 1 0 1 ∧ v ∈ − 1 0 1 → u ⨣ ˙ v = if v = 0 u v
4 ifcl ⊢ u ∈ − 1 0 1 ∧ v ∈ − 1 0 1 → if v = 0 u v ∈ − 1 0 1
5 3 4 eqeltrd ⊢ u ∈ − 1 0 1 ∧ v ∈ − 1 0 1 → u ⨣ ˙ v ∈ − 1 0 1
6 1 signspval ⊢ u ⨣ ˙ v ∈ − 1 0 1 ∧ w ∈ − 1 0 1 → u ⨣ ˙ v ⨣ ˙ w = if w = 0 u ⨣ ˙ v w
7 5 6 stoic3 ⊢ u ∈ − 1 0 1 ∧ v ∈ − 1 0 1 ∧ w ∈ − 1 0 1 → u ⨣ ˙ v ⨣ ˙ w = if w = 0 u ⨣ ˙ v w
8 iftrue ⊢ w = 0 → if w = 0 u ⨣ ˙ v w = u ⨣ ˙ v
9 7 8 sylan9eq ⊢ u ∈ − 1 0 1 ∧ v ∈ − 1 0 1 ∧ w ∈ − 1 0 1 ∧ w = 0 → u ⨣ ˙ v ⨣ ˙ w = u ⨣ ˙ v
10 9 adantr ⊢ u ∈ − 1 0 1 ∧ v ∈ − 1 0 1 ∧ w ∈ − 1 0 1 ∧ w = 0 ∧ v = 0 → u ⨣ ˙ v ⨣ ˙ w = u ⨣ ˙ v
11 3 3adant3 ⊢ u ∈ − 1 0 1 ∧ v ∈ − 1 0 1 ∧ w ∈ − 1 0 1 → u ⨣ ˙ v = if v = 0 u v
12 11 ad2antrr ⊢ u ∈ − 1 0 1 ∧ v ∈ − 1 0 1 ∧ w ∈ − 1 0 1 ∧ w = 0 ∧ v = 0 → u ⨣ ˙ v = if v = 0 u v
13 iftrue ⊢ v = 0 → if v = 0 u v = u
14 13 adantl ⊢ u ∈ − 1 0 1 ∧ v ∈ − 1 0 1 ∧ w ∈ − 1 0 1 ∧ w = 0 ∧ v = 0 → if v = 0 u v = u
15 10 12 14 3eqtrd ⊢ u ∈ − 1 0 1 ∧ v ∈ − 1 0 1 ∧ w ∈ − 1 0 1 ∧ w = 0 ∧ v = 0 → u ⨣ ˙ v ⨣ ˙ w = u
16 simp1 ⊢ u ∈ − 1 0 1 ∧ v ∈ − 1 0 1 ∧ w ∈ − 1 0 1 → u ∈ − 1 0 1
17 1 signspval ⊢ v ∈ − 1 0 1 ∧ w ∈ − 1 0 1 → v ⨣ ˙ w = if w = 0 v w
18 17 3adant1 ⊢ u ∈ − 1 0 1 ∧ v ∈ − 1 0 1 ∧ w ∈ − 1 0 1 → v ⨣ ˙ w = if w = 0 v w
19 simpl2 ⊢ u ∈ − 1 0 1 ∧ v ∈ − 1 0 1 ∧ w ∈ − 1 0 1 ∧ w = 0 → v ∈ − 1 0 1
20 simpl3 ⊢ u ∈ − 1 0 1 ∧ v ∈ − 1 0 1 ∧ w ∈ − 1 0 1 ∧ ¬ w = 0 → w ∈ − 1 0 1
21 19 20 ifclda ⊢ u ∈ − 1 0 1 ∧ v ∈ − 1 0 1 ∧ w ∈ − 1 0 1 → if w = 0 v w ∈ − 1 0 1
22 18 21 eqeltrd ⊢ u ∈ − 1 0 1 ∧ v ∈ − 1 0 1 ∧ w ∈ − 1 0 1 → v ⨣ ˙ w ∈ − 1 0 1
23 1 signspval ⊢ u ∈ − 1 0 1 ∧ v ⨣ ˙ w ∈ − 1 0 1 → u ⨣ ˙ v ⨣ ˙ w = if v ⨣ ˙ w = 0 u v ⨣ ˙ w
24 16 22 23 syl2anc ⊢ u ∈ − 1 0 1 ∧ v ∈ − 1 0 1 ∧ w ∈ − 1 0 1 → u ⨣ ˙ v ⨣ ˙ w = if v ⨣ ˙ w = 0 u v ⨣ ˙ w
25 24 ad2antrr ⊢ u ∈ − 1 0 1 ∧ v ∈ − 1 0 1 ∧ w ∈ − 1 0 1 ∧ w = 0 ∧ v = 0 → u ⨣ ˙ v ⨣ ˙ w = if v ⨣ ˙ w = 0 u v ⨣ ˙ w
26 iftrue ⊢ w = 0 → if w = 0 v w = v
27 18 26 sylan9eq ⊢ u ∈ − 1 0 1 ∧ v ∈ − 1 0 1 ∧ w ∈ − 1 0 1 ∧ w = 0 → v ⨣ ˙ w = v
28 id ⊢ v = 0 → v = 0
29 27 28 sylan9eq ⊢ u ∈ − 1 0 1 ∧ v ∈ − 1 0 1 ∧ w ∈ − 1 0 1 ∧ w = 0 ∧ v = 0 → v ⨣ ˙ w = 0
30 29 iftrued ⊢ u ∈ − 1 0 1 ∧ v ∈ − 1 0 1 ∧ w ∈ − 1 0 1 ∧ w = 0 ∧ v = 0 → if v ⨣ ˙ w = 0 u v ⨣ ˙ w = u
31 25 30 eqtrd ⊢ u ∈ − 1 0 1 ∧ v ∈ − 1 0 1 ∧ w ∈ − 1 0 1 ∧ w = 0 ∧ v = 0 → u ⨣ ˙ v ⨣ ˙ w = u
32 15 31 eqtr4d ⊢ u ∈ − 1 0 1 ∧ v ∈ − 1 0 1 ∧ w ∈ − 1 0 1 ∧ w = 0 ∧ v = 0 → u ⨣ ˙ v ⨣ ˙ w = u ⨣ ˙ v ⨣ ˙ w
33 7 ad2antrr ⊢ u ∈ − 1 0 1 ∧ v ∈ − 1 0 1 ∧ w ∈ − 1 0 1 ∧ w = 0 ∧ ¬ v = 0 → u ⨣ ˙ v ⨣ ˙ w = if w = 0 u ⨣ ˙ v w
34 8 ad2antlr ⊢ u ∈ − 1 0 1 ∧ v ∈ − 1 0 1 ∧ w ∈ − 1 0 1 ∧ w = 0 ∧ ¬ v = 0 → if w = 0 u ⨣ ˙ v w = u ⨣ ˙ v
35 11 ad2antrr ⊢ u ∈ − 1 0 1 ∧ v ∈ − 1 0 1 ∧ w ∈ − 1 0 1 ∧ w = 0 ∧ ¬ v = 0 → u ⨣ ˙ v = if v = 0 u v
36 iffalse ⊢ ¬ v = 0 → if v = 0 u v = v
37 36 adantl ⊢ u ∈ − 1 0 1 ∧ v ∈ − 1 0 1 ∧ w ∈ − 1 0 1 ∧ w = 0 ∧ ¬ v = 0 → if v = 0 u v = v
38 35 37 eqtrd ⊢ u ∈ − 1 0 1 ∧ v ∈ − 1 0 1 ∧ w ∈ − 1 0 1 ∧ w = 0 ∧ ¬ v = 0 → u ⨣ ˙ v = v
39 33 34 38 3eqtrd ⊢ u ∈ − 1 0 1 ∧ v ∈ − 1 0 1 ∧ w ∈ − 1 0 1 ∧ w = 0 ∧ ¬ v = 0 → u ⨣ ˙ v ⨣ ˙ w = v
40 24 ad2antrr ⊢ u ∈ − 1 0 1 ∧ v ∈ − 1 0 1 ∧ w ∈ − 1 0 1 ∧ w = 0 ∧ ¬ v = 0 → u ⨣ ˙ v ⨣ ˙ w = if v ⨣ ˙ w = 0 u v ⨣ ˙ w
41 simpr ⊢ u ∈ − 1 0 1 ∧ v ∈ − 1 0 1 ∧ w ∈ − 1 0 1 ∧ w = 0 ∧ ¬ v = 0 → ¬ v = 0
42 18 ad2antrr ⊢ u ∈ − 1 0 1 ∧ v ∈ − 1 0 1 ∧ w ∈ − 1 0 1 ∧ w = 0 ∧ ¬ v = 0 → v ⨣ ˙ w = if w = 0 v w
43 26 ad2antlr ⊢ u ∈ − 1 0 1 ∧ v ∈ − 1 0 1 ∧ w ∈ − 1 0 1 ∧ w = 0 ∧ ¬ v = 0 → if w = 0 v w = v
44 42 43 eqtrd ⊢ u ∈ − 1 0 1 ∧ v ∈ − 1 0 1 ∧ w ∈ − 1 0 1 ∧ w = 0 ∧ ¬ v = 0 → v ⨣ ˙ w = v
45 44 eqeq1d ⊢ u ∈ − 1 0 1 ∧ v ∈ − 1 0 1 ∧ w ∈ − 1 0 1 ∧ w = 0 ∧ ¬ v = 0 → v ⨣ ˙ w = 0 ↔ v = 0
46 41 45 mtbird ⊢ u ∈ − 1 0 1 ∧ v ∈ − 1 0 1 ∧ w ∈ − 1 0 1 ∧ w = 0 ∧ ¬ v = 0 → ¬ v ⨣ ˙ w = 0
47 46 iffalsed ⊢ u ∈ − 1 0 1 ∧ v ∈ − 1 0 1 ∧ w ∈ − 1 0 1 ∧ w = 0 ∧ ¬ v = 0 → if v ⨣ ˙ w = 0 u v ⨣ ˙ w = v ⨣ ˙ w
48 40 47 44 3eqtrd ⊢ u ∈ − 1 0 1 ∧ v ∈ − 1 0 1 ∧ w ∈ − 1 0 1 ∧ w = 0 ∧ ¬ v = 0 → u ⨣ ˙ v ⨣ ˙ w = v
49 39 48 eqtr4d ⊢ u ∈ − 1 0 1 ∧ v ∈ − 1 0 1 ∧ w ∈ − 1 0 1 ∧ w = 0 ∧ ¬ v = 0 → u ⨣ ˙ v ⨣ ˙ w = u ⨣ ˙ v ⨣ ˙ w
50 32 49 pm2.61dan ⊢ u ∈ − 1 0 1 ∧ v ∈ − 1 0 1 ∧ w ∈ − 1 0 1 ∧ w = 0 → u ⨣ ˙ v ⨣ ˙ w = u ⨣ ˙ v ⨣ ˙ w
51 iffalse ⊢ ¬ w = 0 → if w = 0 u ⨣ ˙ v w = w
52 7 51 sylan9eq ⊢ u ∈ − 1 0 1 ∧ v ∈ − 1 0 1 ∧ w ∈ − 1 0 1 ∧ ¬ w = 0 → u ⨣ ˙ v ⨣ ˙ w = w
53 24 adantr ⊢ u ∈ − 1 0 1 ∧ v ∈ − 1 0 1 ∧ w ∈ − 1 0 1 ∧ ¬ w = 0 → u ⨣ ˙ v ⨣ ˙ w = if v ⨣ ˙ w = 0 u v ⨣ ˙ w
54 simpr ⊢ u ∈ − 1 0 1 ∧ v ∈ − 1 0 1 ∧ w ∈ − 1 0 1 ∧ ¬ w = 0 → ¬ w = 0
55 iffalse ⊢ ¬ w = 0 → if w = 0 v w = w
56 18 55 sylan9eq ⊢ u ∈ − 1 0 1 ∧ v ∈ − 1 0 1 ∧ w ∈ − 1 0 1 ∧ ¬ w = 0 → v ⨣ ˙ w = w
57 56 eqeq1d ⊢ u ∈ − 1 0 1 ∧ v ∈ − 1 0 1 ∧ w ∈ − 1 0 1 ∧ ¬ w = 0 → v ⨣ ˙ w = 0 ↔ w = 0
58 54 57 mtbird ⊢ u ∈ − 1 0 1 ∧ v ∈ − 1 0 1 ∧ w ∈ − 1 0 1 ∧ ¬ w = 0 → ¬ v ⨣ ˙ w = 0
59 58 iffalsed ⊢ u ∈ − 1 0 1 ∧ v ∈ − 1 0 1 ∧ w ∈ − 1 0 1 ∧ ¬ w = 0 → if v ⨣ ˙ w = 0 u v ⨣ ˙ w = v ⨣ ˙ w
60 53 59 56 3eqtrd ⊢ u ∈ − 1 0 1 ∧ v ∈ − 1 0 1 ∧ w ∈ − 1 0 1 ∧ ¬ w = 0 → u ⨣ ˙ v ⨣ ˙ w = w
61 52 60 eqtr4d ⊢ u ∈ − 1 0 1 ∧ v ∈ − 1 0 1 ∧ w ∈ − 1 0 1 ∧ ¬ w = 0 → u ⨣ ˙ v ⨣ ˙ w = u ⨣ ˙ v ⨣ ˙ w
62 50 61 pm2.61dan ⊢ u ∈ − 1 0 1 ∧ v ∈ − 1 0 1 ∧ w ∈ − 1 0 1 → u ⨣ ˙ v ⨣ ˙ w = u ⨣ ˙ v ⨣ ˙ w
63 62 3expa ⊢ u ∈ − 1 0 1 ∧ v ∈ − 1 0 1 ∧ w ∈ − 1 0 1 → u ⨣ ˙ v ⨣ ˙ w = u ⨣ ˙ v ⨣ ˙ w
64 63 ralrimiva ⊢ u ∈ − 1 0 1 ∧ v ∈ − 1 0 1 → ∀ w ∈ − 1 0 1 u ⨣ ˙ v ⨣ ˙ w = u ⨣ ˙ v ⨣ ˙ w
65 5 64 jca ⊢ u ∈ − 1 0 1 ∧ v ∈ − 1 0 1 → u ⨣ ˙ v ∈ − 1 0 1 ∧ ∀ w ∈ − 1 0 1 u ⨣ ˙ v ⨣ ˙ w = u ⨣ ˙ v ⨣ ˙ w
66 65 rgen2 ⊢ ∀ u ∈ − 1 0 1 ∀ v ∈ − 1 0 1 u ⨣ ˙ v ∈ − 1 0 1 ∧ ∀ w ∈ − 1 0 1 u ⨣ ˙ v ⨣ ˙ w = u ⨣ ˙ v ⨣ ˙ w
67 c0ex ⊢ 0 ∈ V
68 67 tpid2 ⊢ 0 ∈ − 1 0 1
69 1 signsw0glem ⊢ ∀ u ∈ − 1 0 1 0 ⨣ ˙ u = u ∧ u ⨣ ˙ 0 = u
70 oveq1 ⊢ e = 0 → e ⨣ ˙ u = 0 ⨣ ˙ u
71 70 eqeq1d ⊢ e = 0 → e ⨣ ˙ u = u ↔ 0 ⨣ ˙ u = u
72 71 ovanraleqv ⊢ e = 0 → ∀ u ∈ − 1 0 1 e ⨣ ˙ u = u ∧ u ⨣ ˙ e = u ↔ ∀ u ∈ − 1 0 1 0 ⨣ ˙ u = u ∧ u ⨣ ˙ 0 = u
73 72 rspcev ⊢ 0 ∈ − 1 0 1 ∧ ∀ u ∈ − 1 0 1 0 ⨣ ˙ u = u ∧ u ⨣ ˙ 0 = u → ∃ e ∈ − 1 0 1 ∀ u ∈ − 1 0 1 e ⨣ ˙ u = u ∧ u ⨣ ˙ e = u
74 68 69 73 mp2an ⊢ ∃ e ∈ − 1 0 1 ∀ u ∈ − 1 0 1 e ⨣ ˙ u = u ∧ u ⨣ ˙ e = u
75 1 2 signswbase ⊢ − 1 0 1 = Base W
76 1 2 signswplusg ⊢ ⨣ ˙ = + W
77 75 76 ismnd ⊢ W ∈ Mnd ↔ ∀ u ∈ − 1 0 1 ∀ v ∈ − 1 0 1 u ⨣ ˙ v ∈ − 1 0 1 ∧ ∀ w ∈ − 1 0 1 u ⨣ ˙ v ⨣ ˙ w = u ⨣ ˙ v ⨣ ˙ w ∧ ∃ e ∈ − 1 0 1 ∀ u ∈ − 1 0 1 e ⨣ ˙ u = u ∧ u ⨣ ˙ e = u
78 66 74 77 mpbir2an ⊢ W ∈ Mnd