Theorem signsvvfval

Description: The value of V , which represents the number of times the sign changes in a word. (Contributed by Thierry Arnoux, 7-Oct-2018)

	Ref	Expression
Hypotheses	signsv.p	|- .+^ = ( a e. { -u 1 , 0 , 1 } , b e. { -u 1 , 0 , 1 } |-> if ( b = 0 , a , b ) )
	signsv.w	|- W = { <. ( Base ` ndx ) , { -u 1 , 0 , 1 } >. , <. ( +g ` ndx ) , .+^ >. }
	signsv.t	|- T = ( f e. Word RR |-> ( n e. ( 0 ..^ ( # ` f ) ) |-> ( W gsum ( i e. ( 0 ... n ) |-> ( sgn ` ( f ` i ) ) ) ) ) )
	signsv.v	|- V = ( f e. Word RR |-> sum_ j e. ( 1 ..^ ( # ` f ) ) if ( ( ( T ` f ) ` j ) =/= ( ( T ` f ) ` ( j - 1 ) ) , 1 , 0 ) )
Assertion	signsvvfval	|- ( F e. Word RR -> ( V ` F ) = sum_ j e. ( 1 ..^ ( # ` F ) ) if ( ( ( T ` F ) ` j ) =/= ( ( T ` F ) ` ( j - 1 ) ) , 1 , 0 ) )

Proof

Step	Hyp	Ref	Expression
1		signsv.p	|- .+^ = ( a e. { -u 1 , 0 , 1 } , b e. { -u 1 , 0 , 1 } |-> if ( b = 0 , a , b ) )
2		signsv.w	|- W = { <. ( Base ` ndx ) , { -u 1 , 0 , 1 } >. , <. ( +g ` ndx ) , .+^ >. }
3		signsv.t	|- T = ( f e. Word RR |-> ( n e. ( 0 ..^ ( # ` f ) ) |-> ( W gsum ( i e. ( 0 ... n ) |-> ( sgn ` ( f ` i ) ) ) ) ) )
4		signsv.v	|- V = ( f e. Word RR |-> sum_ j e. ( 1 ..^ ( # ` f ) ) if ( ( ( T ` f ) ` j ) =/= ( ( T ` f ) ` ( j - 1 ) ) , 1 , 0 ) )
5		fveq2	|- ( f = F -> ( # ` f ) = ( # ` F ) )
6	5	oveq2d	|- ( f = F -> ( 1 ..^ ( # ` f ) ) = ( 1 ..^ ( # ` F ) ) )
7		fveq2	|- ( f = F -> ( T ` f ) = ( T ` F ) )
8	7	fveq1d	|- ( f = F -> ( ( T ` f ) ` j ) = ( ( T ` F ) ` j ) )
9	7	fveq1d	|- ( f = F -> ( ( T ` f ) ` ( j - 1 ) ) = ( ( T ` F ) ` ( j - 1 ) ) )
10	8 9	neeq12d	|- ( f = F -> ( ( ( T ` f ) ` j ) =/= ( ( T ` f ) ` ( j - 1 ) ) <-> ( ( T ` F ) ` j ) =/= ( ( T ` F ) ` ( j - 1 ) ) ) )
11	10	ifbid	|- ( f = F -> if ( ( ( T ` f ) ` j ) =/= ( ( T ` f ) ` ( j - 1 ) ) , 1 , 0 ) = if ( ( ( T ` F ) ` j ) =/= ( ( T ` F ) ` ( j - 1 ) ) , 1 , 0 ) )
12	11	adantr	|- ( ( f = F /\ j e. ( 1 ..^ ( # ` f ) ) ) -> if ( ( ( T ` f ) ` j ) =/= ( ( T ` f ) ` ( j - 1 ) ) , 1 , 0 ) = if ( ( ( T ` F ) ` j ) =/= ( ( T ` F ) ` ( j - 1 ) ) , 1 , 0 ) )
13	6 12	sumeq12dv	|- ( f = F -> sum_ j e. ( 1 ..^ ( # ` f ) ) if ( ( ( T ` f ) ` j ) =/= ( ( T ` f ) ` ( j - 1 ) ) , 1 , 0 ) = sum_ j e. ( 1 ..^ ( # ` F ) ) if ( ( ( T ` F ) ` j ) =/= ( ( T ` F ) ` ( j - 1 ) ) , 1 , 0 ) )
14		sumex	|- sum_ j e. ( 1 ..^ ( # ` F ) ) if ( ( ( T ` F ) ` j ) =/= ( ( T ` F ) ` ( j - 1 ) ) , 1 , 0 ) e. _V
15	13 4 14	fvmpt	|- ( F e. Word RR -> ( V ` F ) = sum_ j e. ( 1 ..^ ( # ` F ) ) if ( ( ( T ` F ) ` j ) =/= ( ( T ` F ) ` ( j - 1 ) ) , 1 , 0 ) )