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

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 ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ 𝑉 ∧ 𝐼 = ( ♯ ‘ 𝑊 ) ) → ( ( 𝑊 ++ ⟨“ 𝑆 ”⟩ ) ‘ 𝐼 ) = 𝑆 )

Proof

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