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	|- M = ( freeMnd ` I )
	frmdup.b	|- B = ( Base ` G )
	frmdup.e	|- E = ( x e. Word I |-> ( G gsum ( A o. x ) ) )
	frmdup.g	|- ( ph -> G e. Mnd )
	frmdup.i	|- ( ph -> I e. X )
	frmdup.a	|- ( ph -> A : I --> B )
	frmdup2.u	|- U = ( varFMnd ` I )
	frmdup2.y	|- ( ph -> Y e. I )
Assertion	frmdup2	|- ( ph -> ( E ` ( U ` Y ) ) = ( A ` Y ) )

Proof

Step	Hyp	Ref	Expression
1		frmdup.m	|- M = ( freeMnd ` I )
2		frmdup.b	|- B = ( Base ` G )
3		frmdup.e	|- E = ( x e. Word I |-> ( G gsum ( A o. x ) ) )
4		frmdup.g	|- ( ph -> G e. Mnd )
5		frmdup.i	|- ( ph -> I e. X )
6		frmdup.a	|- ( ph -> A : I --> B )
7		frmdup2.u	|- U = ( varFMnd ` I )
8		frmdup2.y	|- ( ph -> Y e. I )
9	7	vrmdval	|- ( ( I e. X /\ Y e. I ) -> ( U ` Y ) = <" Y "> )
10	5 8 9	syl2anc	|- ( ph -> ( U ` Y ) = <" Y "> )
11	10	fveq2d	|- ( ph -> ( E ` ( U ` Y ) ) = ( E ` <" Y "> ) )
12	8	s1cld	|- ( ph -> <" Y "> e. Word I )
13		coeq2	|- ( x = <" Y "> -> ( A o. x ) = ( A o. <" Y "> ) )
14	13	oveq2d	|- ( x = <" Y "> -> ( G gsum ( A o. x ) ) = ( G gsum ( A o. <" Y "> ) ) )
15		ovex	|- ( G gsum ( A o. x ) ) e. _V
16	14 3 15	fvmpt3i	|- ( <" Y "> e. Word I -> ( E ` <" Y "> ) = ( G gsum ( A o. <" Y "> ) ) )
17	12 16	syl	|- ( ph -> ( E ` <" Y "> ) = ( G gsum ( A o. <" Y "> ) ) )
18		s1co	|- ( ( Y e. I /\ A : I --> B ) -> ( A o. <" Y "> ) = <" ( A ` Y ) "> )
19	8 6 18	syl2anc	|- ( ph -> ( A o. <" Y "> ) = <" ( A ` Y ) "> )
20	19	oveq2d	|- ( ph -> ( G gsum ( A o. <" Y "> ) ) = ( G gsum <" ( A ` Y ) "> ) )
21	6 8	ffvelrnd	|- ( ph -> ( A ` Y ) e. B )
22	2	gsumws1	|- ( ( A ` Y ) e. B -> ( G gsum <" ( A ` Y ) "> ) = ( A ` Y ) )
23	21 22	syl	|- ( ph -> ( G gsum <" ( A ` Y ) "> ) = ( A ` Y ) )
24	17 20 23	3eqtrd	|- ( ph -> ( E ` <" Y "> ) = ( A ` Y ) )
25	11 24	eqtrd	|- ( ph -> ( E ` ( U ` Y ) ) = ( A ` Y ) )