splfv2a

Description: Symbols within the replacement region of a splice, expressed using the coordinates of the replacement region. (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$
	splfv2a.x	$⊢ φ \to X \in (0 ..^\|R\|)$
Assertion	splfv2a	$⊢ φ \to (S splice ⟨F, T, R⟩) (F + X) = R (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		splfv2a.x	$⊢ φ \to X \in (0 ..^\|R\|)$
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		elfznn0	$⊢ F \in (0 \dots T) \to F \in ℕ_{0}$
9	2 8	syl	$⊢ φ \to F \in ℕ_{0}$
10	9	nn0cnd	$⊢ φ \to F \in ℂ$
11		elfzonn0	$⊢ X \in (0 ..^\|R\|) \to X \in ℕ_{0}$
12	5 11	syl	$⊢ φ \to X \in ℕ_{0}$
13	12	nn0cnd	$⊢ φ \to X \in ℂ$
14	10 13	addcomd	$⊢ φ \to F + X = X + F$
15		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
16	9 15	eleqtrdi	$⊢ φ \to F \in ℤ_{\geq 0}$
17		elfzuz3	$⊢ T \in (0 \dots \|S\|) \to \|S\| \in ℤ_{\geq T}$
18	3 17	syl	$⊢ φ \to \|S\| \in ℤ_{\geq T}$
19		elfzuz3	$⊢ F \in (0 \dots T) \to T \in ℤ_{\geq F}$
20	2 19	syl	$⊢ φ \to T \in ℤ_{\geq F}$
21		uztrn	$⊢ (\|S\| \in ℤ_{\geq T} \land T \in ℤ_{\geq F}) \to \|S\| \in ℤ_{\geq F}$
22	18 20 21	syl2anc	$⊢ φ \to \|S\| \in ℤ_{\geq F}$
23		elfzuzb	$⊢ F \in (0 \dots \|S\|) \leftrightarrow (F \in ℤ_{\geq 0} \land \|S\| \in ℤ_{\geq F})$
24	16 22 23	sylanbrc	$⊢ φ \to F \in (0 \dots \|S\|)$
25		pfxlen	$⊢ (S \in Word A \land F \in (0 \dots \|S\|)) \to \|S prefix F\| = F$
26	1 24 25	syl2anc	$⊢ φ \to \|S prefix F\| = F$
27	26	oveq2d	$⊢ φ \to X + \|S prefix F\| = X + F$
28	14 27	eqtr4d	$⊢ φ \to F + X = X + \|S prefix F\|$
29	7 28	fveq12d	$⊢ φ \to (S splice ⟨F, T, R⟩) (F + X) = (((S prefix F) ++ R) ++ (S substr ⟨T, \|S\|⟩)) (X + \|S prefix F\|)$
30		pfxcl	$⊢ S \in Word A \to S prefix F \in Word A$
31	1 30	syl	$⊢ φ \to S prefix F \in Word A$
32		ccatcl	$⊢ (S prefix F \in Word A \land R \in Word A) \to (S prefix F) ++ R \in Word A$
33	31 4 32	syl2anc	$⊢ φ \to (S prefix F) ++ R \in Word A$
34		swrdcl	$⊢ S \in Word A \to S substr ⟨T, \|S\|⟩ \in Word A$
35	1 34	syl	$⊢ φ \to S substr ⟨T, \|S\|⟩ \in Word A$
36		0nn0	$⊢ 0 \in ℕ_{0}$
37		nn0addcl	$⊢ (0 \in ℕ_{0} \land F \in ℕ_{0}) \to 0 + F \in ℕ_{0}$
38	36 9 37	sylancr	$⊢ φ \to 0 + F \in ℕ_{0}$
39		fzoss1	$⊢ 0 + F \in ℤ_{\geq 0} \to (0 + F ..^\|R\| + F) \subseteq (0 ..^\|R\| + F)$
40	39 15	eleq2s	$⊢ 0 + F \in ℕ_{0} \to (0 + F ..^\|R\| + F) \subseteq (0 ..^\|R\| + F)$
41	38 40	syl	$⊢ φ \to (0 + F ..^\|R\| + F) \subseteq (0 ..^\|R\| + F)$
42		ccatlen	$⊢ (S prefix F \in Word A \land R \in Word A) \to \|(S prefix F) ++ R\| = \|S prefix F\| + \|R\|$
43	31 4 42	syl2anc	$⊢ φ \to \|(S prefix F) ++ R\| = \|S prefix F\| + \|R\|$
44	26	oveq1d	$⊢ φ \to \|S prefix F\| + \|R\| = F + \|R\|$
45		lencl	$⊢ R \in Word A \to \|R\| \in ℕ_{0}$
46	4 45	syl	$⊢ φ \to \|R\| \in ℕ_{0}$
47	46	nn0cnd	$⊢ φ \to \|R\| \in ℂ$
48	10 47	addcomd	$⊢ φ \to F + \|R\| = \|R\| + F$
49	43 44 48	3eqtrd	$⊢ φ \to \|(S prefix F) ++ R\| = \|R\| + F$
50	49	oveq2d	$⊢ φ \to (0 ..^\|(S prefix F) ++ R\|) = (0 ..^\|R\| + F)$
51	41 50	sseqtrrd	$⊢ φ \to (0 + F ..^\|R\| + F) \subseteq (0 ..^\|(S prefix F) ++ R\|)$
52	9	nn0zd	$⊢ φ \to F \in ℤ$
53		fzoaddel	$⊢ (X \in (0 ..^\|R\|) \land F \in ℤ) \to X + F \in (0 + F ..^\|R\| + F)$
54	5 52 53	syl2anc	$⊢ φ \to X + F \in (0 + F ..^\|R\| + F)$
55	51 54	sseldd	$⊢ φ \to X + F \in (0 ..^\|(S prefix F) ++ R\|)$
56	27 55	eqeltrd	$⊢ φ \to X + \|S prefix F\| \in (0 ..^\|(S prefix F) ++ R\|)$
57		ccatval1	$⊢ ((S prefix F) ++ R \in Word A \land S substr ⟨T, \|S\|⟩ \in Word A \land X + \|S prefix F\| \in (0 ..^\|(S prefix F) ++ R\|)) \to (((S prefix F) ++ R) ++ (S substr ⟨T, \|S\|⟩)) (X + \|S prefix F\|) = ((S prefix F) ++ R) (X + \|S prefix F\|)$
58	33 35 56 57	syl3anc	$⊢ φ \to (((S prefix F) ++ R) ++ (S substr ⟨T, \|S\|⟩)) (X + \|S prefix F\|) = ((S prefix F) ++ R) (X + \|S prefix F\|)$
59		ccatval3	$⊢ (S prefix F \in Word A \land R \in Word A \land X \in (0 ..^\|R\|)) \to ((S prefix F) ++ R) (X + \|S prefix F\|) = R (X)$
60	31 4 5 59	syl3anc	$⊢ φ \to ((S prefix F) ++ R) (X + \|S prefix F\|) = R (X)$
61	29 58 60	3eqtrd	$⊢ φ \to (S splice ⟨F, T, R⟩) (F + X) = R (X)$

Metamath Proof Explorer

Theorem splfv2a

Proof