spllen

Description: The length of a splice. (Contributed by Stefan O'Rear, 23-Aug-2015) (Proof shortened by AV, 15-Oct-2022)

	Ref	Expression
Hypotheses	spllen.s	$⊢ φ \to S \in Word A$
	spllen.f	$⊢ φ \to F \in (0 \dots T)$
	spllen.t	$⊢ φ \to T \in (0 \dots \|S\|)$
	spllen.r	$⊢ φ \to R \in Word A$
Assertion	spllen	$⊢ φ \to \|S splice ⟨F, T, R⟩\| = \|S\| + \|R\| - (T - F)$

Proof

Step	Hyp	Ref	Expression
1		spllen.s	$⊢ φ \to S \in Word A$
2		spllen.f	$⊢ φ \to F \in (0 \dots T)$
3		spllen.t	$⊢ φ \to T \in (0 \dots \|S\|)$
4		spllen.r	$⊢ φ \to R \in Word A$
5		splval	$⊢ (S \in Word A \land (F \in (0 \dots T) \land T \in (0 \dots \|S\|) \land R \in Word A)) \to S splice ⟨F, T, R⟩ = ((S prefix F) ++ R) ++ (S substr ⟨T, \|S\|⟩)$
6	1 2 3 4 5	syl13anc	$⊢ φ \to S splice ⟨F, T, R⟩ = ((S prefix F) ++ R) ++ (S substr ⟨T, \|S\|⟩)$
7	6	fveq2d	$⊢ φ \to \|S splice ⟨F, T, R⟩\| = \|((S prefix F) ++ R) ++ (S substr ⟨T, \|S\|⟩)\|$
8		pfxcl	$⊢ S \in Word A \to S prefix F \in Word A$
9	1 8	syl	$⊢ φ \to S prefix F \in Word A$
10		ccatcl	$⊢ (S prefix F \in Word A \land R \in Word A) \to (S prefix F) ++ R \in Word A$
11	9 4 10	syl2anc	$⊢ φ \to (S prefix F) ++ R \in Word A$
12		swrdcl	$⊢ S \in Word A \to S substr ⟨T, \|S\|⟩ \in Word A$
13	1 12	syl	$⊢ φ \to S substr ⟨T, \|S\|⟩ \in Word A$
14		ccatlen	$⊢ ((S prefix F) ++ R \in Word A \land S substr ⟨T, \|S\|⟩ \in Word A) \to \|((S prefix F) ++ R) ++ (S substr ⟨T, \|S\|⟩)\| = \|(S prefix F) ++ R\| + \|S substr ⟨T, \|S\|⟩\|$
15	11 13 14	syl2anc	$⊢ φ \to \|((S prefix F) ++ R) ++ (S substr ⟨T, \|S\|⟩)\| = \|(S prefix F) ++ R\| + \|S substr ⟨T, \|S\|⟩\|$
16		lencl	$⊢ R \in Word A \to \|R\| \in ℕ_{0}$
17	16	nn0cnd	$⊢ R \in Word A \to \|R\| \in ℂ$
18	4 17	syl	$⊢ φ \to \|R\| \in ℂ$
19		elfzelz	$⊢ F \in (0 \dots T) \to F \in ℤ$
20	19	zcnd	$⊢ F \in (0 \dots T) \to F \in ℂ$
21	2 20	syl	$⊢ φ \to F \in ℂ$
22	18 21	addcld	$⊢ φ \to \|R\| + F \in ℂ$
23		elfzel2	$⊢ T \in (0 \dots \|S\|) \to \|S\| \in ℤ$
24	23	zcnd	$⊢ T \in (0 \dots \|S\|) \to \|S\| \in ℂ$
25	3 24	syl	$⊢ φ \to \|S\| \in ℂ$
26		elfzelz	$⊢ T \in (0 \dots \|S\|) \to T \in ℤ$
27	26	zcnd	$⊢ T \in (0 \dots \|S\|) \to T \in ℂ$
28	3 27	syl	$⊢ φ \to T \in ℂ$
29	22 25 28	addsub12d	$⊢ φ \to \|R\| + F + (\|S\| - T) = \|S\| + (\|R\| + F) - T$
30		ccatlen	$⊢ (S prefix F \in Word A \land R \in Word A) \to \|(S prefix F) ++ R\| = \|S prefix F\| + \|R\|$
31	9 4 30	syl2anc	$⊢ φ \to \|(S prefix F) ++ R\| = \|S prefix F\| + \|R\|$
32		elfzuz	$⊢ F \in (0 \dots T) \to F \in ℤ_{\geq 0}$
33	2 32	syl	$⊢ φ \to F \in ℤ_{\geq 0}$
34		elfzuz3	$⊢ T \in (0 \dots \|S\|) \to \|S\| \in ℤ_{\geq T}$
35	3 34	syl	$⊢ φ \to \|S\| \in ℤ_{\geq T}$
36		elfzuz3	$⊢ F \in (0 \dots T) \to T \in ℤ_{\geq F}$
37	2 36	syl	$⊢ φ \to T \in ℤ_{\geq F}$
38		uztrn	$⊢ (\|S\| \in ℤ_{\geq T} \land T \in ℤ_{\geq F}) \to \|S\| \in ℤ_{\geq F}$
39	35 37 38	syl2anc	$⊢ φ \to \|S\| \in ℤ_{\geq F}$
40		elfzuzb	$⊢ F \in (0 \dots \|S\|) \leftrightarrow (F \in ℤ_{\geq 0} \land \|S\| \in ℤ_{\geq F})$
41	33 39 40	sylanbrc	$⊢ φ \to F \in (0 \dots \|S\|)$
42		pfxlen	$⊢ (S \in Word A \land F \in (0 \dots \|S\|)) \to \|S prefix F\| = F$
43	1 41 42	syl2anc	$⊢ φ \to \|S prefix F\| = F$
44	43	oveq1d	$⊢ φ \to \|S prefix F\| + \|R\| = F + \|R\|$
45	21 18	addcomd	$⊢ φ \to F + \|R\| = \|R\| + F$
46	31 44 45	3eqtrd	$⊢ φ \to \|(S prefix F) ++ R\| = \|R\| + F$
47		elfzuz2	$⊢ T \in (0 \dots \|S\|) \to \|S\| \in ℤ_{\geq 0}$
48		eluzfz2	$⊢ \|S\| \in ℤ_{\geq 0} \to \|S\| \in (0 \dots \|S\|)$
49	3 47 48	3syl	$⊢ φ \to \|S\| \in (0 \dots \|S\|)$
50		swrdlen	$⊢ (S \in Word A \land T \in (0 \dots \|S\|) \land \|S\| \in (0 \dots \|S\|)) \to \|S substr ⟨T, \|S\|⟩\| = \|S\| - T$
51	1 3 49 50	syl3anc	$⊢ φ \to \|S substr ⟨T, \|S\|⟩\| = \|S\| - T$
52	46 51	oveq12d	$⊢ φ \to \|(S prefix F) ++ R\| + \|S substr ⟨T, \|S\|⟩\| = \|R\| + F + (\|S\| - T)$
53	18 28 21	subsub3d	$⊢ φ \to \|R\| - (T - F) = \|R\| + F - T$
54	53	oveq2d	$⊢ φ \to \|S\| + \|R\| - (T - F) = \|S\| + (\|R\| + F) - T$
55	29 52 54	3eqtr4d	$⊢ φ \to \|(S prefix F) ++ R\| + \|S substr ⟨T, \|S\|⟩\| = \|S\| + \|R\| - (T - F)$
56	7 15 55	3eqtrd	$⊢ φ \to \|S splice ⟨F, T, R⟩\| = \|S\| + \|R\| - (T - F)$

Metamath Proof Explorer

Theorem spllen

Proof