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	⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( 𝑆 splice ⟨ 𝑋 , 𝑌 , ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ⟩ ) = 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		ovex	⊢ ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ∈ V
2		splval	⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ∧ ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ∈ V ) ) → ( 𝑆 splice ⟨ 𝑋 , 𝑌 , ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ⟩ ) = ( ( ( 𝑆 prefix 𝑋 ) ++ ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ) ++ ( 𝑆 substr ⟨ 𝑌 , ( ♯ ‘ 𝑆 ) ⟩ ) ) )
3	1 2	mp3anr3	⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( 𝑆 splice ⟨ 𝑋 , 𝑌 , ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ⟩ ) = ( ( ( 𝑆 prefix 𝑋 ) ++ ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ) ++ ( 𝑆 substr ⟨ 𝑌 , ( ♯ ‘ 𝑆 ) ⟩ ) ) )
4		ccatpfx	⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( ( 𝑆 prefix 𝑋 ) ++ ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ) = ( 𝑆 prefix 𝑌 ) )
5	4	3expb	⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( ( 𝑆 prefix 𝑋 ) ++ ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ) = ( 𝑆 prefix 𝑌 ) )
6	5	oveq1d	⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( ( ( 𝑆 prefix 𝑋 ) ++ ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ) ++ ( 𝑆 substr ⟨ 𝑌 , ( ♯ ‘ 𝑆 ) ⟩ ) ) = ( ( 𝑆 prefix 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑌 , ( ♯ ‘ 𝑆 ) ⟩ ) ) )
7		simpl	⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → 𝑆 ∈ Word 𝐴 )
8		simprr	⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → 𝑌 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) )
9		elfzuz2	⊢ ( 𝑌 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) → ( ♯ ‘ 𝑆 ) ∈ ( ℤ≥ ‘ 0 ) )
10	9	ad2antll	⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( ♯ ‘ 𝑆 ) ∈ ( ℤ≥ ‘ 0 ) )
11		eluzfz2	⊢ ( ( ♯ ‘ 𝑆 ) ∈ ( ℤ≥ ‘ 0 ) → ( ♯ ‘ 𝑆 ) ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) )
12	10 11	syl	⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( ♯ ‘ 𝑆 ) ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) )
13		ccatpfx	⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ∧ ( ♯ ‘ 𝑆 ) ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( ( 𝑆 prefix 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑌 , ( ♯ ‘ 𝑆 ) ⟩ ) ) = ( 𝑆 prefix ( ♯ ‘ 𝑆 ) ) )
14	7 8 12 13	syl3anc	⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( ( 𝑆 prefix 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑌 , ( ♯ ‘ 𝑆 ) ⟩ ) ) = ( 𝑆 prefix ( ♯ ‘ 𝑆 ) ) )
15		pfxid	⊢ ( 𝑆 ∈ Word 𝐴 → ( 𝑆 prefix ( ♯ ‘ 𝑆 ) ) = 𝑆 )
16	15	adantr	⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( 𝑆 prefix ( ♯ ‘ 𝑆 ) ) = 𝑆 )
17	14 16	eqtrd	⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( ( 𝑆 prefix 𝑌 ) ++ ( 𝑆 substr ⟨ 𝑌 , ( ♯ ‘ 𝑆 ) ⟩ ) ) = 𝑆 )
18	6 17	eqtrd	⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( ( ( 𝑆 prefix 𝑋 ) ++ ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ) ++ ( 𝑆 substr ⟨ 𝑌 , ( ♯ ‘ 𝑆 ) ⟩ ) ) = 𝑆 )
19	3 18	eqtrd	⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑋 ∈ ( 0 ... 𝑌 ) ∧ 𝑌 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ) → ( 𝑆 splice ⟨ 𝑋 , 𝑌 , ( 𝑆 substr ⟨ 𝑋 , 𝑌 ⟩ ) ⟩ ) = 𝑆 )