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

Metamath Proof Explorer

Theorem swrdccat3blem

Description: Lemma for swrdccat3b . (Contributed by AV, 30-May-2018)

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

Proof

Step Hyp Ref Expression
1 swrdccatin2.l ⊢ 𝐿 = ( ♯ ‘ 𝐴 )
2 lencl ⊢ ( 𝐵 ∈ Word 𝑉 → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
3 nn0le0eq0 ⊢ ( ( ♯ ‘ 𝐵 ) ∈ ℕ0 → ( ( ♯ ‘ 𝐵 ) ≤ 0 ↔ ( ♯ ‘ 𝐵 ) = 0 ) )
4 3 biimpd ⊢ ( ( ♯ ‘ 𝐵 ) ∈ ℕ0 → ( ( ♯ ‘ 𝐵 ) ≤ 0 → ( ♯ ‘ 𝐵 ) = 0 ) )
5 2 4 syl ⊢ ( 𝐵 ∈ Word 𝑉 → ( ( ♯ ‘ 𝐵 ) ≤ 0 → ( ♯ ‘ 𝐵 ) = 0 ) )
6 5 adantl ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( ( ♯ ‘ 𝐵 ) ≤ 0 → ( ♯ ‘ 𝐵 ) = 0 ) )
7 hasheq0 ⊢ ( 𝐵 ∈ Word 𝑉 → ( ( ♯ ‘ 𝐵 ) = 0 ↔ 𝐵 = ∅ ) )
8 7 biimpd ⊢ ( 𝐵 ∈ Word 𝑉 → ( ( ♯ ‘ 𝐵 ) = 0 → 𝐵 = ∅ ) )
9 8 adantl ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( ( ♯ ‘ 𝐵 ) = 0 → 𝐵 = ∅ ) )
10 9 imp ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ♯ ‘ 𝐵 ) = 0 ) → 𝐵 = ∅ )
11 lencl ⊢ ( 𝐴 ∈ Word 𝑉 → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
12 1 eqcomi ⊢ ( ♯ ‘ 𝐴 ) = 𝐿
13 12 eleq1i ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 ↔ 𝐿 ∈ ℕ0 )
14 nn0re ⊢ ( 𝐿 ∈ ℕ0 → 𝐿 ∈ ℝ )
15 elfz2nn0 ⊢ ( 𝑀 ∈ ( 0 ... ( 𝐿 + 0 ) ) ↔ ( 𝑀 ∈ ℕ0 ∧ ( 𝐿 + 0 ) ∈ ℕ0 ∧ 𝑀 ≤ ( 𝐿 + 0 ) ) )
16 recn ⊢ ( 𝐿 ∈ ℝ → 𝐿 ∈ ℂ )
17 16 addridd ⊢ ( 𝐿 ∈ ℝ → ( 𝐿 + 0 ) = 𝐿 )
18 17 breq2d ⊢ ( 𝐿 ∈ ℝ → ( 𝑀 ≤ ( 𝐿 + 0 ) ↔ 𝑀 ≤ 𝐿 ) )
19 nn0re ⊢ ( 𝑀 ∈ ℕ0 → 𝑀 ∈ ℝ )
20 19 anim1i ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℝ ) → ( 𝑀 ∈ ℝ ∧ 𝐿 ∈ ℝ ) )
21 20 ancoms ⊢ ( ( 𝐿 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑀 ∈ ℝ ∧ 𝐿 ∈ ℝ ) )
22 letri3 ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝐿 ∈ ℝ ) → ( 𝑀 = 𝐿 ↔ ( 𝑀 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀 ) ) )
23 21 22 syl ⊢ ( ( 𝐿 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑀 = 𝐿 ↔ ( 𝑀 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀 ) ) )
24 23 biimprd ⊢ ( ( 𝐿 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑀 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀 ) → 𝑀 = 𝐿 ) )
25 24 exp4b ⊢ ( 𝐿 ∈ ℝ → ( 𝑀 ∈ ℕ0 → ( 𝑀 ≤ 𝐿 → ( 𝐿 ≤ 𝑀 → 𝑀 = 𝐿 ) ) ) )
26 25 com23 ⊢ ( 𝐿 ∈ ℝ → ( 𝑀 ≤ 𝐿 → ( 𝑀 ∈ ℕ0 → ( 𝐿 ≤ 𝑀 → 𝑀 = 𝐿 ) ) ) )
27 18 26 sylbid ⊢ ( 𝐿 ∈ ℝ → ( 𝑀 ≤ ( 𝐿 + 0 ) → ( 𝑀 ∈ ℕ0 → ( 𝐿 ≤ 𝑀 → 𝑀 = 𝐿 ) ) ) )
28 27 com3l ⊢ ( 𝑀 ≤ ( 𝐿 + 0 ) → ( 𝑀 ∈ ℕ0 → ( 𝐿 ∈ ℝ → ( 𝐿 ≤ 𝑀 → 𝑀 = 𝐿 ) ) ) )
29 28 impcom ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑀 ≤ ( 𝐿 + 0 ) ) → ( 𝐿 ∈ ℝ → ( 𝐿 ≤ 𝑀 → 𝑀 = 𝐿 ) ) )
30 29 3adant2 ⊢ ( ( 𝑀 ∈ ℕ0 ∧ ( 𝐿 + 0 ) ∈ ℕ0 ∧ 𝑀 ≤ ( 𝐿 + 0 ) ) → ( 𝐿 ∈ ℝ → ( 𝐿 ≤ 𝑀 → 𝑀 = 𝐿 ) ) )
31 30 com12 ⊢ ( 𝐿 ∈ ℝ → ( ( 𝑀 ∈ ℕ0 ∧ ( 𝐿 + 0 ) ∈ ℕ0 ∧ 𝑀 ≤ ( 𝐿 + 0 ) ) → ( 𝐿 ≤ 𝑀 → 𝑀 = 𝐿 ) ) )
32 15 31 biimtrid ⊢ ( 𝐿 ∈ ℝ → ( 𝑀 ∈ ( 0 ... ( 𝐿 + 0 ) ) → ( 𝐿 ≤ 𝑀 → 𝑀 = 𝐿 ) ) )
33 14 32 syl ⊢ ( 𝐿 ∈ ℕ0 → ( 𝑀 ∈ ( 0 ... ( 𝐿 + 0 ) ) → ( 𝐿 ≤ 𝑀 → 𝑀 = 𝐿 ) ) )
34 13 33 sylbi ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 → ( 𝑀 ∈ ( 0 ... ( 𝐿 + 0 ) ) → ( 𝐿 ≤ 𝑀 → 𝑀 = 𝐿 ) ) )
35 11 34 syl ⊢ ( 𝐴 ∈ Word 𝑉 → ( 𝑀 ∈ ( 0 ... ( 𝐿 + 0 ) ) → ( 𝐿 ≤ 𝑀 → 𝑀 = 𝐿 ) ) )
36 35 imp ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... ( 𝐿 + 0 ) ) ) → ( 𝐿 ≤ 𝑀 → 𝑀 = 𝐿 ) )
37 elfznn0 ⊢ ( 𝑀 ∈ ( 0 ... ( 𝐿 + 0 ) ) → 𝑀 ∈ ℕ0 )
38 swrd00 ⊢ ( ∅ substr ⟨ 0 , 0 ⟩ ) = ∅
39 swrd00 ⊢ ( 𝐴 substr ⟨ 𝐿 , 𝐿 ⟩ ) = ∅
40 38 39 eqtr4i ⊢ ( ∅ substr ⟨ 0 , 0 ⟩ ) = ( 𝐴 substr ⟨ 𝐿 , 𝐿 ⟩ )
41 nn0cn ⊢ ( 𝐿 ∈ ℕ0 → 𝐿 ∈ ℂ )
42 41 subidd ⊢ ( 𝐿 ∈ ℕ0 → ( 𝐿 − 𝐿 ) = 0 )
43 42 opeq1d ⊢ ( 𝐿 ∈ ℕ0 → ⟨ ( 𝐿 − 𝐿 ) , 0 ⟩ = ⟨ 0 , 0 ⟩ )
44 43 oveq2d ⊢ ( 𝐿 ∈ ℕ0 → ( ∅ substr ⟨ ( 𝐿 − 𝐿 ) , 0 ⟩ ) = ( ∅ substr ⟨ 0 , 0 ⟩ ) )
45 41 addridd ⊢ ( 𝐿 ∈ ℕ0 → ( 𝐿 + 0 ) = 𝐿 )
46 45 opeq2d ⊢ ( 𝐿 ∈ ℕ0 → ⟨ 𝐿 , ( 𝐿 + 0 ) ⟩ = ⟨ 𝐿 , 𝐿 ⟩ )
47 46 oveq2d ⊢ ( 𝐿 ∈ ℕ0 → ( 𝐴 substr ⟨ 𝐿 , ( 𝐿 + 0 ) ⟩ ) = ( 𝐴 substr ⟨ 𝐿 , 𝐿 ⟩ ) )
48 40 44 47 3eqtr4a ⊢ ( 𝐿 ∈ ℕ0 → ( ∅ substr ⟨ ( 𝐿 − 𝐿 ) , 0 ⟩ ) = ( 𝐴 substr ⟨ 𝐿 , ( 𝐿 + 0 ) ⟩ ) )
49 48 a1i ⊢ ( 𝑀 = 𝐿 → ( 𝐿 ∈ ℕ0 → ( ∅ substr ⟨ ( 𝐿 − 𝐿 ) , 0 ⟩ ) = ( 𝐴 substr ⟨ 𝐿 , ( 𝐿 + 0 ) ⟩ ) ) )
50 eleq1 ⊢ ( 𝑀 = 𝐿 → ( 𝑀 ∈ ℕ0 ↔ 𝐿 ∈ ℕ0 ) )
51 oveq1 ⊢ ( 𝑀 = 𝐿 → ( 𝑀 − 𝐿 ) = ( 𝐿 − 𝐿 ) )
52 51 opeq1d ⊢ ( 𝑀 = 𝐿 → ⟨ ( 𝑀 − 𝐿 ) , 0 ⟩ = ⟨ ( 𝐿 − 𝐿 ) , 0 ⟩ )
53 52 oveq2d ⊢ ( 𝑀 = 𝐿 → ( ∅ substr ⟨ ( 𝑀 − 𝐿 ) , 0 ⟩ ) = ( ∅ substr ⟨ ( 𝐿 − 𝐿 ) , 0 ⟩ ) )
54 opeq1 ⊢ ( 𝑀 = 𝐿 → ⟨ 𝑀 , ( 𝐿 + 0 ) ⟩ = ⟨ 𝐿 , ( 𝐿 + 0 ) ⟩ )
55 54 oveq2d ⊢ ( 𝑀 = 𝐿 → ( 𝐴 substr ⟨ 𝑀 , ( 𝐿 + 0 ) ⟩ ) = ( 𝐴 substr ⟨ 𝐿 , ( 𝐿 + 0 ) ⟩ ) )
56 53 55 eqeq12d ⊢ ( 𝑀 = 𝐿 → ( ( ∅ substr ⟨ ( 𝑀 − 𝐿 ) , 0 ⟩ ) = ( 𝐴 substr ⟨ 𝑀 , ( 𝐿 + 0 ) ⟩ ) ↔ ( ∅ substr ⟨ ( 𝐿 − 𝐿 ) , 0 ⟩ ) = ( 𝐴 substr ⟨ 𝐿 , ( 𝐿 + 0 ) ⟩ ) ) )
57 49 50 56 3imtr4d ⊢ ( 𝑀 = 𝐿 → ( 𝑀 ∈ ℕ0 → ( ∅ substr ⟨ ( 𝑀 − 𝐿 ) , 0 ⟩ ) = ( 𝐴 substr ⟨ 𝑀 , ( 𝐿 + 0 ) ⟩ ) ) )
58 57 com12 ⊢ ( 𝑀 ∈ ℕ0 → ( 𝑀 = 𝐿 → ( ∅ substr ⟨ ( 𝑀 − 𝐿 ) , 0 ⟩ ) = ( 𝐴 substr ⟨ 𝑀 , ( 𝐿 + 0 ) ⟩ ) ) )
59 58 a1d ⊢ ( 𝑀 ∈ ℕ0 → ( 𝐴 ∈ Word 𝑉 → ( 𝑀 = 𝐿 → ( ∅ substr ⟨ ( 𝑀 − 𝐿 ) , 0 ⟩ ) = ( 𝐴 substr ⟨ 𝑀 , ( 𝐿 + 0 ) ⟩ ) ) ) )
60 37 59 syl ⊢ ( 𝑀 ∈ ( 0 ... ( 𝐿 + 0 ) ) → ( 𝐴 ∈ Word 𝑉 → ( 𝑀 = 𝐿 → ( ∅ substr ⟨ ( 𝑀 − 𝐿 ) , 0 ⟩ ) = ( 𝐴 substr ⟨ 𝑀 , ( 𝐿 + 0 ) ⟩ ) ) ) )
61 60 impcom ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... ( 𝐿 + 0 ) ) ) → ( 𝑀 = 𝐿 → ( ∅ substr ⟨ ( 𝑀 − 𝐿 ) , 0 ⟩ ) = ( 𝐴 substr ⟨ 𝑀 , ( 𝐿 + 0 ) ⟩ ) ) )
62 36 61 syld ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... ( 𝐿 + 0 ) ) ) → ( 𝐿 ≤ 𝑀 → ( ∅ substr ⟨ ( 𝑀 − 𝐿 ) , 0 ⟩ ) = ( 𝐴 substr ⟨ 𝑀 , ( 𝐿 + 0 ) ⟩ ) ) )
63 62 imp ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... ( 𝐿 + 0 ) ) ) ∧ 𝐿 ≤ 𝑀 ) → ( ∅ substr ⟨ ( 𝑀 − 𝐿 ) , 0 ⟩ ) = ( 𝐴 substr ⟨ 𝑀 , ( 𝐿 + 0 ) ⟩ ) )
64 swrdcl ⊢ ( 𝐴 ∈ Word 𝑉 → ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ∈ Word 𝑉 )
65 ccatrid ⊢ ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ∈ Word 𝑉 → ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ ∅ ) = ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) )
66 64 65 syl ⊢ ( 𝐴 ∈ Word 𝑉 → ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ ∅ ) = ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) )
67 13 41 sylbi ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 → 𝐿 ∈ ℂ )
68 11 67 syl ⊢ ( 𝐴 ∈ Word 𝑉 → 𝐿 ∈ ℂ )
69 addrid ⊢ ( 𝐿 ∈ ℂ → ( 𝐿 + 0 ) = 𝐿 )
70 69 eqcomd ⊢ ( 𝐿 ∈ ℂ → 𝐿 = ( 𝐿 + 0 ) )
71 68 70 syl ⊢ ( 𝐴 ∈ Word 𝑉 → 𝐿 = ( 𝐿 + 0 ) )
72 71 opeq2d ⊢ ( 𝐴 ∈ Word 𝑉 → ⟨ 𝑀 , 𝐿 ⟩ = ⟨ 𝑀 , ( 𝐿 + 0 ) ⟩ )
73 72 oveq2d ⊢ ( 𝐴 ∈ Word 𝑉 → ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) = ( 𝐴 substr ⟨ 𝑀 , ( 𝐿 + 0 ) ⟩ ) )
74 66 73 eqtrd ⊢ ( 𝐴 ∈ Word 𝑉 → ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ ∅ ) = ( 𝐴 substr ⟨ 𝑀 , ( 𝐿 + 0 ) ⟩ ) )
75 74 adantr ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... ( 𝐿 + 0 ) ) ) → ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ ∅ ) = ( 𝐴 substr ⟨ 𝑀 , ( 𝐿 + 0 ) ⟩ ) )
76 75 adantr ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... ( 𝐿 + 0 ) ) ) ∧ ¬ 𝐿 ≤ 𝑀 ) → ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ ∅ ) = ( 𝐴 substr ⟨ 𝑀 , ( 𝐿 + 0 ) ⟩ ) )
77 63 76 ifeqda ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... ( 𝐿 + 0 ) ) ) → if ( 𝐿 ≤ 𝑀 , ( ∅ substr ⟨ ( 𝑀 − 𝐿 ) , 0 ⟩ ) , ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ ∅ ) ) = ( 𝐴 substr ⟨ 𝑀 , ( 𝐿 + 0 ) ⟩ ) )
78 77 ex ⊢ ( 𝐴 ∈ Word 𝑉 → ( 𝑀 ∈ ( 0 ... ( 𝐿 + 0 ) ) → if ( 𝐿 ≤ 𝑀 , ( ∅ substr ⟨ ( 𝑀 − 𝐿 ) , 0 ⟩ ) , ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ ∅ ) ) = ( 𝐴 substr ⟨ 𝑀 , ( 𝐿 + 0 ) ⟩ ) ) )
79 78 ad3antrrr ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ♯ ‘ 𝐵 ) = 0 ) ∧ 𝐵 = ∅ ) → ( 𝑀 ∈ ( 0 ... ( 𝐿 + 0 ) ) → if ( 𝐿 ≤ 𝑀 , ( ∅ substr ⟨ ( 𝑀 − 𝐿 ) , 0 ⟩ ) , ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ ∅ ) ) = ( 𝐴 substr ⟨ 𝑀 , ( 𝐿 + 0 ) ⟩ ) ) )
80 oveq2 ⊢ ( ( ♯ ‘ 𝐵 ) = 0 → ( 𝐿 + ( ♯ ‘ 𝐵 ) ) = ( 𝐿 + 0 ) )
81 80 oveq2d ⊢ ( ( ♯ ‘ 𝐵 ) = 0 → ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) = ( 0 ... ( 𝐿 + 0 ) ) )
82 81 eleq2d ⊢ ( ( ♯ ‘ 𝐵 ) = 0 → ( 𝑀 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ↔ 𝑀 ∈ ( 0 ... ( 𝐿 + 0 ) ) ) )
83 82 adantr ⊢ ( ( ( ♯ ‘ 𝐵 ) = 0 ∧ 𝐵 = ∅ ) → ( 𝑀 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ↔ 𝑀 ∈ ( 0 ... ( 𝐿 + 0 ) ) ) )
84 simpr ⊢ ( ( ( ♯ ‘ 𝐵 ) = 0 ∧ 𝐵 = ∅ ) → 𝐵 = ∅ )
85 opeq2 ⊢ ( ( ♯ ‘ 𝐵 ) = 0 → ⟨ ( 𝑀 − 𝐿 ) , ( ♯ ‘ 𝐵 ) ⟩ = ⟨ ( 𝑀 − 𝐿 ) , 0 ⟩ )
86 85 adantr ⊢ ( ( ( ♯ ‘ 𝐵 ) = 0 ∧ 𝐵 = ∅ ) → ⟨ ( 𝑀 − 𝐿 ) , ( ♯ ‘ 𝐵 ) ⟩ = ⟨ ( 𝑀 − 𝐿 ) , 0 ⟩ )
87 84 86 oveq12d ⊢ ( ( ( ♯ ‘ 𝐵 ) = 0 ∧ 𝐵 = ∅ ) → ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( ♯ ‘ 𝐵 ) ⟩ ) = ( ∅ substr ⟨ ( 𝑀 − 𝐿 ) , 0 ⟩ ) )
88 oveq2 ⊢ ( 𝐵 = ∅ → ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ 𝐵 ) = ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ ∅ ) )
89 88 adantl ⊢ ( ( ( ♯ ‘ 𝐵 ) = 0 ∧ 𝐵 = ∅ ) → ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ 𝐵 ) = ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ ∅ ) )
90 87 89 ifeq12d ⊢ ( ( ( ♯ ‘ 𝐵 ) = 0 ∧ 𝐵 = ∅ ) → if ( 𝐿 ≤ 𝑀 , ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( ♯ ‘ 𝐵 ) ⟩ ) , ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ 𝐵 ) ) = if ( 𝐿 ≤ 𝑀 , ( ∅ substr ⟨ ( 𝑀 − 𝐿 ) , 0 ⟩ ) , ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ ∅ ) ) )
91 80 opeq2d ⊢ ( ( ♯ ‘ 𝐵 ) = 0 → ⟨ 𝑀 , ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ⟩ = ⟨ 𝑀 , ( 𝐿 + 0 ) ⟩ )
92 91 oveq2d ⊢ ( ( ♯ ‘ 𝐵 ) = 0 → ( 𝐴 substr ⟨ 𝑀 , ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ⟩ ) = ( 𝐴 substr ⟨ 𝑀 , ( 𝐿 + 0 ) ⟩ ) )
93 92 adantr ⊢ ( ( ( ♯ ‘ 𝐵 ) = 0 ∧ 𝐵 = ∅ ) → ( 𝐴 substr ⟨ 𝑀 , ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ⟩ ) = ( 𝐴 substr ⟨ 𝑀 , ( 𝐿 + 0 ) ⟩ ) )
94 90 93 eqeq12d ⊢ ( ( ( ♯ ‘ 𝐵 ) = 0 ∧ 𝐵 = ∅ ) → ( if ( 𝐿 ≤ 𝑀 , ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( ♯ ‘ 𝐵 ) ⟩ ) , ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ 𝐵 ) ) = ( 𝐴 substr ⟨ 𝑀 , ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ⟩ ) ↔ if ( 𝐿 ≤ 𝑀 , ( ∅ substr ⟨ ( 𝑀 − 𝐿 ) , 0 ⟩ ) , ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ ∅ ) ) = ( 𝐴 substr ⟨ 𝑀 , ( 𝐿 + 0 ) ⟩ ) ) )
95 83 94 imbi12d ⊢ ( ( ( ♯ ‘ 𝐵 ) = 0 ∧ 𝐵 = ∅ ) → ( ( 𝑀 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) → if ( 𝐿 ≤ 𝑀 , ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( ♯ ‘ 𝐵 ) ⟩ ) , ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ 𝐵 ) ) = ( 𝐴 substr ⟨ 𝑀 , ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ⟩ ) ) ↔ ( 𝑀 ∈ ( 0 ... ( 𝐿 + 0 ) ) → if ( 𝐿 ≤ 𝑀 , ( ∅ substr ⟨ ( 𝑀 − 𝐿 ) , 0 ⟩ ) , ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ ∅ ) ) = ( 𝐴 substr ⟨ 𝑀 , ( 𝐿 + 0 ) ⟩ ) ) ) )
96 95 adantll ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ♯ ‘ 𝐵 ) = 0 ) ∧ 𝐵 = ∅ ) → ( ( 𝑀 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) → if ( 𝐿 ≤ 𝑀 , ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( ♯ ‘ 𝐵 ) ⟩ ) , ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ 𝐵 ) ) = ( 𝐴 substr ⟨ 𝑀 , ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ⟩ ) ) ↔ ( 𝑀 ∈ ( 0 ... ( 𝐿 + 0 ) ) → if ( 𝐿 ≤ 𝑀 , ( ∅ substr ⟨ ( 𝑀 − 𝐿 ) , 0 ⟩ ) , ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ ∅ ) ) = ( 𝐴 substr ⟨ 𝑀 , ( 𝐿 + 0 ) ⟩ ) ) ) )
97 79 96 mpbird ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ♯ ‘ 𝐵 ) = 0 ) ∧ 𝐵 = ∅ ) → ( 𝑀 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) → if ( 𝐿 ≤ 𝑀 , ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( ♯ ‘ 𝐵 ) ⟩ ) , ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ 𝐵 ) ) = ( 𝐴 substr ⟨ 𝑀 , ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ⟩ ) ) )
98 10 97 mpdan ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ♯ ‘ 𝐵 ) = 0 ) → ( 𝑀 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) → if ( 𝐿 ≤ 𝑀 , ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( ♯ ‘ 𝐵 ) ⟩ ) , ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ 𝐵 ) ) = ( 𝐴 substr ⟨ 𝑀 , ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ⟩ ) ) )
99 98 ex ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( ( ♯ ‘ 𝐵 ) = 0 → ( 𝑀 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) → if ( 𝐿 ≤ 𝑀 , ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( ♯ ‘ 𝐵 ) ⟩ ) , ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ 𝐵 ) ) = ( 𝐴 substr ⟨ 𝑀 , ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ⟩ ) ) ) )
100 6 99 syld ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( ( ♯ ‘ 𝐵 ) ≤ 0 → ( 𝑀 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) → if ( 𝐿 ≤ 𝑀 , ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( ♯ ‘ 𝐵 ) ⟩ ) , ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ 𝐵 ) ) = ( 𝐴 substr ⟨ 𝑀 , ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ⟩ ) ) ) )
101 100 com23 ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( 𝑀 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) → ( ( ♯ ‘ 𝐵 ) ≤ 0 → if ( 𝐿 ≤ 𝑀 , ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( ♯ ‘ 𝐵 ) ⟩ ) , ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ 𝐵 ) ) = ( 𝐴 substr ⟨ 𝑀 , ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ⟩ ) ) ) )
102 101 imp ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ 𝑀 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( ( ♯ ‘ 𝐵 ) ≤ 0 → if ( 𝐿 ≤ 𝑀 , ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( ♯ ‘ 𝐵 ) ⟩ ) , ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ 𝐵 ) ) = ( 𝐴 substr ⟨ 𝑀 , ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ⟩ ) ) )
103 102 adantr ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ 𝑀 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ∧ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ≤ 𝐿 ) → ( ( ♯ ‘ 𝐵 ) ≤ 0 → if ( 𝐿 ≤ 𝑀 , ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( ♯ ‘ 𝐵 ) ⟩ ) , ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ 𝐵 ) ) = ( 𝐴 substr ⟨ 𝑀 , ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ⟩ ) ) )
104 1 eleq1i ⊢ ( 𝐿 ∈ ℕ0 ↔ ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
105 104 14 sylbir ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 → 𝐿 ∈ ℝ )
106 11 105 syl ⊢ ( 𝐴 ∈ Word 𝑉 → 𝐿 ∈ ℝ )
107 2 nn0red ⊢ ( 𝐵 ∈ Word 𝑉 → ( ♯ ‘ 𝐵 ) ∈ ℝ )
108 leaddle0 ⊢ ( ( 𝐿 ∈ ℝ ∧ ( ♯ ‘ 𝐵 ) ∈ ℝ ) → ( ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ≤ 𝐿 ↔ ( ♯ ‘ 𝐵 ) ≤ 0 ) )
109 106 107 108 syl2an ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ≤ 𝐿 ↔ ( ♯ ‘ 𝐵 ) ≤ 0 ) )
110 pm2.24 ⊢ ( ( ♯ ‘ 𝐵 ) ≤ 0 → ( ¬ ( ♯ ‘ 𝐵 ) ≤ 0 → if ( 𝐿 ≤ 𝑀 , ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( ♯ ‘ 𝐵 ) ⟩ ) , ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ 𝐵 ) ) = ( 𝐴 substr ⟨ 𝑀 , ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ⟩ ) ) )
111 109 110 biimtrdi ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ≤ 𝐿 → ( ¬ ( ♯ ‘ 𝐵 ) ≤ 0 → if ( 𝐿 ≤ 𝑀 , ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( ♯ ‘ 𝐵 ) ⟩ ) , ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ 𝐵 ) ) = ( 𝐴 substr ⟨ 𝑀 , ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ⟩ ) ) ) )
112 111 adantr ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ 𝑀 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ≤ 𝐿 → ( ¬ ( ♯ ‘ 𝐵 ) ≤ 0 → if ( 𝐿 ≤ 𝑀 , ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( ♯ ‘ 𝐵 ) ⟩ ) , ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ 𝐵 ) ) = ( 𝐴 substr ⟨ 𝑀 , ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ⟩ ) ) ) )
113 112 imp ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ 𝑀 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ∧ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ≤ 𝐿 ) → ( ¬ ( ♯ ‘ 𝐵 ) ≤ 0 → if ( 𝐿 ≤ 𝑀 , ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( ♯ ‘ 𝐵 ) ⟩ ) , ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ 𝐵 ) ) = ( 𝐴 substr ⟨ 𝑀 , ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ⟩ ) ) )
114 103 113 pm2.61d ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ 𝑀 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ∧ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ≤ 𝐿 ) → if ( 𝐿 ≤ 𝑀 , ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( ♯ ‘ 𝐵 ) ⟩ ) , ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ 𝐵 ) ) = ( 𝐴 substr ⟨ 𝑀 , ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ⟩ ) )