Metamath Proof Explorer

Theorem ccats1val2

Description: Value of the symbol concatenated with a word. (Contributed by Alexander van der Vekens, 5-Aug-2018) (Proof shortened by Alexander van der Vekens, 14-Oct-2018)

Ref Expression
Assertion ccats1val2 ⊢ W ∈ Word V ∧ S ∈ V ∧ I = W → W ++ ⟨“ S ”⟩ ⁡ I = S

Proof

Step Hyp Ref Expression
1 simp1 ⊢ W ∈ Word V ∧ S ∈ V ∧ I = W → W ∈ Word V
2 s1cl ⊢ S ∈ V → ⟨“ S ”⟩ ∈ Word V
3 2 3ad2ant2 ⊢ W ∈ Word V ∧ S ∈ V ∧ I = W → ⟨“ S ”⟩ ∈ Word V
4 lencl ⊢ W ∈ Word V → W ∈ ℕ 0
5 4 nn0zd ⊢ W ∈ Word V → W ∈ ℤ
6 elfzomin ⊢ W ∈ ℤ → W ∈ W ..^ W + 1
7 5 6 syl ⊢ W ∈ Word V → W ∈ W ..^ W + 1
8 s1len ⊢ ⟨“ S ”⟩ = 1
9 8 oveq2i ⊢ W + ⟨“ S ”⟩ = W + 1
10 9 oveq2i ⊢ W ..^ W + ⟨“ S ”⟩ = W ..^ W + 1
11 7 10 eleqtrrdi ⊢ W ∈ Word V → W ∈ W ..^ W + ⟨“ S ”⟩
12 11 adantr ⊢ W ∈ Word V ∧ I = W → W ∈ W ..^ W + ⟨“ S ”⟩
13 eleq1 ⊢ I = W → I ∈ W ..^ W + ⟨“ S ”⟩ ↔ W ∈ W ..^ W + ⟨“ S ”⟩
14 13 adantl ⊢ W ∈ Word V ∧ I = W → I ∈ W ..^ W + ⟨“ S ”⟩ ↔ W ∈ W ..^ W + ⟨“ S ”⟩
15 12 14 mpbird ⊢ W ∈ Word V ∧ I = W → I ∈ W ..^ W + ⟨“ S ”⟩
16 15 3adant2 ⊢ W ∈ Word V ∧ S ∈ V ∧ I = W → I ∈ W ..^ W + ⟨“ S ”⟩
17 ccatval2 ⊢ W ∈ Word V ∧ ⟨“ S ”⟩ ∈ Word V ∧ I ∈ W ..^ W + ⟨“ S ”⟩ → W ++ ⟨“ S ”⟩ ⁡ I = ⟨“ S ”⟩ ⁡ I − W
18 1 3 16 17 syl3anc ⊢ W ∈ Word V ∧ S ∈ V ∧ I = W → W ++ ⟨“ S ”⟩ ⁡ I = ⟨“ S ”⟩ ⁡ I − W
19 oveq1 ⊢ I = W → I − W = W − W
20 19 3ad2ant3 ⊢ W ∈ Word V ∧ S ∈ V ∧ I = W → I − W = W − W
21 4 nn0cnd ⊢ W ∈ Word V → W ∈ ℂ
22 21 subidd ⊢ W ∈ Word V → W − W = 0
23 22 3ad2ant1 ⊢ W ∈ Word V ∧ S ∈ V ∧ I = W → W − W = 0
24 20 23 eqtrd ⊢ W ∈ Word V ∧ S ∈ V ∧ I = W → I − W = 0
25 24 fveq2d ⊢ W ∈ Word V ∧ S ∈ V ∧ I = W → ⟨“ S ”⟩ ⁡ I − W = ⟨“ S ”⟩ ⁡ 0
26 s1fv ⊢ S ∈ V → ⟨“ S ”⟩ ⁡ 0 = S
27 26 3ad2ant2 ⊢ W ∈ Word V ∧ S ∈ V ∧ I = W → ⟨“ S ”⟩ ⁡ 0 = S
28 18 25 27 3eqtrd ⊢ W ∈ Word V ∧ S ∈ V ∧ I = W → W ++ ⟨“ S ”⟩ ⁡ I = S