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

Metamath Proof Explorer

Theorem ccatfv0

Description: The first symbol of a concatenation of two words is the first symbol of the first word if the first word is not empty. (Contributed by Alexander van der Vekens, 22-Sep-2018)

Ref Expression
Assertion ccatfv0 ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 0 < ( ♯ ‘ 𝐴 ) ) → ( ( 𝐴 ++ 𝐵 ) ‘ 0 ) = ( 𝐴 ‘ 0 ) )

Proof

Step Hyp Ref Expression
1 lencl ⊢ ( 𝐴 ∈ Word 𝑉 → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
2 elnnnn0b ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ↔ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 ∧ 0 < ( ♯ ‘ 𝐴 ) ) )
3 2 biimpri ⊢ ( ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 ∧ 0 < ( ♯ ‘ 𝐴 ) ) → ( ♯ ‘ 𝐴 ) ∈ ℕ )
4 1 3 sylan ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 0 < ( ♯ ‘ 𝐴 ) ) → ( ♯ ‘ 𝐴 ) ∈ ℕ )
5 lbfzo0 ⊢ ( 0 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ↔ ( ♯ ‘ 𝐴 ) ∈ ℕ )
6 4 5 sylibr ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 0 < ( ♯ ‘ 𝐴 ) ) → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) )
7 6 3adant2 ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 0 < ( ♯ ‘ 𝐴 ) ) → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) )
8 ccatval1 ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 0 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ) → ( ( 𝐴 ++ 𝐵 ) ‘ 0 ) = ( 𝐴 ‘ 0 ) )
9 7 8 syld3an3 ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 0 < ( ♯ ‘ 𝐴 ) ) → ( ( 𝐴 ++ 𝐵 ) ‘ 0 ) = ( 𝐴 ‘ 0 ) )