Metamath Proof Explorer

Theorem ccatval21sw

Description: The first symbol of the right (nonempty) half of a concatenated word. (Contributed by AV, 23-Apr-2022)

Ref Expression
Assertion ccatval21sw 
|- ( ( A e. Word V /\ B e. Word V /\ B =/= (/) ) -> ( ( A ++ B ) ` ( # ` A ) ) = ( B ` 0 ) )

Proof

Step Hyp Ref Expression
1 lencl 
 |-  ( A e. Word V -> ( # ` A ) e. NN0 )
2 1 nn0zd 
 |-  ( A e. Word V -> ( # ` A ) e. ZZ )
3 lennncl 
 |-  ( ( B e. Word V /\ B =/= (/) ) -> ( # ` B ) e. NN )
4 simpl 
 |-  ( ( ( # ` A ) e. ZZ /\ ( # ` B ) e. NN ) -> ( # ` A ) e. ZZ )
5 nnz 
 |-  ( ( # ` B ) e. NN -> ( # ` B ) e. ZZ )
6 zaddcl 
 |-  ( ( ( # ` A ) e. ZZ /\ ( # ` B ) e. ZZ ) -> ( ( # ` A ) + ( # ` B ) ) e. ZZ )
7 5 6 sylan2 
 |-  ( ( ( # ` A ) e. ZZ /\ ( # ` B ) e. NN ) -> ( ( # ` A ) + ( # ` B ) ) e. ZZ )
8 nngt0 
 |-  ( ( # ` B ) e. NN -> 0 < ( # ` B ) )
9 8 adantl 
 |-  ( ( ( # ` A ) e. ZZ /\ ( # ` B ) e. NN ) -> 0 < ( # ` B ) )
10 nnre 
 |-  ( ( # ` B ) e. NN -> ( # ` B ) e. RR )
11 zre 
 |-  ( ( # ` A ) e. ZZ -> ( # ` A ) e. RR )
12 ltaddpos 
 |-  ( ( ( # ` B ) e. RR /\ ( # ` A ) e. RR ) -> ( 0 < ( # ` B ) <-> ( # ` A ) < ( ( # ` A ) + ( # ` B ) ) ) )
13 10 11 12 syl2anr 
 |-  ( ( ( # ` A ) e. ZZ /\ ( # ` B ) e. NN ) -> ( 0 < ( # ` B ) <-> ( # ` A ) < ( ( # ` A ) + ( # ` B ) ) ) )
14 9 13 mpbid 
 |-  ( ( ( # ` A ) e. ZZ /\ ( # ` B ) e. NN ) -> ( # ` A ) < ( ( # ` A ) + ( # ` B ) ) )
15 4 7 14 3jca 
 |-  ( ( ( # ` A ) e. ZZ /\ ( # ` B ) e. NN ) -> ( ( # ` A ) e. ZZ /\ ( ( # ` A ) + ( # ` B ) ) e. ZZ /\ ( # ` A ) < ( ( # ` A ) + ( # ` B ) ) ) )
16 2 3 15 syl2an 
 |-  ( ( A e. Word V /\ ( B e. Word V /\ B =/= (/) ) ) -> ( ( # ` A ) e. ZZ /\ ( ( # ` A ) + ( # ` B ) ) e. ZZ /\ ( # ` A ) < ( ( # ` A ) + ( # ` B ) ) ) )
17 16 3impb 
 |-  ( ( A e. Word V /\ B e. Word V /\ B =/= (/) ) -> ( ( # ` A ) e. ZZ /\ ( ( # ` A ) + ( # ` B ) ) e. ZZ /\ ( # ` A ) < ( ( # ` A ) + ( # ` B ) ) ) )
18 fzolb 
 |-  ( ( # ` A ) e. ( ( # ` A ) ..^ ( ( # ` A ) + ( # ` B ) ) ) <-> ( ( # ` A ) e. ZZ /\ ( ( # ` A ) + ( # ` B ) ) e. ZZ /\ ( # ` A ) < ( ( # ` A ) + ( # ` B ) ) ) )
19 17 18 sylibr 
 |-  ( ( A e. Word V /\ B e. Word V /\ B =/= (/) ) -> ( # ` A ) e. ( ( # ` A ) ..^ ( ( # ` A ) + ( # ` B ) ) ) )
20 ccatval2 
 |-  ( ( A e. Word V /\ B e. Word V /\ ( # ` A ) e. ( ( # ` A ) ..^ ( ( # ` A ) + ( # ` B ) ) ) ) -> ( ( A ++ B ) ` ( # ` A ) ) = ( B ` ( ( # ` A ) - ( # ` A ) ) ) )
21 19 20 syld3an3 
 |-  ( ( A e. Word V /\ B e. Word V /\ B =/= (/) ) -> ( ( A ++ B ) ` ( # ` A ) ) = ( B ` ( ( # ` A ) - ( # ` A ) ) ) )
22 1 nn0cnd 
 |-  ( A e. Word V -> ( # ` A ) e. CC )
23 22 subidd 
 |-  ( A e. Word V -> ( ( # ` A ) - ( # ` A ) ) = 0 )
24 23 fveq2d 
 |-  ( A e. Word V -> ( B ` ( ( # ` A ) - ( # ` A ) ) ) = ( B ` 0 ) )
25 24 3ad2ant1 
 |-  ( ( A e. Word V /\ B e. Word V /\ B =/= (/) ) -> ( B ` ( ( # ` A ) - ( # ` A ) ) ) = ( B ` 0 ) )
26 21 25 eqtrd 
 |-  ( ( A e. Word V /\ B e. Word V /\ B =/= (/) ) -> ( ( A ++ B ) ` ( # ` A ) ) = ( B ` 0 ) )