Description: Value of a symbol in the left half of a word concatenated with a single symbol. (Contributed by Alexander van der Vekens, 5-Aug-2018) (Revised by JJ, 20-Jan-2024)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ccats1val1 | |- ( ( W e. Word V /\ I e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W ++ <" S "> ) ` I ) = ( W ` I ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | s1cli | |- <" S "> e. Word _V |
|
| 2 | ccatval1 | |- ( ( W e. Word V /\ <" S "> e. Word _V /\ I e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W ++ <" S "> ) ` I ) = ( W ` I ) ) |
|
| 3 | 1 2 | mp3an2 | |- ( ( W e. Word V /\ I e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W ++ <" S "> ) ` I ) = ( W ` I ) ) |