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

Metamath Proof Explorer

Theorem ccatval1

Description: Value of a symbol in the left half of a concatenated word. (Contributed by Stefan O'Rear, 15-Aug-2015) (Revised by Mario Carneiro, 22-Sep-2015) (Proof shortened by AV, 30-Apr-2020) (Revised by JJ, 18-Jan-2024)

Ref Expression
Assertion ccatval1 ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → ( ( 𝑆 ++ 𝑇 ) ‘ 𝐼 ) = ( 𝑆 ‘ 𝐼 ) )

Proof

Step Hyp Ref Expression
1 ccatfval ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐵 ) → ( 𝑆 ++ 𝑇 ) = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) , ( 𝑆 ‘ 𝑥 ) , ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) ) ) )
2 1 3adant3 ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → ( 𝑆 ++ 𝑇 ) = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) , ( 𝑆 ‘ 𝑥 ) , ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) ) ) )
3 eleq1 ⊢ ( 𝑥 = 𝐼 → ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ↔ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) )
4 fveq2 ⊢ ( 𝑥 = 𝐼 → ( 𝑆 ‘ 𝑥 ) = ( 𝑆 ‘ 𝐼 ) )
5 fvoveq1 ⊢ ( 𝑥 = 𝐼 → ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) = ( 𝑇 ‘ ( 𝐼 − ( ♯ ‘ 𝑆 ) ) ) )
6 3 4 5 ifbieq12d ⊢ ( 𝑥 = 𝐼 → if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) , ( 𝑆 ‘ 𝑥 ) , ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) ) = if ( 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) , ( 𝑆 ‘ 𝐼 ) , ( 𝑇 ‘ ( 𝐼 − ( ♯ ‘ 𝑆 ) ) ) ) )
7 iftrue ⊢ ( 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) → if ( 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) , ( 𝑆 ‘ 𝐼 ) , ( 𝑇 ‘ ( 𝐼 − ( ♯ ‘ 𝑆 ) ) ) ) = ( 𝑆 ‘ 𝐼 ) )
8 7 3ad2ant3 ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → if ( 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) , ( 𝑆 ‘ 𝐼 ) , ( 𝑇 ‘ ( 𝐼 − ( ♯ ‘ 𝑆 ) ) ) ) = ( 𝑆 ‘ 𝐼 ) )
9 6 8 sylan9eqr ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) ∧ 𝑥 = 𝐼 ) → if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) , ( 𝑆 ‘ 𝑥 ) , ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) ) = ( 𝑆 ‘ 𝐼 ) )
10 id ⊢ ( 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) → 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) )
11 lencl ⊢ ( 𝑇 ∈ Word 𝐵 → ( ♯ ‘ 𝑇 ) ∈ ℕ0 )
12 elfzoext ⊢ ( ( 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ∧ ( ♯ ‘ 𝑇 ) ∈ ℕ0 ) → 𝐼 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) )
13 10 11 12 syl2anr ⊢ ( ( 𝑇 ∈ Word 𝐵 ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → 𝐼 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) )
14 13 3adant1 ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → 𝐼 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) )
15 fvexd ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → ( 𝑆 ‘ 𝐼 ) ∈ V )
16 2 9 14 15 fvmptd ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → ( ( 𝑆 ++ 𝑇 ) ‘ 𝐼 ) = ( 𝑆 ‘ 𝐼 ) )