Metamath Proof Explorer


Theorem frmdup2

Description: The evaluation map has the intended behavior on the generators. (Contributed by Mario Carneiro, 27-Sep-2015)

Ref Expression
Hypotheses frmdup.m 𝑀 = ( freeMnd ‘ 𝐼 )
frmdup.b 𝐵 = ( Base ‘ 𝐺 )
frmdup.e 𝐸 = ( 𝑥 ∈ Word 𝐼 ↦ ( 𝐺 Σg ( 𝐴𝑥 ) ) )
frmdup.g ( 𝜑𝐺 ∈ Mnd )
frmdup.i ( 𝜑𝐼𝑋 )
frmdup.a ( 𝜑𝐴 : 𝐼𝐵 )
frmdup2.u 𝑈 = ( varFMnd𝐼 )
frmdup2.y ( 𝜑𝑌𝐼 )
Assertion frmdup2 ( 𝜑 → ( 𝐸 ‘ ( 𝑈𝑌 ) ) = ( 𝐴𝑌 ) )

Proof

Step Hyp Ref Expression
1 frmdup.m 𝑀 = ( freeMnd ‘ 𝐼 )
2 frmdup.b 𝐵 = ( Base ‘ 𝐺 )
3 frmdup.e 𝐸 = ( 𝑥 ∈ Word 𝐼 ↦ ( 𝐺 Σg ( 𝐴𝑥 ) ) )
4 frmdup.g ( 𝜑𝐺 ∈ Mnd )
5 frmdup.i ( 𝜑𝐼𝑋 )
6 frmdup.a ( 𝜑𝐴 : 𝐼𝐵 )
7 frmdup2.u 𝑈 = ( varFMnd𝐼 )
8 frmdup2.y ( 𝜑𝑌𝐼 )
9 7 vrmdval ( ( 𝐼𝑋𝑌𝐼 ) → ( 𝑈𝑌 ) = ⟨“ 𝑌 ”⟩ )
10 5 8 9 syl2anc ( 𝜑 → ( 𝑈𝑌 ) = ⟨“ 𝑌 ”⟩ )
11 10 fveq2d ( 𝜑 → ( 𝐸 ‘ ( 𝑈𝑌 ) ) = ( 𝐸 ‘ ⟨“ 𝑌 ”⟩ ) )
12 8 s1cld ( 𝜑 → ⟨“ 𝑌 ”⟩ ∈ Word 𝐼 )
13 coeq2 ( 𝑥 = ⟨“ 𝑌 ”⟩ → ( 𝐴𝑥 ) = ( 𝐴 ∘ ⟨“ 𝑌 ”⟩ ) )
14 13 oveq2d ( 𝑥 = ⟨“ 𝑌 ”⟩ → ( 𝐺 Σg ( 𝐴𝑥 ) ) = ( 𝐺 Σg ( 𝐴 ∘ ⟨“ 𝑌 ”⟩ ) ) )
15 ovex ( 𝐺 Σg ( 𝐴𝑥 ) ) ∈ V
16 14 3 15 fvmpt3i ( ⟨“ 𝑌 ”⟩ ∈ Word 𝐼 → ( 𝐸 ‘ ⟨“ 𝑌 ”⟩ ) = ( 𝐺 Σg ( 𝐴 ∘ ⟨“ 𝑌 ”⟩ ) ) )
17 12 16 syl ( 𝜑 → ( 𝐸 ‘ ⟨“ 𝑌 ”⟩ ) = ( 𝐺 Σg ( 𝐴 ∘ ⟨“ 𝑌 ”⟩ ) ) )
18 s1co ( ( 𝑌𝐼𝐴 : 𝐼𝐵 ) → ( 𝐴 ∘ ⟨“ 𝑌 ”⟩ ) = ⟨“ ( 𝐴𝑌 ) ”⟩ )
19 8 6 18 syl2anc ( 𝜑 → ( 𝐴 ∘ ⟨“ 𝑌 ”⟩ ) = ⟨“ ( 𝐴𝑌 ) ”⟩ )
20 19 oveq2d ( 𝜑 → ( 𝐺 Σg ( 𝐴 ∘ ⟨“ 𝑌 ”⟩ ) ) = ( 𝐺 Σg ⟨“ ( 𝐴𝑌 ) ”⟩ ) )
21 6 8 ffvelrnd ( 𝜑 → ( 𝐴𝑌 ) ∈ 𝐵 )
22 2 gsumws1 ( ( 𝐴𝑌 ) ∈ 𝐵 → ( 𝐺 Σg ⟨“ ( 𝐴𝑌 ) ”⟩ ) = ( 𝐴𝑌 ) )
23 21 22 syl ( 𝜑 → ( 𝐺 Σg ⟨“ ( 𝐴𝑌 ) ”⟩ ) = ( 𝐴𝑌 ) )
24 17 20 23 3eqtrd ( 𝜑 → ( 𝐸 ‘ ⟨“ 𝑌 ”⟩ ) = ( 𝐴𝑌 ) )
25 11 24 eqtrd ( 𝜑 → ( 𝐸 ‘ ( 𝑈𝑌 ) ) = ( 𝐴𝑌 ) )