This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ffvelcdmda 
 |-  ( ( 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 biimtrid 
 |-  ( 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 ) ) )