# Metamath Proof Explorer

## Theorem signstfvc

Description: Zero-skipping sign in a word compared to a shorter word. (Contributed by Thierry Arnoux, 11-Oct-2018)

Ref Expression
Hypotheses signsv.p
signsv.w
signsv.t ${⊢}{T}=\left({f}\in \mathrm{Word}ℝ⟼\left({n}\in \left(0..^\left|{f}\right|\right)⟼\underset{{i}=0}{\overset{{n}}{{\sum }_{{W}}}}\mathrm{sgn}\left({f}\left({i}\right)\right)\right)\right)$
signsv.v ${⊢}{V}=\left({f}\in \mathrm{Word}ℝ⟼\sum _{{j}\in \left(1..^\left|{f}\right|\right)}if\left({T}\left({f}\right)\left({j}\right)\ne {T}\left({f}\right)\left({j}-1\right),1,0\right)\right)$
Assertion signstfvc ${⊢}\left({F}\in \mathrm{Word}ℝ\wedge {G}\in \mathrm{Word}ℝ\wedge {N}\in \left(0..^\left|{F}\right|\right)\right)\to {T}\left({F}\mathrm{++}{G}\right)\left({N}\right)={T}\left({F}\right)\left({N}\right)$

### Proof

Step Hyp Ref Expression
1 signsv.p
2 signsv.w
3 signsv.t ${⊢}{T}=\left({f}\in \mathrm{Word}ℝ⟼\left({n}\in \left(0..^\left|{f}\right|\right)⟼\underset{{i}=0}{\overset{{n}}{{\sum }_{{W}}}}\mathrm{sgn}\left({f}\left({i}\right)\right)\right)\right)$
4 signsv.v ${⊢}{V}=\left({f}\in \mathrm{Word}ℝ⟼\sum _{{j}\in \left(1..^\left|{f}\right|\right)}if\left({T}\left({f}\right)\left({j}\right)\ne {T}\left({f}\right)\left({j}-1\right),1,0\right)\right)$
5 oveq2 ${⊢}{g}=\varnothing \to {F}\mathrm{++}{g}={F}\mathrm{++}\varnothing$
6 5 fveq2d ${⊢}{g}=\varnothing \to {T}\left({F}\mathrm{++}{g}\right)={T}\left({F}\mathrm{++}\varnothing \right)$
7 6 fveq1d ${⊢}{g}=\varnothing \to {T}\left({F}\mathrm{++}{g}\right)\left({N}\right)={T}\left({F}\mathrm{++}\varnothing \right)\left({N}\right)$
8 7 eqeq1d ${⊢}{g}=\varnothing \to \left({T}\left({F}\mathrm{++}{g}\right)\left({N}\right)={T}\left({F}\right)\left({N}\right)↔{T}\left({F}\mathrm{++}\varnothing \right)\left({N}\right)={T}\left({F}\right)\left({N}\right)\right)$
9 8 imbi2d ${⊢}{g}=\varnothing \to \left(\left(\left({F}\in \mathrm{Word}ℝ\wedge {N}\in \left(0..^\left|{F}\right|\right)\right)\to {T}\left({F}\mathrm{++}{g}\right)\left({N}\right)={T}\left({F}\right)\left({N}\right)\right)↔\left(\left({F}\in \mathrm{Word}ℝ\wedge {N}\in \left(0..^\left|{F}\right|\right)\right)\to {T}\left({F}\mathrm{++}\varnothing \right)\left({N}\right)={T}\left({F}\right)\left({N}\right)\right)\right)$
10 oveq2 ${⊢}{g}={e}\to {F}\mathrm{++}{g}={F}\mathrm{++}{e}$
11 10 fveq2d ${⊢}{g}={e}\to {T}\left({F}\mathrm{++}{g}\right)={T}\left({F}\mathrm{++}{e}\right)$
12 11 fveq1d ${⊢}{g}={e}\to {T}\left({F}\mathrm{++}{g}\right)\left({N}\right)={T}\left({F}\mathrm{++}{e}\right)\left({N}\right)$
13 12 eqeq1d ${⊢}{g}={e}\to \left({T}\left({F}\mathrm{++}{g}\right)\left({N}\right)={T}\left({F}\right)\left({N}\right)↔{T}\left({F}\mathrm{++}{e}\right)\left({N}\right)={T}\left({F}\right)\left({N}\right)\right)$
14 13 imbi2d ${⊢}{g}={e}\to \left(\left(\left({F}\in \mathrm{Word}ℝ\wedge {N}\in \left(0..^\left|{F}\right|\right)\right)\to {T}\left({F}\mathrm{++}{g}\right)\left({N}\right)={T}\left({F}\right)\left({N}\right)\right)↔\left(\left({F}\in \mathrm{Word}ℝ\wedge {N}\in \left(0..^\left|{F}\right|\right)\right)\to {T}\left({F}\mathrm{++}{e}\right)\left({N}\right)={T}\left({F}\right)\left({N}\right)\right)\right)$
15 oveq2 ${⊢}{g}={e}\mathrm{++}⟨“{k}”⟩\to {F}\mathrm{++}{g}={F}\mathrm{++}\left({e}\mathrm{++}⟨“{k}”⟩\right)$
16 15 fveq2d ${⊢}{g}={e}\mathrm{++}⟨“{k}”⟩\to {T}\left({F}\mathrm{++}{g}\right)={T}\left({F}\mathrm{++}\left({e}\mathrm{++}⟨“{k}”⟩\right)\right)$
17 16 fveq1d ${⊢}{g}={e}\mathrm{++}⟨“{k}”⟩\to {T}\left({F}\mathrm{++}{g}\right)\left({N}\right)={T}\left({F}\mathrm{++}\left({e}\mathrm{++}⟨“{k}”⟩\right)\right)\left({N}\right)$
18 17 eqeq1d ${⊢}{g}={e}\mathrm{++}⟨“{k}”⟩\to \left({T}\left({F}\mathrm{++}{g}\right)\left({N}\right)={T}\left({F}\right)\left({N}\right)↔{T}\left({F}\mathrm{++}\left({e}\mathrm{++}⟨“{k}”⟩\right)\right)\left({N}\right)={T}\left({F}\right)\left({N}\right)\right)$
19 18 imbi2d ${⊢}{g}={e}\mathrm{++}⟨“{k}”⟩\to \left(\left(\left({F}\in \mathrm{Word}ℝ\wedge {N}\in \left(0..^\left|{F}\right|\right)\right)\to {T}\left({F}\mathrm{++}{g}\right)\left({N}\right)={T}\left({F}\right)\left({N}\right)\right)↔\left(\left({F}\in \mathrm{Word}ℝ\wedge {N}\in \left(0..^\left|{F}\right|\right)\right)\to {T}\left({F}\mathrm{++}\left({e}\mathrm{++}⟨“{k}”⟩\right)\right)\left({N}\right)={T}\left({F}\right)\left({N}\right)\right)\right)$
20 oveq2 ${⊢}{g}={G}\to {F}\mathrm{++}{g}={F}\mathrm{++}{G}$
21 20 fveq2d ${⊢}{g}={G}\to {T}\left({F}\mathrm{++}{g}\right)={T}\left({F}\mathrm{++}{G}\right)$
22 21 fveq1d ${⊢}{g}={G}\to {T}\left({F}\mathrm{++}{g}\right)\left({N}\right)={T}\left({F}\mathrm{++}{G}\right)\left({N}\right)$
23 22 eqeq1d ${⊢}{g}={G}\to \left({T}\left({F}\mathrm{++}{g}\right)\left({N}\right)={T}\left({F}\right)\left({N}\right)↔{T}\left({F}\mathrm{++}{G}\right)\left({N}\right)={T}\left({F}\right)\left({N}\right)\right)$
24 23 imbi2d ${⊢}{g}={G}\to \left(\left(\left({F}\in \mathrm{Word}ℝ\wedge {N}\in \left(0..^\left|{F}\right|\right)\right)\to {T}\left({F}\mathrm{++}{g}\right)\left({N}\right)={T}\left({F}\right)\left({N}\right)\right)↔\left(\left({F}\in \mathrm{Word}ℝ\wedge {N}\in \left(0..^\left|{F}\right|\right)\right)\to {T}\left({F}\mathrm{++}{G}\right)\left({N}\right)={T}\left({F}\right)\left({N}\right)\right)\right)$
25 ccatrid ${⊢}{F}\in \mathrm{Word}ℝ\to {F}\mathrm{++}\varnothing ={F}$
26 25 fveq2d ${⊢}{F}\in \mathrm{Word}ℝ\to {T}\left({F}\mathrm{++}\varnothing \right)={T}\left({F}\right)$
27 26 fveq1d ${⊢}{F}\in \mathrm{Word}ℝ\to {T}\left({F}\mathrm{++}\varnothing \right)\left({N}\right)={T}\left({F}\right)\left({N}\right)$
28 27 adantr ${⊢}\left({F}\in \mathrm{Word}ℝ\wedge {N}\in \left(0..^\left|{F}\right|\right)\right)\to {T}\left({F}\mathrm{++}\varnothing \right)\left({N}\right)={T}\left({F}\right)\left({N}\right)$
29 s1cl ${⊢}{k}\in ℝ\to ⟨“{k}”⟩\in \mathrm{Word}ℝ$
30 ccatass ${⊢}\left({F}\in \mathrm{Word}ℝ\wedge {e}\in \mathrm{Word}ℝ\wedge ⟨“{k}”⟩\in \mathrm{Word}ℝ\right)\to \left({F}\mathrm{++}{e}\right)\mathrm{++}⟨“{k}”⟩={F}\mathrm{++}\left({e}\mathrm{++}⟨“{k}”⟩\right)$
31 29 30 syl3an3 ${⊢}\left({F}\in \mathrm{Word}ℝ\wedge {e}\in \mathrm{Word}ℝ\wedge {k}\in ℝ\right)\to \left({F}\mathrm{++}{e}\right)\mathrm{++}⟨“{k}”⟩={F}\mathrm{++}\left({e}\mathrm{++}⟨“{k}”⟩\right)$
32 31 3expb ${⊢}\left({F}\in \mathrm{Word}ℝ\wedge \left({e}\in \mathrm{Word}ℝ\wedge {k}\in ℝ\right)\right)\to \left({F}\mathrm{++}{e}\right)\mathrm{++}⟨“{k}”⟩={F}\mathrm{++}\left({e}\mathrm{++}⟨“{k}”⟩\right)$
33 32 adantlr ${⊢}\left(\left({F}\in \mathrm{Word}ℝ\wedge {N}\in \left(0..^\left|{F}\right|\right)\right)\wedge \left({e}\in \mathrm{Word}ℝ\wedge {k}\in ℝ\right)\right)\to \left({F}\mathrm{++}{e}\right)\mathrm{++}⟨“{k}”⟩={F}\mathrm{++}\left({e}\mathrm{++}⟨“{k}”⟩\right)$
34 33 fveq2d ${⊢}\left(\left({F}\in \mathrm{Word}ℝ\wedge {N}\in \left(0..^\left|{F}\right|\right)\right)\wedge \left({e}\in \mathrm{Word}ℝ\wedge {k}\in ℝ\right)\right)\to {T}\left(\left({F}\mathrm{++}{e}\right)\mathrm{++}⟨“{k}”⟩\right)={T}\left({F}\mathrm{++}\left({e}\mathrm{++}⟨“{k}”⟩\right)\right)$
35 34 fveq1d ${⊢}\left(\left({F}\in \mathrm{Word}ℝ\wedge {N}\in \left(0..^\left|{F}\right|\right)\right)\wedge \left({e}\in \mathrm{Word}ℝ\wedge {k}\in ℝ\right)\right)\to {T}\left(\left({F}\mathrm{++}{e}\right)\mathrm{++}⟨“{k}”⟩\right)\left({N}\right)={T}\left({F}\mathrm{++}\left({e}\mathrm{++}⟨“{k}”⟩\right)\right)\left({N}\right)$
36 ccatcl ${⊢}\left({F}\in \mathrm{Word}ℝ\wedge {e}\in \mathrm{Word}ℝ\right)\to {F}\mathrm{++}{e}\in \mathrm{Word}ℝ$
37 36 ad2ant2r ${⊢}\left(\left({F}\in \mathrm{Word}ℝ\wedge {N}\in \left(0..^\left|{F}\right|\right)\right)\wedge \left({e}\in \mathrm{Word}ℝ\wedge {k}\in ℝ\right)\right)\to {F}\mathrm{++}{e}\in \mathrm{Word}ℝ$
38 simprr ${⊢}\left(\left({F}\in \mathrm{Word}ℝ\wedge {N}\in \left(0..^\left|{F}\right|\right)\right)\wedge \left({e}\in \mathrm{Word}ℝ\wedge {k}\in ℝ\right)\right)\to {k}\in ℝ$
39 lencl ${⊢}{F}\in \mathrm{Word}ℝ\to \left|{F}\right|\in {ℕ}_{0}$
40 39 nn0zd ${⊢}{F}\in \mathrm{Word}ℝ\to \left|{F}\right|\in ℤ$
41 40 adantr ${⊢}\left({F}\in \mathrm{Word}ℝ\wedge {e}\in \mathrm{Word}ℝ\right)\to \left|{F}\right|\in ℤ$
42 lencl ${⊢}{F}\mathrm{++}{e}\in \mathrm{Word}ℝ\to \left|{F}\mathrm{++}{e}\right|\in {ℕ}_{0}$
43 36 42 syl ${⊢}\left({F}\in \mathrm{Word}ℝ\wedge {e}\in \mathrm{Word}ℝ\right)\to \left|{F}\mathrm{++}{e}\right|\in {ℕ}_{0}$
44 43 nn0zd ${⊢}\left({F}\in \mathrm{Word}ℝ\wedge {e}\in \mathrm{Word}ℝ\right)\to \left|{F}\mathrm{++}{e}\right|\in ℤ$
45 39 nn0red ${⊢}{F}\in \mathrm{Word}ℝ\to \left|{F}\right|\in ℝ$
46 lencl ${⊢}{e}\in \mathrm{Word}ℝ\to \left|{e}\right|\in {ℕ}_{0}$
47 nn0addge1 ${⊢}\left(\left|{F}\right|\in ℝ\wedge \left|{e}\right|\in {ℕ}_{0}\right)\to \left|{F}\right|\le \left|{F}\right|+\left|{e}\right|$
48 45 46 47 syl2an ${⊢}\left({F}\in \mathrm{Word}ℝ\wedge {e}\in \mathrm{Word}ℝ\right)\to \left|{F}\right|\le \left|{F}\right|+\left|{e}\right|$
49 ccatlen ${⊢}\left({F}\in \mathrm{Word}ℝ\wedge {e}\in \mathrm{Word}ℝ\right)\to \left|{F}\mathrm{++}{e}\right|=\left|{F}\right|+\left|{e}\right|$
50 48 49 breqtrrd ${⊢}\left({F}\in \mathrm{Word}ℝ\wedge {e}\in \mathrm{Word}ℝ\right)\to \left|{F}\right|\le \left|{F}\mathrm{++}{e}\right|$
51 eluz2 ${⊢}\left|{F}\mathrm{++}{e}\right|\in {ℤ}_{\ge \left|{F}\right|}↔\left(\left|{F}\right|\in ℤ\wedge \left|{F}\mathrm{++}{e}\right|\in ℤ\wedge \left|{F}\right|\le \left|{F}\mathrm{++}{e}\right|\right)$
52 41 44 50 51 syl3anbrc ${⊢}\left({F}\in \mathrm{Word}ℝ\wedge {e}\in \mathrm{Word}ℝ\right)\to \left|{F}\mathrm{++}{e}\right|\in {ℤ}_{\ge \left|{F}\right|}$
53 fzoss2 ${⊢}\left|{F}\mathrm{++}{e}\right|\in {ℤ}_{\ge \left|{F}\right|}\to \left(0..^\left|{F}\right|\right)\subseteq \left(0..^\left|{F}\mathrm{++}{e}\right|\right)$
54 52 53 syl ${⊢}\left({F}\in \mathrm{Word}ℝ\wedge {e}\in \mathrm{Word}ℝ\right)\to \left(0..^\left|{F}\right|\right)\subseteq \left(0..^\left|{F}\mathrm{++}{e}\right|\right)$
55 54 ad2ant2r ${⊢}\left(\left({F}\in \mathrm{Word}ℝ\wedge {N}\in \left(0..^\left|{F}\right|\right)\right)\wedge \left({e}\in \mathrm{Word}ℝ\wedge {k}\in ℝ\right)\right)\to \left(0..^\left|{F}\right|\right)\subseteq \left(0..^\left|{F}\mathrm{++}{e}\right|\right)$
56 simplr ${⊢}\left(\left({F}\in \mathrm{Word}ℝ\wedge {N}\in \left(0..^\left|{F}\right|\right)\right)\wedge \left({e}\in \mathrm{Word}ℝ\wedge {k}\in ℝ\right)\right)\to {N}\in \left(0..^\left|{F}\right|\right)$
57 55 56 sseldd ${⊢}\left(\left({F}\in \mathrm{Word}ℝ\wedge {N}\in \left(0..^\left|{F}\right|\right)\right)\wedge \left({e}\in \mathrm{Word}ℝ\wedge {k}\in ℝ\right)\right)\to {N}\in \left(0..^\left|{F}\mathrm{++}{e}\right|\right)$
58 1 2 3 4 signstfvp ${⊢}\left({F}\mathrm{++}{e}\in \mathrm{Word}ℝ\wedge {k}\in ℝ\wedge {N}\in \left(0..^\left|{F}\mathrm{++}{e}\right|\right)\right)\to {T}\left(\left({F}\mathrm{++}{e}\right)\mathrm{++}⟨“{k}”⟩\right)\left({N}\right)={T}\left({F}\mathrm{++}{e}\right)\left({N}\right)$
59 37 38 57 58 syl3anc ${⊢}\left(\left({F}\in \mathrm{Word}ℝ\wedge {N}\in \left(0..^\left|{F}\right|\right)\right)\wedge \left({e}\in \mathrm{Word}ℝ\wedge {k}\in ℝ\right)\right)\to {T}\left(\left({F}\mathrm{++}{e}\right)\mathrm{++}⟨“{k}”⟩\right)\left({N}\right)={T}\left({F}\mathrm{++}{e}\right)\left({N}\right)$
60 35 59 eqtr3d ${⊢}\left(\left({F}\in \mathrm{Word}ℝ\wedge {N}\in \left(0..^\left|{F}\right|\right)\right)\wedge \left({e}\in \mathrm{Word}ℝ\wedge {k}\in ℝ\right)\right)\to {T}\left({F}\mathrm{++}\left({e}\mathrm{++}⟨“{k}”⟩\right)\right)\left({N}\right)={T}\left({F}\mathrm{++}{e}\right)\left({N}\right)$
61 id ${⊢}{T}\left({F}\mathrm{++}{e}\right)\left({N}\right)={T}\left({F}\right)\left({N}\right)\to {T}\left({F}\mathrm{++}{e}\right)\left({N}\right)={T}\left({F}\right)\left({N}\right)$
62 60 61 sylan9eq ${⊢}\left(\left(\left({F}\in \mathrm{Word}ℝ\wedge {N}\in \left(0..^\left|{F}\right|\right)\right)\wedge \left({e}\in \mathrm{Word}ℝ\wedge {k}\in ℝ\right)\right)\wedge {T}\left({F}\mathrm{++}{e}\right)\left({N}\right)={T}\left({F}\right)\left({N}\right)\right)\to {T}\left({F}\mathrm{++}\left({e}\mathrm{++}⟨“{k}”⟩\right)\right)\left({N}\right)={T}\left({F}\right)\left({N}\right)$
63 62 ex ${⊢}\left(\left({F}\in \mathrm{Word}ℝ\wedge {N}\in \left(0..^\left|{F}\right|\right)\right)\wedge \left({e}\in \mathrm{Word}ℝ\wedge {k}\in ℝ\right)\right)\to \left({T}\left({F}\mathrm{++}{e}\right)\left({N}\right)={T}\left({F}\right)\left({N}\right)\to {T}\left({F}\mathrm{++}\left({e}\mathrm{++}⟨“{k}”⟩\right)\right)\left({N}\right)={T}\left({F}\right)\left({N}\right)\right)$
64 63 expcom ${⊢}\left({e}\in \mathrm{Word}ℝ\wedge {k}\in ℝ\right)\to \left(\left({F}\in \mathrm{Word}ℝ\wedge {N}\in \left(0..^\left|{F}\right|\right)\right)\to \left({T}\left({F}\mathrm{++}{e}\right)\left({N}\right)={T}\left({F}\right)\left({N}\right)\to {T}\left({F}\mathrm{++}\left({e}\mathrm{++}⟨“{k}”⟩\right)\right)\left({N}\right)={T}\left({F}\right)\left({N}\right)\right)\right)$
65 64 a2d ${⊢}\left({e}\in \mathrm{Word}ℝ\wedge {k}\in ℝ\right)\to \left(\left(\left({F}\in \mathrm{Word}ℝ\wedge {N}\in \left(0..^\left|{F}\right|\right)\right)\to {T}\left({F}\mathrm{++}{e}\right)\left({N}\right)={T}\left({F}\right)\left({N}\right)\right)\to \left(\left({F}\in \mathrm{Word}ℝ\wedge {N}\in \left(0..^\left|{F}\right|\right)\right)\to {T}\left({F}\mathrm{++}\left({e}\mathrm{++}⟨“{k}”⟩\right)\right)\left({N}\right)={T}\left({F}\right)\left({N}\right)\right)\right)$
66 9 14 19 24 28 65 wrdind ${⊢}{G}\in \mathrm{Word}ℝ\to \left(\left({F}\in \mathrm{Word}ℝ\wedge {N}\in \left(0..^\left|{F}\right|\right)\right)\to {T}\left({F}\mathrm{++}{G}\right)\left({N}\right)={T}\left({F}\right)\left({N}\right)\right)$
67 66 3impib ${⊢}\left({G}\in \mathrm{Word}ℝ\wedge {F}\in \mathrm{Word}ℝ\wedge {N}\in \left(0..^\left|{F}\right|\right)\right)\to {T}\left({F}\mathrm{++}{G}\right)\left({N}\right)={T}\left({F}\right)\left({N}\right)$
68 67 3com12 ${⊢}\left({F}\in \mathrm{Word}ℝ\wedge {G}\in \mathrm{Word}ℝ\wedge {N}\in \left(0..^\left|{F}\right|\right)\right)\to {T}\left({F}\mathrm{++}{G}\right)\left({N}\right)={T}\left({F}\right)\left({N}\right)$