splcl

Description: Closure of the substring replacement operator. (Contributed by Stefan O'Rear, 26-Aug-2015) (Proof shortened by AV, 15-Oct-2022)

		Ref	Expression
	Assertion	splcl	$⊢ (S \in Word A \land R \in Word A) \to S splice ⟨F, T, R⟩ \in Word A$

Proof

Step	Hyp	Ref	Expression
1		elex	$⊢ S \in Word A \to S \in V$
2		otex	$⊢ ⟨F, T, R⟩ \in V$
3		id	$⊢ s = S \to s = S$
4		2fveq3	$⊢ b = ⟨F, T, R⟩ \to 1^{st} (1^{st} (b)) = 1^{st} (1^{st} (⟨F, T, R⟩))$
5	3 4	oveqan12d	$⊢ (s = S \land b = ⟨F, T, R⟩) \to s prefix 1^{st} (1^{st} (b)) = S prefix 1^{st} (1^{st} (⟨F, T, R⟩))$
6		simpr	$⊢ (s = S \land b = ⟨F, T, R⟩) \to b = ⟨F, T, R⟩$
7	6	fveq2d	$⊢ (s = S \land b = ⟨F, T, R⟩) \to 2^{nd} (b) = 2^{nd} (⟨F, T, R⟩)$
8	5 7	oveq12d	$⊢ (s = S \land b = ⟨F, T, R⟩) \to (s prefix 1^{st} (1^{st} (b))) ++ 2^{nd} (b) = (S prefix 1^{st} (1^{st} (⟨F, T, R⟩))) ++ 2^{nd} (⟨F, T, R⟩)$
9		simpl	$⊢ (s = S \land b = ⟨F, T, R⟩) \to s = S$
10	6	fveq2d	$⊢ (s = S \land b = ⟨F, T, R⟩) \to 1^{st} (b) = 1^{st} (⟨F, T, R⟩)$
11	10	fveq2d	$⊢ (s = S \land b = ⟨F, T, R⟩) \to 2^{nd} (1^{st} (b)) = 2^{nd} (1^{st} (⟨F, T, R⟩))$
12	9	fveq2d	$⊢ (s = S \land b = ⟨F, T, R⟩) \to \|s\| = \|S\|$
13	11 12	opeq12d	$⊢ (s = S \land b = ⟨F, T, R⟩) \to ⟨2^{nd} (1^{st} (b)), \|s\|⟩ = ⟨2^{nd} (1^{st} (⟨F, T, R⟩)), \|S\|⟩$
14	9 13	oveq12d	$⊢ (s = S \land b = ⟨F, T, R⟩) \to s substr ⟨2^{nd} (1^{st} (b)), \|s\|⟩ = S substr ⟨2^{nd} (1^{st} (⟨F, T, R⟩)), \|S\|⟩$
15	8 14	oveq12d	$⊢ (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 1^{st} (1^{st} (⟨F, T, R⟩))) ++ 2^{nd} (⟨F, T, R⟩)) ++ (S substr ⟨2^{nd} (1^{st} (⟨F, T, R⟩)), \|S\|⟩)$
16		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\|⟩))$
17		ovex	$⊢ ((S prefix 1^{st} (1^{st} (⟨F, T, R⟩))) ++ 2^{nd} (⟨F, T, R⟩)) ++ (S substr ⟨2^{nd} (1^{st} (⟨F, T, R⟩)), \|S\|⟩) \in V$
18	15 16 17	ovmpoa	$⊢ (S \in V \land ⟨F, T, R⟩ \in V) \to S splice ⟨F, T, R⟩ = ((S prefix 1^{st} (1^{st} (⟨F, T, R⟩))) ++ 2^{nd} (⟨F, T, R⟩)) ++ (S substr ⟨2^{nd} (1^{st} (⟨F, T, R⟩)), \|S\|⟩)$
19	1 2 18	sylancl	$⊢ S \in Word A \to S splice ⟨F, T, R⟩ = ((S prefix 1^{st} (1^{st} (⟨F, T, R⟩))) ++ 2^{nd} (⟨F, T, R⟩)) ++ (S substr ⟨2^{nd} (1^{st} (⟨F, T, R⟩)), \|S\|⟩)$
20	19	adantr	$⊢ (S \in Word A \land R \in Word A) \to S splice ⟨F, T, R⟩ = ((S prefix 1^{st} (1^{st} (⟨F, T, R⟩))) ++ 2^{nd} (⟨F, T, R⟩)) ++ (S substr ⟨2^{nd} (1^{st} (⟨F, T, R⟩)), \|S\|⟩)$
21		pfxcl	$⊢ S \in Word A \to S prefix 1^{st} (1^{st} (⟨F, T, R⟩)) \in Word A$
22	21	adantr	$⊢ (S \in Word A \land R \in Word A) \to S prefix 1^{st} (1^{st} (⟨F, T, R⟩)) \in Word A$
23		ot3rdg	$⊢ R \in Word A \to 2^{nd} (⟨F, T, R⟩) = R$
24	23	adantl	$⊢ (S \in Word A \land R \in Word A) \to 2^{nd} (⟨F, T, R⟩) = R$
25		simpr	$⊢ (S \in Word A \land R \in Word A) \to R \in Word A$
26	24 25	eqeltrd	$⊢ (S \in Word A \land R \in Word A) \to 2^{nd} (⟨F, T, R⟩) \in Word A$
27		ccatcl	$⊢ (S prefix 1^{st} (1^{st} (⟨F, T, R⟩)) \in Word A \land 2^{nd} (⟨F, T, R⟩) \in Word A) \to (S prefix 1^{st} (1^{st} (⟨F, T, R⟩))) ++ 2^{nd} (⟨F, T, R⟩) \in Word A$
28	22 26 27	syl2anc	$⊢ (S \in Word A \land R \in Word A) \to (S prefix 1^{st} (1^{st} (⟨F, T, R⟩))) ++ 2^{nd} (⟨F, T, R⟩) \in Word A$
29		swrdcl	$⊢ S \in Word A \to S substr ⟨2^{nd} (1^{st} (⟨F, T, R⟩)), \|S\|⟩ \in Word A$
30	29	adantr	$⊢ (S \in Word A \land R \in Word A) \to S substr ⟨2^{nd} (1^{st} (⟨F, T, R⟩)), \|S\|⟩ \in Word A$
31		ccatcl	$⊢ ((S prefix 1^{st} (1^{st} (⟨F, T, R⟩))) ++ 2^{nd} (⟨F, T, R⟩) \in Word A \land S substr ⟨2^{nd} (1^{st} (⟨F, T, R⟩)), \|S\|⟩ \in Word A) \to ((S prefix 1^{st} (1^{st} (⟨F, T, R⟩))) ++ 2^{nd} (⟨F, T, R⟩)) ++ (S substr ⟨2^{nd} (1^{st} (⟨F, T, R⟩)), \|S\|⟩) \in Word A$
32	28 30 31	syl2anc	$⊢ (S \in Word A \land R \in Word A) \to ((S prefix 1^{st} (1^{st} (⟨F, T, R⟩))) ++ 2^{nd} (⟨F, T, R⟩)) ++ (S substr ⟨2^{nd} (1^{st} (⟨F, T, R⟩)), \|S\|⟩) \in Word A$
33	20 32	eqeltrd	$⊢ (S \in Word A \land R \in Word A) \to S splice ⟨F, T, R⟩ \in Word A$

Metamath Proof Explorer

Theorem splcl

Proof