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