This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ccatcan2d

Description: Cancellation law for concatenation. (Contributed by SN, 6-Sep-2023)

Ref Expression
Hypotheses ccatcan2d.a 
|- ( ph -> A e. Word V )
ccatcan2d.b 
|- ( ph -> B e. Word V )
ccatcan2d.c 
|- ( ph -> C e. Word V )
Assertion ccatcan2d 
|- ( ph -> ( ( A ++ C ) = ( B ++ C ) <-> A = B ) )

Proof

Step Hyp Ref Expression
1 ccatcan2d.a 
 |-  ( ph -> A e. Word V )
2 ccatcan2d.b 
 |-  ( ph -> B e. Word V )
3 ccatcan2d.c 
 |-  ( ph -> C e. Word V )
4 simpr 
 |-  ( ( ph /\ ( A ++ C ) = ( B ++ C ) ) -> ( A ++ C ) = ( B ++ C ) )
5 lencl 
 |-  ( A e. Word V -> ( # ` A ) e. NN0 )
6 1 5 syl 
 |-  ( ph -> ( # ` A ) e. NN0 )
7 6 nn0cnd 
 |-  ( ph -> ( # ` A ) e. CC )
8 7 adantr 
 |-  ( ( ph /\ ( A ++ C ) = ( B ++ C ) ) -> ( # ` A ) e. CC )
9 lencl 
 |-  ( B e. Word V -> ( # ` B ) e. NN0 )
10 2 9 syl 
 |-  ( ph -> ( # ` B ) e. NN0 )
11 10 nn0cnd 
 |-  ( ph -> ( # ` B ) e. CC )
12 11 adantr 
 |-  ( ( ph /\ ( A ++ C ) = ( B ++ C ) ) -> ( # ` B ) e. CC )
13 lencl 
 |-  ( C e. Word V -> ( # ` C ) e. NN0 )
14 3 13 syl 
 |-  ( ph -> ( # ` C ) e. NN0 )
15 14 nn0cnd 
 |-  ( ph -> ( # ` C ) e. CC )
16 15 adantr 
 |-  ( ( ph /\ ( A ++ C ) = ( B ++ C ) ) -> ( # ` C ) e. CC )
17 ccatlen 
 |-  ( ( A e. Word V /\ C e. Word V ) -> ( # ` ( A ++ C ) ) = ( ( # ` A ) + ( # ` C ) ) )
18 1 3 17 syl2anc 
 |-  ( ph -> ( # ` ( A ++ C ) ) = ( ( # ` A ) + ( # ` C ) ) )
19 fveq2 
 |-  ( ( A ++ C ) = ( B ++ C ) -> ( # ` ( A ++ C ) ) = ( # ` ( B ++ C ) ) )
20 18 19 sylan9req 
 |-  ( ( ph /\ ( A ++ C ) = ( B ++ C ) ) -> ( ( # ` A ) + ( # ` C ) ) = ( # ` ( B ++ C ) ) )
21 ccatlen 
 |-  ( ( B e. Word V /\ C e. Word V ) -> ( # ` ( B ++ C ) ) = ( ( # ` B ) + ( # ` C ) ) )
22 2 3 21 syl2anc 
 |-  ( ph -> ( # ` ( B ++ C ) ) = ( ( # ` B ) + ( # ` C ) ) )
23 22 adantr 
 |-  ( ( ph /\ ( A ++ C ) = ( B ++ C ) ) -> ( # ` ( B ++ C ) ) = ( ( # ` B ) + ( # ` C ) ) )
24 20 23 eqtrd 
 |-  ( ( ph /\ ( A ++ C ) = ( B ++ C ) ) -> ( ( # ` A ) + ( # ` C ) ) = ( ( # ` B ) + ( # ` C ) ) )
25 8 12 16 24 addcan2ad 
 |-  ( ( ph /\ ( A ++ C ) = ( B ++ C ) ) -> ( # ` A ) = ( # ` B ) )
26 4 25 oveq12d 
 |-  ( ( ph /\ ( A ++ C ) = ( B ++ C ) ) -> ( ( A ++ C ) prefix ( # ` A ) ) = ( ( B ++ C ) prefix ( # ` B ) ) )
27 26 ex 
 |-  ( ph -> ( ( A ++ C ) = ( B ++ C ) -> ( ( A ++ C ) prefix ( # ` A ) ) = ( ( B ++ C ) prefix ( # ` B ) ) ) )
28 pfxccat1 
 |-  ( ( A e. Word V /\ C e. Word V ) -> ( ( A ++ C ) prefix ( # ` A ) ) = A )
29 1 3 28 syl2anc 
 |-  ( ph -> ( ( A ++ C ) prefix ( # ` A ) ) = A )
30 pfxccat1 
 |-  ( ( B e. Word V /\ C e. Word V ) -> ( ( B ++ C ) prefix ( # ` B ) ) = B )
31 2 3 30 syl2anc 
 |-  ( ph -> ( ( B ++ C ) prefix ( # ` B ) ) = B )
32 29 31 eqeq12d 
 |-  ( ph -> ( ( ( A ++ C ) prefix ( # ` A ) ) = ( ( B ++ C ) prefix ( # ` B ) ) <-> A = B ) )
33 27 32 sylibd 
 |-  ( ph -> ( ( A ++ C ) = ( B ++ C ) -> A = B ) )
34 oveq1 
 |-  ( A = B -> ( A ++ C ) = ( B ++ C ) )
35 33 34 impbid1 
 |-  ( ph -> ( ( A ++ C ) = ( B ++ C ) <-> A = B ) )