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

Metamath Proof Explorer

Theorem splfv1

Proof