frmdup1

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, 27-Sep-2015)

	Ref	Expression
Hypotheses	frmdup.m	$⊢ M = freeMnd (I)$
	frmdup.b	$⊢ B = {Base}_{G}$
	frmdup.e	$⊢ E = (x \in Word I ⟼ \sum_{G} (A \circ x))$
	frmdup.g	$⊢ φ \to G \in Mnd$
	frmdup.i	$⊢ φ \to I \in X$
	frmdup.a	$⊢ φ \to A : I ⟶ B$
Assertion	frmdup1	$⊢ φ \to E \in (M MndHom G)$

Proof

Step	Hyp	Ref	Expression
1		frmdup.m	$⊢ M = freeMnd (I)$
2		frmdup.b	$⊢ B = {Base}_{G}$
3		frmdup.e	$⊢ E = (x \in Word I ⟼ \sum_{G} (A \circ x))$
4		frmdup.g	$⊢ φ \to G \in Mnd$
5		frmdup.i	$⊢ φ \to I \in X$
6		frmdup.a	$⊢ φ \to A : I ⟶ B$
7	1	frmdmnd	$⊢ I \in X \to M \in Mnd$
8	5 7	syl	$⊢ φ \to M \in Mnd$
9	4	adantr	$⊢ (φ \land x \in Word I) \to G \in Mnd$
10		simpr	$⊢ (φ \land x \in Word I) \to x \in Word I$
11	6	adantr	$⊢ (φ \land x \in Word I) \to A : I ⟶ B$
12		wrdco	$⊢ (x \in Word I \land A : I ⟶ B) \to A \circ x \in Word B$
13	10 11 12	syl2anc	$⊢ (φ \land x \in Word I) \to A \circ x \in Word B$
14	2	gsumwcl	$⊢ (G \in Mnd \land A \circ x \in Word B) \to \sum_{G} (A \circ x) \in B$
15	9 13 14	syl2anc	$⊢ (φ \land x \in Word I) \to \sum_{G} (A \circ x) \in B$
16	15 3	fmptd	$⊢ φ \to E : Word I ⟶ B$
17		eqid	$⊢ {Base}_{M} = {Base}_{M}$
18	1 17	frmdbas	$⊢ I \in X \to {Base}_{M} = Word I$
19	5 18	syl	$⊢ φ \to {Base}_{M} = Word I$
20	19	feq2d	$⊢ φ \to (E : {Base}_{M} ⟶ B \leftrightarrow E : Word I ⟶ B)$
21	16 20	mpbird	$⊢ φ \to E : {Base}_{M} ⟶ B$
22	1 17	frmdelbas	$⊢ y \in {Base}_{M} \to y \in Word I$
23	22	ad2antrl	$⊢ (φ \land (y \in {Base}_{M} \land z \in {Base}_{M})) \to y \in Word I$
24	1 17	frmdelbas	$⊢ z \in {Base}_{M} \to z \in Word I$
25	24	ad2antll	$⊢ (φ \land (y \in {Base}_{M} \land z \in {Base}_{M})) \to z \in Word I$
26	6	adantr	$⊢ (φ \land (y \in {Base}_{M} \land z \in {Base}_{M})) \to A : I ⟶ B$
27		ccatco	$⊢ (y \in Word I \land z \in Word I \land A : I ⟶ B) \to A \circ (y ++ z) = (A \circ y) ++ (A \circ z)$
28	23 25 26 27	syl3anc	$⊢ (φ \land (y \in {Base}_{M} \land z \in {Base}_{M})) \to A \circ (y ++ z) = (A \circ y) ++ (A \circ z)$
29	28	oveq2d	$⊢ (φ \land (y \in {Base}_{M} \land z \in {Base}_{M})) \to \sum_{G} (A \circ (y ++ z)) = \sum_{G} ((A \circ y) ++ (A \circ z))$
30	4	adantr	$⊢ (φ \land (y \in {Base}_{M} \land z \in {Base}_{M})) \to G \in Mnd$
31		wrdco	$⊢ (y \in Word I \land A : I ⟶ B) \to A \circ y \in Word B$
32	23 26 31	syl2anc	$⊢ (φ \land (y \in {Base}_{M} \land z \in {Base}_{M})) \to A \circ y \in Word B$
33		wrdco	$⊢ (z \in Word I \land A : I ⟶ B) \to A \circ z \in Word B$
34	25 26 33	syl2anc	$⊢ (φ \land (y \in {Base}_{M} \land z \in {Base}_{M})) \to A \circ z \in Word B$
35		eqid	$⊢ +_{G} = +_{G}$
36	2 35	gsumccat	$⊢ (G \in Mnd \land A \circ y \in Word B \land A \circ z \in Word B) \to \sum_{G} ((A \circ y) ++ (A \circ z)) = (\sum_{G}, (A \circ y)) +_{G} (\sum_{G}, (A \circ z))$
37	30 32 34 36	syl3anc	$⊢ (φ \land (y \in {Base}_{M} \land z \in {Base}_{M})) \to \sum_{G} ((A \circ y) ++ (A \circ z)) = (\sum_{G}, (A \circ y)) +_{G} (\sum_{G}, (A \circ z))$
38	29 37	eqtrd	$⊢ (φ \land (y \in {Base}_{M} \land z \in {Base}_{M})) \to \sum_{G} (A \circ (y ++ z)) = (\sum_{G}, (A \circ y)) +_{G} (\sum_{G}, (A \circ z))$
39		eqid	$⊢ +_{M} = +_{M}$
40	1 17 39	frmdadd	$⊢ (y \in {Base}_{M} \land z \in {Base}_{M}) \to y +_{M} z = y ++ z$
41	40	adantl	$⊢ (φ \land (y \in {Base}_{M} \land z \in {Base}_{M})) \to y +_{M} z = y ++ z$
42	41	fveq2d	$⊢ (φ \land (y \in {Base}_{M} \land z \in {Base}_{M})) \to E (y +_{M} z) = E (y ++ z)$
43		ccatcl	$⊢ (y \in Word I \land z \in Word I) \to y ++ z \in Word I$
44	23 25 43	syl2anc	$⊢ (φ \land (y \in {Base}_{M} \land z \in {Base}_{M})) \to y ++ z \in Word I$
45		coeq2	$⊢ x = y ++ z \to A \circ x = A \circ (y ++ z)$
46	45	oveq2d	$⊢ x = y ++ z \to \sum_{G} (A \circ x) = \sum_{G} (A \circ (y ++ z))$
47		ovex	$⊢ \sum_{G} (A \circ x) \in V$
48	46 3 47	fvmpt3i	$⊢ y ++ z \in Word I \to E (y ++ z) = \sum_{G} (A \circ (y ++ z))$
49	44 48	syl	$⊢ (φ \land (y \in {Base}_{M} \land z \in {Base}_{M})) \to E (y ++ z) = \sum_{G} (A \circ (y ++ z))$
50	42 49	eqtrd	$⊢ (φ \land (y \in {Base}_{M} \land z \in {Base}_{M})) \to E (y +_{M} z) = \sum_{G} (A \circ (y ++ z))$
51		coeq2	$⊢ x = y \to A \circ x = A \circ y$
52	51	oveq2d	$⊢ x = y \to \sum_{G} (A \circ x) = \sum_{G} (A \circ y)$
53	52 3 47	fvmpt3i	$⊢ y \in Word I \to E (y) = \sum_{G} (A \circ y)$
54		coeq2	$⊢ x = z \to A \circ x = A \circ z$
55	54	oveq2d	$⊢ x = z \to \sum_{G} (A \circ x) = \sum_{G} (A \circ z)$
56	55 3 47	fvmpt3i	$⊢ z \in Word I \to E (z) = \sum_{G} (A \circ z)$
57	53 56	oveqan12d	$⊢ (y \in Word I \land z \in Word I) \to E (y) +_{G} E (z) = (\sum_{G}, (A \circ y)) +_{G} (\sum_{G}, (A \circ z))$
58	23 25 57	syl2anc	$⊢ (φ \land (y \in {Base}_{M} \land z \in {Base}_{M})) \to E (y) +_{G} E (z) = (\sum_{G}, (A \circ y)) +_{G} (\sum_{G}, (A \circ z))$
59	38 50 58	3eqtr4d	$⊢ (φ \land (y \in {Base}_{M} \land z \in {Base}_{M})) \to E (y +_{M} z) = E (y) +_{G} E (z)$
60	59	ralrimivva	$⊢ φ \to \forall y \in {Base}_{M} \forall z \in {Base}_{M} E (y +_{M} z) = E (y) +_{G} E (z)$
61		wrd0	$⊢ \emptyset \in Word I$
62		coeq2	$⊢ x = \emptyset \to A \circ x = A \circ \emptyset$
63		co02	$⊢ A \circ \emptyset = \emptyset$
64	62 63	eqtrdi	$⊢ x = \emptyset \to A \circ x = \emptyset$
65	64	oveq2d	$⊢ x = \emptyset \to \sum_{G} (A \circ x) = \sum_{G} \emptyset$
66		eqid	$⊢ 0_{G} = 0_{G}$
67	66	gsum0	$⊢ \sum_{G} \emptyset = 0_{G}$
68	65 67	eqtrdi	$⊢ x = \emptyset \to \sum_{G} (A \circ x) = 0_{G}$
69	68 3 47	fvmpt3i	$⊢ \emptyset \in Word I \to E (\emptyset) = 0_{G}$
70	61 69	mp1i	$⊢ φ \to E (\emptyset) = 0_{G}$
71	21 60 70	3jca	$⊢ φ \to (E : {Base}_{M} ⟶ B \land \forall y \in {Base}_{M} \forall z \in {Base}_{M} E (y +_{M} z) = E (y) +_{G} E (z) \land E (\emptyset) = 0_{G})$
72	1	frmd0	$⊢ \emptyset = 0_{M}$
73	17 2 39 35 72 66	ismhm	$⊢ E \in (M MndHom G) \leftrightarrow ((M \in Mnd \land G \in Mnd) \land (E : {Base}_{M} ⟶ B \land \forall y \in {Base}_{M} \forall z \in {Base}_{M} E (y +_{M} z) = E (y) +_{G} E (z) \land E (\emptyset) = 0_{G}))$
74	8 4 71 73	syl21anbrc	$⊢ φ \to E \in (M MndHom G)$

Metamath Proof Explorer

Theorem frmdup1

Proof