Metamath Proof Explorer

Theorem splid

Description: Splicing a subword for the same subword makes no difference. (Contributed by Stefan O'Rear, 20-Aug-2015) (Proof shortened by AV, 14-Oct-2022)

		Ref	Expression
	Assertion	splid	$⊢ (S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots \|S\|))) \to S splice ⟨X, Y, S substr ⟨X, Y⟩⟩ = S$

Proof

Step	Hyp	Ref	Expression
1		ovex	$⊢ S substr ⟨X, Y⟩ \in V$
2		splval	$⊢ (S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots \|S\|) \land S substr ⟨X, Y⟩ \in V)) \to S splice ⟨X, Y, S substr ⟨X, Y⟩⟩ = ((S prefix X) ++ (S substr ⟨X, Y⟩)) ++ (S substr ⟨Y, \|S\|⟩)$
3	1 2	mp3anr3	$⊢ (S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots \|S\|))) \to S splice ⟨X, Y, S substr ⟨X, Y⟩⟩ = ((S prefix X) ++ (S substr ⟨X, Y⟩)) ++ (S substr ⟨Y, \|S\|⟩)$
4		ccatpfx	$⊢ (S \in Word A \land X \in (0 \dots Y) \land Y \in (0 \dots \|S\|)) \to (S prefix X) ++ (S substr ⟨X, Y⟩) = S prefix Y$
5	4	3expb	$⊢ (S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots \|S\|))) \to (S prefix X) ++ (S substr ⟨X, Y⟩) = S prefix Y$
6	5	oveq1d	$⊢ (S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots \|S\|))) \to ((S prefix X) ++ (S substr ⟨X, Y⟩)) ++ (S substr ⟨Y, \|S\|⟩) = (S prefix Y) ++ (S substr ⟨Y, \|S\|⟩)$
7		simpl	$⊢ (S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots \|S\|))) \to S \in Word A$
8		simprr	$⊢ (S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots \|S\|))) \to Y \in (0 \dots \|S\|)$
9		elfzuz2	$⊢ Y \in (0 \dots \|S\|) \to \|S\| \in ℤ_{\geq 0}$
10	9	ad2antll	$⊢ (S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots \|S\|))) \to \|S\| \in ℤ_{\geq 0}$
11		eluzfz2	$⊢ \|S\| \in ℤ_{\geq 0} \to \|S\| \in (0 \dots \|S\|)$
12	10 11	syl	$⊢ (S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots \|S\|))) \to \|S\| \in (0 \dots \|S\|)$
13		ccatpfx	$⊢ (S \in Word A \land Y \in (0 \dots \|S\|) \land \|S\| \in (0 \dots \|S\|)) \to (S prefix Y) ++ (S substr ⟨Y, \|S\|⟩) = S prefix \|S\|$
14	7 8 12 13	syl3anc	$⊢ (S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots \|S\|))) \to (S prefix Y) ++ (S substr ⟨Y, \|S\|⟩) = S prefix \|S\|$
15		pfxid	$⊢ S \in Word A \to S prefix \|S\| = S$
16	15	adantr	$⊢ (S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots \|S\|))) \to S prefix \|S\| = S$
17	14 16	eqtrd	$⊢ (S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots \|S\|))) \to (S prefix Y) ++ (S substr ⟨Y, \|S\|⟩) = S$
18	6 17	eqtrd	$⊢ (S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots \|S\|))) \to ((S prefix X) ++ (S substr ⟨X, Y⟩)) ++ (S substr ⟨Y, \|S\|⟩) = S$
19	3 18	eqtrd	$⊢ (S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots \|S\|))) \to S splice ⟨X, Y, S substr ⟨X, Y⟩⟩ = S$