elrgspnlem3

	Ref	Expression
Hypotheses	elrgspn.b	$⊢ B = {Base}_{R}$
	elrgspn.m	$⊢ M = {mulGrp}_{R}$
	elrgspn.x	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	elrgspn.n	$⊢ N = RingSpan (R)$
	elrgspn.f	$⊢ F = \{f \in (ℤ^{Word A}) \| {finSupp}_{0} (f)\}$
	elrgspn.r	$⊢ φ \to R \in Ring$
	elrgspn.a	$⊢ φ \to A \subseteq B$
	elrgspnlem1.1	$⊢ S = ran (g \in F ⟼ \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w)))$
Assertion	elrgspnlem3	$⊢ φ \to A \subseteq S$

Proof

Step	Hyp	Ref	Expression
1		elrgspn.b	$⊢ B = {Base}_{R}$
2		elrgspn.m	$⊢ M = {mulGrp}_{R}$
3		elrgspn.x	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4		elrgspn.n	$⊢ N = RingSpan (R)$
5		elrgspn.f	$⊢ F = \{f \in (ℤ^{Word A}) \| {finSupp}_{0} (f)\}$
6		elrgspn.r	$⊢ φ \to R \in Ring$
7		elrgspn.a	$⊢ φ \to A \subseteq B$
8		elrgspnlem1.1	$⊢ S = ran (g \in F ⟼ \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w)))$
9		eqid	$⊢ (g \in F ⟼ \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w))) = (g \in F ⟼ \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w)))$
10		fveq1	$⊢ g = (v \in Word A ⟼ if (v = ⟨“ x ”⟩, 1, 0)) \to g (w) = (v \in Word A ⟼ if (v = ⟨“ x ”⟩, 1, 0)) (w)$
11	10	oveq1d	$⊢ g = (v \in Word A ⟼ if (v = ⟨“ x ”⟩, 1, 0)) \to g (w) \underset{˙}{\cdot} (\sum_{M}, w) = (v \in Word A ⟼ if (v = ⟨“ x ”⟩, 1, 0)) (w) \underset{˙}{\cdot} (\sum_{M}, w)$
12	11	mpteq2dv	$⊢ g = (v \in Word A ⟼ if (v = ⟨“ x ”⟩, 1, 0)) \to (w \in Word A ⟼ g (w) \underset{˙}{\cdot} (\sum_{M}, w)) = (w \in Word A ⟼ (v \in Word A ⟼ if (v = ⟨“ x ”⟩, 1, 0)) (w) \underset{˙}{\cdot} (\sum_{M}, w))$
13	12	oveq2d	$⊢ g = (v \in Word A ⟼ if (v = ⟨“ x ”⟩, 1, 0)) \to \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w)) = \underset{w \in Word A}{\sum_{R}} ((v \in Word A ⟼ if (v = ⟨“ x ”⟩, 1, 0)) (w) \underset{˙}{\cdot} (\sum_{M}, w))$
14	13	eqeq2d	$⊢ g = (v \in Word A ⟼ if (v = ⟨“ x ”⟩, 1, 0)) \to (x = \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w)) \leftrightarrow x = \underset{w \in Word A}{\sum_{R}} ((v \in Word A ⟼ if (v = ⟨“ x ”⟩, 1, 0)) (w) \underset{˙}{\cdot} (\sum_{M}, w)))$
15		breq1	$⊢ f = (v \in Word A ⟼ if (v = ⟨“ x ”⟩, 1, 0)) \to ({finSupp}_{0} (f) \leftrightarrow {finSupp}_{0} ((v \in Word A ⟼ if (v = ⟨“ x ”⟩, 1, 0))))$
16		zex	$⊢ ℤ \in V$
17	16	a1i	$⊢ (φ \land x \in A) \to ℤ \in V$
18	1	fvexi	$⊢ B \in V$
19	18	a1i	$⊢ φ \to B \in V$
20	19 7	ssexd	$⊢ φ \to A \in V$
21		wrdexg	$⊢ A \in V \to Word A \in V$
22	20 21	syl	$⊢ φ \to Word A \in V$
23	22	adantr	$⊢ (φ \land x \in A) \to Word A \in V$
24		1zzd	$⊢ (((φ \land x \in A) \land v \in Word A) \land v = ⟨“ x ”⟩) \to 1 \in ℤ$
25		0zd	$⊢ (((φ \land x \in A) \land v \in Word A) \land \neg v = ⟨“ x ”⟩) \to 0 \in ℤ$
26	24 25	ifclda	$⊢ ((φ \land x \in A) \land v \in Word A) \to if (v = ⟨“ x ”⟩, 1, 0) \in ℤ$
27	26	fmpttd	$⊢ (φ \land x \in A) \to (v \in Word A ⟼ if (v = ⟨“ x ”⟩, 1, 0)) : Word A ⟶ ℤ$
28	17 23 27	elmapdd	$⊢ (φ \land x \in A) \to (v \in Word A ⟼ if (v = ⟨“ x ”⟩, 1, 0)) \in (ℤ^{Word A})$
29	28	elexd	$⊢ (φ \land x \in A) \to (v \in Word A ⟼ if (v = ⟨“ x ”⟩, 1, 0)) \in V$
30	27	ffund	$⊢ (φ \land x \in A) \to Fun (v \in Word A ⟼ if (v = ⟨“ x ”⟩, 1, 0))$
31		0zd	$⊢ (φ \land x \in A) \to 0 \in ℤ$
32		snfi	$⊢ \{⟨“ x ”⟩\} \in Fin$
33	32	a1i	$⊢ (φ \land x \in A) \to \{⟨“ x ”⟩\} \in Fin$
34		eldifsni	$⊢ v \in (Word A ∖ \{⟨“ x ”⟩\}) \to v \neq ⟨“ x ”⟩$
35	34	adantl	$⊢ ((φ \land x \in A) \land v \in (Word A ∖ \{⟨“ x ”⟩\})) \to v \neq ⟨“ x ”⟩$
36	35	neneqd	$⊢ ((φ \land x \in A) \land v \in (Word A ∖ \{⟨“ x ”⟩\})) \to \neg v = ⟨“ x ”⟩$
37	36	iffalsed	$⊢ ((φ \land x \in A) \land v \in (Word A ∖ \{⟨“ x ”⟩\})) \to if (v = ⟨“ x ”⟩, 1, 0) = 0$
38	37 23	suppss2	$⊢ (φ \land x \in A) \to (v \in Word A ⟼ if (v = ⟨“ x ”⟩, 1, 0)) supp 0 \subseteq \{⟨“ x ”⟩\}$
39		suppssfifsupp	$⊢ (((v \in Word A ⟼ if (v = ⟨“ x ”⟩, 1, 0)) \in V \land Fun (v \in Word A ⟼ if (v = ⟨“ x ”⟩, 1, 0)) \land 0 \in ℤ) \land (\{⟨“ x ”⟩\} \in Fin \land (v \in Word A ⟼ if (v = ⟨“ x ”⟩, 1, 0)) supp 0 \subseteq \{⟨“ x ”⟩\})) \to {finSupp}_{0} ((v \in Word A ⟼ if (v = ⟨“ x ”⟩, 1, 0)))$
40	29 30 31 33 38 39	syl32anc	$⊢ (φ \land x \in A) \to {finSupp}_{0} ((v \in Word A ⟼ if (v = ⟨“ x ”⟩, 1, 0)))$
41	15 28 40	elrabd	$⊢ (φ \land x \in A) \to (v \in Word A ⟼ if (v = ⟨“ x ”⟩, 1, 0)) \in \{f \in (ℤ^{Word A}) \| {finSupp}_{0} (f)\}$
42	41 5	eleqtrrdi	$⊢ (φ \land x \in A) \to (v \in Word A ⟼ if (v = ⟨“ x ”⟩, 1, 0)) \in F$
43		eqeq2	$⊢ x = if (w = ⟨“ x ”⟩, x, 0_{R}) \to ((v \in Word A ⟼ if (v = ⟨“ x ”⟩, 1, 0)) (w) \underset{˙}{\cdot} (\sum_{M}, w) = x \leftrightarrow (v \in Word A ⟼ if (v = ⟨“ x ”⟩, 1, 0)) (w) \underset{˙}{\cdot} (\sum_{M}, w) = if (w = ⟨“ x ”⟩, x, 0_{R}))$
44		eqeq2	$⊢ 0_{R} = if (w = ⟨“ x ”⟩, x, 0_{R}) \to ((v \in Word A ⟼ if (v = ⟨“ x ”⟩, 1, 0)) (w) \underset{˙}{\cdot} (\sum_{M}, w) = 0_{R} \leftrightarrow (v \in Word A ⟼ if (v = ⟨“ x ”⟩, 1, 0)) (w) \underset{˙}{\cdot} (\sum_{M}, w) = if (w = ⟨“ x ”⟩, x, 0_{R}))$
45		eqid	$⊢ (v \in Word A ⟼ if (v = ⟨“ x ”⟩, 1, 0)) = (v \in Word A ⟼ if (v = ⟨“ x ”⟩, 1, 0))$
46		simpr	$⊢ ((((φ \land x \in A) \land w \in Word A) \land w = ⟨“ x ”⟩) \land v = w) \to v = w$
47		simplr	$⊢ ((((φ \land x \in A) \land w \in Word A) \land w = ⟨“ x ”⟩) \land v = w) \to w = ⟨“ x ”⟩$
48	46 47	eqtrd	$⊢ ((((φ \land x \in A) \land w \in Word A) \land w = ⟨“ x ”⟩) \land v = w) \to v = ⟨“ x ”⟩$
49	48	iftrued	$⊢ ((((φ \land x \in A) \land w \in Word A) \land w = ⟨“ x ”⟩) \land v = w) \to if (v = ⟨“ x ”⟩, 1, 0) = 1$
50		simplr	$⊢ (((φ \land x \in A) \land w \in Word A) \land w = ⟨“ x ”⟩) \to w \in Word A$
51		1zzd	$⊢ (((φ \land x \in A) \land w \in Word A) \land w = ⟨“ x ”⟩) \to 1 \in ℤ$
52	45 49 50 51	fvmptd2	$⊢ (((φ \land x \in A) \land w \in Word A) \land w = ⟨“ x ”⟩) \to (v \in Word A ⟼ if (v = ⟨“ x ”⟩, 1, 0)) (w) = 1$
53		simpr	$⊢ (((φ \land x \in A) \land w \in Word A) \land w = ⟨“ x ”⟩) \to w = ⟨“ x ”⟩$
54	53	oveq2d	$⊢ (((φ \land x \in A) \land w \in Word A) \land w = ⟨“ x ”⟩) \to \sum_{M} w = \sum_{M} ⟨“ x ”⟩$
55	7	sselda	$⊢ (φ \land x \in A) \to x \in B$
56	55	ad2antrr	$⊢ (((φ \land x \in A) \land w \in Word A) \land w = ⟨“ x ”⟩) \to x \in B$
57	2 1	mgpbas	$⊢ B = {Base}_{M}$
58	57	gsumws1	$⊢ x \in B \to \sum_{M} ⟨“ x ”⟩ = x$
59	56 58	syl	$⊢ (((φ \land x \in A) \land w \in Word A) \land w = ⟨“ x ”⟩) \to \sum_{M} ⟨“ x ”⟩ = x$
60	54 59	eqtrd	$⊢ (((φ \land x \in A) \land w \in Word A) \land w = ⟨“ x ”⟩) \to \sum_{M} w = x$
61	52 60	oveq12d	$⊢ (((φ \land x \in A) \land w \in Word A) \land w = ⟨“ x ”⟩) \to (v \in Word A ⟼ if (v = ⟨“ x ”⟩, 1, 0)) (w) \underset{˙}{\cdot} (\sum_{M}, w) = 1 \underset{˙}{\cdot} x$
62	1 3	mulg1	$⊢ x \in B \to 1 \underset{˙}{\cdot} x = x$
63	56 62	syl	$⊢ (((φ \land x \in A) \land w \in Word A) \land w = ⟨“ x ”⟩) \to 1 \underset{˙}{\cdot} x = x$
64	61 63	eqtrd	$⊢ (((φ \land x \in A) \land w \in Word A) \land w = ⟨“ x ”⟩) \to (v \in Word A ⟼ if (v = ⟨“ x ”⟩, 1, 0)) (w) \underset{˙}{\cdot} (\sum_{M}, w) = x$
65		eqeq1	$⊢ v = w \to (v = ⟨“ x ”⟩ \leftrightarrow w = ⟨“ x ”⟩)$
66	65	notbid	$⊢ v = w \to (\neg v = ⟨“ x ”⟩ \leftrightarrow \neg w = ⟨“ x ”⟩)$
67	66	biimparc	$⊢ (\neg w = ⟨“ x ”⟩ \land v = w) \to \neg v = ⟨“ x ”⟩$
68	67	adantll	$⊢ ((((φ \land x \in A) \land w \in Word A) \land \neg w = ⟨“ x ”⟩) \land v = w) \to \neg v = ⟨“ x ”⟩$
69	68	iffalsed	$⊢ ((((φ \land x \in A) \land w \in Word A) \land \neg w = ⟨“ x ”⟩) \land v = w) \to if (v = ⟨“ x ”⟩, 1, 0) = 0$
70		simplr	$⊢ (((φ \land x \in A) \land w \in Word A) \land \neg w = ⟨“ x ”⟩) \to w \in Word A$
71		0zd	$⊢ (((φ \land x \in A) \land w \in Word A) \land \neg w = ⟨“ x ”⟩) \to 0 \in ℤ$
72	45 69 70 71	fvmptd2	$⊢ (((φ \land x \in A) \land w \in Word A) \land \neg w = ⟨“ x ”⟩) \to (v \in Word A ⟼ if (v = ⟨“ x ”⟩, 1, 0)) (w) = 0$
73	72	oveq1d	$⊢ (((φ \land x \in A) \land w \in Word A) \land \neg w = ⟨“ x ”⟩) \to (v \in Word A ⟼ if (v = ⟨“ x ”⟩, 1, 0)) (w) \underset{˙}{\cdot} (\sum_{M}, w) = 0 \underset{˙}{\cdot} (\sum_{M}, w)$
74	2	ringmgp	$⊢ R \in Ring \to M \in Mnd$
75	6 74	syl	$⊢ φ \to M \in Mnd$
76	75	ad3antrrr	$⊢ (((φ \land x \in A) \land w \in Word A) \land \neg w = ⟨“ x ”⟩) \to M \in Mnd$
77		sswrd	$⊢ A \subseteq B \to Word A \subseteq Word B$
78	7 77	syl	$⊢ φ \to Word A \subseteq Word B$
79	78	adantr	$⊢ (φ \land x \in A) \to Word A \subseteq Word B$
80	79	sselda	$⊢ ((φ \land x \in A) \land w \in Word A) \to w \in Word B$
81	80	adantr	$⊢ (((φ \land x \in A) \land w \in Word A) \land \neg w = ⟨“ x ”⟩) \to w \in Word B$
82	57	gsumwcl	$⊢ (M \in Mnd \land w \in Word B) \to \sum_{M} w \in B$
83	76 81 82	syl2anc	$⊢ (((φ \land x \in A) \land w \in Word A) \land \neg w = ⟨“ x ”⟩) \to \sum_{M} w \in B$
84		eqid	$⊢ 0_{R} = 0_{R}$
85	1 84 3	mulg0	$⊢ \sum_{M} w \in B \to 0 \underset{˙}{\cdot} (\sum_{M}, w) = 0_{R}$
86	83 85	syl	$⊢ (((φ \land x \in A) \land w \in Word A) \land \neg w = ⟨“ x ”⟩) \to 0 \underset{˙}{\cdot} (\sum_{M}, w) = 0_{R}$
87	73 86	eqtrd	$⊢ (((φ \land x \in A) \land w \in Word A) \land \neg w = ⟨“ x ”⟩) \to (v \in Word A ⟼ if (v = ⟨“ x ”⟩, 1, 0)) (w) \underset{˙}{\cdot} (\sum_{M}, w) = 0_{R}$
88	43 44 64 87	ifbothda	$⊢ ((φ \land x \in A) \land w \in Word A) \to (v \in Word A ⟼ if (v = ⟨“ x ”⟩, 1, 0)) (w) \underset{˙}{\cdot} (\sum_{M}, w) = if (w = ⟨“ x ”⟩, x, 0_{R})$
89	88	mpteq2dva	$⊢ (φ \land x \in A) \to (w \in Word A ⟼ (v \in Word A ⟼ if (v = ⟨“ x ”⟩, 1, 0)) (w) \underset{˙}{\cdot} (\sum_{M}, w)) = (w \in Word A ⟼ if (w = ⟨“ x ”⟩, x, 0_{R}))$
90	89	oveq2d	$⊢ (φ \land x \in A) \to \underset{w \in Word A}{\sum_{R}} ((v \in Word A ⟼ if (v = ⟨“ x ”⟩, 1, 0)) (w) \underset{˙}{\cdot} (\sum_{M}, w)) = \underset{w \in Word A}{\sum_{R}} if (w = ⟨“ x ”⟩, x, 0_{R})$
91		ringmnd	$⊢ R \in Ring \to R \in Mnd$
92	6 91	syl	$⊢ φ \to R \in Mnd$
93	92	adantr	$⊢ (φ \land x \in A) \to R \in Mnd$
94		simpr	$⊢ (φ \land x \in A) \to x \in A$
95	94	s1cld	$⊢ (φ \land x \in A) \to ⟨“ x ”⟩ \in Word A$
96		eqid	$⊢ (w \in Word A ⟼ if (w = ⟨“ x ”⟩, x, 0_{R})) = (w \in Word A ⟼ if (w = ⟨“ x ”⟩, x, 0_{R}))$
97	7 1	sseqtrdi	$⊢ φ \to A \subseteq {Base}_{R}$
98	97	sselda	$⊢ (φ \land x \in A) \to x \in {Base}_{R}$
99	84 93 23 95 96 98	gsummptif1n0	$⊢ (φ \land x \in A) \to \underset{w \in Word A}{\sum_{R}} if (w = ⟨“ x ”⟩, x, 0_{R}) = x$
100	90 99	eqtr2d	$⊢ (φ \land x \in A) \to x = \underset{w \in Word A}{\sum_{R}} ((v \in Word A ⟼ if (v = ⟨“ x ”⟩, 1, 0)) (w) \underset{˙}{\cdot} (\sum_{M}, w))$
101	14 42 100	rspcedvdw	$⊢ (φ \land x \in A) \to \exists g \in F x = \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w))$
102	9 101 94	elrnmptd	$⊢ (φ \land x \in A) \to x \in ran (g \in F ⟼ \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w)))$
103	102 8	eleqtrrdi	$⊢ (φ \land x \in A) \to x \in S$
104	103	ex	$⊢ φ \to (x \in A \to x \in S)$
105	104	ssrdv	$⊢ φ \to A \subseteq S$

Metamath Proof Explorer

Theorem elrgspnlem3

Proof