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 ⊢ S ∈ Word B ∧ T ∈ Word B ∧ I ∈ S ..^ S + T → S ++ T ⁡ I = T ⁡ I − S

Proof

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