frmdgsum

Description: Any word in a free monoid can be expressed as the sum of the singletons composing it. (Contributed by Mario Carneiro, 27-Sep-2015)

	Ref	Expression
Hypotheses	frmdmnd.m	$⊢ M = freeMnd (I)$
	frmdgsum.u	$⊢ U = {var}_{FMnd} (I)$
Assertion	frmdgsum	$⊢ (I \in V \land W \in Word I) \to \sum_{M} (U \circ W) = W$

Proof

Step	Hyp	Ref	Expression
1		frmdmnd.m	$⊢ M = freeMnd (I)$
2		frmdgsum.u	$⊢ U = {var}_{FMnd} (I)$
3		coeq2	$⊢ x = \emptyset \to U \circ x = U \circ \emptyset$
4		co02	$⊢ U \circ \emptyset = \emptyset$
5	3 4	syl6eq	$⊢ x = \emptyset \to U \circ x = \emptyset$
6	5	oveq2d	$⊢ x = \emptyset \to \sum_{M} (U \circ x) = \sum_{M} \emptyset$
7		id	$⊢ x = \emptyset \to x = \emptyset$
8	6 7	eqeq12d	$⊢ x = \emptyset \to (\sum_{M} (U \circ x) = x \leftrightarrow \sum_{M} \emptyset = \emptyset)$
9	8	imbi2d	$⊢ x = \emptyset \to ((I \in V \to \sum_{M} (U \circ x) = x) \leftrightarrow (I \in V \to \sum_{M} \emptyset = \emptyset))$
10		coeq2	$⊢ x = y \to U \circ x = U \circ y$
11	10	oveq2d	$⊢ x = y \to \sum_{M} (U \circ x) = \sum_{M} (U \circ y)$
12		id	$⊢ x = y \to x = y$
13	11 12	eqeq12d	$⊢ x = y \to (\sum_{M} (U \circ x) = x \leftrightarrow \sum_{M} (U \circ y) = y)$
14	13	imbi2d	$⊢ x = y \to ((I \in V \to \sum_{M} (U \circ x) = x) \leftrightarrow (I \in V \to \sum_{M} (U \circ y) = y))$
15		coeq2	$⊢ x = y ++ ⟨“ z ”⟩ \to U \circ x = U \circ (y ++ ⟨“ z ”⟩)$
16	15	oveq2d	$⊢ x = y ++ ⟨“ z ”⟩ \to \sum_{M} (U \circ x) = \sum_{M} (U \circ (y ++ ⟨“ z ”⟩))$
17		id	$⊢ x = y ++ ⟨“ z ”⟩ \to x = y ++ ⟨“ z ”⟩$
18	16 17	eqeq12d	$⊢ x = y ++ ⟨“ z ”⟩ \to (\sum_{M} (U \circ x) = x \leftrightarrow \sum_{M} (U \circ (y ++ ⟨“ z ”⟩)) = y ++ ⟨“ z ”⟩)$
19	18	imbi2d	$⊢ x = y ++ ⟨“ z ”⟩ \to ((I \in V \to \sum_{M} (U \circ x) = x) \leftrightarrow (I \in V \to \sum_{M} (U \circ (y ++ ⟨“ z ”⟩)) = y ++ ⟨“ z ”⟩))$
20		coeq2	$⊢ x = W \to U \circ x = U \circ W$
21	20	oveq2d	$⊢ x = W \to \sum_{M} (U \circ x) = \sum_{M} (U \circ W)$
22		id	$⊢ x = W \to x = W$
23	21 22	eqeq12d	$⊢ x = W \to (\sum_{M} (U \circ x) = x \leftrightarrow \sum_{M} (U \circ W) = W)$
24	23	imbi2d	$⊢ x = W \to ((I \in V \to \sum_{M} (U \circ x) = x) \leftrightarrow (I \in V \to \sum_{M} (U \circ W) = W))$
25	1	frmd0	$⊢ \emptyset = 0_{M}$
26	25	gsum0	$⊢ \sum_{M} \emptyset = \emptyset$
27	26	a1i	$⊢ I \in V \to \sum_{M} \emptyset = \emptyset$
28		oveq1	$⊢ \sum_{M} (U \circ y) = y \to (\sum_{M}, (U \circ y)) ++ ⟨“ z ”⟩ = y ++ ⟨“ z ”⟩$
29		simprl	$⊢ (I \in V \land (y \in Word I \land z \in I)) \to y \in Word I$
30		simprr	$⊢ (I \in V \land (y \in Word I \land z \in I)) \to z \in I$
31	30	s1cld	$⊢ (I \in V \land (y \in Word I \land z \in I)) \to ⟨“ z ”⟩ \in Word I$
32	2	vrmdf	$⊢ I \in V \to U : I ⟶ Word I$
33	32	adantr	$⊢ (I \in V \land (y \in Word I \land z \in I)) \to U : I ⟶ Word I$
34		ccatco	$⊢ (y \in Word I \land ⟨“ z ”⟩ \in Word I \land U : I ⟶ Word I) \to U \circ (y ++ ⟨“ z ”⟩) = (U \circ y) ++ (U \circ ⟨“ z ”⟩)$
35	29 31 33 34	syl3anc	$⊢ (I \in V \land (y \in Word I \land z \in I)) \to U \circ (y ++ ⟨“ z ”⟩) = (U \circ y) ++ (U \circ ⟨“ z ”⟩)$
36		s1co	$⊢ (z \in I \land U : I ⟶ Word I) \to U \circ ⟨“ z ”⟩ = ⟨“ U (z) ”⟩$
37	30 33 36	syl2anc	$⊢ (I \in V \land (y \in Word I \land z \in I)) \to U \circ ⟨“ z ”⟩ = ⟨“ U (z) ”⟩$
38	2	vrmdval	$⊢ (I \in V \land z \in I) \to U (z) = ⟨“ z ”⟩$
39	38	adantrl	$⊢ (I \in V \land (y \in Word I \land z \in I)) \to U (z) = ⟨“ z ”⟩$
40	39	s1eqd	$⊢ (I \in V \land (y \in Word I \land z \in I)) \to ⟨“ U (z) ”⟩ = ⟨“ ⟨“ z ”⟩ ”⟩$
41	37 40	eqtrd	$⊢ (I \in V \land (y \in Word I \land z \in I)) \to U \circ ⟨“ z ”⟩ = ⟨“ ⟨“ z ”⟩ ”⟩$
42	41	oveq2d	$⊢ (I \in V \land (y \in Word I \land z \in I)) \to (U \circ y) ++ (U \circ ⟨“ z ”⟩) = (U \circ y) ++ ⟨“ ⟨“ z ”⟩ ”⟩$
43	35 42	eqtrd	$⊢ (I \in V \land (y \in Word I \land z \in I)) \to U \circ (y ++ ⟨“ z ”⟩) = (U \circ y) ++ ⟨“ ⟨“ z ”⟩ ”⟩$
44	43	oveq2d	$⊢ (I \in V \land (y \in Word I \land z \in I)) \to \sum_{M} (U \circ (y ++ ⟨“ z ”⟩)) = \sum_{M} ((U \circ y) ++ ⟨“ ⟨“ z ”⟩ ”⟩)$
45	1	frmdmnd	$⊢ I \in V \to M \in Mnd$
46	45	adantr	$⊢ (I \in V \land (y \in Word I \land z \in I)) \to M \in Mnd$
47		wrdco	$⊢ (y \in Word I \land U : I ⟶ Word I) \to U \circ y \in Word Word I$
48	29 33 47	syl2anc	$⊢ (I \in V \land (y \in Word I \land z \in I)) \to U \circ y \in Word Word I$
49		eqid	$⊢ {Base}_{M} = {Base}_{M}$
50	1 49	frmdbas	$⊢ I \in V \to {Base}_{M} = Word I$
51	50	adantr	$⊢ (I \in V \land (y \in Word I \land z \in I)) \to {Base}_{M} = Word I$
52		wrdeq	$⊢ {Base}_{M} = Word I \to Word {Base}_{M} = Word Word I$
53	51 52	syl	$⊢ (I \in V \land (y \in Word I \land z \in I)) \to Word {Base}_{M} = Word Word I$
54	48 53	eleqtrrd	$⊢ (I \in V \land (y \in Word I \land z \in I)) \to U \circ y \in Word {Base}_{M}$
55	31 51	eleqtrrd	$⊢ (I \in V \land (y \in Word I \land z \in I)) \to ⟨“ z ”⟩ \in {Base}_{M}$
56	55	s1cld	$⊢ (I \in V \land (y \in Word I \land z \in I)) \to ⟨“ ⟨“ z ”⟩ ”⟩ \in Word {Base}_{M}$
57		eqid	$⊢ +_{M} = +_{M}$
58	49 57	gsumccat	$⊢ (M \in Mnd \land U \circ y \in Word {Base}_{M} \land ⟨“ ⟨“ z ”⟩ ”⟩ \in Word {Base}_{M}) \to \sum_{M} ((U \circ y) ++ ⟨“ ⟨“ z ”⟩ ”⟩) = (\sum_{M}, (U \circ y)) +_{M} (\sum_{M}, ⟨“ ⟨“ z ”⟩ ”⟩)$
59	46 54 56 58	syl3anc	$⊢ (I \in V \land (y \in Word I \land z \in I)) \to \sum_{M} ((U \circ y) ++ ⟨“ ⟨“ z ”⟩ ”⟩) = (\sum_{M}, (U \circ y)) +_{M} (\sum_{M}, ⟨“ ⟨“ z ”⟩ ”⟩)$
60	49	gsumws1	$⊢ ⟨“ z ”⟩ \in {Base}_{M} \to \sum_{M} ⟨“ ⟨“ z ”⟩ ”⟩ = ⟨“ z ”⟩$
61	55 60	syl	$⊢ (I \in V \land (y \in Word I \land z \in I)) \to \sum_{M} ⟨“ ⟨“ z ”⟩ ”⟩ = ⟨“ z ”⟩$
62	61	oveq2d	$⊢ (I \in V \land (y \in Word I \land z \in I)) \to (\sum_{M}, (U \circ y)) +_{M} (\sum_{M}, ⟨“ ⟨“ z ”⟩ ”⟩) = (\sum_{M}, (U \circ y)) +_{M} ⟨“ z ”⟩$
63	49	gsumwcl	$⊢ (M \in Mnd \land U \circ y \in Word {Base}_{M}) \to \sum_{M} (U \circ y) \in {Base}_{M}$
64	46 54 63	syl2anc	$⊢ (I \in V \land (y \in Word I \land z \in I)) \to \sum_{M} (U \circ y) \in {Base}_{M}$
65	1 49 57	frmdadd	$⊢ (\sum_{M} (U \circ y) \in {Base}_{M} \land ⟨“ z ”⟩ \in {Base}_{M}) \to (\sum_{M}, (U \circ y)) +_{M} ⟨“ z ”⟩ = (\sum_{M}, (U \circ y)) ++ ⟨“ z ”⟩$
66	64 55 65	syl2anc	$⊢ (I \in V \land (y \in Word I \land z \in I)) \to (\sum_{M}, (U \circ y)) +_{M} ⟨“ z ”⟩ = (\sum_{M}, (U \circ y)) ++ ⟨“ z ”⟩$
67	62 66	eqtrd	$⊢ (I \in V \land (y \in Word I \land z \in I)) \to (\sum_{M}, (U \circ y)) +_{M} (\sum_{M}, ⟨“ ⟨“ z ”⟩ ”⟩) = (\sum_{M}, (U \circ y)) ++ ⟨“ z ”⟩$
68	59 67	eqtrd	$⊢ (I \in V \land (y \in Word I \land z \in I)) \to \sum_{M} ((U \circ y) ++ ⟨“ ⟨“ z ”⟩ ”⟩) = (\sum_{M}, (U \circ y)) ++ ⟨“ z ”⟩$
69	44 68	eqtrd	$⊢ (I \in V \land (y \in Word I \land z \in I)) \to \sum_{M} (U \circ (y ++ ⟨“ z ”⟩)) = (\sum_{M}, (U \circ y)) ++ ⟨“ z ”⟩$
70	69	eqeq1d	$⊢ (I \in V \land (y \in Word I \land z \in I)) \to (\sum_{M} (U \circ (y ++ ⟨“ z ”⟩)) = y ++ ⟨“ z ”⟩ \leftrightarrow (\sum_{M}, (U \circ y)) ++ ⟨“ z ”⟩ = y ++ ⟨“ z ”⟩)$
71	28 70	syl5ibr	$⊢ (I \in V \land (y \in Word I \land z \in I)) \to (\sum_{M} (U \circ y) = y \to \sum_{M} (U \circ (y ++ ⟨“ z ”⟩)) = y ++ ⟨“ z ”⟩)$
72	71	expcom	$⊢ (y \in Word I \land z \in I) \to (I \in V \to (\sum_{M} (U \circ y) = y \to \sum_{M} (U \circ (y ++ ⟨“ z ”⟩)) = y ++ ⟨“ z ”⟩))$
73	72	a2d	$⊢ (y \in Word I \land z \in I) \to ((I \in V \to \sum_{M} (U \circ y) = y) \to (I \in V \to \sum_{M} (U \circ (y ++ ⟨“ z ”⟩)) = y ++ ⟨“ z ”⟩))$
74	9 14 19 24 27 73	wrdind	$⊢ W \in Word I \to (I \in V \to \sum_{M} (U \circ W) = W)$
75	74	impcom	$⊢ (I \in V \land W \in Word I) \to \sum_{M} (U \circ W) = W$

Metamath Proof Explorer

Theorem frmdgsum

Proof