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

Metamath Proof Explorer

Theorem pfxccat3a

Description: A prefix of a concatenation is either a prefix of the first concatenated word or a concatenation of the first word with a prefix of the second word. (Contributed by Alexander van der Vekens, 31-Mar-2018) (Revised by AV, 10-May-2020)

Ref Expression
Hypotheses swrdccatin2.l ⊢ 𝐿 = ( ♯ ‘ 𝐴 )
pfxccatpfx2.m ⊢ 𝑀 = ( ♯ ‘ 𝐵 )
Assertion pfxccat3a ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( 𝑁 ∈ ( 0 ... ( 𝐿 + 𝑀 ) ) → ( ( 𝐴 ++ 𝐵 ) prefix 𝑁 ) = if ( 𝑁 ≤ 𝐿 , ( 𝐴 prefix 𝑁 ) , ( 𝐴 ++ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 swrdccatin2.l ⊢ 𝐿 = ( ♯ ‘ 𝐴 )
2 pfxccatpfx2.m ⊢ 𝑀 = ( ♯ ‘ 𝐵 )
3 simprl ⊢ ( ( 𝑁 ≤ 𝐿 ∧ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + 𝑀 ) ) ) ) → ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) )
4 elfznn0 ⊢ ( 𝑁 ∈ ( 0 ... ( 𝐿 + 𝑀 ) ) → 𝑁 ∈ ℕ0 )
5 4 adantl ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + 𝑀 ) ) ) → 𝑁 ∈ ℕ0 )
6 5 adantl ⊢ ( ( 𝑁 ≤ 𝐿 ∧ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + 𝑀 ) ) ) ) → 𝑁 ∈ ℕ0 )
7 lencl ⊢ ( 𝐴 ∈ Word 𝑉 → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
8 1 7 eqeltrid ⊢ ( 𝐴 ∈ Word 𝑉 → 𝐿 ∈ ℕ0 )
9 8 adantr ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → 𝐿 ∈ ℕ0 )
10 9 adantr ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + 𝑀 ) ) ) → 𝐿 ∈ ℕ0 )
11 10 adantl ⊢ ( ( 𝑁 ≤ 𝐿 ∧ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + 𝑀 ) ) ) ) → 𝐿 ∈ ℕ0 )
12 simpl ⊢ ( ( 𝑁 ≤ 𝐿 ∧ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + 𝑀 ) ) ) ) → 𝑁 ≤ 𝐿 )
13 elfz2nn0 ⊢ ( 𝑁 ∈ ( 0 ... 𝐿 ) ↔ ( 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝑁 ≤ 𝐿 ) )
14 6 11 12 13 syl3anbrc ⊢ ( ( 𝑁 ≤ 𝐿 ∧ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + 𝑀 ) ) ) ) → 𝑁 ∈ ( 0 ... 𝐿 ) )
15 df-3an ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... 𝐿 ) ) ↔ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ 𝑁 ∈ ( 0 ... 𝐿 ) ) )
16 3 14 15 sylanbrc ⊢ ( ( 𝑁 ≤ 𝐿 ∧ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + 𝑀 ) ) ) ) → ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... 𝐿 ) ) )
17 1 pfxccatpfx1 ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... 𝐿 ) ) → ( ( 𝐴 ++ 𝐵 ) prefix 𝑁 ) = ( 𝐴 prefix 𝑁 ) )
18 16 17 syl ⊢ ( ( 𝑁 ≤ 𝐿 ∧ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + 𝑀 ) ) ) ) → ( ( 𝐴 ++ 𝐵 ) prefix 𝑁 ) = ( 𝐴 prefix 𝑁 ) )
19 iftrue ⊢ ( 𝑁 ≤ 𝐿 → if ( 𝑁 ≤ 𝐿 , ( 𝐴 prefix 𝑁 ) , ( 𝐴 ++ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) ) = ( 𝐴 prefix 𝑁 ) )
20 19 adantr ⊢ ( ( 𝑁 ≤ 𝐿 ∧ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + 𝑀 ) ) ) ) → if ( 𝑁 ≤ 𝐿 , ( 𝐴 prefix 𝑁 ) , ( 𝐴 ++ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) ) = ( 𝐴 prefix 𝑁 ) )
21 18 20 eqtr4d ⊢ ( ( 𝑁 ≤ 𝐿 ∧ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + 𝑀 ) ) ) ) → ( ( 𝐴 ++ 𝐵 ) prefix 𝑁 ) = if ( 𝑁 ≤ 𝐿 , ( 𝐴 prefix 𝑁 ) , ( 𝐴 ++ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) ) )
22 simprl ⊢ ( ( ¬ 𝑁 ≤ 𝐿 ∧ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + 𝑀 ) ) ) ) → ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) )
23 elfz2nn0 ⊢ ( 𝑁 ∈ ( 0 ... ( 𝐿 + 𝑀 ) ) ↔ ( 𝑁 ∈ ℕ0 ∧ ( 𝐿 + 𝑀 ) ∈ ℕ0 ∧ 𝑁 ≤ ( 𝐿 + 𝑀 ) ) )
24 1 eleq1i ⊢ ( 𝐿 ∈ ℕ0 ↔ ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
25 nn0ltp1le ⊢ ( ( 𝐿 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝐿 < 𝑁 ↔ ( 𝐿 + 1 ) ≤ 𝑁 ) )
26 nn0re ⊢ ( 𝐿 ∈ ℕ0 → 𝐿 ∈ ℝ )
27 nn0re ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
28 ltnle ⊢ ( ( 𝐿 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝐿 < 𝑁 ↔ ¬ 𝑁 ≤ 𝐿 ) )
29 26 27 28 syl2an ⊢ ( ( 𝐿 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝐿 < 𝑁 ↔ ¬ 𝑁 ≤ 𝐿 ) )
30 25 29 bitr3d ⊢ ( ( 𝐿 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐿 + 1 ) ≤ 𝑁 ↔ ¬ 𝑁 ≤ 𝐿 ) )
31 30 3ad2antr1 ⊢ ( ( 𝐿 ∈ ℕ0 ∧ ( 𝑁 ∈ ℕ0 ∧ ( 𝐿 + 𝑀 ) ∈ ℕ0 ∧ 𝑁 ≤ ( 𝐿 + 𝑀 ) ) ) → ( ( 𝐿 + 1 ) ≤ 𝑁 ↔ ¬ 𝑁 ≤ 𝐿 ) )
32 simpr3 ⊢ ( ( 𝐿 ∈ ℕ0 ∧ ( 𝑁 ∈ ℕ0 ∧ ( 𝐿 + 𝑀 ) ∈ ℕ0 ∧ 𝑁 ≤ ( 𝐿 + 𝑀 ) ) ) → 𝑁 ≤ ( 𝐿 + 𝑀 ) )
33 32 anim1ci ⊢ ( ( ( 𝐿 ∈ ℕ0 ∧ ( 𝑁 ∈ ℕ0 ∧ ( 𝐿 + 𝑀 ) ∈ ℕ0 ∧ 𝑁 ≤ ( 𝐿 + 𝑀 ) ) ) ∧ ( 𝐿 + 1 ) ≤ 𝑁 ) → ( ( 𝐿 + 1 ) ≤ 𝑁 ∧ 𝑁 ≤ ( 𝐿 + 𝑀 ) ) )
34 nn0z ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
35 34 3ad2ant1 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝐿 + 𝑀 ) ∈ ℕ0 ∧ 𝑁 ≤ ( 𝐿 + 𝑀 ) ) → 𝑁 ∈ ℤ )
36 35 adantl ⊢ ( ( 𝐿 ∈ ℕ0 ∧ ( 𝑁 ∈ ℕ0 ∧ ( 𝐿 + 𝑀 ) ∈ ℕ0 ∧ 𝑁 ≤ ( 𝐿 + 𝑀 ) ) ) → 𝑁 ∈ ℤ )
37 36 adantr ⊢ ( ( ( 𝐿 ∈ ℕ0 ∧ ( 𝑁 ∈ ℕ0 ∧ ( 𝐿 + 𝑀 ) ∈ ℕ0 ∧ 𝑁 ≤ ( 𝐿 + 𝑀 ) ) ) ∧ ( 𝐿 + 1 ) ≤ 𝑁 ) → 𝑁 ∈ ℤ )
38 peano2nn0 ⊢ ( 𝐿 ∈ ℕ0 → ( 𝐿 + 1 ) ∈ ℕ0 )
39 38 nn0zd ⊢ ( 𝐿 ∈ ℕ0 → ( 𝐿 + 1 ) ∈ ℤ )
40 39 adantr ⊢ ( ( 𝐿 ∈ ℕ0 ∧ ( 𝑁 ∈ ℕ0 ∧ ( 𝐿 + 𝑀 ) ∈ ℕ0 ∧ 𝑁 ≤ ( 𝐿 + 𝑀 ) ) ) → ( 𝐿 + 1 ) ∈ ℤ )
41 40 adantr ⊢ ( ( ( 𝐿 ∈ ℕ0 ∧ ( 𝑁 ∈ ℕ0 ∧ ( 𝐿 + 𝑀 ) ∈ ℕ0 ∧ 𝑁 ≤ ( 𝐿 + 𝑀 ) ) ) ∧ ( 𝐿 + 1 ) ≤ 𝑁 ) → ( 𝐿 + 1 ) ∈ ℤ )
42 nn0z ⊢ ( ( 𝐿 + 𝑀 ) ∈ ℕ0 → ( 𝐿 + 𝑀 ) ∈ ℤ )
43 42 3ad2ant2 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝐿 + 𝑀 ) ∈ ℕ0 ∧ 𝑁 ≤ ( 𝐿 + 𝑀 ) ) → ( 𝐿 + 𝑀 ) ∈ ℤ )
44 43 adantl ⊢ ( ( 𝐿 ∈ ℕ0 ∧ ( 𝑁 ∈ ℕ0 ∧ ( 𝐿 + 𝑀 ) ∈ ℕ0 ∧ 𝑁 ≤ ( 𝐿 + 𝑀 ) ) ) → ( 𝐿 + 𝑀 ) ∈ ℤ )
45 44 adantr ⊢ ( ( ( 𝐿 ∈ ℕ0 ∧ ( 𝑁 ∈ ℕ0 ∧ ( 𝐿 + 𝑀 ) ∈ ℕ0 ∧ 𝑁 ≤ ( 𝐿 + 𝑀 ) ) ) ∧ ( 𝐿 + 1 ) ≤ 𝑁 ) → ( 𝐿 + 𝑀 ) ∈ ℤ )
46 elfz ⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝐿 + 1 ) ∈ ℤ ∧ ( 𝐿 + 𝑀 ) ∈ ℤ ) → ( 𝑁 ∈ ( ( 𝐿 + 1 ) ... ( 𝐿 + 𝑀 ) ) ↔ ( ( 𝐿 + 1 ) ≤ 𝑁 ∧ 𝑁 ≤ ( 𝐿 + 𝑀 ) ) ) )
47 37 41 45 46 syl3anc ⊢ ( ( ( 𝐿 ∈ ℕ0 ∧ ( 𝑁 ∈ ℕ0 ∧ ( 𝐿 + 𝑀 ) ∈ ℕ0 ∧ 𝑁 ≤ ( 𝐿 + 𝑀 ) ) ) ∧ ( 𝐿 + 1 ) ≤ 𝑁 ) → ( 𝑁 ∈ ( ( 𝐿 + 1 ) ... ( 𝐿 + 𝑀 ) ) ↔ ( ( 𝐿 + 1 ) ≤ 𝑁 ∧ 𝑁 ≤ ( 𝐿 + 𝑀 ) ) ) )
48 33 47 mpbird ⊢ ( ( ( 𝐿 ∈ ℕ0 ∧ ( 𝑁 ∈ ℕ0 ∧ ( 𝐿 + 𝑀 ) ∈ ℕ0 ∧ 𝑁 ≤ ( 𝐿 + 𝑀 ) ) ) ∧ ( 𝐿 + 1 ) ≤ 𝑁 ) → 𝑁 ∈ ( ( 𝐿 + 1 ) ... ( 𝐿 + 𝑀 ) ) )
49 48 ex ⊢ ( ( 𝐿 ∈ ℕ0 ∧ ( 𝑁 ∈ ℕ0 ∧ ( 𝐿 + 𝑀 ) ∈ ℕ0 ∧ 𝑁 ≤ ( 𝐿 + 𝑀 ) ) ) → ( ( 𝐿 + 1 ) ≤ 𝑁 → 𝑁 ∈ ( ( 𝐿 + 1 ) ... ( 𝐿 + 𝑀 ) ) ) )
50 31 49 sylbird ⊢ ( ( 𝐿 ∈ ℕ0 ∧ ( 𝑁 ∈ ℕ0 ∧ ( 𝐿 + 𝑀 ) ∈ ℕ0 ∧ 𝑁 ≤ ( 𝐿 + 𝑀 ) ) ) → ( ¬ 𝑁 ≤ 𝐿 → 𝑁 ∈ ( ( 𝐿 + 1 ) ... ( 𝐿 + 𝑀 ) ) ) )
51 50 ex ⊢ ( 𝐿 ∈ ℕ0 → ( ( 𝑁 ∈ ℕ0 ∧ ( 𝐿 + 𝑀 ) ∈ ℕ0 ∧ 𝑁 ≤ ( 𝐿 + 𝑀 ) ) → ( ¬ 𝑁 ≤ 𝐿 → 𝑁 ∈ ( ( 𝐿 + 1 ) ... ( 𝐿 + 𝑀 ) ) ) ) )
52 24 51 sylbir ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 → ( ( 𝑁 ∈ ℕ0 ∧ ( 𝐿 + 𝑀 ) ∈ ℕ0 ∧ 𝑁 ≤ ( 𝐿 + 𝑀 ) ) → ( ¬ 𝑁 ≤ 𝐿 → 𝑁 ∈ ( ( 𝐿 + 1 ) ... ( 𝐿 + 𝑀 ) ) ) ) )
53 7 52 syl ⊢ ( 𝐴 ∈ Word 𝑉 → ( ( 𝑁 ∈ ℕ0 ∧ ( 𝐿 + 𝑀 ) ∈ ℕ0 ∧ 𝑁 ≤ ( 𝐿 + 𝑀 ) ) → ( ¬ 𝑁 ≤ 𝐿 → 𝑁 ∈ ( ( 𝐿 + 1 ) ... ( 𝐿 + 𝑀 ) ) ) ) )
54 53 adantr ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( ( 𝑁 ∈ ℕ0 ∧ ( 𝐿 + 𝑀 ) ∈ ℕ0 ∧ 𝑁 ≤ ( 𝐿 + 𝑀 ) ) → ( ¬ 𝑁 ≤ 𝐿 → 𝑁 ∈ ( ( 𝐿 + 1 ) ... ( 𝐿 + 𝑀 ) ) ) ) )
55 23 54 biimtrid ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( 𝑁 ∈ ( 0 ... ( 𝐿 + 𝑀 ) ) → ( ¬ 𝑁 ≤ 𝐿 → 𝑁 ∈ ( ( 𝐿 + 1 ) ... ( 𝐿 + 𝑀 ) ) ) ) )
56 55 imp ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + 𝑀 ) ) ) → ( ¬ 𝑁 ≤ 𝐿 → 𝑁 ∈ ( ( 𝐿 + 1 ) ... ( 𝐿 + 𝑀 ) ) ) )
57 56 impcom ⊢ ( ( ¬ 𝑁 ≤ 𝐿 ∧ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + 𝑀 ) ) ) ) → 𝑁 ∈ ( ( 𝐿 + 1 ) ... ( 𝐿 + 𝑀 ) ) )
58 df-3an ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ( ( 𝐿 + 1 ) ... ( 𝐿 + 𝑀 ) ) ) ↔ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ 𝑁 ∈ ( ( 𝐿 + 1 ) ... ( 𝐿 + 𝑀 ) ) ) )
59 22 57 58 sylanbrc ⊢ ( ( ¬ 𝑁 ≤ 𝐿 ∧ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + 𝑀 ) ) ) ) → ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ( ( 𝐿 + 1 ) ... ( 𝐿 + 𝑀 ) ) ) )
60 1 2 pfxccatpfx2 ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ( ( 𝐿 + 1 ) ... ( 𝐿 + 𝑀 ) ) ) → ( ( 𝐴 ++ 𝐵 ) prefix 𝑁 ) = ( 𝐴 ++ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) )
61 59 60 syl ⊢ ( ( ¬ 𝑁 ≤ 𝐿 ∧ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + 𝑀 ) ) ) ) → ( ( 𝐴 ++ 𝐵 ) prefix 𝑁 ) = ( 𝐴 ++ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) )
62 iffalse ⊢ ( ¬ 𝑁 ≤ 𝐿 → if ( 𝑁 ≤ 𝐿 , ( 𝐴 prefix 𝑁 ) , ( 𝐴 ++ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) ) = ( 𝐴 ++ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) )
63 62 adantr ⊢ ( ( ¬ 𝑁 ≤ 𝐿 ∧ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + 𝑀 ) ) ) ) → if ( 𝑁 ≤ 𝐿 , ( 𝐴 prefix 𝑁 ) , ( 𝐴 ++ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) ) = ( 𝐴 ++ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) )
64 61 63 eqtr4d ⊢ ( ( ¬ 𝑁 ≤ 𝐿 ∧ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + 𝑀 ) ) ) ) → ( ( 𝐴 ++ 𝐵 ) prefix 𝑁 ) = if ( 𝑁 ≤ 𝐿 , ( 𝐴 prefix 𝑁 ) , ( 𝐴 ++ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) ) )
65 21 64 pm2.61ian ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + 𝑀 ) ) ) → ( ( 𝐴 ++ 𝐵 ) prefix 𝑁 ) = if ( 𝑁 ≤ 𝐿 , ( 𝐴 prefix 𝑁 ) , ( 𝐴 ++ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) ) )
66 65 ex ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( 𝑁 ∈ ( 0 ... ( 𝐿 + 𝑀 ) ) → ( ( 𝐴 ++ 𝐵 ) prefix 𝑁 ) = if ( 𝑁 ≤ 𝐿 , ( 𝐴 prefix 𝑁 ) , ( 𝐴 ++ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) ) ) )