Theorem vrmdval

Description: The value of the generating elements of a free monoid. (Contributed by Mario Carneiro, 27-Feb-2016)

	Ref	Expression
Hypothesis	vrmdfval.u	⊢ 𝑈 = ( varFMnd ‘ 𝐼 )
Assertion	vrmdval	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) → ( 𝑈 ‘ 𝐴 ) = ⟨“ 𝐴 ”⟩ )

Proof

Step	Hyp	Ref	Expression
1		vrmdfval.u	⊢ 𝑈 = ( varFMnd ‘ 𝐼 )
2	1	vrmdfval	⊢ ( 𝐼 ∈ 𝑉 → 𝑈 = ( 𝑗 ∈ 𝐼 ↦ ⟨“ 𝑗 ”⟩ ) )
3	2	adantr	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) → 𝑈 = ( 𝑗 ∈ 𝐼 ↦ ⟨“ 𝑗 ”⟩ ) )
4		s1eq	⊢ ( 𝑗 = 𝐴 → ⟨“ 𝑗 ”⟩ = ⟨“ 𝐴 ”⟩ )
5	4	adantl	⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) ∧ 𝑗 = 𝐴 ) → ⟨“ 𝑗 ”⟩ = ⟨“ 𝐴 ”⟩ )
6		simpr	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) → 𝐴 ∈ 𝐼 )
7		s1cl	⊢ ( 𝐴 ∈ 𝐼 → ⟨“ 𝐴 ”⟩ ∈ Word 𝐼 )
8	7	adantl	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) → ⟨“ 𝐴 ”⟩ ∈ Word 𝐼 )
9	3 5 6 8	fvmptd	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) → ( 𝑈 ‘ 𝐴 ) = ⟨“ 𝐴 ”⟩ )