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	syl5bi	⊢ ( ( 𝐴 ∈ 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 ( 𝑁 − 𝐿 ) ) ) ) ) )