frmdup3

Description: Universal property of the free monoid by existential uniqueness. (Contributed by Mario Carneiro, 2-Oct-2015) (Revised by Mario Carneiro, 18-Jul-2016)

	Ref	Expression
Hypotheses	frmdup3.m	$⊢ M = freeMnd (I)$
	frmdup3.b	$⊢ B = {Base}_{G}$
	frmdup3.u	$⊢ U = {var}_{FMnd} (I)$
Assertion	frmdup3	$⊢ (G \in Mnd \land I \in V \land A : I ⟶ B) \to \exists! m \in (M MndHom G) m \circ U = A$

Proof

Step	Hyp	Ref	Expression
1		frmdup3.m	$⊢ M = freeMnd (I)$
2		frmdup3.b	$⊢ B = {Base}_{G}$
3		frmdup3.u	$⊢ U = {var}_{FMnd} (I)$
4		eqid	$⊢ (x \in Word I ⟼ \sum_{G} (A \circ x)) = (x \in Word I ⟼ \sum_{G} (A \circ x))$
5		simp1	$⊢ (G \in Mnd \land I \in V \land A : I ⟶ B) \to G \in Mnd$
6		simp2	$⊢ (G \in Mnd \land I \in V \land A : I ⟶ B) \to I \in V$
7		simp3	$⊢ (G \in Mnd \land I \in V \land A : I ⟶ B) \to A : I ⟶ B$
8	1 2 4 5 6 7	frmdup1	$⊢ (G \in Mnd \land I \in V \land A : I ⟶ B) \to (x \in Word I ⟼ \sum_{G} (A \circ x)) \in (M MndHom G)$
9	5	adantr	$⊢ ((G \in Mnd \land I \in V \land A : I ⟶ B) \land y \in I) \to G \in Mnd$
10	6	adantr	$⊢ ((G \in Mnd \land I \in V \land A : I ⟶ B) \land y \in I) \to I \in V$
11	7	adantr	$⊢ ((G \in Mnd \land I \in V \land A : I ⟶ B) \land y \in I) \to A : I ⟶ B$
12		simpr	$⊢ ((G \in Mnd \land I \in V \land A : I ⟶ B) \land y \in I) \to y \in I$
13	1 2 4 9 10 11 3 12	frmdup2	$⊢ ((G \in Mnd \land I \in V \land A : I ⟶ B) \land y \in I) \to (x \in Word I ⟼ \sum_{G} (A \circ x)) (U (y)) = A (y)$
14	13	mpteq2dva	$⊢ (G \in Mnd \land I \in V \land A : I ⟶ B) \to (y \in I ⟼ (x \in Word I ⟼ \sum_{G} (A \circ x)) (U (y))) = (y \in I ⟼ A (y))$
15		eqid	$⊢ {Base}_{M} = {Base}_{M}$
16	15 2	mhmf	$⊢ (x \in Word I ⟼ \sum_{G} (A \circ x)) \in (M MndHom G) \to (x \in Word I ⟼ \sum_{G} (A \circ x)) : {Base}_{M} ⟶ B$
17	8 16	syl	$⊢ (G \in Mnd \land I \in V \land A : I ⟶ B) \to (x \in Word I ⟼ \sum_{G} (A \circ x)) : {Base}_{M} ⟶ B$
18	3	vrmdf	$⊢ I \in V \to U : I ⟶ Word I$
19	18	3ad2ant2	$⊢ (G \in Mnd \land I \in V \land A : I ⟶ B) \to U : I ⟶ Word I$
20	1 15	frmdbas	$⊢ I \in V \to {Base}_{M} = Word I$
21	20	3ad2ant2	$⊢ (G \in Mnd \land I \in V \land A : I ⟶ B) \to {Base}_{M} = Word I$
22	21	feq3d	$⊢ (G \in Mnd \land I \in V \land A : I ⟶ B) \to (U : I ⟶ {Base}_{M} \leftrightarrow U : I ⟶ Word I)$
23	19 22	mpbird	$⊢ (G \in Mnd \land I \in V \land A : I ⟶ B) \to U : I ⟶ {Base}_{M}$
24		fcompt	$⊢ ((x \in Word I ⟼ \sum_{G} (A \circ x)) : {Base}_{M} ⟶ B \land U : I ⟶ {Base}_{M}) \to (x \in Word I ⟼ \sum_{G} (A \circ x)) \circ U = (y \in I ⟼ (x \in Word I ⟼ \sum_{G} (A \circ x)) (U (y)))$
25	17 23 24	syl2anc	$⊢ (G \in Mnd \land I \in V \land A : I ⟶ B) \to (x \in Word I ⟼ \sum_{G} (A \circ x)) \circ U = (y \in I ⟼ (x \in Word I ⟼ \sum_{G} (A \circ x)) (U (y)))$
26	7	feqmptd	$⊢ (G \in Mnd \land I \in V \land A : I ⟶ B) \to A = (y \in I ⟼ A (y))$
27	14 25 26	3eqtr4d	$⊢ (G \in Mnd \land I \in V \land A : I ⟶ B) \to (x \in Word I ⟼ \sum_{G} (A \circ x)) \circ U = A$
28	1 2 3	frmdup3lem	$⊢ ((G \in Mnd \land I \in V \land A : I ⟶ B) \land (m \in (M MndHom G) \land m \circ U = A)) \to m = (x \in Word I ⟼ \sum_{G} (A \circ x))$
29	28	expr	$⊢ ((G \in Mnd \land I \in V \land A : I ⟶ B) \land m \in (M MndHom G)) \to (m \circ U = A \to m = (x \in Word I ⟼ \sum_{G} (A \circ x)))$
30	29	ralrimiva	$⊢ (G \in Mnd \land I \in V \land A : I ⟶ B) \to \forall m \in (M MndHom G) (m \circ U = A \to m = (x \in Word I ⟼ \sum_{G} (A \circ x)))$
31		coeq1	$⊢ m = (x \in Word I ⟼ \sum_{G} (A \circ x)) \to m \circ U = (x \in Word I ⟼ \sum_{G} (A \circ x)) \circ U$
32	31	eqeq1d	$⊢ m = (x \in Word I ⟼ \sum_{G} (A \circ x)) \to (m \circ U = A \leftrightarrow (x \in Word I ⟼ \sum_{G} (A \circ x)) \circ U = A)$
33	32	eqreu	$⊢ ((x \in Word I ⟼ \sum_{G} (A \circ x)) \in (M MndHom G) \land (x \in Word I ⟼ \sum_{G} (A \circ x)) \circ U = A \land \forall m \in (M MndHom G) (m \circ U = A \to m = (x \in Word I ⟼ \sum_{G} (A \circ x)))) \to \exists! m \in (M MndHom G) m \circ U = A$
34	8 27 30 33	syl3anc	$⊢ (G \in Mnd \land I \in V \land A : I ⟶ B) \to \exists! m \in (M MndHom G) m \circ U = A$

Metamath Proof Explorer

Theorem frmdup3

Proof