Metamath Proof Explorer

Theorem frgpup2

Description: The evaluation map has the intended behavior on the generators. (Contributed by Mario Carneiro, 2-Oct-2015) (Revised by Mario Carneiro, 28-Feb-2016)

Ref Expression
Hypotheses frgpup.b 
|- B = ( Base ` H )
frgpup.n 
|- N = ( invg ` H )
frgpup.t 
|- T = ( y e. I , z e. 2o |-> if ( z = (/) , ( F ` y ) , ( N ` ( F ` y ) ) ) )
frgpup.h 
|- ( ph -> H e. Grp )
frgpup.i 
|- ( ph -> I e. V )
frgpup.a 
|- ( ph -> F : I --> B )
frgpup.w 
|- W = ( _I ` Word ( I X. 2o ) )
frgpup.r 
|- .~ = ( ~FG ` I )
frgpup.g 
|- G = ( freeGrp ` I )
frgpup.x 
|- X = ( Base ` G )
frgpup.e 
|- E = ran ( g e. W |-> <. [ g ] .~ , ( H gsum ( T o. g ) ) >. )
frgpup.u 
|- U = ( varFGrp ` I )
frgpup.y 
|- ( ph -> A e. I )
Assertion frgpup2 
|- ( ph -> ( E ` ( U ` A ) ) = ( F ` A ) )

Proof

Step Hyp Ref Expression
1 frgpup.b 
 |-  B = ( Base ` H )
2 frgpup.n 
 |-  N = ( invg ` H )
3 frgpup.t 
 |-  T = ( y e. I , z e. 2o |-> if ( z = (/) , ( F ` y ) , ( N ` ( F ` y ) ) ) )
4 frgpup.h 
 |-  ( ph -> H e. Grp )
5 frgpup.i 
 |-  ( ph -> I e. V )
6 frgpup.a 
 |-  ( ph -> F : I --> B )
7 frgpup.w 
 |-  W = ( _I ` Word ( I X. 2o ) )
8 frgpup.r 
 |-  .~ = ( ~FG ` I )
9 frgpup.g 
 |-  G = ( freeGrp ` I )
10 frgpup.x 
 |-  X = ( Base ` G )
11 frgpup.e 
 |-  E = ran ( g e. W |-> <. [ g ] .~ , ( H gsum ( T o. g ) ) >. )
12 frgpup.u 
 |-  U = ( varFGrp ` I )
13 frgpup.y 
 |-  ( ph -> A e. I )
14 8 12 vrgpval 
 |-  ( ( I e. V /\ A e. I ) -> ( U ` A ) = [ <" <. A , (/) >. "> ] .~ )
15 5 13 14 syl2anc 
 |-  ( ph -> ( U ` A ) = [ <" <. A , (/) >. "> ] .~ )
16 15 fveq2d 
 |-  ( ph -> ( E ` ( U ` A ) ) = ( E ` [ <" <. A , (/) >. "> ] .~ ) )
17 0ex 
 |-  (/) e. _V
18 17 prid1 
 |-  (/) e. { (/) , 1o }
19 df2o3 
 |-  2o = { (/) , 1o }
20 18 19 eleqtrri 
 |-  (/) e. 2o
21 opelxpi 
 |-  ( ( A e. I /\ (/) e. 2o ) -> <. A , (/) >. e. ( I X. 2o ) )
22 13 20 21 sylancl 
 |-  ( ph -> <. A , (/) >. e. ( I X. 2o ) )
23 22 s1cld 
 |-  ( ph -> <" <. A , (/) >. "> e. Word ( I X. 2o ) )
24 2on 
 |-  2o e. On
25 xpexg 
 |-  ( ( I e. V /\ 2o e. On ) -> ( I X. 2o ) e. _V )
26 5 24 25 sylancl 
 |-  ( ph -> ( I X. 2o ) e. _V )
27 wrdexg 
 |-  ( ( I X. 2o ) e. _V -> Word ( I X. 2o ) e. _V )
28 fvi 
 |-  ( Word ( I X. 2o ) e. _V -> ( _I ` Word ( I X. 2o ) ) = Word ( I X. 2o ) )
29 26 27 28 3syl 
 |-  ( ph -> ( _I ` Word ( I X. 2o ) ) = Word ( I X. 2o ) )
30 7 29 syl5eq 
 |-  ( ph -> W = Word ( I X. 2o ) )
31 23 30 eleqtrrd 
 |-  ( ph -> <" <. A , (/) >. "> e. W )
32 1 2 3 4 5 6 7 8 9 10 11 frgpupval 
 |-  ( ( ph /\ <" <. A , (/) >. "> e. W ) -> ( E ` [ <" <. A , (/) >. "> ] .~ ) = ( H gsum ( T o. <" <. A , (/) >. "> ) ) )
33 31 32 mpdan 
 |-  ( ph -> ( E ` [ <" <. A , (/) >. "> ] .~ ) = ( H gsum ( T o. <" <. A , (/) >. "> ) ) )
34 1 2 3 4 5 6 frgpuptf 
 |-  ( ph -> T : ( I X. 2o ) --> B )
35 s1co 
 |-  ( ( <. A , (/) >. e. ( I X. 2o ) /\ T : ( I X. 2o ) --> B ) -> ( T o. <" <. A , (/) >. "> ) = <" ( T ` <. A , (/) >. ) "> )
36 22 34 35 syl2anc 
 |-  ( ph -> ( T o. <" <. A , (/) >. "> ) = <" ( T ` <. A , (/) >. ) "> )
37 df-ov 
 |-  ( A T (/) ) = ( T ` <. A , (/) >. )
38 iftrue 
 |-  ( z = (/) -> if ( z = (/) , ( F ` y ) , ( N ` ( F ` y ) ) ) = ( F ` y ) )
39 fveq2 
 |-  ( y = A -> ( F ` y ) = ( F ` A ) )
40 38 39 sylan9eqr 
 |-  ( ( y = A /\ z = (/) ) -> if ( z = (/) , ( F ` y ) , ( N ` ( F ` y ) ) ) = ( F ` A ) )
41 fvex 
 |-  ( F ` A ) e. _V
42 40 3 41 ovmpoa 
 |-  ( ( A e. I /\ (/) e. 2o ) -> ( A T (/) ) = ( F ` A ) )
43 13 20 42 sylancl 
 |-  ( ph -> ( A T (/) ) = ( F ` A ) )
44 37 43 eqtr3id 
 |-  ( ph -> ( T ` <. A , (/) >. ) = ( F ` A ) )
45 44 s1eqd 
 |-  ( ph -> <" ( T ` <. A , (/) >. ) "> = <" ( F ` A ) "> )
46 36 45 eqtrd 
 |-  ( ph -> ( T o. <" <. A , (/) >. "> ) = <" ( F ` A ) "> )
47 46 oveq2d 
 |-  ( ph -> ( H gsum ( T o. <" <. A , (/) >. "> ) ) = ( H gsum <" ( F ` A ) "> ) )
48 6 13 ffvelrnd 
 |-  ( ph -> ( F ` A ) e. B )
49 1 gsumws1 
 |-  ( ( F ` A ) e. B -> ( H gsum <" ( F ` A ) "> ) = ( F ` A ) )
50 48 49 syl 
 |-  ( ph -> ( H gsum <" ( F ` A ) "> ) = ( F ` A ) )
51 47 50 eqtrd 
 |-  ( ph -> ( H gsum ( T o. <" <. A , (/) >. "> ) ) = ( F ` A ) )
52 16 33 51 3eqtrd 
 |-  ( ph -> ( E ` ( U ` A ) ) = ( F ` A ) )