Metamath Proof Explorer

Theorem ccat2s1p2OLD

Description: Obsolete version of ccat2s1p2 as of 20-Jan-2024. Extract the second of two concatenated singleton words. (Contributed by Alexander van der Vekens, 22-Sep-2018) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 s1cl ⊢ ( 𝑋 ∈ 𝑉 → ⟨“ 𝑋 ”⟩ ∈ Word 𝑉 )
2 1 adantr ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ⟨“ 𝑋 ”⟩ ∈ Word 𝑉 )
3 s1cl ⊢ ( 𝑌 ∈ 𝑉 → ⟨“ 𝑌 ”⟩ ∈ Word 𝑉 )
4 3 adantl ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ⟨“ 𝑌 ”⟩ ∈ Word 𝑉 )
5 1z ⊢ 1 ∈ ℤ
6 2z ⊢ 2 ∈ ℤ
7 1lt2 ⊢ 1 < 2
8 fzolb ⊢ ( 1 ∈ ( 1 ..^ 2 ) ↔ ( 1 ∈ ℤ ∧ 2 ∈ ℤ ∧ 1 < 2 ) )
9 5 6 7 8 mpbir3an ⊢ 1 ∈ ( 1 ..^ 2 )
10 s1len ⊢ ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) = 1
11 s1len ⊢ ( ♯ ‘ ⟨“ 𝑌 ”⟩ ) = 1
12 10 11 oveq12i ⊢ ( ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) + ( ♯ ‘ ⟨“ 𝑌 ”⟩ ) ) = ( 1 + 1 )
13 1p1e2 ⊢ ( 1 + 1 ) = 2
14 12 13 eqtri ⊢ ( ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) + ( ♯ ‘ ⟨“ 𝑌 ”⟩ ) ) = 2
15 10 14 oveq12i ⊢ ( ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) ..^ ( ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) + ( ♯ ‘ ⟨“ 𝑌 ”⟩ ) ) ) = ( 1 ..^ 2 )
16 9 15 eleqtrri ⊢ 1 ∈ ( ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) ..^ ( ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) + ( ♯ ‘ ⟨“ 𝑌 ”⟩ ) ) )
17 16 a1i ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → 1 ∈ ( ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) ..^ ( ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) + ( ♯ ‘ ⟨“ 𝑌 ”⟩ ) ) ) )
18 ccatval2 ⊢ ( ( ⟨“ 𝑋 ”⟩ ∈ Word 𝑉 ∧ ⟨“ 𝑌 ”⟩ ∈ Word 𝑉 ∧ 1 ∈ ( ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) ..^ ( ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) + ( ♯ ‘ ⟨“ 𝑌 ”⟩ ) ) ) ) → ( ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑌 ”⟩ ) ‘ 1 ) = ( ⟨“ 𝑌 ”⟩ ‘ ( 1 − ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) ) ) )
19 2 4 17 18 syl3anc ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑌 ”⟩ ) ‘ 1 ) = ( ⟨“ 𝑌 ”⟩ ‘ ( 1 − ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) ) ) )
20 10 oveq2i ⊢ ( 1 − ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) ) = ( 1 − 1 )
21 1m1e0 ⊢ ( 1 − 1 ) = 0
22 20 21 eqtri ⊢ ( 1 − ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) ) = 0
23 22 a1i ⊢ ( 𝑌 ∈ 𝑉 → ( 1 − ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) ) = 0 )
24 23 fveq2d ⊢ ( 𝑌 ∈ 𝑉 → ( ⟨“ 𝑌 ”⟩ ‘ ( 1 − ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) ) ) = ( ⟨“ 𝑌 ”⟩ ‘ 0 ) )
25 s1fv ⊢ ( 𝑌 ∈ 𝑉 → ( ⟨“ 𝑌 ”⟩ ‘ 0 ) = 𝑌 )
26 24 25 eqtrd ⊢ ( 𝑌 ∈ 𝑉 → ( ⟨“ 𝑌 ”⟩ ‘ ( 1 − ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) ) ) = 𝑌 )
27 26 adantl ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ⟨“ 𝑌 ”⟩ ‘ ( 1 − ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) ) ) = 𝑌 )
28 19 27 eqtrd ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑌 ”⟩ ) ‘ 1 ) = 𝑌 )