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	eqtrid	|- ( 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	ffvelcdmd	|- ( 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 ) )