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∈−101,b∈−101⟼ifb=0ab
signsw.w ⊢W=Basendx−101+ndx⨣˙
Assertion signswmnd ⊢W∈Mnd

Proof

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