Metamath Proof Explorer


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 ( ( 𝐼𝑉𝐴𝐼 ) → ( 𝑈𝐴 ) = ⟨“ 𝐴 ”⟩ )