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 ) ) → ( 𝑇 ‘ ( 𝑀 ‘ 𝐴 ) ) = ( 𝑁 ‘ ( 𝑇 ‘ 𝐴 ) ) )