Metamath Proof Explorer

Theorem swrdccat3b

Description: A suffix of a concatenation is either a suffix of the second concatenated word or a concatenation of a suffix of the first word with the second word. (Contributed by Alexander van der Vekens, 31-Mar-2018) (Revised by Alexander van der Vekens, 30-May-2018) (Proof shortened by AV, 14-Oct-2022)

Ref Expression
Hypothesis swrdccatin2.l ⊢ 𝐿 = ( ♯ ‘ 𝐴 )
Assertion swrdccat3b ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( 𝑀 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) → ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ⟩ ) = if ( 𝐿 ≤ 𝑀 , ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( ♯ ‘ 𝐵 ) ⟩ ) , ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ 𝐵 ) ) ) )

Proof

Step Hyp Ref Expression
1 swrdccatin2.l ⊢ 𝐿 = ( ♯ ‘ 𝐴 )
2 simpl ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ 𝑀 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) )
3 simpr ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ 𝑀 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → 𝑀 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) )
4 elfzubelfz ⊢ ( 𝑀 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) → ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) )
5 4 adantl ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ 𝑀 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) )
6 1 pfxccat3 ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( ( 𝑀 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ∧ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ⟩ ) = if ( ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ≤ 𝐿 , ( 𝐴 substr ⟨ 𝑀 , ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ⟩ ) , if ( 𝐿 ≤ 𝑀 , ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( ( 𝐿 + ( ♯ ‘ 𝐵 ) ) − 𝐿 ) ⟩ ) , ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ ( 𝐵 prefix ( ( 𝐿 + ( ♯ ‘ 𝐵 ) ) − 𝐿 ) ) ) ) ) ) )
7 6 imp ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ∧ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) → ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ⟩ ) = if ( ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ≤ 𝐿 , ( 𝐴 substr ⟨ 𝑀 , ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ⟩ ) , if ( 𝐿 ≤ 𝑀 , ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( ( 𝐿 + ( ♯ ‘ 𝐵 ) ) − 𝐿 ) ⟩ ) , ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ ( 𝐵 prefix ( ( 𝐿 + ( ♯ ‘ 𝐵 ) ) − 𝐿 ) ) ) ) ) )
8 2 3 5 7 syl12anc ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ 𝑀 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ⟩ ) = if ( ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ≤ 𝐿 , ( 𝐴 substr ⟨ 𝑀 , ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ⟩ ) , if ( 𝐿 ≤ 𝑀 , ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( ( 𝐿 + ( ♯ ‘ 𝐵 ) ) − 𝐿 ) ⟩ ) , ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ ( 𝐵 prefix ( ( 𝐿 + ( ♯ ‘ 𝐵 ) ) − 𝐿 ) ) ) ) ) )
9 1 swrdccat3blem ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ 𝑀 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ∧ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ≤ 𝐿 ) → if ( 𝐿 ≤ 𝑀 , ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( ♯ ‘ 𝐵 ) ⟩ ) , ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ 𝐵 ) ) = ( 𝐴 substr ⟨ 𝑀 , ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ⟩ ) )
10 iftrue ⊢ ( 𝐿 ≤ 𝑀 → if ( 𝐿 ≤ 𝑀 , ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( ♯ ‘ 𝐵 ) ⟩ ) , ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ 𝐵 ) ) = ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( ♯ ‘ 𝐵 ) ⟩ ) )
11 10 3ad2ant3 ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ 𝑀 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ∧ ¬ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ≤ 𝐿 ∧ 𝐿 ≤ 𝑀 ) → if ( 𝐿 ≤ 𝑀 , ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( ♯ ‘ 𝐵 ) ⟩ ) , ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ 𝐵 ) ) = ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( ♯ ‘ 𝐵 ) ⟩ ) )
12 lencl ⊢ ( 𝐴 ∈ Word 𝑉 → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
13 12 nn0cnd ⊢ ( 𝐴 ∈ Word 𝑉 → ( ♯ ‘ 𝐴 ) ∈ ℂ )
14 lencl ⊢ ( 𝐵 ∈ Word 𝑉 → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
15 14 nn0cnd ⊢ ( 𝐵 ∈ Word 𝑉 → ( ♯ ‘ 𝐵 ) ∈ ℂ )
16 1 eqcomi ⊢ ( ♯ ‘ 𝐴 ) = 𝐿
17 16 eleq1i ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℂ ↔ 𝐿 ∈ ℂ )
18 pncan2 ⊢ ( ( 𝐿 ∈ ℂ ∧ ( ♯ ‘ 𝐵 ) ∈ ℂ ) → ( ( 𝐿 + ( ♯ ‘ 𝐵 ) ) − 𝐿 ) = ( ♯ ‘ 𝐵 ) )
19 17 18 sylanb ⊢ ( ( ( ♯ ‘ 𝐴 ) ∈ ℂ ∧ ( ♯ ‘ 𝐵 ) ∈ ℂ ) → ( ( 𝐿 + ( ♯ ‘ 𝐵 ) ) − 𝐿 ) = ( ♯ ‘ 𝐵 ) )
20 13 15 19 syl2an ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( ( 𝐿 + ( ♯ ‘ 𝐵 ) ) − 𝐿 ) = ( ♯ ‘ 𝐵 ) )
21 20 eqcomd ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( ♯ ‘ 𝐵 ) = ( ( 𝐿 + ( ♯ ‘ 𝐵 ) ) − 𝐿 ) )
22 21 adantr ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ 𝑀 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( ♯ ‘ 𝐵 ) = ( ( 𝐿 + ( ♯ ‘ 𝐵 ) ) − 𝐿 ) )
23 22 3ad2ant1 ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ 𝑀 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ∧ ¬ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ≤ 𝐿 ∧ 𝐿 ≤ 𝑀 ) → ( ♯ ‘ 𝐵 ) = ( ( 𝐿 + ( ♯ ‘ 𝐵 ) ) − 𝐿 ) )
24 23 opeq2d ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ 𝑀 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ∧ ¬ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ≤ 𝐿 ∧ 𝐿 ≤ 𝑀 ) → ⟨ ( 𝑀 − 𝐿 ) , ( ♯ ‘ 𝐵 ) ⟩ = ⟨ ( 𝑀 − 𝐿 ) , ( ( 𝐿 + ( ♯ ‘ 𝐵 ) ) − 𝐿 ) ⟩ )
25 24 oveq2d ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ 𝑀 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ∧ ¬ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ≤ 𝐿 ∧ 𝐿 ≤ 𝑀 ) → ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( ♯ ‘ 𝐵 ) ⟩ ) = ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( ( 𝐿 + ( ♯ ‘ 𝐵 ) ) − 𝐿 ) ⟩ ) )
26 11 25 eqtrd ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ 𝑀 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ∧ ¬ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ≤ 𝐿 ∧ 𝐿 ≤ 𝑀 ) → if ( 𝐿 ≤ 𝑀 , ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( ♯ ‘ 𝐵 ) ⟩ ) , ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ 𝐵 ) ) = ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( ( 𝐿 + ( ♯ ‘ 𝐵 ) ) − 𝐿 ) ⟩ ) )
27 iffalse ⊢ ( ¬ 𝐿 ≤ 𝑀 → if ( 𝐿 ≤ 𝑀 , ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( ♯ ‘ 𝐵 ) ⟩ ) , ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ 𝐵 ) ) = ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ 𝐵 ) )
28 27 3ad2ant3 ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ 𝑀 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ∧ ¬ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀 ) → if ( 𝐿 ≤ 𝑀 , ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( ♯ ‘ 𝐵 ) ⟩ ) , ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ 𝐵 ) ) = ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ 𝐵 ) )
29 20 adantr ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ 𝑀 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( ( 𝐿 + ( ♯ ‘ 𝐵 ) ) − 𝐿 ) = ( ♯ ‘ 𝐵 ) )
30 29 3ad2ant1 ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ 𝑀 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ∧ ¬ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀 ) → ( ( 𝐿 + ( ♯ ‘ 𝐵 ) ) − 𝐿 ) = ( ♯ ‘ 𝐵 ) )
31 30 oveq2d ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ 𝑀 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ∧ ¬ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀 ) → ( 𝐵 prefix ( ( 𝐿 + ( ♯ ‘ 𝐵 ) ) − 𝐿 ) ) = ( 𝐵 prefix ( ♯ ‘ 𝐵 ) ) )
32 pfxid ⊢ ( 𝐵 ∈ Word 𝑉 → ( 𝐵 prefix ( ♯ ‘ 𝐵 ) ) = 𝐵 )
33 32 adantl ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( 𝐵 prefix ( ♯ ‘ 𝐵 ) ) = 𝐵 )
34 33 adantr ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ 𝑀 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( 𝐵 prefix ( ♯ ‘ 𝐵 ) ) = 𝐵 )
35 34 3ad2ant1 ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ 𝑀 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ∧ ¬ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀 ) → ( 𝐵 prefix ( ♯ ‘ 𝐵 ) ) = 𝐵 )
36 31 35 eqtr2d ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ 𝑀 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ∧ ¬ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀 ) → 𝐵 = ( 𝐵 prefix ( ( 𝐿 + ( ♯ ‘ 𝐵 ) ) − 𝐿 ) ) )
37 36 oveq2d ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ 𝑀 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ∧ ¬ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀 ) → ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ 𝐵 ) = ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ ( 𝐵 prefix ( ( 𝐿 + ( ♯ ‘ 𝐵 ) ) − 𝐿 ) ) ) )
38 28 37 eqtrd ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ 𝑀 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ∧ ¬ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀 ) → if ( 𝐿 ≤ 𝑀 , ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( ♯ ‘ 𝐵 ) ⟩ ) , ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ 𝐵 ) ) = ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ ( 𝐵 prefix ( ( 𝐿 + ( ♯ ‘ 𝐵 ) ) − 𝐿 ) ) ) )
39 9 26 38 2if2 ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ 𝑀 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → if ( 𝐿 ≤ 𝑀 , ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( ♯ ‘ 𝐵 ) ⟩ ) , ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ 𝐵 ) ) = if ( ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ≤ 𝐿 , ( 𝐴 substr ⟨ 𝑀 , ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ⟩ ) , if ( 𝐿 ≤ 𝑀 , ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( ( 𝐿 + ( ♯ ‘ 𝐵 ) ) − 𝐿 ) ⟩ ) , ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ ( 𝐵 prefix ( ( 𝐿 + ( ♯ ‘ 𝐵 ) ) − 𝐿 ) ) ) ) ) )
40 8 39 eqtr4d ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ 𝑀 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ⟩ ) = if ( 𝐿 ≤ 𝑀 , ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( ♯ ‘ 𝐵 ) ⟩ ) , ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ 𝐵 ) ) )
41 40 ex ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( 𝑀 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) → ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ⟩ ) = if ( 𝐿 ≤ 𝑀 , ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( ♯ ‘ 𝐵 ) ⟩ ) , ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ 𝐵 ) ) ) )