Theorem frgpuptinv 18184

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.)

Hypotheses

Ref	Expression
frgpup.b	⊢ 𝐵 = (Base‘𝐻)
frgpup.n	⊢ 𝑁 = (invg‘𝐻)
frgpup.t	⊢ 𝑇 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦))))
frgpup.h	⊢ (𝜑 → 𝐻 ∈ Grp)
frgpup.i	⊢ (𝜑 → 𝐼 ∈ 𝑉)
frgpup.a	⊢ (𝜑 → 𝐹:𝐼⟶𝐵)
frgpuptinv.m	⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜 ∖ 𝑧)⟩)

Assertion

Ref	Expression
frgpuptinv	⊢ ((𝜑 ∧ 𝐴 ∈ (𝐼 × 2𝑜)) → (𝑇‘(𝑀‘𝐴)) = (𝑁‘(𝑇‘𝐴)))

Distinct variable groups:   𝑦,𝑧,𝐴   𝑦,𝐹,𝑧   𝑦,𝑁,𝑧   𝑦,𝐵,𝑧   𝜑,𝑦,𝑧   𝑦,𝐼,𝑧

Allowed substitution hints:   𝑇(𝑦,𝑧)   𝐻(𝑦,𝑧)   𝑀(𝑦,𝑧)   𝑉(𝑦,𝑧)

Proof of Theorem frgpuptinv

