frgpup1

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) (Revised by Mario Carneiro, 28-Feb-2016)

	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$
	frgpup.w	$⊢ W = I (Word (I \times 2_{𝑜}))$
	frgpup.r	$⊢ \underset{˙}{\sim} = ~_{FG} (I)$
	frgpup.g	$⊢ G = freeGrp (I)$
	frgpup.x	$⊢ X = {Base}_{G}$
	frgpup.e	$⊢ E = ran (g \in W ⟼ ⟨[g] \underset{˙}{\sim}, \sum_{H} (T \circ g)⟩)$
Assertion	frgpup1	$⊢ φ \to E \in (G GrpHom H)$

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		frgpup.w	$⊢ W = I (Word (I \times 2_{𝑜}))$
8		frgpup.r	$⊢ \underset{˙}{\sim} = ~_{FG} (I)$
9		frgpup.g	$⊢ G = freeGrp (I)$
10		frgpup.x	$⊢ X = {Base}_{G}$
11		frgpup.e	$⊢ E = ran (g \in W ⟼ ⟨[g] \underset{˙}{\sim}, \sum_{H} (T \circ g)⟩)$
12		eqid	$⊢ +_{G} = +_{G}$
13		eqid	$⊢ +_{H} = +_{H}$
14	9	frgpgrp	$⊢ I \in V \to G \in Grp$
15	5 14	syl	$⊢ φ \to G \in Grp$
16	1 2 3 4 5 6 7 8 9 10 11	frgpupf	$⊢ φ \to E : X ⟶ B$
17		eqid	$⊢ freeMnd (I \times 2_{𝑜}) = freeMnd (I \times 2_{𝑜})$
18	9 17 8	frgpval	$⊢ I \in V \to G = freeMnd (I \times 2_{𝑜}) /_{𝑠} \underset{˙}{\sim}$
19	5 18	syl	$⊢ φ \to G = freeMnd (I \times 2_{𝑜}) /_{𝑠} \underset{˙}{\sim}$
20		2on	$⊢ 2_{𝑜} \in On$
21		xpexg	$⊢ (I \in V \land 2_{𝑜} \in On) \to I \times 2_{𝑜} \in V$
22	5 20 21	sylancl	$⊢ φ \to I \times 2_{𝑜} \in V$
23		wrdexg	$⊢ I \times 2_{𝑜} \in V \to Word (I \times 2_{𝑜}) \in V$
24		fvi	$⊢ Word (I \times 2_{𝑜}) \in V \to I (Word (I \times 2_{𝑜})) = Word (I \times 2_{𝑜})$
25	22 23 24	3syl	$⊢ φ \to I (Word (I \times 2_{𝑜})) = Word (I \times 2_{𝑜})$
26	7 25	eqtrid	$⊢ φ \to W = Word (I \times 2_{𝑜})$
27		eqid	$⊢ {Base}_{freeMnd (I \times 2_{𝑜})} = {Base}_{freeMnd (I \times 2_{𝑜})}$
28	17 27	frmdbas	$⊢ I \times 2_{𝑜} \in V \to {Base}_{freeMnd (I \times 2_{𝑜})} = Word (I \times 2_{𝑜})$
29	22 28	syl	$⊢ φ \to {Base}_{freeMnd (I \times 2_{𝑜})} = Word (I \times 2_{𝑜})$
30	26 29	eqtr4d	$⊢ φ \to W = {Base}_{freeMnd (I \times 2_{𝑜})}$
31	8	fvexi	$⊢ \underset{˙}{\sim} \in V$
32	31	a1i	$⊢ φ \to \underset{˙}{\sim} \in V$
33		fvexd	$⊢ φ \to freeMnd (I \times 2_{𝑜}) \in V$
34	19 30 32 33	qusbas	$⊢ φ \to W / \underset{˙}{\sim} = {Base}_{G}$
35	10 34	eqtr4id	$⊢ φ \to X = W / \underset{˙}{\sim}$
36		eqimss	$⊢ X = W / \underset{˙}{\sim} \to X \subseteq W / \underset{˙}{\sim}$
37	35 36	syl	$⊢ φ \to X \subseteq W / \underset{˙}{\sim}$
38	37	adantr	$⊢ (φ \land a \in X) \to X \subseteq W / \underset{˙}{\sim}$
39	38	sselda	$⊢ ((φ \land a \in X) \land c \in X) \to c \in (W / \underset{˙}{\sim})$
40		eqid	$⊢ W / \underset{˙}{\sim} = W / \underset{˙}{\sim}$
41		oveq2	$⊢ [u] \underset{˙}{\sim} = c \to a +_{G} [u] \underset{˙}{\sim} = a +_{G} c$
42	41	fveq2d	$⊢ [u] \underset{˙}{\sim} = c \to E (a +_{G} [u] \underset{˙}{\sim}) = E (a +_{G} c)$
43		fveq2	$⊢ [u] \underset{˙}{\sim} = c \to E ([u] \underset{˙}{\sim}) = E (c)$
44	43	oveq2d	$⊢ [u] \underset{˙}{\sim} = c \to E (a) +_{H} E ([u] \underset{˙}{\sim}) = E (a) +_{H} E (c)$
45	42 44	eqeq12d	$⊢ [u] \underset{˙}{\sim} = c \to (E (a +_{G} [u] \underset{˙}{\sim}) = E (a) +_{H} E ([u] \underset{˙}{\sim}) \leftrightarrow E (a +_{G} c) = E (a) +_{H} E (c))$
46	37	sselda	$⊢ (φ \land a \in X) \to a \in (W / \underset{˙}{\sim})$
47	46	adantlr	$⊢ ((φ \land u \in W) \land a \in X) \to a \in (W / \underset{˙}{\sim})$
48		fvoveq1	$⊢ [t] \underset{˙}{\sim} = a \to E ([t] \underset{˙}{\sim} +_{G} [u] \underset{˙}{\sim}) = E (a +_{G} [u] \underset{˙}{\sim})$
49		fveq2	$⊢ [t] \underset{˙}{\sim} = a \to E ([t] \underset{˙}{\sim}) = E (a)$
50	49	oveq1d	$⊢ [t] \underset{˙}{\sim} = a \to E ([t] \underset{˙}{\sim}) +_{H} E ([u] \underset{˙}{\sim}) = E (a) +_{H} E ([u] \underset{˙}{\sim})$
51	48 50	eqeq12d	$⊢ [t] \underset{˙}{\sim} = a \to (E ([t] \underset{˙}{\sim} +_{G} [u] \underset{˙}{\sim}) = E ([t] \underset{˙}{\sim}) +_{H} E ([u] \underset{˙}{\sim}) \leftrightarrow E (a +_{G} [u] \underset{˙}{\sim}) = E (a) +_{H} E ([u] \underset{˙}{\sim}))$
52		fviss	$⊢ I (Word (I \times 2_{𝑜})) \subseteq Word (I \times 2_{𝑜})$
53	7 52	eqsstri	$⊢ W \subseteq Word (I \times 2_{𝑜})$
54	53	sseli	$⊢ t \in W \to t \in Word (I \times 2_{𝑜})$
55	53	sseli	$⊢ u \in W \to u \in Word (I \times 2_{𝑜})$
56		ccatcl	$⊢ (t \in Word (I \times 2_{𝑜}) \land u \in Word (I \times 2_{𝑜})) \to t ++ u \in Word (I \times 2_{𝑜})$
57	54 55 56	syl2an	$⊢ (t \in W \land u \in W) \to t ++ u \in Word (I \times 2_{𝑜})$
58	7	efgrcl	$⊢ t \in W \to (I \in V \land W = Word (I \times 2_{𝑜}))$
59	58	adantr	$⊢ (t \in W \land u \in W) \to (I \in V \land W = Word (I \times 2_{𝑜}))$
60	59	simprd	$⊢ (t \in W \land u \in W) \to W = Word (I \times 2_{𝑜})$
61	57 60	eleqtrrd	$⊢ (t \in W \land u \in W) \to t ++ u \in W$
62	1 2 3 4 5 6 7 8 9 10 11	frgpupval	$⊢ (φ \land t ++ u \in W) \to E ([(t ++ u)] \underset{˙}{\sim}) = \sum_{H} (T \circ (t ++ u))$
63	61 62	sylan2	$⊢ (φ \land (t \in W \land u \in W)) \to E ([(t ++ u)] \underset{˙}{\sim}) = \sum_{H} (T \circ (t ++ u))$
64	54	ad2antrl	$⊢ (φ \land (t \in W \land u \in W)) \to t \in Word (I \times 2_{𝑜})$
65	55	ad2antll	$⊢ (φ \land (t \in W \land u \in W)) \to u \in Word (I \times 2_{𝑜})$
66	1 2 3 4 5 6	frgpuptf	$⊢ φ \to T : I \times 2_{𝑜} ⟶ B$
67	66	adantr	$⊢ (φ \land (t \in W \land u \in W)) \to T : I \times 2_{𝑜} ⟶ B$
68		ccatco	$⊢ (t \in Word (I \times 2_{𝑜}) \land u \in Word (I \times 2_{𝑜}) \land T : I \times 2_{𝑜} ⟶ B) \to T \circ (t ++ u) = (T \circ t) ++ (T \circ u)$
69	64 65 67 68	syl3anc	$⊢ (φ \land (t \in W \land u \in W)) \to T \circ (t ++ u) = (T \circ t) ++ (T \circ u)$
70	69	oveq2d	$⊢ (φ \land (t \in W \land u \in W)) \to \sum_{H} (T \circ (t ++ u)) = \sum_{H} ((T \circ t) ++ (T \circ u))$
71	4	grpmndd	$⊢ φ \to H \in Mnd$
72	71	adantr	$⊢ (φ \land (t \in W \land u \in W)) \to H \in Mnd$
73		wrdco	$⊢ (t \in Word (I \times 2_{𝑜}) \land T : I \times 2_{𝑜} ⟶ B) \to T \circ t \in Word B$
74	54 66 73	syl2anr	$⊢ (φ \land t \in W) \to T \circ t \in Word B$
75	74	adantrr	$⊢ (φ \land (t \in W \land u \in W)) \to T \circ t \in Word B$
76		wrdco	$⊢ (u \in Word (I \times 2_{𝑜}) \land T : I \times 2_{𝑜} ⟶ B) \to T \circ u \in Word B$
77	65 67 76	syl2anc	$⊢ (φ \land (t \in W \land u \in W)) \to T \circ u \in Word B$
78	1 13	gsumccat	$⊢ (H \in Mnd \land T \circ t \in Word B \land T \circ u \in Word B) \to \sum_{H} ((T \circ t) ++ (T \circ u)) = (\sum_{H}, (T \circ t)) +_{H} (\sum_{H}, (T \circ u))$
79	72 75 77 78	syl3anc	$⊢ (φ \land (t \in W \land u \in W)) \to \sum_{H} ((T \circ t) ++ (T \circ u)) = (\sum_{H}, (T \circ t)) +_{H} (\sum_{H}, (T \circ u))$
80	63 70 79	3eqtrd	$⊢ (φ \land (t \in W \land u \in W)) \to E ([(t ++ u)] \underset{˙}{\sim}) = (\sum_{H}, (T \circ t)) +_{H} (\sum_{H}, (T \circ u))$
81	7 9 8 12	frgpadd	$⊢ (t \in W \land u \in W) \to [t] \underset{˙}{\sim} +_{G} [u] \underset{˙}{\sim} = [(t ++ u)] \underset{˙}{\sim}$
82	81	adantl	$⊢ (φ \land (t \in W \land u \in W)) \to [t] \underset{˙}{\sim} +_{G} [u] \underset{˙}{\sim} = [(t ++ u)] \underset{˙}{\sim}$
83	82	fveq2d	$⊢ (φ \land (t \in W \land u \in W)) \to E ([t] \underset{˙}{\sim} +_{G} [u] \underset{˙}{\sim}) = E ([(t ++ u)] \underset{˙}{\sim})$
84	1 2 3 4 5 6 7 8 9 10 11	frgpupval	$⊢ (φ \land t \in W) \to E ([t] \underset{˙}{\sim}) = \sum_{H} (T \circ t)$
85	84	adantrr	$⊢ (φ \land (t \in W \land u \in W)) \to E ([t] \underset{˙}{\sim}) = \sum_{H} (T \circ t)$
86	1 2 3 4 5 6 7 8 9 10 11	frgpupval	$⊢ (φ \land u \in W) \to E ([u] \underset{˙}{\sim}) = \sum_{H} (T \circ u)$
87	86	adantrl	$⊢ (φ \land (t \in W \land u \in W)) \to E ([u] \underset{˙}{\sim}) = \sum_{H} (T \circ u)$
88	85 87	oveq12d	$⊢ (φ \land (t \in W \land u \in W)) \to E ([t] \underset{˙}{\sim}) +_{H} E ([u] \underset{˙}{\sim}) = (\sum_{H}, (T \circ t)) +_{H} (\sum_{H}, (T \circ u))$
89	80 83 88	3eqtr4d	$⊢ (φ \land (t \in W \land u \in W)) \to E ([t] \underset{˙}{\sim} +_{G} [u] \underset{˙}{\sim}) = E ([t] \underset{˙}{\sim}) +_{H} E ([u] \underset{˙}{\sim})$
90	89	anass1rs	$⊢ ((φ \land u \in W) \land t \in W) \to E ([t] \underset{˙}{\sim} +_{G} [u] \underset{˙}{\sim}) = E ([t] \underset{˙}{\sim}) +_{H} E ([u] \underset{˙}{\sim})$
91	40 51 90	ectocld	$⊢ ((φ \land u \in W) \land a \in (W / \underset{˙}{\sim})) \to E (a +_{G} [u] \underset{˙}{\sim}) = E (a) +_{H} E ([u] \underset{˙}{\sim})$
92	47 91	syldan	$⊢ ((φ \land u \in W) \land a \in X) \to E (a +_{G} [u] \underset{˙}{\sim}) = E (a) +_{H} E ([u] \underset{˙}{\sim})$
93	92	an32s	$⊢ ((φ \land a \in X) \land u \in W) \to E (a +_{G} [u] \underset{˙}{\sim}) = E (a) +_{H} E ([u] \underset{˙}{\sim})$
94	40 45 93	ectocld	$⊢ ((φ \land a \in X) \land c \in (W / \underset{˙}{\sim})) \to E (a +_{G} c) = E (a) +_{H} E (c)$
95	39 94	syldan	$⊢ ((φ \land a \in X) \land c \in X) \to E (a +_{G} c) = E (a) +_{H} E (c)$
96	95	anasss	$⊢ (φ \land (a \in X \land c \in X)) \to E (a +_{G} c) = E (a) +_{H} E (c)$
97	10 1 12 13 15 4 16 96	isghmd	$⊢ φ \to E \in (G GrpHom H)$

Metamath Proof Explorer

Theorem frgpup1

Proof