Metamath Proof Explorer

Theorem ccatw2s1p2

Description: Extract the second of two single symbols concatenated with a word. (Contributed by Alexander van der Vekens, 22-Sep-2018) (Proof shortened by AV, 1-May-2020)

Ref Expression
Assertion ccatw2s1p2 
|- ( ( ( W e. Word V /\ ( # ` W ) = N ) /\ ( X e. V /\ Y e. V ) ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( N + 1 ) ) = Y )

Proof

Step Hyp Ref Expression
1 ccatws1cl 
 |-  ( ( W e. Word V /\ X e. V ) -> ( W ++ <" X "> ) e. Word V )
2 1 ad2ant2r 
 |-  ( ( ( W e. Word V /\ ( # ` W ) = N ) /\ ( X e. V /\ Y e. V ) ) -> ( W ++ <" X "> ) e. Word V )
3 simprr 
 |-  ( ( ( W e. Word V /\ ( # ` W ) = N ) /\ ( X e. V /\ Y e. V ) ) -> Y e. V )
4 ccatws1len 
 |-  ( W e. Word V -> ( # ` ( W ++ <" X "> ) ) = ( ( # ` W ) + 1 ) )
5 4 ad2antrr 
 |-  ( ( ( W e. Word V /\ ( # ` W ) = N ) /\ ( X e. V /\ Y e. V ) ) -> ( # ` ( W ++ <" X "> ) ) = ( ( # ` W ) + 1 ) )
6 oveq1 
 |-  ( ( # ` W ) = N -> ( ( # ` W ) + 1 ) = ( N + 1 ) )
7 6 ad2antlr 
 |-  ( ( ( W e. Word V /\ ( # ` W ) = N ) /\ ( X e. V /\ Y e. V ) ) -> ( ( # ` W ) + 1 ) = ( N + 1 ) )
8 5 7 eqtr2d 
 |-  ( ( ( W e. Word V /\ ( # ` W ) = N ) /\ ( X e. V /\ Y e. V ) ) -> ( N + 1 ) = ( # ` ( W ++ <" X "> ) ) )
9 ccats1val2 
 |-  ( ( ( W ++ <" X "> ) e. Word V /\ Y e. V /\ ( N + 1 ) = ( # ` ( W ++ <" X "> ) ) ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( N + 1 ) ) = Y )
10 2 3 8 9 syl3anc 
 |-  ( ( ( W e. Word V /\ ( # ` W ) = N ) /\ ( X e. V /\ Y e. V ) ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( N + 1 ) ) = Y )