This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ffvelcdmd ⊢ ( 𝜑 → ( 𝐴 ‘ 𝑌 ) ∈ 𝐵 )
22 2 gsumws1 ⊢ ( ( 𝐴 ‘ 𝑌 ) ∈ 𝐵 → ( 𝐺 Σg ⟨“ ( 𝐴 ‘ 𝑌 ) ”⟩ ) = ( 𝐴 ‘ 𝑌 ) )
23 21 22 syl ⊢ ( 𝜑 → ( 𝐺 Σg ⟨“ ( 𝐴 ‘ 𝑌 ) ”⟩ ) = ( 𝐴 ‘ 𝑌 ) )
24 17 20 23 3eqtrd ⊢ ( 𝜑 → ( 𝐸 ‘ ⟨“ 𝑌 ”⟩ ) = ( 𝐴 ‘ 𝑌 ) )
25 11 24 eqtrd ⊢ ( 𝜑 → ( 𝐸 ‘ ( 𝑈 ‘ 𝑌 ) ) = ( 𝐴 ‘ 𝑌 ) )