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 ⊢ ⨣ = ( 𝑎 ∈ { - 1 , 0 , 1 } , 𝑏 ∈ { - 1 , 0 , 1 } ↦ if ( 𝑏 = 0 , 𝑎 , 𝑏 ) )
signsw.w ⊢ 𝑊 = { ⟨ ( Base ‘ ndx ) , { - 1 , 0 , 1 } ⟩ , ⟨ ( +g ‘ ndx ) , ⨣ ⟩ }
Assertion signswmnd 𝑊 ∈ Mnd

Proof

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