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 ) = 𝑌 )