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 ⊢ S ∈ Word A ∧ X ∈ 0 … Y ∧ Y ∈ 0 … S → S splice X Y S substr X Y = S

Proof

Step Hyp Ref Expression
1 ovex ⊢ S substr X Y ∈ V
2 splval ⊢ S ∈ Word A ∧ X ∈ 0 … Y ∧ Y ∈ 0 … S ∧ S substr X Y ∈ V → S splice X Y S substr X Y = S prefix X ++ S substr X Y ++ S substr Y S
3 1 2 mp3anr3 ⊢ S ∈ Word A ∧ X ∈ 0 … Y ∧ Y ∈ 0 … S → S splice X Y S substr X Y = S prefix X ++ S substr X Y ++ S substr Y S
4 ccatpfx ⊢ S ∈ Word A ∧ X ∈ 0 … Y ∧ Y ∈ 0 … S → S prefix X ++ S substr X Y = S prefix Y
5 4 3expb ⊢ S ∈ Word A ∧ X ∈ 0 … Y ∧ Y ∈ 0 … S → S prefix X ++ S substr X Y = S prefix Y
6 5 oveq1d ⊢ S ∈ Word A ∧ X ∈ 0 … Y ∧ Y ∈ 0 … S → S prefix X ++ S substr X Y ++ S substr Y S = S prefix Y ++ S substr Y S
7 simpl ⊢ S ∈ Word A ∧ X ∈ 0 … Y ∧ Y ∈ 0 … S → S ∈ Word A
8 simprr ⊢ S ∈ Word A ∧ X ∈ 0 … Y ∧ Y ∈ 0 … S → Y ∈ 0 … S
9 elfzuz2 ⊢ Y ∈ 0 … S → S ∈ ℤ ≥ 0
10 9 ad2antll ⊢ S ∈ Word A ∧ X ∈ 0 … Y ∧ Y ∈ 0 … S → S ∈ ℤ ≥ 0
11 eluzfz2 ⊢ S ∈ ℤ ≥ 0 → S ∈ 0 … S
12 10 11 syl ⊢ S ∈ Word A ∧ X ∈ 0 … Y ∧ Y ∈ 0 … S → S ∈ 0 … S
13 ccatpfx ⊢ S ∈ Word A ∧ Y ∈ 0 … S ∧ S ∈ 0 … S → S prefix Y ++ S substr Y S = S prefix S
14 7 8 12 13 syl3anc ⊢ S ∈ Word A ∧ X ∈ 0 … Y ∧ Y ∈ 0 … S → S prefix Y ++ S substr Y S = S prefix S
15 pfxid ⊢ S ∈ Word A → S prefix S = S
16 15 adantr ⊢ S ∈ Word A ∧ X ∈ 0 … Y ∧ Y ∈ 0 … S → S prefix S = S
17 14 16 eqtrd ⊢ S ∈ Word A ∧ X ∈ 0 … Y ∧ Y ∈ 0 … S → S prefix Y ++ S substr Y S = S
18 6 17 eqtrd ⊢ S ∈ Word A ∧ X ∈ 0 … Y ∧ Y ∈ 0 … S → S prefix X ++ S substr X Y ++ S substr Y S = S
19 3 18 eqtrd ⊢ S ∈ Word A ∧ X ∈ 0 … Y ∧ Y ∈ 0 … S → S splice X Y S substr X Y = S