This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝑆 ∈ 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 ⟨ 𝑋 , 𝑌 ⟩ ) ⟩ ) = 𝑆 )