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