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 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁𝑋𝑉 ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 𝑁 ) = 𝑋 )