splfv1

Description: Symbols to the left of a splice are unaffected. (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$
	splfv1.x	$⊢ φ \to X \in (0 ..^F)$
Assertion	splfv1	$⊢ φ \to (S splice ⟨F, T, R⟩) (X) = S (X)$

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		splfv1.x	$⊢ φ \to X \in (0 ..^F)$
6		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\|⟩)$
7	1 2 3 4 6	syl13anc	$⊢ φ \to S splice ⟨F, T, R⟩ = ((S prefix F) ++ R) ++ (S substr ⟨T, \|S\|⟩)$
8	7	fveq1d	$⊢ φ \to (S splice ⟨F, T, R⟩) (X) = (((S prefix F) ++ R) ++ (S substr ⟨T, \|S\|⟩)) (X)$
9		pfxcl	$⊢ S \in Word A \to S prefix F \in Word A$
10	1 9	syl	$⊢ φ \to S prefix F \in Word A$
11		ccatcl	$⊢ (S prefix F \in Word A \land R \in Word A) \to (S prefix F) ++ R \in Word A$
12	10 4 11	syl2anc	$⊢ φ \to (S prefix F) ++ R \in Word A$
13		swrdcl	$⊢ S \in Word A \to S substr ⟨T, \|S\|⟩ \in Word A$
14	1 13	syl	$⊢ φ \to S substr ⟨T, \|S\|⟩ \in Word A$
15		elfzelz	$⊢ F \in (0 \dots T) \to F \in ℤ$
16	2 15	syl	$⊢ φ \to F \in ℤ$
17	16	uzidd	$⊢ φ \to F \in ℤ_{\geq F}$
18		lencl	$⊢ R \in Word A \to \|R\| \in ℕ_{0}$
19	4 18	syl	$⊢ φ \to \|R\| \in ℕ_{0}$
20		uzaddcl	$⊢ (F \in ℤ_{\geq F} \land \|R\| \in ℕ_{0}) \to F + \|R\| \in ℤ_{\geq F}$
21	17 19 20	syl2anc	$⊢ φ \to F + \|R\| \in ℤ_{\geq F}$
22		fzoss2	$⊢ F + \|R\| \in ℤ_{\geq F} \to (0 ..^F) \subseteq (0 ..^F + \|R\|)$
23	21 22	syl	$⊢ φ \to (0 ..^F) \subseteq (0 ..^F + \|R\|)$
24	23 5	sseldd	$⊢ φ \to X \in (0 ..^F + \|R\|)$
25		ccatlen	$⊢ (S prefix F \in Word A \land R \in Word A) \to \|(S prefix F) ++ R\| = \|S prefix F\| + \|R\|$
26	10 4 25	syl2anc	$⊢ φ \to \|(S prefix F) ++ R\| = \|S prefix F\| + \|R\|$
27		fzass4	$⊢ (F \in (0 \dots \|S\|) \land T \in (F \dots \|S\|)) \leftrightarrow (F \in (0 \dots T) \land T \in (0 \dots \|S\|))$
28	27	biimpri	$⊢ (F \in (0 \dots T) \land T \in (0 \dots \|S\|)) \to (F \in (0 \dots \|S\|) \land T \in (F \dots \|S\|))$
29	28	simpld	$⊢ (F \in (0 \dots T) \land T \in (0 \dots \|S\|)) \to F \in (0 \dots \|S\|)$
30	2 3 29	syl2anc	$⊢ φ \to F \in (0 \dots \|S\|)$
31		pfxlen	$⊢ (S \in Word A \land F \in (0 \dots \|S\|)) \to \|S prefix F\| = F$
32	1 30 31	syl2anc	$⊢ φ \to \|S prefix F\| = F$
33	32	oveq1d	$⊢ φ \to \|S prefix F\| + \|R\| = F + \|R\|$
34	26 33	eqtrd	$⊢ φ \to \|(S prefix F) ++ R\| = F + \|R\|$
35	34	oveq2d	$⊢ φ \to (0 ..^\|(S prefix F) ++ R\|) = (0 ..^F + \|R\|)$
36	24 35	eleqtrrd	$⊢ φ \to X \in (0 ..^\|(S prefix F) ++ R\|)$
37		ccatval1	$⊢ ((S prefix F) ++ R \in Word A \land S substr ⟨T, \|S\|⟩ \in Word A \land X \in (0 ..^\|(S prefix F) ++ R\|)) \to (((S prefix F) ++ R) ++ (S substr ⟨T, \|S\|⟩)) (X) = ((S prefix F) ++ R) (X)$
38	12 14 36 37	syl3anc	$⊢ φ \to (((S prefix F) ++ R) ++ (S substr ⟨T, \|S\|⟩)) (X) = ((S prefix F) ++ R) (X)$
39	32	oveq2d	$⊢ φ \to (0 ..^\|S prefix F\|) = (0 ..^F)$
40	5 39	eleqtrrd	$⊢ φ \to X \in (0 ..^\|S prefix F\|)$
41		ccatval1	$⊢ (S prefix F \in Word A \land R \in Word A \land X \in (0 ..^\|S prefix F\|)) \to ((S prefix F) ++ R) (X) = (S prefix F) (X)$
42	10 4 40 41	syl3anc	$⊢ φ \to ((S prefix F) ++ R) (X) = (S prefix F) (X)$
43		pfxfv	$⊢ (S \in Word A \land F \in (0 \dots \|S\|) \land X \in (0 ..^F)) \to (S prefix F) (X) = S (X)$
44	1 30 5 43	syl3anc	$⊢ φ \to (S prefix F) (X) = S (X)$
45	42 44	eqtrd	$⊢ φ \to ((S prefix F) ++ R) (X) = S (X)$
46	8 38 45	3eqtrd	$⊢ φ \to (S splice ⟨F, T, R⟩) (X) = S (X)$

Metamath Proof Explorer

Theorem splfv1

Proof