Metamath Proof Explorer


Theorem signstlen

Description: Length of the zero skipping sign word. (Contributed by Thierry Arnoux, 8-Oct-2018)

Ref Expression
Hypotheses signsv.p ˙=a101,b101ifb=0ab
signsv.w W=Basendx101+ndx˙
signsv.t T=fWordn0..^fWi=0nsgnfi
signsv.v V=fWordj1..^fifTfjTfj110
Assertion signstlen FWordTF=F

Proof

Step Hyp Ref Expression
1 signsv.p ˙=a101,b101ifb=0ab
2 signsv.w W=Basendx101+ndx˙
3 signsv.t T=fWordn0..^fWi=0nsgnfi
4 signsv.v V=fWordj1..^fifTfjTfj110
5 ovex Wi=0nsgnFiV
6 eqid n0..^FWi=0nsgnFi=n0..^FWi=0nsgnFi
7 5 6 fnmpti n0..^FWi=0nsgnFiFn0..^F
8 1 2 3 4 signstfv FWordTF=n0..^FWi=0nsgnFi
9 8 fneq1d FWordTFFn0..^Fn0..^FWi=0nsgnFiFn0..^F
10 7 9 mpbiri FWordTFFn0..^F
11 hashfn TFFn0..^FTF=0..^F
12 10 11 syl FWordTF=0..^F
13 lencl FWordF0
14 hashfzo0 F00..^F=F
15 13 14 syl FWord0..^F=F
16 12 15 eqtrd FWordTF=F