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

Metamath Proof Explorer

Theorem s3rn

Description: Range of a length 3 string. (Contributed by Thierry Arnoux, 19-Sep-2023) (Proof shortened by AV, 1-Aug-2025)

Ref Expression
Hypotheses s2rn.i ⊢ φ → I ∈ D
s2rn.j ⊢ φ → J ∈ D
s3rn.k ⊢ φ → K ∈ D
Assertion s3rn ⊢ φ → ran ⁡ ⟨“ IJK ”⟩ = I J K

Proof

Step Hyp Ref Expression
1 s2rn.i ⊢ φ → I ∈ D
2 s2rn.j ⊢ φ → J ∈ D
3 s3rn.k ⊢ φ → K ∈ D
4 df-s3 ⊢ ⟨“ IJK ”⟩ = ⟨“ IJ ”⟩ ++ ⟨“ K ”⟩
5 4 a1i ⊢ φ → ⟨“ IJK ”⟩ = ⟨“ IJ ”⟩ ++ ⟨“ K ”⟩
6 5 rneqd ⊢ φ → ran ⁡ ⟨“ IJK ”⟩ = ran ⁡ ⟨“ IJ ”⟩ ++ ⟨“ K ”⟩
7 s2cli ⊢ ⟨“ IJ ”⟩ ∈ Word V
8 s1cli ⊢ ⟨“ K ”⟩ ∈ Word V
9 7 8 pm3.2i ⊢ ⟨“ IJ ”⟩ ∈ Word V ∧ ⟨“ K ”⟩ ∈ Word V
10 ccatrn ⊢ ⟨“ IJ ”⟩ ∈ Word V ∧ ⟨“ K ”⟩ ∈ Word V → ran ⁡ ⟨“ IJ ”⟩ ++ ⟨“ K ”⟩ = ran ⁡ ⟨“ IJ ”⟩ ∪ ran ⁡ ⟨“ K ”⟩
11 9 10 mp1i ⊢ φ → ran ⁡ ⟨“ IJ ”⟩ ++ ⟨“ K ”⟩ = ran ⁡ ⟨“ IJ ”⟩ ∪ ran ⁡ ⟨“ K ”⟩
12 1 2 s2rn ⊢ φ → ran ⁡ ⟨“ IJ ”⟩ = I J
13 s1rn ⊢ K ∈ D → ran ⁡ ⟨“ K ”⟩ = K
14 3 13 syl ⊢ φ → ran ⁡ ⟨“ K ”⟩ = K
15 12 14 uneq12d ⊢ φ → ran ⁡ ⟨“ IJ ”⟩ ∪ ran ⁡ ⟨“ K ”⟩ = I J ∪ K
16 df-tp ⊢ I J K = I J ∪ K
17 15 16 eqtr4di ⊢ φ → ran ⁡ ⟨“ IJ ”⟩ ∪ ran ⁡ ⟨“ K ”⟩ = I J K
18 6 11 17 3eqtrd ⊢ φ → ran ⁡ ⟨“ IJK ”⟩ = I J K