splval

Description: Value of the substring replacement operator. (Contributed by Stefan O'Rear, 15-Aug-2015) (Revised by AV, 11-May-2020) (Revised by AV, 15-Oct-2022)

		Ref	Expression
	Assertion	splval	$⊢ (S \in V \land (F \in W \land T \in X \land R \in Y)) \to S splice ⟨F, T, R⟩ = ((S prefix F) ++ R) ++ (S substr ⟨T, \|S\|⟩)$

Proof

Step	Hyp	Ref	Expression
1		df-splice	$⊢ splice = (s \in V, b \in V ⟼ ((s prefix 1^{st} (1^{st} (b))) ++ 2^{nd} (b)) ++ (s substr ⟨2^{nd} (1^{st} (b)), \|s\|⟩))$
2	1	a1i	$⊢ (S \in V \land (F \in W \land T \in X \land R \in Y)) \to splice = (s \in V, b \in V ⟼ ((s prefix 1^{st} (1^{st} (b))) ++ 2^{nd} (b)) ++ (s substr ⟨2^{nd} (1^{st} (b)), \|s\|⟩))$
3		simprl	$⊢ ((S \in V \land (F \in W \land T \in X \land R \in Y)) \land (s = S \land b = ⟨F, T, R⟩)) \to s = S$
4		2fveq3	$⊢ b = ⟨F, T, R⟩ \to 1^{st} (1^{st} (b)) = 1^{st} (1^{st} (⟨F, T, R⟩))$
5	4	adantl	$⊢ (s = S \land b = ⟨F, T, R⟩) \to 1^{st} (1^{st} (b)) = 1^{st} (1^{st} (⟨F, T, R⟩))$
6		ot1stg	$⊢ (F \in W \land T \in X \land R \in Y) \to 1^{st} (1^{st} (⟨F, T, R⟩)) = F$
7	6	adantl	$⊢ (S \in V \land (F \in W \land T \in X \land R \in Y)) \to 1^{st} (1^{st} (⟨F, T, R⟩)) = F$
8	5 7	sylan9eqr	$⊢ ((S \in V \land (F \in W \land T \in X \land R \in Y)) \land (s = S \land b = ⟨F, T, R⟩)) \to 1^{st} (1^{st} (b)) = F$
9	3 8	oveq12d	$⊢ ((S \in V \land (F \in W \land T \in X \land R \in Y)) \land (s = S \land b = ⟨F, T, R⟩)) \to s prefix 1^{st} (1^{st} (b)) = S prefix F$
10		fveq2	$⊢ b = ⟨F, T, R⟩ \to 2^{nd} (b) = 2^{nd} (⟨F, T, R⟩)$
11	10	adantl	$⊢ (s = S \land b = ⟨F, T, R⟩) \to 2^{nd} (b) = 2^{nd} (⟨F, T, R⟩)$
12		ot3rdg	$⊢ R \in Y \to 2^{nd} (⟨F, T, R⟩) = R$
13	12	3ad2ant3	$⊢ (F \in W \land T \in X \land R \in Y) \to 2^{nd} (⟨F, T, R⟩) = R$
14	13	adantl	$⊢ (S \in V \land (F \in W \land T \in X \land R \in Y)) \to 2^{nd} (⟨F, T, R⟩) = R$
15	11 14	sylan9eqr	$⊢ ((S \in V \land (F \in W \land T \in X \land R \in Y)) \land (s = S \land b = ⟨F, T, R⟩)) \to 2^{nd} (b) = R$
16	9 15	oveq12d	$⊢ ((S \in V \land (F \in W \land T \in X \land R \in Y)) \land (s = S \land b = ⟨F, T, R⟩)) \to (s prefix 1^{st} (1^{st} (b))) ++ 2^{nd} (b) = (S prefix F) ++ R$
17		2fveq3	$⊢ b = ⟨F, T, R⟩ \to 2^{nd} (1^{st} (b)) = 2^{nd} (1^{st} (⟨F, T, R⟩))$
18	17	adantl	$⊢ (s = S \land b = ⟨F, T, R⟩) \to 2^{nd} (1^{st} (b)) = 2^{nd} (1^{st} (⟨F, T, R⟩))$
19		ot2ndg	$⊢ (F \in W \land T \in X \land R \in Y) \to 2^{nd} (1^{st} (⟨F, T, R⟩)) = T$
20	19	adantl	$⊢ (S \in V \land (F \in W \land T \in X \land R \in Y)) \to 2^{nd} (1^{st} (⟨F, T, R⟩)) = T$
21	18 20	sylan9eqr	$⊢ ((S \in V \land (F \in W \land T \in X \land R \in Y)) \land (s = S \land b = ⟨F, T, R⟩)) \to 2^{nd} (1^{st} (b)) = T$
22	3	fveq2d	$⊢ ((S \in V \land (F \in W \land T \in X \land R \in Y)) \land (s = S \land b = ⟨F, T, R⟩)) \to \|s\| = \|S\|$
23	21 22	opeq12d	$⊢ ((S \in V \land (F \in W \land T \in X \land R \in Y)) \land (s = S \land b = ⟨F, T, R⟩)) \to ⟨2^{nd} (1^{st} (b)), \|s\|⟩ = ⟨T, \|S\|⟩$
24	3 23	oveq12d	$⊢ ((S \in V \land (F \in W \land T \in X \land R \in Y)) \land (s = S \land b = ⟨F, T, R⟩)) \to s substr ⟨2^{nd} (1^{st} (b)), \|s\|⟩ = S substr ⟨T, \|S\|⟩$
25	16 24	oveq12d	$⊢ ((S \in V \land (F \in W \land T \in X \land R \in Y)) \land (s = S \land b = ⟨F, T, R⟩)) \to ((s prefix 1^{st} (1^{st} (b))) ++ 2^{nd} (b)) ++ (s substr ⟨2^{nd} (1^{st} (b)), \|s\|⟩) = ((S prefix F) ++ R) ++ (S substr ⟨T, \|S\|⟩)$
26		elex	$⊢ S \in V \to S \in V$
27	26	adantr	$⊢ (S \in V \land (F \in W \land T \in X \land R \in Y)) \to S \in V$
28		otex	$⊢ ⟨F, T, R⟩ \in V$
29	28	a1i	$⊢ (S \in V \land (F \in W \land T \in X \land R \in Y)) \to ⟨F, T, R⟩ \in V$
30		ovexd	$⊢ (S \in V \land (F \in W \land T \in X \land R \in Y)) \to ((S prefix F) ++ R) ++ (S substr ⟨T, \|S\|⟩) \in V$
31	2 25 27 29 30	ovmpod	$⊢ (S \in V \land (F \in W \land T \in X \land R \in Y)) \to S splice ⟨F, T, R⟩ = ((S prefix F) ++ R) ++ (S substr ⟨T, \|S\|⟩)$

Metamath Proof Explorer

Theorem splval

Proof