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