Theorem frgpuptinv

Description: Any assignment of the generators to target elements can be extended (uniquely) to a homomorphism from a free monoid to an arbitrary other monoid. (Contributed by Mario Carneiro, 2-Oct-2015)

	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 )
	frgpuptinv.m	|- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )
Assertion	frgpuptinv	|- ( ( ph /\ A e. ( I X. 2o ) ) -> ( T ` ( M ` A ) ) = ( N ` ( T ` 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		frgpuptinv.m	|- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )
8		elxp2	|- ( A e. ( I X. 2o ) <-> E. a e. I E. b e. 2o A = <. a , b >. )
9	7	efgmval	|- ( ( a e. I /\ b e. 2o ) -> ( a M b ) = <. a , ( 1o \ b ) >. )
10	9	adantl	|- ( ( ph /\ ( a e. I /\ b e. 2o ) ) -> ( a M b ) = <. a , ( 1o \ b ) >. )
11	10	fveq2d	|- ( ( ph /\ ( a e. I /\ b e. 2o ) ) -> ( T ` ( a M b ) ) = ( T ` <. a , ( 1o \ b ) >. ) )
12		df-ov	|- ( a T ( 1o \ b ) ) = ( T ` <. a , ( 1o \ b ) >. )
13	11 12	eqtr4di	|- ( ( ph /\ ( a e. I /\ b e. 2o ) ) -> ( T ` ( a M b ) ) = ( a T ( 1o \ b ) ) )
14		elpri	|- ( b e. { (/) , 1o } -> ( b = (/) \/ b = 1o ) )
15		df2o3	|- 2o = { (/) , 1o }
16	14 15	eleq2s	|- ( b e. 2o -> ( b = (/) \/ b = 1o ) )
17		simpr	|- ( ( ph /\ a e. I ) -> a e. I )
18		1oex	|- 1o e. _V
19	18	prid2	|- 1o e. { (/) , 1o }
20	19 15	eleqtrri	|- 1o e. 2o
21		1n0	|- 1o =/= (/)
22		neeq1	|- ( z = 1o -> ( z =/= (/) <-> 1o =/= (/) ) )
23	21 22	mpbiri	|- ( z = 1o -> z =/= (/) )
24		ifnefalse	|- ( z =/= (/) -> if ( z = (/) , ( F ` y ) , ( N ` ( F ` y ) ) ) = ( N ` ( F ` y ) ) )
25	23 24	syl	|- ( z = 1o -> if ( z = (/) , ( F ` y ) , ( N ` ( F ` y ) ) ) = ( N ` ( F ` y ) ) )
26		fveq2	|- ( y = a -> ( F ` y ) = ( F ` a ) )
27	26	fveq2d	|- ( y = a -> ( N ` ( F ` y ) ) = ( N ` ( F ` a ) ) )
28	25 27	sylan9eqr	|- ( ( y = a /\ z = 1o ) -> if ( z = (/) , ( F ` y ) , ( N ` ( F ` y ) ) ) = ( N ` ( F ` a ) ) )
29		fvex	|- ( N ` ( F ` a ) ) e. _V
30	28 3 29	ovmpoa	|- ( ( a e. I /\ 1o e. 2o ) -> ( a T 1o ) = ( N ` ( F ` a ) ) )
31	17 20 30	sylancl	|- ( ( ph /\ a e. I ) -> ( a T 1o ) = ( N ` ( F ` a ) ) )
32		0ex	|- (/) e. _V
33	32	prid1	|- (/) e. { (/) , 1o }
34	33 15	eleqtrri	|- (/) e. 2o
35		iftrue	|- ( z = (/) -> if ( z = (/) , ( F ` y ) , ( N ` ( F ` y ) ) ) = ( F ` y ) )
36	35 26	sylan9eqr	|- ( ( y = a /\ z = (/) ) -> if ( z = (/) , ( F ` y ) , ( N ` ( F ` y ) ) ) = ( F ` a ) )
37		fvex	|- ( F ` a ) e. _V
38	36 3 37	ovmpoa	|- ( ( a e. I /\ (/) e. 2o ) -> ( a T (/) ) = ( F ` a ) )
39	17 34 38	sylancl	|- ( ( ph /\ a e. I ) -> ( a T (/) ) = ( F ` a ) )
40	39	fveq2d	|- ( ( ph /\ a e. I ) -> ( N ` ( a T (/) ) ) = ( N ` ( F ` a ) ) )
41	31 40	eqtr4d	|- ( ( ph /\ a e. I ) -> ( a T 1o ) = ( N ` ( a T (/) ) ) )
42		difeq2	|- ( b = (/) -> ( 1o \ b ) = ( 1o \ (/) ) )
43		dif0	|- ( 1o \ (/) ) = 1o
44	42 43	eqtrdi	|- ( b = (/) -> ( 1o \ b ) = 1o )
45	44	oveq2d	|- ( b = (/) -> ( a T ( 1o \ b ) ) = ( a T 1o ) )
46		oveq2	|- ( b = (/) -> ( a T b ) = ( a T (/) ) )
47	46	fveq2d	|- ( b = (/) -> ( N ` ( a T b ) ) = ( N ` ( a T (/) ) ) )
48	45 47	eqeq12d	|- ( b = (/) -> ( ( a T ( 1o \ b ) ) = ( N ` ( a T b ) ) <-> ( a T 1o ) = ( N ` ( a T (/) ) ) ) )
49	41 48	syl5ibrcom	|- ( ( ph /\ a e. I ) -> ( b = (/) -> ( a T ( 1o \ b ) ) = ( N ` ( a T b ) ) ) )
50	41	fveq2d	|- ( ( ph /\ a e. I ) -> ( N ` ( a T 1o ) ) = ( N ` ( N ` ( a T (/) ) ) ) )
51	6	ffvelrnda	|- ( ( ph /\ a e. I ) -> ( F ` a ) e. B )
52	39 51	eqeltrd	|- ( ( ph /\ a e. I ) -> ( a T (/) ) e. B )
53	1 2	grpinvinv	|- ( ( H e. Grp /\ ( a T (/) ) e. B ) -> ( N ` ( N ` ( a T (/) ) ) ) = ( a T (/) ) )
54	4 52 53	syl2an2r	|- ( ( ph /\ a e. I ) -> ( N ` ( N ` ( a T (/) ) ) ) = ( a T (/) ) )
55	50 54	eqtr2d	|- ( ( ph /\ a e. I ) -> ( a T (/) ) = ( N ` ( a T 1o ) ) )
56		difeq2	|- ( b = 1o -> ( 1o \ b ) = ( 1o \ 1o ) )
57		difid	|- ( 1o \ 1o ) = (/)
58	56 57	eqtrdi	|- ( b = 1o -> ( 1o \ b ) = (/) )
59	58	oveq2d	|- ( b = 1o -> ( a T ( 1o \ b ) ) = ( a T (/) ) )
60		oveq2	|- ( b = 1o -> ( a T b ) = ( a T 1o ) )
61	60	fveq2d	|- ( b = 1o -> ( N ` ( a T b ) ) = ( N ` ( a T 1o ) ) )
62	59 61	eqeq12d	|- ( b = 1o -> ( ( a T ( 1o \ b ) ) = ( N ` ( a T b ) ) <-> ( a T (/) ) = ( N ` ( a T 1o ) ) ) )
63	55 62	syl5ibrcom	|- ( ( ph /\ a e. I ) -> ( b = 1o -> ( a T ( 1o \ b ) ) = ( N ` ( a T b ) ) ) )
64	49 63	jaod	|- ( ( ph /\ a e. I ) -> ( ( b = (/) \/ b = 1o ) -> ( a T ( 1o \ b ) ) = ( N ` ( a T b ) ) ) )
65	16 64	syl5	|- ( ( ph /\ a e. I ) -> ( b e. 2o -> ( a T ( 1o \ b ) ) = ( N ` ( a T b ) ) ) )
66	65	impr	|- ( ( ph /\ ( a e. I /\ b e. 2o ) ) -> ( a T ( 1o \ b ) ) = ( N ` ( a T b ) ) )
67	13 66	eqtrd	|- ( ( ph /\ ( a e. I /\ b e. 2o ) ) -> ( T ` ( a M b ) ) = ( N ` ( a T b ) ) )
68		fveq2	|- ( A = <. a , b >. -> ( M ` A ) = ( M ` <. a , b >. ) )
69		df-ov	|- ( a M b ) = ( M ` <. a , b >. )
70	68 69	eqtr4di	|- ( A = <. a , b >. -> ( M ` A ) = ( a M b ) )
71	70	fveq2d	|- ( A = <. a , b >. -> ( T ` ( M ` A ) ) = ( T ` ( a M b ) ) )
72		fveq2	|- ( A = <. a , b >. -> ( T ` A ) = ( T ` <. a , b >. ) )
73		df-ov	|- ( a T b ) = ( T ` <. a , b >. )
74	72 73	eqtr4di	|- ( A = <. a , b >. -> ( T ` A ) = ( a T b ) )
75	74	fveq2d	|- ( A = <. a , b >. -> ( N ` ( T ` A ) ) = ( N ` ( a T b ) ) )
76	71 75	eqeq12d	|- ( A = <. a , b >. -> ( ( T ` ( M ` A ) ) = ( N ` ( T ` A ) ) <-> ( T ` ( a M b ) ) = ( N ` ( a T b ) ) ) )
77	67 76	syl5ibrcom	|- ( ( ph /\ ( a e. I /\ b e. 2o ) ) -> ( A = <. a , b >. -> ( T ` ( M ` A ) ) = ( N ` ( T ` A ) ) ) )
78	77	rexlimdvva	|- ( ph -> ( E. a e. I E. b e. 2o A = <. a , b >. -> ( T ` ( M ` A ) ) = ( N ` ( T ` A ) ) ) )
79	8 78	syl5bi	|- ( ph -> ( A e. ( I X. 2o ) -> ( T ` ( M ` A ) ) = ( N ` ( T ` A ) ) ) )
80	79	imp	|- ( ( ph /\ A e. ( I X. 2o ) ) -> ( T ` ( M ` A ) ) = ( N ` ( T ` A ) ) )