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 𝐵 ∧ 𝐼 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) → ( ( 𝑆 ++ 𝑇 ) ‘ 𝐼 ) = ( 𝑇 ‘ ( 𝐼 − ( ♯ ‘ 𝑆 ) ) ) )