Metamath Proof Explorer

Theorem ccatw2s1p1

Description: Extract the symbol of the first singleton word of a word concatenated with this singleton word and another singleton word. (Contributed by Alexander van der Vekens, 22-Sep-2018) (Proof shortened by AV, 1-May-2020) (Revised by AV, 1-May-2020) (Revised by AV, 29-Jan-2024)

Ref Expression
Assertion ccatw2s1p1 ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ∧ 𝑋 ∈ 𝑉 ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 𝑁 ) = 𝑋 )

Proof

Step Hyp Ref Expression
1 ccatws1cl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ Word 𝑉 )
2 1 3adant2 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ Word 𝑉 )
3 lencl ⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
4 fzonn0p1 ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( ♯ ‘ 𝑊 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) + 1 ) ) )
5 3 4 syl ⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) + 1 ) ) )
6 5 adantr ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) → ( ♯ ‘ 𝑊 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) + 1 ) ) )
7 simpr ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) → ( ♯ ‘ 𝑊 ) = 𝑁 )
8 7 eqcomd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) → 𝑁 = ( ♯ ‘ 𝑊 ) )
9 ccatws1len ⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ) = ( ( ♯ ‘ 𝑊 ) + 1 ) )
10 9 adantr ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) → ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ) = ( ( ♯ ‘ 𝑊 ) + 1 ) )
11 10 oveq2d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) → ( 0 ..^ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ) ) = ( 0 ..^ ( ( ♯ ‘ 𝑊 ) + 1 ) ) )
12 6 8 11 3eltr4d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) → 𝑁 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ) ) )
13 12 3adant3 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ∧ 𝑋 ∈ 𝑉 ) → 𝑁 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ) ) )
14 ccats1val1 ⊢ ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ) ) ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 𝑁 ) = ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ 𝑁 ) )
15 2 13 14 syl2anc ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ∧ 𝑋 ∈ 𝑉 ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 𝑁 ) = ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ 𝑁 ) )
16 simp1 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ∧ 𝑋 ∈ 𝑉 ) → 𝑊 ∈ Word 𝑉 )
17 simp3 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ∧ 𝑋 ∈ 𝑉 ) → 𝑋 ∈ 𝑉 )
18 eqcom ⊢ ( ( ♯ ‘ 𝑊 ) = 𝑁 ↔ 𝑁 = ( ♯ ‘ 𝑊 ) )
19 18 biimpi ⊢ ( ( ♯ ‘ 𝑊 ) = 𝑁 → 𝑁 = ( ♯ ‘ 𝑊 ) )
20 19 3ad2ant2 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ∧ 𝑋 ∈ 𝑉 ) → 𝑁 = ( ♯ ‘ 𝑊 ) )
21 ccats1val2 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 = ( ♯ ‘ 𝑊 ) ) → ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ 𝑁 ) = 𝑋 )
22 16 17 20 21 syl3anc ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ 𝑁 ) = 𝑋 )
23 15 22 eqtrd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ∧ 𝑋 ∈ 𝑉 ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 𝑁 ) = 𝑋 )