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 ⊢ ( 𝜑 → 𝐴 ∈ Word 𝑉 )
ccatcan2d.b ⊢ ( 𝜑 → 𝐵 ∈ Word 𝑉 )
ccatcan2d.c ⊢ ( 𝜑 → 𝐶 ∈ Word 𝑉 )
Assertion ccatcan2d ( 𝜑 → ( ( 𝐴 ++ 𝐶 ) = ( 𝐵 ++ 𝐶 ) ↔ 𝐴 = 𝐵 ) )

Proof

Step Hyp Ref Expression
1 ccatcan2d.a ⊢ ( 𝜑 → 𝐴 ∈ Word 𝑉 )
2 ccatcan2d.b ⊢ ( 𝜑 → 𝐵 ∈ Word 𝑉 )
3 ccatcan2d.c ⊢ ( 𝜑 → 𝐶 ∈ Word 𝑉 )
4 simpr ⊢ ( ( 𝜑 ∧ ( 𝐴 ++ 𝐶 ) = ( 𝐵 ++ 𝐶 ) ) → ( 𝐴 ++ 𝐶 ) = ( 𝐵 ++ 𝐶 ) )
5 lencl ⊢ ( 𝐴 ∈ Word 𝑉 → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
6 1 5 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
7 6 nn0cnd ⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) ∈ ℂ )
8 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ++ 𝐶 ) = ( 𝐵 ++ 𝐶 ) ) → ( ♯ ‘ 𝐴 ) ∈ ℂ )
9 lencl ⊢ ( 𝐵 ∈ Word 𝑉 → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
10 2 9 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
11 10 nn0cnd ⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) ∈ ℂ )
12 11 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ++ 𝐶 ) = ( 𝐵 ++ 𝐶 ) ) → ( ♯ ‘ 𝐵 ) ∈ ℂ )
13 lencl ⊢ ( 𝐶 ∈ Word 𝑉 → ( ♯ ‘ 𝐶 ) ∈ ℕ0 )
14 3 13 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝐶 ) ∈ ℕ0 )
15 14 nn0cnd ⊢ ( 𝜑 → ( ♯ ‘ 𝐶 ) ∈ ℂ )
16 15 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ++ 𝐶 ) = ( 𝐵 ++ 𝐶 ) ) → ( ♯ ‘ 𝐶 ) ∈ ℂ )
17 ccatlen ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐶 ∈ Word 𝑉 ) → ( ♯ ‘ ( 𝐴 ++ 𝐶 ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐶 ) ) )
18 1 3 17 syl2anc ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐴 ++ 𝐶 ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐶 ) ) )
19 fveq2 ⊢ ( ( 𝐴 ++ 𝐶 ) = ( 𝐵 ++ 𝐶 ) → ( ♯ ‘ ( 𝐴 ++ 𝐶 ) ) = ( ♯ ‘ ( 𝐵 ++ 𝐶 ) ) )
20 18 19 sylan9req ⊢ ( ( 𝜑 ∧ ( 𝐴 ++ 𝐶 ) = ( 𝐵 ++ 𝐶 ) ) → ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐶 ) ) = ( ♯ ‘ ( 𝐵 ++ 𝐶 ) ) )
21 ccatlen ⊢ ( ( 𝐵 ∈ Word 𝑉 ∧ 𝐶 ∈ Word 𝑉 ) → ( ♯ ‘ ( 𝐵 ++ 𝐶 ) ) = ( ( ♯ ‘ 𝐵 ) + ( ♯ ‘ 𝐶 ) ) )
22 2 3 21 syl2anc ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐵 ++ 𝐶 ) ) = ( ( ♯ ‘ 𝐵 ) + ( ♯ ‘ 𝐶 ) ) )
23 22 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ++ 𝐶 ) = ( 𝐵 ++ 𝐶 ) ) → ( ♯ ‘ ( 𝐵 ++ 𝐶 ) ) = ( ( ♯ ‘ 𝐵 ) + ( ♯ ‘ 𝐶 ) ) )
24 20 23 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝐴 ++ 𝐶 ) = ( 𝐵 ++ 𝐶 ) ) → ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐶 ) ) = ( ( ♯ ‘ 𝐵 ) + ( ♯ ‘ 𝐶 ) ) )
25 8 12 16 24 addcan2ad ⊢ ( ( 𝜑 ∧ ( 𝐴 ++ 𝐶 ) = ( 𝐵 ++ 𝐶 ) ) → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) )
26 4 25 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝐴 ++ 𝐶 ) = ( 𝐵 ++ 𝐶 ) ) → ( ( 𝐴 ++ 𝐶 ) prefix ( ♯ ‘ 𝐴 ) ) = ( ( 𝐵 ++ 𝐶 ) prefix ( ♯ ‘ 𝐵 ) ) )
27 26 ex ⊢ ( 𝜑 → ( ( 𝐴 ++ 𝐶 ) = ( 𝐵 ++ 𝐶 ) → ( ( 𝐴 ++ 𝐶 ) prefix ( ♯ ‘ 𝐴 ) ) = ( ( 𝐵 ++ 𝐶 ) prefix ( ♯ ‘ 𝐵 ) ) ) )
28 pfxccat1 ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐶 ∈ Word 𝑉 ) → ( ( 𝐴 ++ 𝐶 ) prefix ( ♯ ‘ 𝐴 ) ) = 𝐴 )
29 1 3 28 syl2anc ⊢ ( 𝜑 → ( ( 𝐴 ++ 𝐶 ) prefix ( ♯ ‘ 𝐴 ) ) = 𝐴 )
30 pfxccat1 ⊢ ( ( 𝐵 ∈ Word 𝑉 ∧ 𝐶 ∈ Word 𝑉 ) → ( ( 𝐵 ++ 𝐶 ) prefix ( ♯ ‘ 𝐵 ) ) = 𝐵 )
31 2 3 30 syl2anc ⊢ ( 𝜑 → ( ( 𝐵 ++ 𝐶 ) prefix ( ♯ ‘ 𝐵 ) ) = 𝐵 )
32 29 31 eqeq12d ⊢ ( 𝜑 → ( ( ( 𝐴 ++ 𝐶 ) prefix ( ♯ ‘ 𝐴 ) ) = ( ( 𝐵 ++ 𝐶 ) prefix ( ♯ ‘ 𝐵 ) ) ↔ 𝐴 = 𝐵 ) )
33 27 32 sylibd ⊢ ( 𝜑 → ( ( 𝐴 ++ 𝐶 ) = ( 𝐵 ++ 𝐶 ) → 𝐴 = 𝐵 ) )
34 oveq1 ⊢ ( 𝐴 = 𝐵 → ( 𝐴 ++ 𝐶 ) = ( 𝐵 ++ 𝐶 ) )
35 33 34 impbid1 ⊢ ( 𝜑 → ( ( 𝐴 ++ 𝐶 ) = ( 𝐵 ++ 𝐶 ) ↔ 𝐴 = 𝐵 ) )