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 e. { -u 1 , 0 , 1 } , b e. { -u 1 , 0 , 1 } |-> if ( b = 0 , a , b ) )
signsw.w 
|- W = { <. ( Base ` ndx ) , { -u 1 , 0 , 1 } >. , <. ( +g ` ndx ) , .+^ >. }
Assertion signswmnd 
|- W e. Mnd

Proof

Step Hyp Ref Expression
1 signsw.p 
 |-  .+^ = ( a e. { -u 1 , 0 , 1 } , b e. { -u 1 , 0 , 1 } |-> if ( b = 0 , a , b ) )
2 signsw.w 
 |-  W = { <. ( Base ` ndx ) , { -u 1 , 0 , 1 } >. , <. ( +g ` ndx ) , .+^ >. }
3 1 signspval 
 |-  ( ( u e. { -u 1 , 0 , 1 } /\ v e. { -u 1 , 0 , 1 } ) -> ( u .+^ v ) = if ( v = 0 , u , v ) )
4 ifcl 
 |-  ( ( u e. { -u 1 , 0 , 1 } /\ v e. { -u 1 , 0 , 1 } ) -> if ( v = 0 , u , v ) e. { -u 1 , 0 , 1 } )
5 3 4 eqeltrd 
 |-  ( ( u e. { -u 1 , 0 , 1 } /\ v e. { -u 1 , 0 , 1 } ) -> ( u .+^ v ) e. { -u 1 , 0 , 1 } )
6 1 signspval 
 |-  ( ( ( u .+^ v ) e. { -u 1 , 0 , 1 } /\ w e. { -u 1 , 0 , 1 } ) -> ( ( u .+^ v ) .+^ w ) = if ( w = 0 , ( u .+^ v ) , w ) )
7 5 6 stoic3 
 |-  ( ( u e. { -u 1 , 0 , 1 } /\ v e. { -u 1 , 0 , 1 } /\ w e. { -u 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 e. { -u 1 , 0 , 1 } /\ v e. { -u 1 , 0 , 1 } /\ w e. { -u 1 , 0 , 1 } ) /\ w = 0 ) -> ( ( u .+^ v ) .+^ w ) = ( u .+^ v ) )
10 9 adantr 
 |-  ( ( ( ( u e. { -u 1 , 0 , 1 } /\ v e. { -u 1 , 0 , 1 } /\ w e. { -u 1 , 0 , 1 } ) /\ w = 0 ) /\ v = 0 ) -> ( ( u .+^ v ) .+^ w ) = ( u .+^ v ) )
11 3 3adant3 
 |-  ( ( u e. { -u 1 , 0 , 1 } /\ v e. { -u 1 , 0 , 1 } /\ w e. { -u 1 , 0 , 1 } ) -> ( u .+^ v ) = if ( v = 0 , u , v ) )
