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 | ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) → ( 𝑈 ‘ 𝐴 ) = 〈“ 𝐴 ”〉 ) |
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 | ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) → ( 𝑈 ‘ 𝐴 ) = 〈“ 𝐴 ”〉 ) |