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