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	⊢ ( 𝜑 → ( 𝐸 ‘ ( 𝑈 ‘ 𝑌 ) ) = ( 𝐴 ‘ 𝑌 ) )