12 11 ad2antrr 
 |-  ( ( ( ( u e. { -u 1 , 0 , 1 } /\ v e. { -u 1 , 0 , 1 } /\ w e. { -u 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 e. { -u 1 , 0 , 1 } /\ v e. { -u 1 , 0 , 1 } /\ w e. { -u 1 , 0 , 1 } ) /\ w = 0 ) /\ v = 0 ) -> if ( v = 0 , u , v ) = u )
15 10 12 14 3eqtrd 
 |-  ( ( ( ( u e. { -u 1 , 0 , 1 } /\ v e. { -u 1 , 0 , 1 } /\ w e. { -u 1 , 0 , 1 } ) /\ w = 0 ) /\ v = 0 ) -> ( ( u .+^ v ) .+^ w ) = u )
16 simp1 
 |-  ( ( u e. { -u 1 , 0 , 1 } /\ v e. { -u 1 , 0 , 1 } /\ w e. { -u 1 , 0 , 1 } ) -> u e. { -u 1 , 0 , 1 } )
17 1 signspval 
 |-  ( ( v e. { -u 1 , 0 , 1 } /\ w e. { -u 1 , 0 , 1 } ) -> ( v .+^ w ) = if ( w = 0 , v , w ) )
18 17 3adant1 
 |-  ( ( u e. { -u 1 , 0 , 1 } /\ v e. { -u 1 , 0 , 1 } /\ w e. { -u 1 , 0 , 1 } ) -> ( v .+^ w ) = if ( w = 0 , v , w ) )
19 simpl2 
 |-  ( ( ( u e. { -u 1 , 0 , 1 } /\ v e. { -u 1 , 0 , 1 } /\ w e. { -u 1 , 0 , 1 } ) /\ w = 0 ) -> v e. { -u 1 , 0 , 1 } )
20 simpl3 
 |-  ( ( ( u e. { -u 1 , 0 , 1 } /\ v e. { -u 1 , 0 , 1 } /\ w e. { -u 1 , 0 , 1 } ) /\ -. w = 0 ) -> w e. { -u 1 , 0 , 1 } )
21 19 20 ifclda 
 |-  ( ( u e. { -u 1 , 0 , 1 } /\ v e. { -u 1 , 0 , 1 } /\ w e. { -u 1 , 0 , 1 } ) -> if ( w = 0 , v , w ) e. { -u 1 , 0 , 1 } )
22 18 21 eqeltrd 
 |-  ( ( u e. { -u 1 , 0 , 1 } /\ v e. { -u 1 , 0 , 1 } /\ w e. { -u 1 , 0 , 1 } ) -> ( v .+^ w ) e. { -u 1 , 0 , 1 } )
23 1 signspval 
 |-  ( ( u e. { -u 1 , 0 , 1 } /\ ( v .+^ w ) e. { -u 1 , 0 , 1 } ) -> ( u .+^ ( v .+^ w ) ) = if ( ( v .+^ w ) = 0 , u , ( v .+^ w ) ) )
24 16 22 23 syl2anc 
 |-  ( ( u e. { -u 1 , 0 , 1 } /\ v e. { -u 1 , 0 , 1 } /\ w e. { -u 1 , 0 , 1 } ) -> ( u .+^ ( v .+^ w ) ) = if ( ( v .+^ w ) = 0 , u , ( v .+^ w ) ) )
25 24 ad2antrr 
 |-  ( ( ( ( u e. { -u 1 , 0 , 1 } /\ v e. { -u 1 , 0 , 1 } /\ w e. { -u 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 e. { -u 1 , 0 , 1 } /\ v e. { -u 1 , 0 , 1 } /\ w e. { -u 1 , 0 , 1 } ) /\ w = 0 ) -> ( v .+^ w ) = v )
28 id 
 |-  ( v = 0 -> v = 0 )
29 27 28 sylan9eq 
 |-  ( ( ( ( u e. { -u 1 , 0 , 1 } /\ v e. { -u 1 , 0 , 1 } /\ w e. { -u 1 , 0 , 1 } ) /\ w = 0 ) /\ v = 0 ) -> ( v .+^ w ) = 0 )
30 29 iftrued 
 |-  ( ( ( ( u e. { -u 1 , 0 , 1 } /\ v e. { -u 1 , 0 , 1 } /\ w e. { -u 1 , 0 , 1 } ) /\ w = 0 ) /\ v = 0 ) -> if ( ( v .+^ w ) = 0 , u , ( v .+^ w ) ) = u )
31 25 30 eqtrd 
 |-  ( ( ( ( u e. { -u 1 , 0 , 1 } /\ v e. { -u 1 , 0 , 1 } /\ w e. { -u 1 , 0 , 1 } ) /\ w = 0 ) /\ v = 0 ) -> ( u .+^ ( v .+^ w ) ) = u )
32 15 31 eqtr4d 
 |-  ( ( ( ( u e. { -u 1 , 0 , 1 } /\ v e. { -u 1 , 0 , 1 } /\ w e. { -u 1 , 0 , 1 } ) /\ w = 0 ) /\ v = 0 ) -> ( ( u .+^ v ) .+^ w ) = ( u .+^ ( v .+^ w ) ) )
33 7 ad2antrr 
 |-  ( ( ( ( u e. { -u 1 , 0 , 1 } /\ v e. { -u 1 , 0 , 1 } /\ w e. { -u 1 , 0 , 1 } ) /\ w = 0 ) /\ -. v = 0 ) -> ( ( u .+^ v ) .+^ w ) = if ( w = 0 , ( u .+^ v ) , w ) )
34 8 ad2antlr 
 |-  ( ( ( ( u e. { -u 1 , 0 , 1 } /\ v e. { -u 1 , 0 , 1 } /\ w e. { -u 1 , 0 , 1 } ) /\ w = 0 ) /\ -. v = 0 ) -> if ( w = 0 , ( u .+^ v ) , w ) = ( u .+^ v ) )
35 11 ad2antrr 
 |-  ( ( ( ( u e. { -u 1 , 0 , 1 } /\ v e. { -u 1 , 0 , 1 } /\ w e. { -u 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 e. { -u 1 , 0 , 1 } /\ v e. { -u 1 , 0 , 1 } /\ w e. { -u 1 , 0 , 1 } ) /\ w = 0 ) /\ -. v = 0 ) -> if ( v = 0 , u , v ) = v )
38 35 37 eqtrd 
 |-  ( ( ( ( u e. { -u 1 , 0 , 1 } /\ v e. { -u 1 , 0 , 1 } /\ w e. { -u 1 , 0 , 1 } ) /\ w = 0 ) /\ -. v = 0 ) -> ( u .+^ v ) = v )
39 33 34 38 3eqtrd 
 |-  ( ( ( ( u e. { -u 1 , 0 , 1 } /\ v e. { -u 1 , 0 , 1 } /\ w e. { -u 1 , 0 , 1 } ) /\ w = 0 ) /\ -. v = 0 ) -> ( ( u .+^ v ) .+^ w ) = v )
40 24 ad2antrr 
 |-  ( ( ( ( u e. { -u 1 , 0 , 1 } /\ v e. { -u 1 , 0 , 1 } /\ w e. { -u 1 , 0 , 1 } ) /\ w = 0 ) /\ -. v = 0 ) -> ( u .+^ ( v .+^ w ) ) = if ( ( v .+^ w ) = 0 , u , ( v .+^ w ) ) )
41 simpr 
 |-  ( ( ( ( u e. { -u 1 , 0 , 1 } /\ v e. { -u 1 , 0 , 1 } /\ w e. { -u 1 , 0 , 1 } ) /\ w = 0 ) /\ -. v = 0 ) -> -. v = 0 )
42 18 ad2antrr 
 |-  ( ( ( ( u e. { -u 1 , 0 , 1 } /\ v e. { -u 1 , 0 , 1 } /\ w e. { -u 1 , 0 , 1 } ) /\ w = 0 ) /\ -. v = 0 ) -> ( v .+^ w ) = if ( w = 0 , v , w ) )
43 26 ad2antlr 
 |-  ( ( ( ( u e. { -u 1 , 0 , 1 } /\ v e. { -u 1 , 0 , 1 } /\ w e. { -u 1 , 0 , 1 } ) /\ w = 0 ) /\ -. v = 0 ) -> if ( w = 0 , v , w ) = v )
44 42 43 eqtrd 
 |-  ( ( ( ( u e. { -u 1 , 0 , 1 } /\ v e. { -u 1 , 0 , 1 } /\ w e. { -u 1 , 0 , 1 } ) /\ w = 0 ) /\ -. v = 0 ) -> ( v .+^ w ) = v )
45 44 eqeq1d 
 |-  ( ( ( ( u e. { -u 1 , 0 , 1 } /\ v e. { -u 1 , 0 , 1 } /\ w e. { -u 1 , 0 , 1 } ) /\ w = 0 ) /\ -. v = 0 ) -> ( ( v .+^ w ) = 0 <-> v = 0 ) )
46 41 45 mtbird 
 |-  ( ( ( ( u e. { -u 1 , 0 , 1 } /\ v e. { -u 1 , 0 , 1 } /\ w e. { -u 1 , 0 , 1 } ) /\ w = 0 ) /\ -. v = 0 ) -> -. ( v .+^ w ) = 0 )
47 46 iffalsed 
 |-  ( ( ( ( u e. { -u 1 , 0 , 1 } /\ v e. { -u 1 , 0 , 1 } /\ w e. { -u 1 , 0 , 1 } ) /\ w = 0 ) /\ -. v = 0 ) -> if ( ( v .+^ w ) = 0 , u , ( v .+^ w ) ) = ( v .+^ w ) )
48 40 47 44 3eqtrd 
 |-  ( ( ( ( u e. { -u 1 , 0 , 1 } /\ v e. { -u 1 , 0 , 1 } /\ w e. { -u 1 , 0 , 1 } ) /\ w = 0 ) /\ -. v = 0 ) -> ( u .+^ ( v .+^ w ) ) = v )
49 39 48 eqtr4d 
 |-  ( ( ( ( u e. { -u 1 , 0 , 1 } /\ v e. { -u 1 , 0 , 1 } /\ w e. { -u 1 , 0 , 1 } ) /\ w = 0 ) /\ -. v = 0 ) -> ( ( u .+^ v ) .+^ w ) = ( u .+^ ( v .+^ w ) ) )
50 32 49 pm2.61dan 
 |-  ( ( ( u e. { -u 1 , 0 , 1 } /\ v e. { -u 1 , 0 , 1 } /\ w e. { -u 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 e. { -u 1 , 0 , 1 } /\ v e. { -u 1 , 0 , 1 } /\ w e. { -u 1 , 0 , 1 } ) /\ -. w = 0 ) -> ( ( u .+^ v ) .+^ w ) = w )
53 24 adantr 
 |-  ( ( ( u e. { -u 1 , 0 , 1 } /\ v e. { -u 1 , 0 , 1 } /\ w e. { -u 1 , 0 , 1 } ) /\ -. w = 0 ) -> ( u .+^ ( v .+^ w ) ) = if ( ( v .+^ w ) = 0 , u , ( v .+^ w ) ) )
54 simpr 
 |-  ( ( ( u e. { -u 1 , 0 , 1 } /\ v e. { -u 1 , 0 , 1 } /\ w e. { -u 1 , 0 , 1 } ) /\ -. w = 0 ) -> -. w = 0 )
55 iffalse 
 |-  ( -. w = 0 -> if ( w = 0 , v , w ) = w )
56 18 55 sylan9eq 
 |-  ( ( ( u e. { -u 1 , 0 , 1 } /\ v e. { -u 1 , 0 , 1 } /\ w e. { -u 1 , 0 , 1 } ) /\ -. w = 0 ) -> ( v .+^ w ) = w )
57 56 eqeq1d 
 |-  ( ( ( u e. { -u 1 , 0 , 1 } /\ v e. { -u 1 , 0 , 1 } /\ w e. { -u 1 , 0 , 1 } ) /\ -. w = 0 ) -> ( ( v .+^ w ) = 0 <-> w = 0 ) )
58 54 57 mtbird 
 |-  ( ( ( u e. { -u 1 , 0 , 1 } /\ v e. { -u 1 , 0 , 1 } /\ w e. { -u 1 , 0 , 1 } ) /\ -. w = 0 ) -> -. ( v .+^ w ) = 0 )
59 58 iffalsed 
 |-  ( ( ( u e. { -u 1 , 0 , 1 } /\ v e. { -u 1 , 0 , 1 } /\ w e. { -u 1 , 0 , 1 } ) /\ -. w = 0 ) -> if ( ( v .+^ w ) = 0 , u , ( v .+^ w ) ) = ( v .+^ w ) )
60 53 59 56 3eqtrd 
 |-  ( ( ( u e. { -u 1 , 0 , 1 } /\ v e. { -u 1 , 0 , 1 } /\ w e. { -u 1 , 0 , 1 } ) /\ -. w = 0 ) -> ( u .+^ ( v .+^ w ) ) = w )
61 52 60 eqtr4d 
 |-  ( ( ( u e. { -u 1 , 0 , 1 } /\ v e. { -u 1 , 0 , 1 } /\ w e. { -u 1 , 0 , 1 } ) /\ -. w = 0 ) -> ( ( u .+^ v ) .+^ w ) = ( u .+^ ( v .+^ w ) ) )
62 50 61 pm2.61dan 
 |-  ( ( u e. { -u 1 , 0 , 1 } /\ v e. { -u 1 , 0 , 1 } /\ w e. { -u 1 , 0 , 1 } ) -> ( ( u .+^ v ) .+^ w ) = ( u .+^ ( v .+^ w ) ) )
63 62 3expa 
 |-  ( ( ( u e. { -u 1 , 0 , 1 } /\ v e. { -u 1 , 0 , 1 } ) /\ w e. { -u 1 , 0 , 1 } ) -> ( ( u .+^ v ) .+^ w ) = ( u .+^ ( v .+^ w ) ) )
64 63 ralrimiva 
 |-  ( ( u e. { -u 1 , 0 , 1 } /\ v e. { -u 1 , 0 , 1 } ) -> A. w e. { -u 1 , 0 , 1 } ( ( u .+^ v ) .+^ w ) = ( u .+^ ( v .+^ w ) ) )
65 5 64 jca 
 |-  ( ( u e. { -u 1 , 0 , 1 } /\ v e. { -u 1 , 0 , 1 } ) -> ( ( u .+^ v ) e. { -u 1 , 0 , 1 } /\ A. w e. { -u 1 , 0 , 1 } ( ( u .+^ v ) .+^ w ) = ( u .+^ ( v .+^ w ) ) ) )
66 65 rgen2 
 |-  A. u e. { -u 1 , 0 , 1 } A. v e. { -u 1 , 0 , 1 } ( ( u .+^ v ) e. { -u 1 , 0 , 1 } /\ A. w e. { -u 1 , 0 , 1 } ( ( u .+^ v ) .+^ w ) = ( u .+^ ( v .+^ w ) ) )
67 c0ex 
 |-  0 e. _V
68 67 tpid2 
 |-  0 e. { -u 1 , 0 , 1 }
69 1 signsw0glem 
 |-  A. u e. { -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 -> ( A. u e. { -u 1 , 0 , 1 } ( ( e .+^ u ) = u /\ ( u .+^ e ) = u ) <-> A. u e. { -u 1 , 0 , 1 } ( ( 0 .+^ u ) = u /\ ( u .+^ 0 ) = u ) ) )
73 72 rspcev 
 |-  ( ( 0 e. { -u 1 , 0 , 1 } /\ A. u e. { -u 1 , 0 , 1 } ( ( 0 .+^ u ) = u /\ ( u .+^ 0 ) = u ) ) -> E. e e. { -u 1 , 0 , 1 } A. u e. { -u 1 , 0 , 1 } ( ( e .+^ u ) = u /\ ( u .+^ e ) = u ) )
74 68 69 73 mp2an 
 |-  E. e e. { -u 1 , 0 , 1 } A. u e. { -u 1 , 0 , 1 } ( ( e .+^ u ) = u /\ ( u .+^ e ) = u )
75 1 2 signswbase 
 |-  { -u 1 , 0 , 1 } = ( Base ` W )
76 1 2 signswplusg 
 |-  .+^ = ( +g ` W )
77 75 76 ismnd 
 |-  ( W e. Mnd <-> ( A. u e. { -u 1 , 0 , 1 } A. v e. { -u 1 , 0 , 1 } ( ( u .+^ v ) e. { -u 1 , 0 , 1 } /\ A. w e. { -u 1 , 0 , 1 } ( ( u .+^ v ) .+^ w ) = ( u .+^ ( v .+^ w ) ) ) /\ E. e e. { -u 1 , 0 , 1 } A. u e. { -u 1 , 0 , 1 } ( ( e .+^ u ) = u /\ ( u .+^ e ) = u ) ) )
78 66 74 77 mpbir2an 
 |-  W e. Mnd