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	$⊢ B = {Base}_{H}$
	frgpup.n	$⊢ N = {inv}_{g} (H)$
	frgpup.t	$⊢ T = (y \in I, z \in 2_{𝑜} ⟼ if (z = \emptyset, F (y), N (F (y))))$
	frgpup.h	$⊢ φ \to H \in Grp$
	frgpup.i	$⊢ φ \to I \in V$
	frgpup.a	$⊢ φ \to F : I ⟶ B$
	frgpuptinv.m	$⊢ M = (y \in I, z \in 2_{𝑜} ⟼ ⟨y, 1_{𝑜} ∖ z⟩)$
Assertion	frgpuptinv	$⊢ (φ \land A \in (I \times 2_{𝑜})) \to T (M (A)) = N (T (A))$

Proof

Step	Hyp	Ref	Expression
1		frgpup.b	$⊢ B = {Base}_{H}$
2		frgpup.n	$⊢ N = {inv}_{g} (H)$
3		frgpup.t	$⊢ T = (y \in I, z \in 2_{𝑜} ⟼ if (z = \emptyset, F (y), N (F (y))))$
4		frgpup.h	$⊢ φ \to H \in Grp$
5		frgpup.i	$⊢ φ \to I \in V$
6		frgpup.a	$⊢ φ \to F : I ⟶ B$
7		frgpuptinv.m	$⊢ M = (y \in I, z \in 2_{𝑜} ⟼ ⟨y, 1_{𝑜} ∖ z⟩)$
8		elxp2	$⊢ A \in (I \times 2_{𝑜}) \leftrightarrow \exists a \in I \exists b \in 2_{𝑜} A = ⟨a, b⟩$
9	7	efgmval	$⊢ (a \in I \land b \in 2_{𝑜}) \to a M b = ⟨a, 1_{𝑜} ∖ b⟩$
10	9	adantl	$⊢ (φ \land (a \in I \land b \in 2_{𝑜})) \to a M b = ⟨a, 1_{𝑜} ∖ b⟩$
11	10	fveq2d	$⊢ (φ \land (a \in I \land b \in 2_{𝑜})) \to T (a M b) = T (⟨a, 1_{𝑜} ∖ b⟩)$
12		df-ov	$⊢ a T (1_{𝑜} ∖ b) = T (⟨a, 1_{𝑜} ∖ b⟩)$
13	11 12	eqtr4di	$⊢ (φ \land (a \in I \land b \in 2_{𝑜})) \to T (a M b) = a T (1_{𝑜} ∖ b)$
14		elpri	$⊢ b \in \{\emptyset, 1_{𝑜}\} \to (b = \emptyset \lor b = 1_{𝑜})$
15		df2o3	$⊢ 2_{𝑜} = \{\emptyset, 1_{𝑜}\}$
16	14 15	eleq2s	$⊢ b \in 2_{𝑜} \to (b = \emptyset \lor b = 1_{𝑜})$
17		simpr	$⊢ (φ \land a \in I) \to a \in I$
18		1oex	$⊢ 1_{𝑜} \in V$
19	18	prid2	$⊢ 1_{𝑜} \in \{\emptyset, 1_{𝑜}\}$
20	19 15	eleqtrri	$⊢ 1_{𝑜} \in 2_{𝑜}$
21		1n0	$⊢ 1_{𝑜} \neq \emptyset$
22		neeq1	$⊢ z = 1_{𝑜} \to (z \neq \emptyset \leftrightarrow 1_{𝑜} \neq \emptyset)$
23	21 22	mpbiri	$⊢ z = 1_{𝑜} \to z \neq \emptyset$
24		ifnefalse	$⊢ z \neq \emptyset \to if (z = \emptyset, F (y), N (F (y))) = N (F (y))$
25	23 24	syl	$⊢ z = 1_{𝑜} \to if (z = \emptyset, F (y), N (F (y))) = N (F (y))$
26		fveq2	$⊢ y = a \to F (y) = F (a)$
27	26	fveq2d	$⊢ y = a \to N (F (y)) = N (F (a))$
28	25 27	sylan9eqr	$⊢ (y = a \land z = 1_{𝑜}) \to if (z = \emptyset, F (y), N (F (y))) = N (F (a))$
29		fvex	$⊢ N (F (a)) \in V$
30	28 3 29	ovmpoa	$⊢ (a \in I \land 1_{𝑜} \in 2_{𝑜}) \to a T 1_{𝑜} = N (F (a))$
31	17 20 30	sylancl	$⊢ (φ \land a \in I) \to a T 1_{𝑜} = N (F (a))$
32		0ex	$⊢ \emptyset \in V$
33	32	prid1	$⊢ \emptyset \in \{\emptyset, 1_{𝑜}\}$
34	33 15	eleqtrri	$⊢ \emptyset \in 2_{𝑜}$
35		iftrue	$⊢ z = \emptyset \to if (z = \emptyset, F (y), N (F (y))) = F (y)$
36	35 26	sylan9eqr	$⊢ (y = a \land z = \emptyset) \to if (z = \emptyset, F (y), N (F (y))) = F (a)$
37		fvex	$⊢ F (a) \in V$
38	36 3 37	ovmpoa	$⊢ (a \in I \land \emptyset \in 2_{𝑜}) \to a T \emptyset = F (a)$
39	17 34 38	sylancl	$⊢ (φ \land a \in I) \to a T \emptyset = F (a)$
40	39	fveq2d	$⊢ (φ \land a \in I) \to N (a T \emptyset) = N (F (a))$
41	31 40	eqtr4d	$⊢ (φ \land a \in I) \to a T 1_{𝑜} = N (a T \emptyset)$
42		difeq2	$⊢ b = \emptyset \to 1_{𝑜} ∖ b = 1_{𝑜} ∖ \emptyset$
43		dif0	$⊢ 1_{𝑜} ∖ \emptyset = 1_{𝑜}$
44	42 43	eqtrdi	$⊢ b = \emptyset \to 1_{𝑜} ∖ b = 1_{𝑜}$
45	44	oveq2d	$⊢ b = \emptyset \to a T (1_{𝑜} ∖ b) = a T 1_{𝑜}$
46		oveq2	$⊢ b = \emptyset \to a T b = a T \emptyset$
47	46	fveq2d	$⊢ b = \emptyset \to N (a T b) = N (a T \emptyset)$
48	45 47	eqeq12d	$⊢ b = \emptyset \to (a T (1_{𝑜} ∖ b) = N (a T b) \leftrightarrow a T 1_{𝑜} = N (a T \emptyset))$
49	41 48	syl5ibrcom	$⊢ (φ \land a \in I) \to (b = \emptyset \to a T (1_{𝑜} ∖ b) = N (a T b))$
50	41	fveq2d	$⊢ (φ \land a \in I) \to N (a T 1_{𝑜}) = N (N (a T \emptyset))$
51	6	ffvelcdmda	$⊢ (φ \land a \in I) \to F (a) \in B$
52	39 51	eqeltrd	$⊢ (φ \land a \in I) \to a T \emptyset \in B$
53	1 2	grpinvinv	$⊢ (H \in Grp \land a T \emptyset \in B) \to N (N (a T \emptyset)) = a T \emptyset$
54	4 52 53	syl2an2r	$⊢ (φ \land a \in I) \to N (N (a T \emptyset)) = a T \emptyset$
55	50 54	eqtr2d	$⊢ (φ \land a \in I) \to a T \emptyset = N (a T 1_{𝑜})$
56		difeq2	$⊢ b = 1_{𝑜} \to 1_{𝑜} ∖ b = 1_{𝑜} ∖ 1_{𝑜}$
57		difid	$⊢ 1_{𝑜} ∖ 1_{𝑜} = \emptyset$
58	56 57	eqtrdi	$⊢ b = 1_{𝑜} \to 1_{𝑜} ∖ b = \emptyset$
59	58	oveq2d	$⊢ b = 1_{𝑜} \to a T (1_{𝑜} ∖ b) = a T \emptyset$
60		oveq2	$⊢ b = 1_{𝑜} \to a T b = a T 1_{𝑜}$
61	60	fveq2d	$⊢ b = 1_{𝑜} \to N (a T b) = N (a T 1_{𝑜})$
62	59 61	eqeq12d	$⊢ b = 1_{𝑜} \to (a T (1_{𝑜} ∖ b) = N (a T b) \leftrightarrow a T \emptyset = N (a T 1_{𝑜}))$
63	55 62	syl5ibrcom	$⊢ (φ \land a \in I) \to (b = 1_{𝑜} \to a T (1_{𝑜} ∖ b) = N (a T b))$
64	49 63	jaod	$⊢ (φ \land a \in I) \to ((b = \emptyset \lor b = 1_{𝑜}) \to a T (1_{𝑜} ∖ b) = N (a T b))$
65	16 64	syl5	$⊢ (φ \land a \in I) \to (b \in 2_{𝑜} \to a T (1_{𝑜} ∖ b) = N (a T b))$
66	65	impr	$⊢ (φ \land (a \in I \land b \in 2_{𝑜})) \to a T (1_{𝑜} ∖ b) = N (a T b)$
67	13 66	eqtrd	$⊢ (φ \land (a \in I \land b \in 2_{𝑜})) \to T (a M b) = N (a T b)$
68		fveq2	$⊢ A = ⟨a, b⟩ \to M (A) = M (⟨a, b⟩)$
69		df-ov	$⊢ a M b = M (⟨a, b⟩)$
70	68 69	eqtr4di	$⊢ A = ⟨a, b⟩ \to M (A) = a M b$
71	70	fveq2d	$⊢ A = ⟨a, b⟩ \to T (M (A)) = T (a M b)$
72		fveq2	$⊢ A = ⟨a, b⟩ \to T (A) = T (⟨a, b⟩)$
73		df-ov	$⊢ a T b = T (⟨a, b⟩)$
74	72 73	eqtr4di	$⊢ A = ⟨a, b⟩ \to T (A) = a T b$
75	74	fveq2d	$⊢ A = ⟨a, b⟩ \to N (T (A)) = N (a T b)$
76	71 75	eqeq12d	$⊢ A = ⟨a, b⟩ \to (T (M (A)) = N (T (A)) \leftrightarrow T (a M b) = N (a T b))$
77	67 76	syl5ibrcom	$⊢ (φ \land (a \in I \land b \in 2_{𝑜})) \to (A = ⟨a, b⟩ \to T (M (A)) = N (T (A)))$
78	77	rexlimdvva	$⊢ φ \to (\exists a \in I \exists b \in 2_{𝑜} A = ⟨a, b⟩ \to T (M (A)) = N (T (A)))$
79	8 78	biimtrid	$⊢ φ \to (A \in (I \times 2_{𝑜}) \to T (M (A)) = N (T (A)))$
80	79	imp	$⊢ (φ \land A \in (I \times 2_{𝑜})) \to T (M (A)) = N (T (A))$

Metamath Proof Explorer

Theorem frgpuptinv

Proof