splfv3

Description: Symbols to the right of a splice are unaffected. (Contributed by Thierry Arnoux, 14-Dec-2023)

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

Proof

Step	Hyp	Ref	Expression
1		splfv3.s	$⊢ φ \to S \in Word A$
2		splfv3.f	$⊢ φ \to F \in (0 \dots T)$
3		splfv3.t	$⊢ φ \to T \in (0 \dots \|S\|)$
4		splfv3.r	$⊢ φ \to R \in Word A$
5		splfv3.x	$⊢ φ \to X \in (0 ..^\|S\| - T)$
6		splfv3.k	$⊢ φ \to K = F + \|R\|$
7		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\|⟩)$
8	1 2 3 4 7	syl13anc	$⊢ φ \to S splice ⟨F, T, R⟩ = ((S prefix F) ++ R) ++ (S substr ⟨T, \|S\|⟩)$
9		elfzuz3	$⊢ T \in (0 \dots \|S\|) \to \|S\| \in ℤ_{\geq T}$
10		fzss2	$⊢ \|S\| \in ℤ_{\geq T} \to (0 \dots T) \subseteq (0 \dots \|S\|)$
11	3 9 10	3syl	$⊢ φ \to (0 \dots T) \subseteq (0 \dots \|S\|)$
12	11 2	sseldd	$⊢ φ \to F \in (0 \dots \|S\|)$
13		pfxlen	$⊢ (S \in Word A \land F \in (0 \dots \|S\|)) \to \|S prefix F\| = F$
14	1 12 13	syl2anc	$⊢ φ \to \|S prefix F\| = F$
15	14	oveq1d	$⊢ φ \to \|S prefix F\| + \|R\| = F + \|R\|$
16		pfxcl	$⊢ S \in Word A \to S prefix F \in Word A$
17	1 16	syl	$⊢ φ \to S prefix F \in Word A$
18		ccatlen	$⊢ (S prefix F \in Word A \land R \in Word A) \to \|(S prefix F) ++ R\| = \|S prefix F\| + \|R\|$
19	17 4 18	syl2anc	$⊢ φ \to \|(S prefix F) ++ R\| = \|S prefix F\| + \|R\|$
20	15 19 6	3eqtr4rd	$⊢ φ \to K = \|(S prefix F) ++ R\|$
21	20	oveq2d	$⊢ φ \to X + K = X + \|(S prefix F) ++ R\|$
22	8 21	fveq12d	$⊢ φ \to (S splice ⟨F, T, R⟩) (X + K) = (((S prefix F) ++ R) ++ (S substr ⟨T, \|S\|⟩)) (X + \|(S prefix F) ++ R\|)$
23		ccatcl	$⊢ (S prefix F \in Word A \land R \in Word A) \to (S prefix F) ++ R \in Word A$
24	17 4 23	syl2anc	$⊢ φ \to (S prefix F) ++ R \in Word A$
25		swrdcl	$⊢ S \in Word A \to S substr ⟨T, \|S\|⟩ \in Word A$
26	1 25	syl	$⊢ φ \to S substr ⟨T, \|S\|⟩ \in Word A$
27		lencl	$⊢ S \in Word A \to \|S\| \in ℕ_{0}$
28		nn0fz0	$⊢ \|S\| \in ℕ_{0} \leftrightarrow \|S\| \in (0 \dots \|S\|)$
29	27 28	sylib	$⊢ S \in Word A \to \|S\| \in (0 \dots \|S\|)$
30	1 29	syl	$⊢ φ \to \|S\| \in (0 \dots \|S\|)$
31		swrdlen	$⊢ (S \in Word A \land T \in (0 \dots \|S\|) \land \|S\| \in (0 \dots \|S\|)) \to \|S substr ⟨T, \|S\|⟩\| = \|S\| - T$
32	1 3 30 31	syl3anc	$⊢ φ \to \|S substr ⟨T, \|S\|⟩\| = \|S\| - T$
33	32	oveq2d	$⊢ φ \to (0 ..^\|S substr ⟨T, \|S\|⟩\|) = (0 ..^\|S\| - T)$
34	5 33	eleqtrrd	$⊢ φ \to X \in (0 ..^\|S substr ⟨T, \|S\|⟩\|)$
35		ccatval3	$⊢ ((S prefix F) ++ R \in Word A \land S substr ⟨T, \|S\|⟩ \in Word A \land X \in (0 ..^\|S substr ⟨T, \|S\|⟩\|)) \to (((S prefix F) ++ R) ++ (S substr ⟨T, \|S\|⟩)) (X + \|(S prefix F) ++ R\|) = (S substr ⟨T, \|S\|⟩) (X)$
36	24 26 34 35	syl3anc	$⊢ φ \to (((S prefix F) ++ R) ++ (S substr ⟨T, \|S\|⟩)) (X + \|(S prefix F) ++ R\|) = (S substr ⟨T, \|S\|⟩) (X)$
37		swrdfv	$⊢ ((S \in Word A \land T \in (0 \dots \|S\|) \land \|S\| \in (0 \dots \|S\|)) \land X \in (0 ..^\|S\| - T)) \to (S substr ⟨T, \|S\|⟩) (X) = S (X + T)$
38	1 3 30 5 37	syl31anc	$⊢ φ \to (S substr ⟨T, \|S\|⟩) (X) = S (X + T)$
39	22 36 38	3eqtrd	$⊢ φ \to (S splice ⟨F, T, R⟩) (X + K) = S (X + T)$

Metamath Proof Explorer

Theorem splfv3

Proof