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
|- 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 ) )