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

Metamath Proof Explorer

Theorem ccatval2

Description: Value of a symbol in the right half of a concatenated word. (Contributed by Stefan O'Rear, 15-Aug-2015) (Revised by Mario Carneiro, 22-Sep-2015)

Ref Expression
Assertion ccatval2 ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝐼 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) → ( ( 𝑆 ++ 𝑇 ) ‘ 𝐼 ) = ( 𝑇 ‘ ( 𝐼 − ( ♯ ‘ 𝑆 ) ) ) )

Proof

Step Hyp Ref Expression
1 ccatfval ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) → ( 𝑆 ++ 𝑇 ) = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) , ( 𝑆 ‘ 𝑥 ) , ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) ) ) )
2 1 3adant3 ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝐼 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) → ( 𝑆 ++ 𝑇 ) = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) , ( 𝑆 ‘ 𝑥 ) , ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) ) ) )
3 eleq1 ⊢ ( 𝑥 = 𝐼 → ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ↔ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) )
4 fveq2 ⊢ ( 𝑥 = 𝐼 → ( 𝑆 ‘ 𝑥 ) = ( 𝑆 ‘ 𝐼 ) )
5 fvoveq1 ⊢ ( 𝑥 = 𝐼 → ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) = ( 𝑇 ‘ ( 𝐼 − ( ♯ ‘ 𝑆 ) ) ) )
6 3 4 5 ifbieq12d ⊢ ( 𝑥 = 𝐼 → if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) , ( 𝑆 ‘ 𝑥 ) , ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) ) = if ( 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) , ( 𝑆 ‘ 𝐼 ) , ( 𝑇 ‘ ( 𝐼 − ( ♯ ‘ 𝑆 ) ) ) ) )
7 fzodisj ⊢ ( ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ∩ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) = ∅
8 minel ⊢ ( ( 𝐼 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ∧ ( ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ∩ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) = ∅ ) → ¬ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) )
9 7 8 mpan2 ⊢ ( 𝐼 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) → ¬ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) )
10 9 3ad2ant3 ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝐼 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) → ¬ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) )
11 10 iffalsed ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝐼 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) → if ( 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) , ( 𝑆 ‘ 𝐼 ) , ( 𝑇 ‘ ( 𝐼 − ( ♯ ‘ 𝑆 ) ) ) ) = ( 𝑇 ‘ ( 𝐼 − ( ♯ ‘ 𝑆 ) ) ) )
12 6 11 sylan9eqr ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝐼 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) ∧ 𝑥 = 𝐼 ) → if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) , ( 𝑆 ‘ 𝑥 ) , ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) ) = ( 𝑇 ‘ ( 𝐼 − ( ♯ ‘ 𝑆 ) ) ) )
13 wrdfin ⊢ ( 𝑆 ∈ Word 𝐵 → 𝑆 ∈ Fin )
14 13 adantr ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) → 𝑆 ∈ Fin )
15 hashcl ⊢ ( 𝑆 ∈ Fin → ( ♯ ‘ 𝑆 ) ∈ ℕ0 )
16 fzoss1 ⊢ ( ( ♯ ‘ 𝑆 ) ∈ ( ℤ≥ ‘ 0 ) → ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ⊆ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) )
17 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
18 16 17 eleq2s ⊢ ( ( ♯ ‘ 𝑆 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ⊆ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) )
19 14 15 18 3syl ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) → ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ⊆ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) )
20 19 sseld ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) → ( 𝐼 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) → 𝐼 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) )
21 20 3impia ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝐼 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) → 𝐼 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) )
22 fvexd ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝐼 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) → ( 𝑇 ‘ ( 𝐼 − ( ♯ ‘ 𝑆 ) ) ) ∈ V )
23 2 12 21 22 fvmptd ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝐼 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) → ( ( 𝑆 ++ 𝑇 ) ‘ 𝐼 ) = ( 𝑇 ‘ ( 𝐼 − ( ♯ ‘ 𝑆 ) ) ) )