Step |
Hyp |
Ref |
Expression |
1 |
|
frmdup3.m |
|- M = ( freeMnd ` I ) |
2 |
|
frmdup3.b |
|- B = ( Base ` G ) |
3 |
|
frmdup3.u |
|- U = ( varFMnd ` I ) |
4 |
|
eqid |
|- ( Base ` M ) = ( Base ` M ) |
5 |
4 2
|
mhmf |
|- ( F e. ( M MndHom G ) -> F : ( Base ` M ) --> B ) |
6 |
5
|
ad2antrl |
|- ( ( ( G e. Mnd /\ I e. V /\ A : I --> B ) /\ ( F e. ( M MndHom G ) /\ ( F o. U ) = A ) ) -> F : ( Base ` M ) --> B ) |
7 |
1 4
|
frmdbas |
|- ( I e. V -> ( Base ` M ) = Word I ) |
8 |
7
|
3ad2ant2 |
|- ( ( G e. Mnd /\ I e. V /\ A : I --> B ) -> ( Base ` M ) = Word I ) |
9 |
8
|
adantr |
|- ( ( ( G e. Mnd /\ I e. V /\ A : I --> B ) /\ ( F e. ( M MndHom G ) /\ ( F o. U ) = A ) ) -> ( Base ` M ) = Word I ) |
10 |
9
|
feq2d |
|- ( ( ( G e. Mnd /\ I e. V /\ A : I --> B ) /\ ( F e. ( M MndHom G ) /\ ( F o. U ) = A ) ) -> ( F : ( Base ` M ) --> B <-> F : Word I --> B ) ) |
11 |
6 10
|
mpbid |
|- ( ( ( G e. Mnd /\ I e. V /\ A : I --> B ) /\ ( F e. ( M MndHom G ) /\ ( F o. U ) = A ) ) -> F : Word I --> B ) |
12 |
11
|
feqmptd |
|- ( ( ( G e. Mnd /\ I e. V /\ A : I --> B ) /\ ( F e. ( M MndHom G ) /\ ( F o. U ) = A ) ) -> F = ( x e. Word I |-> ( F ` x ) ) ) |
13 |
|
simplrl |
|- ( ( ( ( G e. Mnd /\ I e. V /\ A : I --> B ) /\ ( F e. ( M MndHom G ) /\ ( F o. U ) = A ) ) /\ x e. Word I ) -> F e. ( M MndHom G ) ) |
14 |
|
simpr |
|- ( ( ( ( G e. Mnd /\ I e. V /\ A : I --> B ) /\ ( F e. ( M MndHom G ) /\ ( F o. U ) = A ) ) /\ x e. Word I ) -> x e. Word I ) |
15 |
3
|
vrmdf |
|- ( I e. V -> U : I --> Word I ) |
16 |
15
|
3ad2ant2 |
|- ( ( G e. Mnd /\ I e. V /\ A : I --> B ) -> U : I --> Word I ) |
17 |
8
|
feq3d |
|- ( ( G e. Mnd /\ I e. V /\ A : I --> B ) -> ( U : I --> ( Base ` M ) <-> U : I --> Word I ) ) |
18 |
16 17
|
mpbird |
|- ( ( G e. Mnd /\ I e. V /\ A : I --> B ) -> U : I --> ( Base ` M ) ) |
19 |
18
|
ad2antrr |
|- ( ( ( ( G e. Mnd /\ I e. V /\ A : I --> B ) /\ ( F e. ( M MndHom G ) /\ ( F o. U ) = A ) ) /\ x e. Word I ) -> U : I --> ( Base ` M ) ) |
20 |
|
wrdco |
|- ( ( x e. Word I /\ U : I --> ( Base ` M ) ) -> ( U o. x ) e. Word ( Base ` M ) ) |
21 |
14 19 20
|
syl2anc |
|- ( ( ( ( G e. Mnd /\ I e. V /\ A : I --> B ) /\ ( F e. ( M MndHom G ) /\ ( F o. U ) = A ) ) /\ x e. Word I ) -> ( U o. x ) e. Word ( Base ` M ) ) |
22 |
4
|
gsumwmhm |
|- ( ( F e. ( M MndHom G ) /\ ( U o. x ) e. Word ( Base ` M ) ) -> ( F ` ( M gsum ( U o. x ) ) ) = ( G gsum ( F o. ( U o. x ) ) ) ) |
23 |
13 21 22
|
syl2anc |
|- ( ( ( ( G e. Mnd /\ I e. V /\ A : I --> B ) /\ ( F e. ( M MndHom G ) /\ ( F o. U ) = A ) ) /\ x e. Word I ) -> ( F ` ( M gsum ( U o. x ) ) ) = ( G gsum ( F o. ( U o. x ) ) ) ) |
24 |
|
simpll2 |
|- ( ( ( ( G e. Mnd /\ I e. V /\ A : I --> B ) /\ ( F e. ( M MndHom G ) /\ ( F o. U ) = A ) ) /\ x e. Word I ) -> I e. V ) |
25 |
1 3
|
frmdgsum |
|- ( ( I e. V /\ x e. Word I ) -> ( M gsum ( U o. x ) ) = x ) |
26 |
24 14 25
|
syl2anc |
|- ( ( ( ( G e. Mnd /\ I e. V /\ A : I --> B ) /\ ( F e. ( M MndHom G ) /\ ( F o. U ) = A ) ) /\ x e. Word I ) -> ( M gsum ( U o. x ) ) = x ) |
27 |
26
|
fveq2d |
|- ( ( ( ( G e. Mnd /\ I e. V /\ A : I --> B ) /\ ( F e. ( M MndHom G ) /\ ( F o. U ) = A ) ) /\ x e. Word I ) -> ( F ` ( M gsum ( U o. x ) ) ) = ( F ` x ) ) |
28 |
|
coass |
|- ( ( F o. U ) o. x ) = ( F o. ( U o. x ) ) |
29 |
|
simplrr |
|- ( ( ( ( G e. Mnd /\ I e. V /\ A : I --> B ) /\ ( F e. ( M MndHom G ) /\ ( F o. U ) = A ) ) /\ x e. Word I ) -> ( F o. U ) = A ) |
30 |
29
|
coeq1d |
|- ( ( ( ( G e. Mnd /\ I e. V /\ A : I --> B ) /\ ( F e. ( M MndHom G ) /\ ( F o. U ) = A ) ) /\ x e. Word I ) -> ( ( F o. U ) o. x ) = ( A o. x ) ) |
31 |
28 30
|
eqtr3id |
|- ( ( ( ( G e. Mnd /\ I e. V /\ A : I --> B ) /\ ( F e. ( M MndHom G ) /\ ( F o. U ) = A ) ) /\ x e. Word I ) -> ( F o. ( U o. x ) ) = ( A o. x ) ) |
32 |
31
|
oveq2d |
|- ( ( ( ( G e. Mnd /\ I e. V /\ A : I --> B ) /\ ( F e. ( M MndHom G ) /\ ( F o. U ) = A ) ) /\ x e. Word I ) -> ( G gsum ( F o. ( U o. x ) ) ) = ( G gsum ( A o. x ) ) ) |
33 |
23 27 32
|
3eqtr3d |
|- ( ( ( ( G e. Mnd /\ I e. V /\ A : I --> B ) /\ ( F e. ( M MndHom G ) /\ ( F o. U ) = A ) ) /\ x e. Word I ) -> ( F ` x ) = ( G gsum ( A o. x ) ) ) |
34 |
33
|
mpteq2dva |
|- ( ( ( G e. Mnd /\ I e. V /\ A : I --> B ) /\ ( F e. ( M MndHom G ) /\ ( F o. U ) = A ) ) -> ( x e. Word I |-> ( F ` x ) ) = ( x e. Word I |-> ( G gsum ( A o. x ) ) ) ) |
35 |
12 34
|
eqtrd |
|- ( ( ( G e. Mnd /\ I e. V /\ A : I --> B ) /\ ( F e. ( M MndHom G ) /\ ( F o. U ) = A ) ) -> F = ( x e. Word I |-> ( G gsum ( A o. x ) ) ) ) |