Metamath Proof Explorer


Theorem signshwrd

Description: H , corresponding to the word F multiplied by ( x - C ) , is a word. (Contributed by Thierry Arnoux, 29-Sep-2018)

Ref Expression
Hypotheses signsv.p โŠข โจฃ = ( ๐‘Ž โˆˆ { - 1 , 0 , 1 } , ๐‘ โˆˆ { - 1 , 0 , 1 } โ†ฆ if ( ๐‘ = 0 , ๐‘Ž , ๐‘ ) )
signsv.w โŠข ๐‘Š = { โŸจ ( Base โ€˜ ndx ) , { - 1 , 0 , 1 } โŸฉ , โŸจ ( +g โ€˜ ndx ) , โจฃ โŸฉ }
signsv.t โŠข ๐‘‡ = ( ๐‘“ โˆˆ Word โ„ โ†ฆ ( ๐‘› โˆˆ ( 0 ..^ ( โ™ฏ โ€˜ ๐‘“ ) ) โ†ฆ ( ๐‘Š ฮฃg ( ๐‘– โˆˆ ( 0 ... ๐‘› ) โ†ฆ ( sgn โ€˜ ( ๐‘“ โ€˜ ๐‘– ) ) ) ) ) )
signsv.v โŠข ๐‘‰ = ( ๐‘“ โˆˆ Word โ„ โ†ฆ ฮฃ ๐‘— โˆˆ ( 1 ..^ ( โ™ฏ โ€˜ ๐‘“ ) ) if ( ( ( ๐‘‡ โ€˜ ๐‘“ ) โ€˜ ๐‘— ) โ‰  ( ( ๐‘‡ โ€˜ ๐‘“ ) โ€˜ ( ๐‘— โˆ’ 1 ) ) , 1 , 0 ) )
signs.h โŠข ๐ป = ( ( โŸจโ€œ 0 โ€โŸฉ ++ ๐น ) โˆ˜f โˆ’ ( ( ๐น ++ โŸจโ€œ 0 โ€โŸฉ ) โˆ˜f/c ยท ๐ถ ) )
Assertion signshwrd ( ( ๐น โˆˆ Word โ„ โˆง ๐ถ โˆˆ โ„+ ) โ†’ ๐ป โˆˆ Word โ„ )

Proof

Step Hyp Ref Expression
1 signsv.p โŠข โจฃ = ( ๐‘Ž โˆˆ { - 1 , 0 , 1 } , ๐‘ โˆˆ { - 1 , 0 , 1 } โ†ฆ if ( ๐‘ = 0 , ๐‘Ž , ๐‘ ) )
2 signsv.w โŠข ๐‘Š = { โŸจ ( Base โ€˜ ndx ) , { - 1 , 0 , 1 } โŸฉ , โŸจ ( +g โ€˜ ndx ) , โจฃ โŸฉ }
3 signsv.t โŠข ๐‘‡ = ( ๐‘“ โˆˆ Word โ„ โ†ฆ ( ๐‘› โˆˆ ( 0 ..^ ( โ™ฏ โ€˜ ๐‘“ ) ) โ†ฆ ( ๐‘Š ฮฃg ( ๐‘– โˆˆ ( 0 ... ๐‘› ) โ†ฆ ( sgn โ€˜ ( ๐‘“ โ€˜ ๐‘– ) ) ) ) ) )
4 signsv.v โŠข ๐‘‰ = ( ๐‘“ โˆˆ Word โ„ โ†ฆ ฮฃ ๐‘— โˆˆ ( 1 ..^ ( โ™ฏ โ€˜ ๐‘“ ) ) if ( ( ( ๐‘‡ โ€˜ ๐‘“ ) โ€˜ ๐‘— ) โ‰  ( ( ๐‘‡ โ€˜ ๐‘“ ) โ€˜ ( ๐‘— โˆ’ 1 ) ) , 1 , 0 ) )
5 signs.h โŠข ๐ป = ( ( โŸจโ€œ 0 โ€โŸฉ ++ ๐น ) โˆ˜f โˆ’ ( ( ๐น ++ โŸจโ€œ 0 โ€โŸฉ ) โˆ˜f/c ยท ๐ถ ) )
6 1 2 3 4 5 signshf โŠข ( ( ๐น โˆˆ Word โ„ โˆง ๐ถ โˆˆ โ„+ ) โ†’ ๐ป : ( 0 ..^ ( ( โ™ฏ โ€˜ ๐น ) + 1 ) ) โŸถ โ„ )
7 iswrdi โŠข ( ๐ป : ( 0 ..^ ( ( โ™ฏ โ€˜ ๐น ) + 1 ) ) โŸถ โ„ โ†’ ๐ป โˆˆ Word โ„ )
8 6 7 syl โŠข ( ( ๐น โˆˆ Word โ„ โˆง ๐ถ โˆˆ โ„+ ) โ†’ ๐ป โˆˆ Word โ„ )