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

Metamath Proof Explorer

Theorem ccat2s1p2

Description: Extract the second of two concatenated singleton words. (Contributed by Alexander van der Vekens, 22-Sep-2018) (Revised by JJ, 20-Jan-2024)

Ref Expression
Assertion ccat2s1p2 ( 𝑌 ∈ 𝑉 → ( ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑌 ”⟩ ) ‘ 1 ) = 𝑌 )

Proof

Step Hyp Ref Expression
1 s1cli ⊢ ⟨“ 𝑋 ”⟩ ∈ Word V
2 s1cli ⊢ ⟨“ 𝑌 ”⟩ ∈ Word V
3 1z ⊢ 1 ∈ ℤ
4 2z ⊢ 2 ∈ ℤ
5 1lt2 ⊢ 1 < 2
6 fzolb ⊢ ( 1 ∈ ( 1 ..^ 2 ) ↔ ( 1 ∈ ℤ ∧ 2 ∈ ℤ ∧ 1 < 2 ) )
7 3 4 5 6 mpbir3an ⊢ 1 ∈ ( 1 ..^ 2 )
8 s1len ⊢ ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) = 1
9 s1len ⊢ ( ♯ ‘ ⟨“ 𝑌 ”⟩ ) = 1
10 8 9 oveq12i ⊢ ( ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) + ( ♯ ‘ ⟨“ 𝑌 ”⟩ ) ) = ( 1 + 1 )
11 1p1e2 ⊢ ( 1 + 1 ) = 2
12 10 11 eqtri ⊢ ( ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) + ( ♯ ‘ ⟨“ 𝑌 ”⟩ ) ) = 2
13 8 12 oveq12i ⊢ ( ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) ..^ ( ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) + ( ♯ ‘ ⟨“ 𝑌 ”⟩ ) ) ) = ( 1 ..^ 2 )
14 7 13 eleqtrri ⊢ 1 ∈ ( ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) ..^ ( ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) + ( ♯ ‘ ⟨“ 𝑌 ”⟩ ) ) )
15 ccatval2 ⊢ ( ( ⟨“ 𝑋 ”⟩ ∈ Word V ∧ ⟨“ 𝑌 ”⟩ ∈ Word V ∧ 1 ∈ ( ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) ..^ ( ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) + ( ♯ ‘ ⟨“ 𝑌 ”⟩ ) ) ) ) → ( ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑌 ”⟩ ) ‘ 1 ) = ( ⟨“ 𝑌 ”⟩ ‘ ( 1 − ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) ) ) )
16 1 2 14 15 mp3an ⊢ ( ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑌 ”⟩ ) ‘ 1 ) = ( ⟨“ 𝑌 ”⟩ ‘ ( 1 − ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) ) )
17 8 oveq2i ⊢ ( 1 − ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) ) = ( 1 − 1 )
18 1m1e0 ⊢ ( 1 − 1 ) = 0
19 17 18 eqtri ⊢ ( 1 − ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) ) = 0
20 19 fveq2i ⊢ ( ⟨“ 𝑌 ”⟩ ‘ ( 1 − ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) ) ) = ( ⟨“ 𝑌 ”⟩ ‘ 0 )
21 16 20 eqtri ⊢ ( ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑌 ”⟩ ) ‘ 1 ) = ( ⟨“ 𝑌 ”⟩ ‘ 0 )
22 s1fv ⊢ ( 𝑌 ∈ 𝑉 → ( ⟨“ 𝑌 ”⟩ ‘ 0 ) = 𝑌 )
23 21 22 eqtrid ⊢ ( 𝑌 ∈ 𝑉 → ( ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑌 ”⟩ ) ‘ 1 ) = 𝑌 )