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 = inv g H
frgpup.t T = y I , z 2 𝑜 if z = F y N F y
frgpup.h φ H Grp
frgpup.i φ I V
frgpup.a φ F : I B
frgpuptinv.m M = y I , z 2 𝑜 y 1 𝑜 z
Assertion frgpuptinv φ A I × 2 𝑜 T M A = N T A

Proof

Step Hyp Ref Expression
1 frgpup.b B = Base H
2 frgpup.n N = inv g H
3 frgpup.t T = y I , z 2 𝑜 if z = F y N F y
4 frgpup.h φ H Grp
5 frgpup.i φ I V
6 frgpup.a φ F : I B
7 frgpuptinv.m M = y I , z 2 𝑜 y 1 𝑜 z
8 elxp2 A I × 2 𝑜 a I b 2 𝑜 A = a b
9 7 efgmval a I b 2 𝑜 a M b = a 1 𝑜 b
10 9 adantl φ a I b 2 𝑜 a M b = a 1 𝑜 b
11 10 fveq2d φ a I b 2 𝑜 T a M b = T a 1 𝑜 b
12 df-ov a T 1 𝑜 b = T a 1 𝑜 b
13 11 12 eqtr4di φ a I b 2 𝑜 T a M b = a T 1 𝑜 b
14 elpri b 1 𝑜 b = b = 1 𝑜
15 df2o3 2 𝑜 = 1 𝑜
16 14 15 eleq2s b 2 𝑜 b = b = 1 𝑜
17 simpr φ a I a I
18 1oex 1 𝑜 V
19 18 prid2 1 𝑜 1 𝑜
20 19 15 eleqtrri 1 𝑜 2 𝑜
21 1n0 1 𝑜
22 neeq1 z = 1 𝑜 z 1 𝑜
23 21 22 mpbiri z = 1 𝑜 z
24 ifnefalse z if z = F y N F y = N F y
25 23 24 syl z = 1 𝑜 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 = 1 𝑜 if z = F y N F y = N F a
29 fvex N F a V
30 28 3 29 ovmpoa a I 1 𝑜 2 𝑜 a T 1 𝑜 = N F a
31 17 20 30 sylancl φ a I a T 1 𝑜 = N F a
32 0ex V
33 32 prid1 1 𝑜
34 33 15 eleqtrri 2 𝑜
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 V
38 36 3 37 ovmpoa a I 2 𝑜 a T = F a
39 17 34 38 sylancl φ a I a T = F a
40 39 fveq2d φ a I N a T = N F a
41 31 40 eqtr4d φ a I a T 1 𝑜 = N a T
42 difeq2 b = 1 𝑜 b = 1 𝑜
43 dif0 1 𝑜 = 1 𝑜
44 42 43 eqtrdi b = 1 𝑜 b = 1 𝑜
45 44 oveq2d b = a T 1 𝑜 b = a T 1 𝑜
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 1 𝑜 b = N a T b a T 1 𝑜 = N a T
49 41 48 syl5ibrcom φ a I b = a T 1 𝑜 b = N a T b
50 41 fveq2d φ a I N a T 1 𝑜 = N N a T
51 6 ffvelrnda φ a I F a B
52 39 51 eqeltrd φ a I a T B
53 1 2 grpinvinv H Grp a T B N N a T = a T
54 4 52 53 syl2an2r φ a I N N a T = a T
55 50 54 eqtr2d φ a I a T = N a T 1 𝑜
56 difeq2 b = 1 𝑜 1 𝑜 b = 1 𝑜 1 𝑜
57 difid 1 𝑜 1 𝑜 =
58 56 57 eqtrdi b = 1 𝑜 1 𝑜 b =
59 58 oveq2d b = 1 𝑜 a T 1 𝑜 b = a T
60 oveq2 b = 1 𝑜 a T b = a T 1 𝑜
61 60 fveq2d b = 1 𝑜 N a T b = N a T 1 𝑜
62 59 61 eqeq12d b = 1 𝑜 a T 1 𝑜 b = N a T b a T = N a T 1 𝑜
63 55 62 syl5ibrcom φ a I b = 1 𝑜 a T 1 𝑜 b = N a T b
64 49 63 jaod φ a I b = b = 1 𝑜 a T 1 𝑜 b = N a T b
65 16 64 syl5 φ a I b 2 𝑜 a T 1 𝑜 b = N a T b
66 65 impr φ a I b 2 𝑜 a T 1 𝑜 b = N a T b
67 13 66 eqtrd φ a I b 2 𝑜 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 φ a I b 2 𝑜 A = a b T M A = N T A
78 77 rexlimdvva φ a I b 2 𝑜 A = a b T M A = N T A
79 8 78 syl5bi φ A I × 2 𝑜 T M A = N T A
80 79 imp φ A I × 2 𝑜 T M A = N T A