Theorem frgpuptinv 18889

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

Assertion

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

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 5572	. . 3 ⊢ (𝐴 ∈ (𝐼 × 2o) ↔ ∃𝑎 ∈ 𝐼 ∃𝑏 ∈ 2o 𝐴 = ⟨𝑎, 𝑏⟩)
2		frgpuptinv.m	. . . . . . . . . 10 ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o ∖ 𝑧)⟩)
3	2	efgmval 18830	. . . . . . . . 9 ⊢ ((𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o) → (𝑎𝑀𝑏) = ⟨𝑎, (1o ∖ 𝑏)⟩)
4	3	adantl 484	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → (𝑎𝑀𝑏) = ⟨𝑎, (1o ∖ 𝑏)⟩)
5	4	fveq2d 6667	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → (𝑇‘(𝑎𝑀𝑏)) = (𝑇‘⟨𝑎, (1o ∖ 𝑏)⟩))
6		df-ov 7151	. . . . . . 7 ⊢ (𝑎𝑇(1o ∖ 𝑏)) = (𝑇‘⟨𝑎, (1o ∖ 𝑏)⟩)
7	5, 6	syl6eqr 2872	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → (𝑇‘(𝑎𝑀𝑏)) = (𝑎𝑇(1o ∖ 𝑏)))
8		elpri 4581	. . . . . . . . 9 ⊢ (𝑏 ∈ {∅, 1o} → (𝑏 = ∅ ∨ 𝑏 = 1o))
9		df2o3 8109	. . . . . . . . 9 ⊢ 2o = {∅, 1o}
10	8, 9	eleq2s 2929	. . . . . . . 8 ⊢ (𝑏 ∈ 2o → (𝑏 = ∅ ∨ 𝑏 = 1o))
11		simpr 487	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → 𝑎 ∈ 𝐼)
12		1oex 8102	. . . . . . . . . . . . . 14 ⊢ 1o ∈ V
13	12	prid2 4691	. . . . . . . . . . . . 13 ⊢ 1o ∈ {∅, 1o}
14	13, 9	eleqtrri 2910	. . . . . . . . . . . 12 ⊢ 1o ∈ 2o
15		1n0 8111	. . . . . . . . . . . . . . . 16 ⊢ 1o ≠ ∅
16		neeq1 3076	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 1o → (𝑧 ≠ ∅ ↔ 1o ≠ ∅))
17	15, 16	mpbiri 260	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 1o → 𝑧 ≠ ∅)
18		ifnefalse 4477	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ≠ ∅ → if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦))) = (𝑁‘(𝐹‘𝑦)))
19	17, 18	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 1o → if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦))) = (𝑁‘(𝐹‘𝑦)))
20		fveq2 6663	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑎 → (𝐹‘𝑦) = (𝐹‘𝑎))
21	20	fveq2d 6667	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑎 → (𝑁‘(𝐹‘𝑦)) = (𝑁‘(𝐹‘𝑎)))
22	19, 21	sylan9eqr 2876	. . . . . . . . . . . . 13 ⊢ ((𝑦 = 𝑎 ∧ 𝑧 = 1o) → if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦))) = (𝑁‘(𝐹‘𝑎)))
23		frgpup.t	. . . . . . . . . . . . 13 ⊢ 𝑇 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦))))
24		fvex 6676	. . . . . . . . . . . . 13 ⊢ (𝑁‘(𝐹‘𝑎)) ∈ V
25	22, 23, 24	ovmpoa 7297	. . . . . . . . . . . 12 ⊢ ((𝑎 ∈ 𝐼 ∧ 1o ∈ 2o) → (𝑎𝑇1o) = (𝑁‘(𝐹‘𝑎)))
26	11, 14, 25	sylancl 588	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → (𝑎𝑇1o) = (𝑁‘(𝐹‘𝑎)))
27		0ex 5202	. . . . . . . . . . . . . . 15 ⊢ ∅ ∈ V
28	27	prid1 4690	. . . . . . . . . . . . . 14 ⊢ ∅ ∈ {∅, 1o}
29	28, 9	eleqtrri 2910	. . . . . . . . . . . . 13 ⊢ ∅ ∈ 2o
30		iftrue 4471	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = ∅ → if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦))) = (𝐹‘𝑦))
31	30, 20	sylan9eqr 2876	. . . . . . . . . . . . . 14 ⊢ ((𝑦 = 𝑎 ∧ 𝑧 = ∅) → if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦))) = (𝐹‘𝑎))
32		fvex 6676	. . . . . . . . . . . . . 14 ⊢ (𝐹‘𝑎) ∈ V
33	31, 23, 32	ovmpoa 7297	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ 𝐼 ∧ ∅ ∈ 2o) → (𝑎𝑇∅) = (𝐹‘𝑎))
34	11, 29, 33	sylancl 588	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → (𝑎𝑇∅) = (𝐹‘𝑎))
35	34	fveq2d 6667	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → (𝑁‘(𝑎𝑇∅)) = (𝑁‘(𝐹‘𝑎)))
36	26, 35	eqtr4d 2857	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → (𝑎𝑇1o) = (𝑁‘(𝑎𝑇∅)))
37		difeq2 4091	. . . . . . . . . . . . 13 ⊢ (𝑏 = ∅ → (1o ∖ 𝑏) = (1o ∖ ∅))
38		dif0 4330	. . . . . . . . . . . . 13 ⊢ (1o ∖ ∅) = 1o
39	37, 38	syl6eq 2870	. . . . . . . . . . . 12 ⊢ (𝑏 = ∅ → (1o ∖ 𝑏) = 1o)
40	39	oveq2d 7164	. . . . . . . . . . 11 ⊢ (𝑏 = ∅ → (𝑎𝑇(1o ∖ 𝑏)) = (𝑎𝑇1o))
41		oveq2 7156	. . . . . . . . . . . 12 ⊢ (𝑏 = ∅ → (𝑎𝑇𝑏) = (𝑎𝑇∅))
42	41	fveq2d 6667	. . . . . . . . . . 11 ⊢ (𝑏 = ∅ → (𝑁‘(𝑎𝑇𝑏)) = (𝑁‘(𝑎𝑇∅)))
43	40, 42	eqeq12d 2835	. . . . . . . . . 10 ⊢ (𝑏 = ∅ → ((𝑎𝑇(1o ∖ 𝑏)) = (𝑁‘(𝑎𝑇𝑏)) ↔ (𝑎𝑇1o) = (𝑁‘(𝑎𝑇∅))))
44	36, 43	syl5ibrcom 249	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → (𝑏 = ∅ → (𝑎𝑇(1o ∖ 𝑏)) = (𝑁‘(𝑎𝑇𝑏))))
45	36	fveq2d 6667	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → (𝑁‘(𝑎𝑇1o)) = (𝑁‘(𝑁‘(𝑎𝑇∅))))
46		frgpup.h	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐻 ∈ Grp)
47		frgpup.a	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹:𝐼⟶𝐵)
48	47	ffvelrnda 6844	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → (𝐹‘𝑎) ∈ 𝐵)
49	34, 48	eqeltrd 2911	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → (𝑎𝑇∅) ∈ 𝐵)
50		frgpup.b	. . . . . . . . . . . . 13 ⊢ 𝐵 = (Base‘𝐻)
51		frgpup.n	. . . . . . . . . . . . 13 ⊢ 𝑁 = (invg‘𝐻)
52	50, 51	grpinvinv 18158	. . . . . . . . . . . 12 ⊢ ((𝐻 ∈ Grp ∧ (𝑎𝑇∅) ∈ 𝐵) → (𝑁‘(𝑁‘(𝑎𝑇∅))) = (𝑎𝑇∅))
53	46, 49, 52	syl2an2r 683	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → (𝑁‘(𝑁‘(𝑎𝑇∅))) = (𝑎𝑇∅))
54	45, 53	eqtr2d 2855	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → (𝑎𝑇∅) = (𝑁‘(𝑎𝑇1o)))
55		difeq2 4091	. . . . . . . . . . . . 13 ⊢ (𝑏 = 1o → (1o ∖ 𝑏) = (1o ∖ 1o))
56		difid 4328	. . . . . . . . . . . . 13 ⊢ (1o ∖ 1o) = ∅
57	55, 56	syl6eq 2870	. . . . . . . . . . . 12 ⊢ (𝑏 = 1o → (1o ∖ 𝑏) = ∅)
58	57	oveq2d 7164	. . . . . . . . . . 11 ⊢ (𝑏 = 1o → (𝑎𝑇(1o ∖ 𝑏)) = (𝑎𝑇∅))
59		oveq2 7156	. . . . . . . . . . . 12 ⊢ (𝑏 = 1o → (𝑎𝑇𝑏) = (𝑎𝑇1o))
60	59	fveq2d 6667	. . . . . . . . . . 11 ⊢ (𝑏 = 1o → (𝑁‘(𝑎𝑇𝑏)) = (𝑁‘(𝑎𝑇1o)))
61	58, 60	eqeq12d 2835	. . . . . . . . . 10 ⊢ (𝑏 = 1o → ((𝑎𝑇(1o ∖ 𝑏)) = (𝑁‘(𝑎𝑇𝑏)) ↔ (𝑎𝑇∅) = (𝑁‘(𝑎𝑇1o))))
62	54, 61	syl5ibrcom 249	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → (𝑏 = 1o → (𝑎𝑇(1o ∖ 𝑏)) = (𝑁‘(𝑎𝑇𝑏))))
63	44, 62	jaod 855	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → ((𝑏 = ∅ ∨ 𝑏 = 1o) → (𝑎𝑇(1o ∖ 𝑏)) = (𝑁‘(𝑎𝑇𝑏))))
64	10, 63	syl5 34	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → (𝑏 ∈ 2o → (𝑎𝑇(1o ∖ 𝑏)) = (𝑁‘(𝑎𝑇𝑏))))
65	64	impr 457	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → (𝑎𝑇(1o ∖ 𝑏)) = (𝑁‘(𝑎𝑇𝑏)))
66	7, 65	eqtrd 2854	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → (𝑇‘(𝑎𝑀𝑏)) = (𝑁‘(𝑎𝑇𝑏)))
67		fveq2 6663	. . . . . . . 8 ⊢ (𝐴 = ⟨𝑎, 𝑏⟩ → (𝑀‘𝐴) = (𝑀‘⟨𝑎, 𝑏⟩))
68		df-ov 7151	. . . . . . . 8 ⊢ (𝑎𝑀𝑏) = (𝑀‘⟨𝑎, 𝑏⟩)
69	67, 68	syl6eqr 2872	. . . . . . 7 ⊢ (𝐴 = ⟨𝑎, 𝑏⟩ → (𝑀‘𝐴) = (𝑎𝑀𝑏))
70	69	fveq2d 6667	. . . . . 6 ⊢ (𝐴 = ⟨𝑎, 𝑏⟩ → (𝑇‘(𝑀‘𝐴)) = (𝑇‘(𝑎𝑀𝑏)))
71		fveq2 6663	. . . . . . . 8 ⊢ (𝐴 = ⟨𝑎, 𝑏⟩ → (𝑇‘𝐴) = (𝑇‘⟨𝑎, 𝑏⟩))
72		df-ov 7151	. . . . . . . 8 ⊢ (𝑎𝑇𝑏) = (𝑇‘⟨𝑎, 𝑏⟩)
73	71, 72	syl6eqr 2872	. . . . . . 7 ⊢ (𝐴 = ⟨𝑎, 𝑏⟩ → (𝑇‘𝐴) = (𝑎𝑇𝑏))
74	73	fveq2d 6667	. . . . . 6 ⊢ (𝐴 = ⟨𝑎, 𝑏⟩ → (𝑁‘(𝑇‘𝐴)) = (𝑁‘(𝑎𝑇𝑏)))
75	70, 74	eqeq12d 2835	. . . . 5 ⊢ (𝐴 = ⟨𝑎, 𝑏⟩ → ((𝑇‘(𝑀‘𝐴)) = (𝑁‘(𝑇‘𝐴)) ↔ (𝑇‘(𝑎𝑀𝑏)) = (𝑁‘(𝑎𝑇𝑏))))
76	66, 75	syl5ibrcom 249	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → (𝐴 = ⟨𝑎, 𝑏⟩ → (𝑇‘(𝑀‘𝐴)) = (𝑁‘(𝑇‘𝐴))))
77	76	rexlimdvva 3292	. . 3 ⊢ (𝜑 → (∃𝑎 ∈ 𝐼 ∃𝑏 ∈ 2o 𝐴 = ⟨𝑎, 𝑏⟩ → (𝑇‘(𝑀‘𝐴)) = (𝑁‘(𝑇‘𝐴))))
78	1, 77	syl5bi 244	. 2 ⊢ (𝜑 → (𝐴 ∈ (𝐼 × 2o) → (𝑇‘(𝑀‘𝐴)) = (𝑁‘(𝑇‘𝐴))))
79	78	imp 409	1 ⊢ ((𝜑 ∧ 𝐴 ∈ (𝐼 × 2o)) → (𝑇‘(𝑀‘𝐴)) = (𝑁‘(𝑇‘𝐴)))

Syntax hints:   → wi 4   ∧ wa 398   ∨ wo 843   = wceq 1531   ∈ wcel 2108   ≠ wne 3014  ∃wrex 3137   ∖ cdif 3931  ∅c0 4289  ifcif 4465  {cpr 4561  ⟨cop 4565   × cxp 5546  ⟶wf 6344  ‘cfv 6348  (class class class)co 7148   ∈ cmpo 7150  1_oc1o 8087  2_oc2o 8088  Basecbs 16475  Grpcgrp 18095  inv_gcminusg 18096

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1083  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-ral 3141  df-rex 3142  df-reu 3143  df-rmo 3144  df-rab 3145  df-v 3495  df-sbc 3771  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-pss 3952  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4831  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-ord 6187  df-on 6188  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-fv 6356  df-riota 7106  df-ov 7151  df-oprab 7152  df-mpo 7153  df-1o 8094  df-2o 8095  df-0g 16707  df-mgm 17844  df-sgrp 17893  df-mnd 17904  df-grp 18098  df-minusg 18099

This theorem is referenced by:  frgpuplem  18890