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 𝐵 = ( Base ‘ 𝐻 )
frgpup.n 𝑁 = ( invg𝐻 )
frgpup.t 𝑇 = ( 𝑦𝐼 , 𝑧 ∈ 2o ↦ if ( 𝑧 = ∅ , ( 𝐹𝑦 ) , ( 𝑁 ‘ ( 𝐹𝑦 ) ) ) )
frgpup.h ( 𝜑𝐻 ∈ Grp )
frgpup.i ( 𝜑𝐼𝑉 )
frgpup.a ( 𝜑𝐹 : 𝐼𝐵 )
frgpuptinv.m 𝑀 = ( 𝑦𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o𝑧 ) ⟩ )
Assertion frgpuptinv ( ( 𝜑𝐴 ∈ ( 𝐼 × 2o ) ) → ( 𝑇 ‘ ( 𝑀𝐴 ) ) = ( 𝑁 ‘ ( 𝑇𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 frgpup.b 𝐵 = ( Base ‘ 𝐻 )
2 frgpup.n 𝑁 = ( invg𝐻 )
3 frgpup.t 𝑇 = ( 𝑦𝐼 , 𝑧 ∈ 2o ↦ if ( 𝑧 = ∅ , ( 𝐹𝑦 ) , ( 𝑁 ‘ ( 𝐹𝑦 ) ) ) )
4 frgpup.h ( 𝜑𝐻 ∈ Grp )
5 frgpup.i ( 𝜑𝐼𝑉 )
6 frgpup.a ( 𝜑𝐹 : 𝐼𝐵 )
7 frgpuptinv.m 𝑀 = ( 𝑦𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o𝑧 ) ⟩ )
8 elxp2 ( 𝐴 ∈ ( 𝐼 × 2o ) ↔ ∃ 𝑎𝐼𝑏 ∈ 2o 𝐴 = ⟨ 𝑎 , 𝑏 ⟩ )
9 7 efgmval ( ( 𝑎𝐼𝑏 ∈ 2o ) → ( 𝑎 𝑀 𝑏 ) = ⟨ 𝑎 , ( 1o𝑏 ) ⟩ )
10 9 adantl ( ( 𝜑 ∧ ( 𝑎𝐼𝑏 ∈ 2o ) ) → ( 𝑎 𝑀 𝑏 ) = ⟨ 𝑎 , ( 1o𝑏 ) ⟩ )
11 10 fveq2d ( ( 𝜑 ∧ ( 𝑎𝐼𝑏 ∈ 2o ) ) → ( 𝑇 ‘ ( 𝑎 𝑀 𝑏 ) ) = ( 𝑇 ‘ ⟨ 𝑎 , ( 1o𝑏 ) ⟩ ) )
12 df-ov ( 𝑎 𝑇 ( 1o𝑏 ) ) = ( 𝑇 ‘ ⟨ 𝑎 , ( 1o𝑏 ) ⟩ )
13 11 12 eqtr4di ( ( 𝜑 ∧ ( 𝑎𝐼𝑏 ∈ 2o ) ) → ( 𝑇 ‘ ( 𝑎 𝑀 𝑏 ) ) = ( 𝑎 𝑇 ( 1o𝑏 ) ) )
14 elpri ( 𝑏 ∈ { ∅ , 1o } → ( 𝑏 = ∅ ∨ 𝑏 = 1o ) )
15 df2o3 2o = { ∅ , 1o }
16 14 15 eleq2s ( 𝑏 ∈ 2o → ( 𝑏 = ∅ ∨ 𝑏 = 1o ) )
17 simpr ( ( 𝜑𝑎𝐼 ) → 𝑎𝐼 )
18 1oex 1o ∈ V
19 18 prid2 1o ∈ { ∅ , 1o }
20 19 15 eleqtrri 1o ∈ 2o
21 1n0 1o ≠ ∅
22 neeq1 ( 𝑧 = 1o → ( 𝑧 ≠ ∅ ↔ 1o ≠ ∅ ) )
23 21 22 mpbiri ( 𝑧 = 1o𝑧 ≠ ∅ )
24 ifnefalse ( 𝑧 ≠ ∅ → if ( 𝑧 = ∅ , ( 𝐹𝑦 ) , ( 𝑁 ‘ ( 𝐹𝑦 ) ) ) = ( 𝑁 ‘ ( 𝐹𝑦 ) ) )
25 23 24 syl ( 𝑧 = 1o → if ( 𝑧 = ∅ , ( 𝐹𝑦 ) , ( 𝑁 ‘ ( 𝐹𝑦 ) ) ) = ( 𝑁 ‘ ( 𝐹𝑦 ) ) )
26 fveq2 ( 𝑦 = 𝑎 → ( 𝐹𝑦 ) = ( 𝐹𝑎 ) )
27 26 fveq2d ( 𝑦 = 𝑎 → ( 𝑁 ‘ ( 𝐹𝑦 ) ) = ( 𝑁 ‘ ( 𝐹𝑎 ) ) )
28 25 27 sylan9eqr ( ( 𝑦 = 𝑎𝑧 = 1o ) → if ( 𝑧 = ∅ , ( 𝐹𝑦 ) , ( 𝑁 ‘ ( 𝐹𝑦 ) ) ) = ( 𝑁 ‘ ( 𝐹𝑎 ) ) )
29 fvex ( 𝑁 ‘ ( 𝐹𝑎 ) ) ∈ V
30 28 3 29 ovmpoa ( ( 𝑎𝐼 ∧ 1o ∈ 2o ) → ( 𝑎 𝑇 1o ) = ( 𝑁 ‘ ( 𝐹𝑎 ) ) )
31 17 20 30 sylancl ( ( 𝜑𝑎𝐼 ) → ( 𝑎 𝑇 1o ) = ( 𝑁 ‘ ( 𝐹𝑎 ) ) )
32 0ex ∅ ∈ V
33 32 prid1 ∅ ∈ { ∅ , 1o }
34 33 15 eleqtrri ∅ ∈ 2o
35 iftrue ( 𝑧 = ∅ → if ( 𝑧 = ∅ , ( 𝐹𝑦 ) , ( 𝑁 ‘ ( 𝐹𝑦 ) ) ) = ( 𝐹𝑦 ) )
36 35 26 sylan9eqr ( ( 𝑦 = 𝑎𝑧 = ∅ ) → if ( 𝑧 = ∅ , ( 𝐹𝑦 ) , ( 𝑁 ‘ ( 𝐹𝑦 ) ) ) = ( 𝐹𝑎 ) )
37 fvex ( 𝐹𝑎 ) ∈ V
38 36 3 37 ovmpoa ( ( 𝑎𝐼 ∧ ∅ ∈ 2o ) → ( 𝑎 𝑇 ∅ ) = ( 𝐹𝑎 ) )
39 17 34 38 sylancl ( ( 𝜑𝑎𝐼 ) → ( 𝑎 𝑇 ∅ ) = ( 𝐹𝑎 ) )
40 39 fveq2d ( ( 𝜑𝑎𝐼 ) → ( 𝑁 ‘ ( 𝑎 𝑇 ∅ ) ) = ( 𝑁 ‘ ( 𝐹𝑎 ) ) )
41 31 40 eqtr4d ( ( 𝜑𝑎𝐼 ) → ( 𝑎 𝑇 1o ) = ( 𝑁 ‘ ( 𝑎 𝑇 ∅ ) ) )
42 difeq2 ( 𝑏 = ∅ → ( 1o𝑏 ) = ( 1o ∖ ∅ ) )
43 dif0 ( 1o ∖ ∅ ) = 1o
44 42 43 eqtrdi ( 𝑏 = ∅ → ( 1o𝑏 ) = 1o )
45 44 oveq2d ( 𝑏 = ∅ → ( 𝑎 𝑇 ( 1o𝑏 ) ) = ( 𝑎 𝑇 1o ) )
46 oveq2 ( 𝑏 = ∅ → ( 𝑎 𝑇 𝑏 ) = ( 𝑎 𝑇 ∅ ) )
47 46 fveq2d ( 𝑏 = ∅ → ( 𝑁 ‘ ( 𝑎 𝑇 𝑏 ) ) = ( 𝑁 ‘ ( 𝑎 𝑇 ∅ ) ) )
48 45 47 eqeq12d ( 𝑏 = ∅ → ( ( 𝑎 𝑇 ( 1o𝑏 ) ) = ( 𝑁 ‘ ( 𝑎 𝑇 𝑏 ) ) ↔ ( 𝑎 𝑇 1o ) = ( 𝑁 ‘ ( 𝑎 𝑇 ∅ ) ) ) )
49 41 48 syl5ibrcom ( ( 𝜑𝑎𝐼 ) → ( 𝑏 = ∅ → ( 𝑎 𝑇 ( 1o𝑏 ) ) = ( 𝑁 ‘ ( 𝑎 𝑇 𝑏 ) ) ) )
50 41 fveq2d ( ( 𝜑𝑎𝐼 ) → ( 𝑁 ‘ ( 𝑎 𝑇 1o ) ) = ( 𝑁 ‘ ( 𝑁 ‘ ( 𝑎 𝑇 ∅ ) ) ) )
51 6 ffvelrnda ( ( 𝜑𝑎𝐼 ) → ( 𝐹𝑎 ) ∈ 𝐵 )
52 39 51 eqeltrd ( ( 𝜑𝑎𝐼 ) → ( 𝑎 𝑇 ∅ ) ∈ 𝐵 )
53 1 2 grpinvinv ( ( 𝐻 ∈ Grp ∧ ( 𝑎 𝑇 ∅ ) ∈ 𝐵 ) → ( 𝑁 ‘ ( 𝑁 ‘ ( 𝑎 𝑇 ∅ ) ) ) = ( 𝑎 𝑇 ∅ ) )
54 4 52 53 syl2an2r ( ( 𝜑𝑎𝐼 ) → ( 𝑁 ‘ ( 𝑁 ‘ ( 𝑎 𝑇 ∅ ) ) ) = ( 𝑎 𝑇 ∅ ) )
55 50 54 eqtr2d ( ( 𝜑𝑎𝐼 ) → ( 𝑎 𝑇 ∅ ) = ( 𝑁 ‘ ( 𝑎 𝑇 1o ) ) )
56 difeq2 ( 𝑏 = 1o → ( 1o𝑏 ) = ( 1o ∖ 1o ) )
57 difid ( 1o ∖ 1o ) = ∅
58 56 57 eqtrdi ( 𝑏 = 1o → ( 1o𝑏 ) = ∅ )
59 58 oveq2d ( 𝑏 = 1o → ( 𝑎 𝑇 ( 1o𝑏 ) ) = ( 𝑎 𝑇 ∅ ) )
60 oveq2 ( 𝑏 = 1o → ( 𝑎 𝑇 𝑏 ) = ( 𝑎 𝑇 1o ) )
61 60 fveq2d ( 𝑏 = 1o → ( 𝑁 ‘ ( 𝑎 𝑇 𝑏 ) ) = ( 𝑁 ‘ ( 𝑎 𝑇 1o ) ) )
62 59 61 eqeq12d ( 𝑏 = 1o → ( ( 𝑎 𝑇 ( 1o𝑏 ) ) = ( 𝑁 ‘ ( 𝑎 𝑇 𝑏 ) ) ↔ ( 𝑎 𝑇 ∅ ) = ( 𝑁 ‘ ( 𝑎 𝑇 1o ) ) ) )
63 55 62 syl5ibrcom ( ( 𝜑𝑎𝐼 ) → ( 𝑏 = 1o → ( 𝑎 𝑇 ( 1o𝑏 ) ) = ( 𝑁 ‘ ( 𝑎 𝑇 𝑏 ) ) ) )
64 49 63 jaod ( ( 𝜑𝑎𝐼 ) → ( ( 𝑏 = ∅ ∨ 𝑏 = 1o ) → ( 𝑎 𝑇 ( 1o𝑏 ) ) = ( 𝑁 ‘ ( 𝑎 𝑇 𝑏 ) ) ) )
65 16 64 syl5 ( ( 𝜑𝑎𝐼 ) → ( 𝑏 ∈ 2o → ( 𝑎 𝑇 ( 1o𝑏 ) ) = ( 𝑁 ‘ ( 𝑎 𝑇 𝑏 ) ) ) )
66 65 impr ( ( 𝜑 ∧ ( 𝑎𝐼𝑏 ∈ 2o ) ) → ( 𝑎 𝑇 ( 1o𝑏 ) ) = ( 𝑁 ‘ ( 𝑎 𝑇 𝑏 ) ) )
67 13 66 eqtrd ( ( 𝜑 ∧ ( 𝑎𝐼𝑏 ∈ 2o ) ) → ( 𝑇 ‘ ( 𝑎 𝑀 𝑏 ) ) = ( 𝑁 ‘ ( 𝑎 𝑇 𝑏 ) ) )
68 fveq2 ( 𝐴 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑀𝐴 ) = ( 𝑀 ‘ ⟨ 𝑎 , 𝑏 ⟩ ) )
69 df-ov ( 𝑎 𝑀 𝑏 ) = ( 𝑀 ‘ ⟨ 𝑎 , 𝑏 ⟩ )
70 68 69 eqtr4di ( 𝐴 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑀𝐴 ) = ( 𝑎 𝑀 𝑏 ) )
71 70 fveq2d ( 𝐴 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑇 ‘ ( 𝑀𝐴 ) ) = ( 𝑇 ‘ ( 𝑎 𝑀 𝑏 ) ) )
72 fveq2 ( 𝐴 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑇𝐴 ) = ( 𝑇 ‘ ⟨ 𝑎 , 𝑏 ⟩ ) )
73 df-ov ( 𝑎 𝑇 𝑏 ) = ( 𝑇 ‘ ⟨ 𝑎 , 𝑏 ⟩ )
74 72 73 eqtr4di ( 𝐴 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑇𝐴 ) = ( 𝑎 𝑇 𝑏 ) )
75 74 fveq2d ( 𝐴 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑁 ‘ ( 𝑇𝐴 ) ) = ( 𝑁 ‘ ( 𝑎 𝑇 𝑏 ) ) )
76 71 75 eqeq12d ( 𝐴 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( 𝑇 ‘ ( 𝑀𝐴 ) ) = ( 𝑁 ‘ ( 𝑇𝐴 ) ) ↔ ( 𝑇 ‘ ( 𝑎 𝑀 𝑏 ) ) = ( 𝑁 ‘ ( 𝑎 𝑇 𝑏 ) ) ) )
77 67 76 syl5ibrcom ( ( 𝜑 ∧ ( 𝑎𝐼𝑏 ∈ 2o ) ) → ( 𝐴 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑇 ‘ ( 𝑀𝐴 ) ) = ( 𝑁 ‘ ( 𝑇𝐴 ) ) ) )
78 77 rexlimdvva ( 𝜑 → ( ∃ 𝑎𝐼𝑏 ∈ 2o 𝐴 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑇 ‘ ( 𝑀𝐴 ) ) = ( 𝑁 ‘ ( 𝑇𝐴 ) ) ) )
79 8 78 syl5bi ( 𝜑 → ( 𝐴 ∈ ( 𝐼 × 2o ) → ( 𝑇 ‘ ( 𝑀𝐴 ) ) = ( 𝑁 ‘ ( 𝑇𝐴 ) ) ) )
80 79 imp ( ( 𝜑𝐴 ∈ ( 𝐼 × 2o ) ) → ( 𝑇 ‘ ( 𝑀𝐴 ) ) = ( 𝑁 ‘ ( 𝑇𝐴 ) ) )