Dummy variables 𝑎 𝑏 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elxp2 5132	. . 3 ⊢ (𝐴 ∈ (𝐼 × 2𝑜) ↔ ∃𝑎 ∈ 𝐼 ∃𝑏 ∈ 2𝑜 𝐴 = ⟨𝑎, 𝑏⟩)
2		frgpuptinv.m	. . . . . . . . . 10 ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜 ∖ 𝑧)⟩)
3	2	efgmval 18125	. . . . . . . . 9 ⊢ ((𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜) → (𝑎𝑀𝑏) = ⟨𝑎, (1𝑜 ∖ 𝑏)⟩)
4	3	adantl 482	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑎𝑀𝑏) = ⟨𝑎, (1𝑜 ∖ 𝑏)⟩)
5	4	fveq2d 6195	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑇‘(𝑎𝑀𝑏)) = (𝑇‘⟨𝑎, (1𝑜 ∖ 𝑏)⟩))
6		df-ov 6653	. . . . . . 7 ⊢ (𝑎𝑇(1𝑜 ∖ 𝑏)) = (𝑇‘⟨𝑎, (1𝑜 ∖ 𝑏)⟩)
7	5, 6	syl6eqr 2674	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑇‘(𝑎𝑀𝑏)) = (𝑎𝑇(1𝑜 ∖ 𝑏)))
8		elpri 4197	. . . . . . . . 9 ⊢ (𝑏 ∈ {∅, 1𝑜} → (𝑏 = ∅ ∨ 𝑏 = 1𝑜))
9		df2o3 7573	. . . . . . . . 9 ⊢ 2𝑜 = {∅, 1𝑜}
10	8, 9	eleq2s 2719	. . . . . . . 8 ⊢ (𝑏 ∈ 2𝑜 → (𝑏 = ∅ ∨ 𝑏 = 1𝑜))
11		simpr 477	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → 𝑎 ∈ 𝐼)
12		1on 7567	. . . . . . . . . . . . . . 15 ⊢ 1𝑜 ∈ On
13	12	elexi 3213	. . . . . . . . . . . . . 14 ⊢ 1𝑜 ∈ V
14	13	prid2 4298	. . . . . . . . . . . . 13 ⊢ 1𝑜 ∈ {∅, 1𝑜}
15	14, 9	eleqtrri 2700	. . . . . . . . . . . 12 ⊢ 1𝑜 ∈ 2𝑜
16		1n0 7575	. . . . . . . . . . . . . . . 16 ⊢ 1𝑜 ≠ ∅
17		neeq1 2856	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 1𝑜 → (𝑧 ≠ ∅ ↔ 1𝑜 ≠ ∅))
18	16, 17	mpbiri 248	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 1𝑜 → 𝑧 ≠ ∅)
19		ifnefalse 4098	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ≠ ∅ → if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦))) = (𝑁‘(𝐹‘𝑦)))
20	18, 19	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 1𝑜 → if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦))) = (𝑁‘(𝐹‘𝑦)))
21		fveq2 6191	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑎 → (𝐹‘𝑦) = (𝐹‘𝑎))
22	21	fveq2d 6195	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑎 → (𝑁‘(𝐹‘𝑦)) = (𝑁‘(𝐹‘𝑎)))
23	20, 22	sylan9eqr 2678	. . . . . . . . . . . . 13 ⊢ ((𝑦 = 𝑎 ∧ 𝑧 = 1𝑜) → if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦))) = (𝑁‘(𝐹‘𝑎)))
24		frgpup.t	. . . . . . . . . . . . 13 ⊢ 𝑇 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦))))
25		fvex 6201	. . . . . . . . . . . . 13 ⊢ (𝑁‘(𝐹‘𝑎)) ∈ V
26	23, 24, 25	ovmpt2a 6791	. . . . . . . . . . . 12 ⊢ ((𝑎 ∈ 𝐼 ∧ 1𝑜 ∈ 2𝑜) → (𝑎𝑇1𝑜) = (𝑁‘(𝐹‘𝑎)))
27	11, 15, 26	sylancl 694	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → (𝑎𝑇1𝑜) = (𝑁‘(𝐹‘𝑎)))
28		0ex 4790	. . . . . . . . . . . . . . 15 ⊢ ∅ ∈ V
29	28	prid1 4297	. . . . . . . . . . . . . 14 ⊢ ∅ ∈ {∅, 1𝑜}
30	29, 9	eleqtrri 2700	. . . . . . . . . . . . 13 ⊢ ∅ ∈ 2𝑜
31		iftrue 4092	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = ∅ → if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦))) = (𝐹‘𝑦))
32	31, 21	sylan9eqr 2678	. . . . . . . . . . . . . 14 ⊢ ((𝑦 = 𝑎 ∧ 𝑧 = ∅) → if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦))) = (𝐹‘𝑎))
33		fvex 6201	. . . . . . . . . . . . . 14 ⊢ (𝐹‘𝑎) ∈ V
34	32, 24, 33	ovmpt2a 6791	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ 𝐼 ∧ ∅ ∈ 2𝑜) → (𝑎𝑇∅) = (𝐹‘𝑎))
35	11, 30, 34	sylancl 694	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → (𝑎𝑇∅) = (𝐹‘𝑎))
36	35	fveq2d 6195	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → (𝑁‘(𝑎𝑇∅)) = (𝑁‘(𝐹‘𝑎)))
37	27, 36	eqtr4d 2659	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → (𝑎𝑇1𝑜) = (𝑁‘(𝑎𝑇∅)))
38		difeq2 3722	. . . . . . . . . . . . 13 ⊢ (𝑏 = ∅ → (1𝑜 ∖ 𝑏) = (1𝑜 ∖ ∅))
39		dif0 3950	. . . . . . . . . . . . 13 ⊢ (1𝑜 ∖ ∅) = 1𝑜
40	38, 39	syl6eq 2672	. . . . . . . . . . . 12 ⊢ (𝑏 = ∅ → (1𝑜 ∖ 𝑏) = 1𝑜)
41	40	oveq2d 6666	. . . . . . . . . . 11 ⊢ (𝑏 = ∅ → (𝑎𝑇(1𝑜 ∖ 𝑏)) = (𝑎𝑇1𝑜))
42		oveq2 6658	. . . . . . . . . . . 12 ⊢ (𝑏 = ∅ → (𝑎𝑇𝑏) = (𝑎𝑇∅))
43	42	fveq2d 6195	. . . . . . . . . . 11 ⊢ (𝑏 = ∅ → (𝑁‘(𝑎𝑇𝑏)) = (𝑁‘(𝑎𝑇∅)))
44	41, 43	eqeq12d 2637	. . . . . . . . . 10 ⊢ (𝑏 = ∅ → ((𝑎𝑇(1𝑜 ∖ 𝑏)) = (𝑁‘(𝑎𝑇𝑏)) ↔ (𝑎𝑇1𝑜) = (𝑁‘(𝑎𝑇∅))))
45	37, 44	syl5ibrcom 237	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → (𝑏 = ∅ → (𝑎𝑇(1𝑜 ∖ 𝑏)) = (𝑁‘(𝑎𝑇𝑏))))
46	37	fveq2d 6195	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → (𝑁‘(𝑎𝑇1𝑜)) = (𝑁‘(𝑁‘(𝑎𝑇∅))))
47		frgpup.h	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐻 ∈ Grp)
48	47	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → 𝐻 ∈ Grp)
49		frgpup.a	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹:𝐼⟶𝐵)
50	49	ffvelrnda 6359	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → (𝐹‘𝑎) ∈ 𝐵)
51	35, 50	eqeltrd 2701	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → (𝑎𝑇∅) ∈ 𝐵)
52		frgpup.b	. . . . . . . . . . . . 13 ⊢ 𝐵 = (Base‘𝐻)
53		frgpup.n	. . . . . . . . . . . . 13 ⊢ 𝑁 = (invg‘𝐻)
54	52, 53	grpinvinv 17482	. . . . . . . . . . . 12 ⊢ ((𝐻 ∈ Grp ∧ (𝑎𝑇∅) ∈ 𝐵) → (𝑁‘(𝑁‘(𝑎𝑇∅))) = (𝑎𝑇∅))
55	48, 51, 54	syl2anc 693	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → (𝑁‘(𝑁‘(𝑎𝑇∅))) = (𝑎𝑇∅))
56	46, 55	eqtr2d 2657	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → (𝑎𝑇∅) = (𝑁‘(𝑎𝑇1𝑜)))
57		difeq2 3722	. . . . . . . . . . . . 13 ⊢ (𝑏 = 1𝑜 → (1𝑜 ∖ 𝑏) = (1𝑜 ∖ 1𝑜))
58		difid 3948	. . . . . . . . . . . . 13 ⊢ (1𝑜 ∖ 1𝑜) = ∅
59	57, 58	syl6eq 2672	. . . . . . . . . . . 12 ⊢ (𝑏 = 1𝑜 → (1𝑜 ∖ 𝑏) = ∅)
60	59	oveq2d 6666	. . . . . . . . . . 11 ⊢ (𝑏 = 1𝑜 → (𝑎𝑇(1𝑜 ∖ 𝑏)) = (𝑎𝑇∅))
61		oveq2 6658	. . . . . . . . . . . 12 ⊢ (𝑏 = 1𝑜 → (𝑎𝑇𝑏) = (𝑎𝑇1𝑜))
62	61	fveq2d 6195	. . . . . . . . . . 11 ⊢ (𝑏 = 1𝑜 → (𝑁‘(𝑎𝑇𝑏)) = (𝑁‘(𝑎𝑇1𝑜)))
63	60, 62	eqeq12d 2637	. . . . . . . . . 10 ⊢ (𝑏 = 1𝑜 → ((𝑎𝑇(1𝑜 ∖ 𝑏)) = (𝑁‘(𝑎𝑇𝑏)) ↔ (𝑎𝑇∅) = (𝑁‘(𝑎𝑇1𝑜))))
64	56, 63	syl5ibrcom 237	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → (𝑏 = 1𝑜 → (𝑎𝑇(1𝑜 ∖ 𝑏)) = (𝑁‘(𝑎𝑇𝑏))))
65	45, 64	jaod 395	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → ((𝑏 = ∅ ∨ 𝑏 = 1𝑜) → (𝑎𝑇(1𝑜 ∖ 𝑏)) = (𝑁‘(𝑎𝑇𝑏))))
66	10, 65	syl5 34	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → (𝑏 ∈ 2𝑜 → (𝑎𝑇(1𝑜 ∖ 𝑏)) = (𝑁‘(𝑎𝑇𝑏))))
67	66	impr 649	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑎𝑇(1𝑜 ∖ 𝑏)) = (𝑁‘(𝑎𝑇𝑏)))
68	7, 67	eqtrd 2656	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑇‘(𝑎𝑀𝑏)) = (𝑁‘(𝑎𝑇𝑏)))
69		fveq2 6191	. . . . . . . 8 ⊢ (𝐴 = ⟨𝑎, 𝑏⟩ → (𝑀‘𝐴) = (𝑀‘⟨𝑎, 𝑏⟩))
70		df-ov 6653	. . . . . . . 8 ⊢ (𝑎𝑀𝑏) = (𝑀‘⟨𝑎, 𝑏⟩)
71	69, 70	syl6eqr 2674	. . . . . . 7 ⊢ (𝐴 = ⟨𝑎, 𝑏⟩ → (𝑀‘𝐴) = (𝑎𝑀𝑏))
72	71	fveq2d 6195	. . . . . 6 ⊢ (𝐴 = ⟨𝑎, 𝑏⟩ → (𝑇‘(𝑀‘𝐴)) = (𝑇‘(𝑎𝑀𝑏)))
73		fveq2 6191	. . . . . . . 8 ⊢ (𝐴 = ⟨𝑎, 𝑏⟩ → (𝑇‘𝐴) = (𝑇‘⟨𝑎, 𝑏⟩))
74		df-ov 6653	. . . . . . . 8 ⊢ (𝑎𝑇𝑏) = (𝑇‘⟨𝑎, 𝑏⟩)
75	73, 74	syl6eqr 2674	. . . . . . 7 ⊢ (𝐴 = ⟨𝑎, 𝑏⟩ → (𝑇‘𝐴) = (𝑎𝑇𝑏))
76	75	fveq2d 6195	. . . . . 6 ⊢ (𝐴 = ⟨𝑎, 𝑏⟩ → (𝑁‘(𝑇‘𝐴)) = (𝑁‘(𝑎𝑇𝑏)))
77	72, 76	eqeq12d 2637	. . . . 5 ⊢ (𝐴 = ⟨𝑎, 𝑏⟩ → ((𝑇‘(𝑀‘𝐴)) = (𝑁‘(𝑇‘𝐴)) ↔ (𝑇‘(𝑎𝑀𝑏)) = (𝑁‘(𝑎𝑇𝑏))))
78	68, 77	syl5ibrcom 237	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝐴 = ⟨𝑎, 𝑏⟩ → (𝑇‘(𝑀‘𝐴)) = (𝑁‘(𝑇‘𝐴))))
79	78	rexlimdvva 3038	. . 3 ⊢ (𝜑 → (∃𝑎 ∈ 𝐼 ∃𝑏 ∈ 2𝑜 𝐴 = ⟨𝑎, 𝑏⟩ → (𝑇‘(𝑀‘𝐴)) = (𝑁‘(𝑇‘𝐴))))
80	1, 79	syl5bi 232	. 2 ⊢ (𝜑 → (𝐴 ∈ (𝐼 × 2𝑜) → (𝑇‘(𝑀‘𝐴)) = (𝑁‘(𝑇‘𝐴))))
81	80	imp 445	1 ⊢ ((𝜑 ∧ 𝐴 ∈ (𝐼 × 2𝑜)) → (𝑇‘(𝑀‘𝐴)) = (𝑁‘(𝑇‘𝐴)))

Syntax hints:   → wi 4   ∨ wo 383   ∧ wa 384   = wceq 1483   ∈ wcel 1990   ≠ wne 2794  ∃wrex 2913   ∖ cdif 3571  ∅c0 3915  ifcif 4086  {cpr 4179  ⟨cop 4183   × cxp 5112  Oncon0 5723  ⟶wf 5884  ‘cfv 5888  (class class class)co 6650   ↦ cmpt2 6652  1_𝑜c1o 7553  2_𝑜c2o 7554  Basecbs 15857  Grpcgrp 17422  inv_gcminusg 17423

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-ord 5726  df-on 5727  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-1o 7560  df-2o 7561  df-0g 16102  df-mgm 17242  df-sgrp 17284  df-mnd 17295  df-grp 17425  df-minusg 17426

This theorem is referenced by:  frgpuplem  18185