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