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		1oelpr	⊢ 1o ∈ { ∅ , 1o }
19	18 15	eleqtrri	⊢ 1o ∈ 2o
20		1n0	⊢ 1o ≠ ∅
21		neeq1	⊢ ( 𝑧 = 1o → ( 𝑧 ≠ ∅ ↔ 1o ≠ ∅ ) )
22	20 21	mpbiri	⊢ ( 𝑧 = 1o → 𝑧 ≠ ∅ )
23		ifnefalse	⊢ ( 𝑧 ≠ ∅ → if ( 𝑧 = ∅ , ( 𝐹 ‘ 𝑦 ) , ( 𝑁 ‘ ( 𝐹 ‘ 𝑦 ) ) ) = ( 𝑁 ‘ ( 𝐹 ‘ 𝑦 ) ) )
24	22 23	syl	⊢ ( 𝑧 = 1o → if ( 𝑧 = ∅ , ( 𝐹 ‘ 𝑦 ) , ( 𝑁 ‘ ( 𝐹 ‘ 𝑦 ) ) ) = ( 𝑁 ‘ ( 𝐹 ‘ 𝑦 ) ) )
25		fveq2	⊢ ( 𝑦 = 𝑎 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑎 ) )
26	25	fveq2d	⊢ ( 𝑦 = 𝑎 → ( 𝑁 ‘ ( 𝐹 ‘ 𝑦 ) ) = ( 𝑁 ‘ ( 𝐹 ‘ 𝑎 ) ) )
27	24 26	sylan9eqr	⊢ ( ( 𝑦 = 𝑎 ∧ 𝑧 = 1o ) → if ( 𝑧 = ∅ , ( 𝐹 ‘ 𝑦 ) , ( 𝑁 ‘ ( 𝐹 ‘ 𝑦 ) ) ) = ( 𝑁 ‘ ( 𝐹 ‘ 𝑎 ) ) )
28		fvex	⊢ ( 𝑁 ‘ ( 𝐹 ‘ 𝑎 ) ) ∈ V
29	27 3 28	ovmpoa	⊢ ( ( 𝑎 ∈ 𝐼 ∧ 1o ∈ 2o ) → ( 𝑎 𝑇 1o ) = ( 𝑁 ‘ ( 𝐹 ‘ 𝑎 ) ) )
30	17 19 29	sylancl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐼 ) → ( 𝑎 𝑇 1o ) = ( 𝑁 ‘ ( 𝐹 ‘ 𝑎 ) ) )
31		0ex	⊢ ∅ ∈ V
32	31	prid1	⊢ ∅ ∈ { ∅ , 1o }
33	32 15	eleqtrri	⊢ ∅ ∈ 2o
34		iftrue	⊢ ( 𝑧 = ∅ → if ( 𝑧 = ∅ , ( 𝐹 ‘ 𝑦 ) , ( 𝑁 ‘ ( 𝐹 ‘ 𝑦 ) ) ) = ( 𝐹 ‘ 𝑦 ) )
35	34 25	sylan9eqr	⊢ ( ( 𝑦 = 𝑎 ∧ 𝑧 = ∅ ) → if ( 𝑧 = ∅ , ( 𝐹 ‘ 𝑦 ) , ( 𝑁 ‘ ( 𝐹 ‘ 𝑦 ) ) ) = ( 𝐹 ‘ 𝑎 ) )
36		fvex	⊢ ( 𝐹 ‘ 𝑎 ) ∈ V
37	35 3 36	ovmpoa	⊢ ( ( 𝑎 ∈ 𝐼 ∧ ∅ ∈ 2o ) → ( 𝑎 𝑇 ∅ ) = ( 𝐹 ‘ 𝑎 ) )
38	17 33 37	sylancl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐼 ) → ( 𝑎 𝑇 ∅ ) = ( 𝐹 ‘ 𝑎 ) )
39	38	fveq2d	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐼 ) → ( 𝑁 ‘ ( 𝑎 𝑇 ∅ ) ) = ( 𝑁 ‘ ( 𝐹 ‘ 𝑎 ) ) )
40	30 39	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐼 ) → ( 𝑎 𝑇 1o ) = ( 𝑁 ‘ ( 𝑎 𝑇 ∅ ) ) )
41		difeq2	⊢ ( 𝑏 = ∅ → ( 1o ∖ 𝑏 ) = ( 1o ∖ ∅ ) )
42		dif0	⊢ ( 1o ∖ ∅ ) = 1o
43	41 42	eqtrdi	⊢ ( 𝑏 = ∅ → ( 1o ∖ 𝑏 ) = 1o )
44	43	oveq2d	⊢ ( 𝑏 = ∅ → ( 𝑎 𝑇 ( 1o ∖ 𝑏 ) ) = ( 𝑎 𝑇 1o ) )
45		oveq2	⊢ ( 𝑏 = ∅ → ( 𝑎 𝑇 𝑏 ) = ( 𝑎 𝑇 ∅ ) )
46	45	fveq2d	⊢ ( 𝑏 = ∅ → ( 𝑁 ‘ ( 𝑎 𝑇 𝑏 ) ) = ( 𝑁 ‘ ( 𝑎 𝑇 ∅ ) ) )
47	44 46	eqeq12d	⊢ ( 𝑏 = ∅ → ( ( 𝑎 𝑇 ( 1o ∖ 𝑏 ) ) = ( 𝑁 ‘ ( 𝑎 𝑇 𝑏 ) ) ↔ ( 𝑎 𝑇 1o ) = ( 𝑁 ‘ ( 𝑎 𝑇 ∅ ) ) ) )
48	40 47	syl5ibrcom	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐼 ) → ( 𝑏 = ∅ → ( 𝑎 𝑇 ( 1o ∖ 𝑏 ) ) = ( 𝑁 ‘ ( 𝑎 𝑇 𝑏 ) ) ) )
49	40	fveq2d	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐼 ) → ( 𝑁 ‘ ( 𝑎 𝑇 1o ) ) = ( 𝑁 ‘ ( 𝑁 ‘ ( 𝑎 𝑇 ∅ ) ) ) )
50	6	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑎 ) ∈ 𝐵 )
51	38 50	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐼 ) → ( 𝑎 𝑇 ∅ ) ∈ 𝐵 )
52	1 2	grpinvinv	⊢ ( ( 𝐻 ∈ Grp ∧ ( 𝑎 𝑇 ∅ ) ∈ 𝐵 ) → ( 𝑁 ‘ ( 𝑁 ‘ ( 𝑎 𝑇 ∅ ) ) ) = ( 𝑎 𝑇 ∅ ) )
53	4 51 52	syl2an2r	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐼 ) → ( 𝑁 ‘ ( 𝑁 ‘ ( 𝑎 𝑇 ∅ ) ) ) = ( 𝑎 𝑇 ∅ ) )
54	49 53	eqtr2d	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐼 ) → ( 𝑎 𝑇 ∅ ) = ( 𝑁 ‘ ( 𝑎 𝑇 1o ) ) )
55		difeq2	⊢ ( 𝑏 = 1o → ( 1o ∖ 𝑏 ) = ( 1o ∖ 1o ) )
56		difid	⊢ ( 1o ∖ 1o ) = ∅
57	55 56	eqtrdi	⊢ ( 𝑏 = 1o → ( 1o ∖ 𝑏 ) = ∅ )
58	57	oveq2d	⊢ ( 𝑏 = 1o → ( 𝑎 𝑇 ( 1o ∖ 𝑏 ) ) = ( 𝑎 𝑇 ∅ ) )
59		oveq2	⊢ ( 𝑏 = 1o → ( 𝑎 𝑇 𝑏 ) = ( 𝑎 𝑇 1o ) )
60	59	fveq2d	⊢ ( 𝑏 = 1o → ( 𝑁 ‘ ( 𝑎 𝑇 𝑏 ) ) = ( 𝑁 ‘ ( 𝑎 𝑇 1o ) ) )
61	58 60	eqeq12d	⊢ ( 𝑏 = 1o → ( ( 𝑎 𝑇 ( 1o ∖ 𝑏 ) ) = ( 𝑁 ‘ ( 𝑎 𝑇 𝑏 ) ) ↔ ( 𝑎 𝑇 ∅ ) = ( 𝑁 ‘ ( 𝑎 𝑇 1o ) ) ) )
62	54 61	syl5ibrcom	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐼 ) → ( 𝑏 = 1o → ( 𝑎 𝑇 ( 1o ∖ 𝑏 ) ) = ( 𝑁 ‘ ( 𝑎 𝑇 𝑏 ) ) ) )
63	48 62	jaod	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐼 ) → ( ( 𝑏 = ∅ ∨ 𝑏 = 1o ) → ( 𝑎 𝑇 ( 1o ∖ 𝑏 ) ) = ( 𝑁 ‘ ( 𝑎 𝑇 𝑏 ) ) ) )
64	16 63	syl5	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐼 ) → ( 𝑏 ∈ 2o → ( 𝑎 𝑇 ( 1o ∖ 𝑏 ) ) = ( 𝑁 ‘ ( 𝑎 𝑇 𝑏 ) ) ) )
65	64	impr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ( 𝑎 𝑇 ( 1o ∖ 𝑏 ) ) = ( 𝑁 ‘ ( 𝑎 𝑇 𝑏 ) ) )
66	13 65	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ( 𝑇 ‘ ( 𝑎 𝑀 𝑏 ) ) = ( 𝑁 ‘ ( 𝑎 𝑇 𝑏 ) ) )
67		fveq2	⊢ ( 𝐴 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑀 ‘ 𝐴 ) = ( 𝑀 ‘ ⟨ 𝑎 , 𝑏 ⟩ ) )
68		df-ov	⊢ ( 𝑎 𝑀 𝑏 ) = ( 𝑀 ‘ ⟨ 𝑎 , 𝑏 ⟩ )
69	67 68	eqtr4di	⊢ ( 𝐴 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑀 ‘ 𝐴 ) = ( 𝑎 𝑀 𝑏 ) )
70	69	fveq2d	⊢ ( 𝐴 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑇 ‘ ( 𝑀 ‘ 𝐴 ) ) = ( 𝑇 ‘ ( 𝑎 𝑀 𝑏 ) ) )
71		fveq2	⊢ ( 𝐴 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑇 ‘ 𝐴 ) = ( 𝑇 ‘ ⟨ 𝑎 , 𝑏 ⟩ ) )
72		df-ov	⊢ ( 𝑎 𝑇 𝑏 ) = ( 𝑇 ‘ ⟨ 𝑎 , 𝑏 ⟩ )
73	71 72	eqtr4di	⊢ ( 𝐴 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑇 ‘ 𝐴 ) = ( 𝑎 𝑇 𝑏 ) )
74	73	fveq2d	⊢ ( 𝐴 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑁 ‘ ( 𝑇 ‘ 𝐴 ) ) = ( 𝑁 ‘ ( 𝑎 𝑇 𝑏 ) ) )
75	70 74	eqeq12d	⊢ ( 𝐴 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( 𝑇 ‘ ( 𝑀 ‘ 𝐴 ) ) = ( 𝑁 ‘ ( 𝑇 ‘ 𝐴 ) ) ↔ ( 𝑇 ‘ ( 𝑎 𝑀 𝑏 ) ) = ( 𝑁 ‘ ( 𝑎 𝑇 𝑏 ) ) ) )
76	66 75	syl5ibrcom	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ( 𝐴 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑇 ‘ ( 𝑀 ‘ 𝐴 ) ) = ( 𝑁 ‘ ( 𝑇 ‘ 𝐴 ) ) ) )
77	76	rexlimdvva	⊢ ( 𝜑 → ( ∃ 𝑎 ∈ 𝐼 ∃ 𝑏 ∈ 2o 𝐴 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑇 ‘ ( 𝑀 ‘ 𝐴 ) ) = ( 𝑁 ‘ ( 𝑇 ‘ 𝐴 ) ) ) )
78	8 77	biimtrid	⊢ ( 𝜑 → ( 𝐴 ∈ ( 𝐼 × 2o ) → ( 𝑇 ‘ ( 𝑀 ‘ 𝐴 ) ) = ( 𝑁 ‘ ( 𝑇 ‘ 𝐴 ) ) ) )
79	78	imp	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐼 × 2o ) ) → ( 𝑇 ‘ ( 𝑀 ‘ 𝐴 ) ) = ( 𝑁 ‘ ( 𝑇 ‘ 𝐴 ) ) )