Metamath Proof Explorer


Theorem frmdup3lem

Description: Lemma for frmdup3 . (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypotheses frmdup3.m
|- M = ( freeMnd ` I )
frmdup3.b
|- B = ( Base ` G )
frmdup3.u
|- U = ( varFMnd ` I )
Assertion frmdup3lem
|- ( ( ( 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 ) ) ) )

Proof

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