Theorem gsumvsca2

Description: Scalar product of a finite group sum for a left module over a semiring. (Contributed by Thierry Arnoux, 16-Mar-2018) (Proof shortened by AV, 12-Dec-2019)

	Ref	Expression
Hypotheses	gsumvsca.b	$$⊢B={\mathrm{Base}}_W$$
	gsumvsca.g	$$⊢G=\mathrm{Scalar}\left(W\right)$$
	gsumvsca.z	$$⊢\underset{\dot{}}{0}=0_W$$
	gsumvsca.t	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
	gsumvsca.p	$$⊢\underset{\dot{}}{+}={+}_W$$
	gsumvsca.k	$$⊢\phi \to K\subseteq {\mathrm{Base}}_G$$
	gsumvsca.a	$$⊢\phi \to A\in \mathrm{Fin}$$
	gsumvsca.w	$$⊢\phi \to W\in \mathrm{SLMod}$$
	gsumvsca2.n	$$⊢\phi \to Q\in B$$
	gsumvsca2.c	$$⊢\left(\phi \wedge k\in A\right)\to P\in K$$
Assertion	gsumvsca2	$$⊢\phi \to \underset{k\in A}{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=\left(\underset{k\in A}{{\sum }_G},P\right)\underset{\dot{}}{·}Q$$

Proof

Step	Hyp	Ref	Expression
1		gsumvsca.b	$$⊢B={\mathrm{Base}}_W$$
2		gsumvsca.g	$$⊢G=\mathrm{Scalar}\left(W\right)$$
3		gsumvsca.z	$$⊢\underset{\dot{}}{0}=0_W$$
4		gsumvsca.t	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
5		gsumvsca.p	$$⊢\underset{\dot{}}{+}={+}_W$$
6		gsumvsca.k	$$⊢\phi \to K\subseteq {\mathrm{Base}}_G$$
7		gsumvsca.a	$$⊢\phi \to A\in \mathrm{Fin}$$
8		gsumvsca.w	$$⊢\phi \to W\in \mathrm{SLMod}$$
9		gsumvsca2.n	$$⊢\phi \to Q\in B$$
10		gsumvsca2.c	$$⊢\left(\phi \wedge k\in A\right)\to P\in K$$
11		ssid	$$⊢A\subseteq A$$
12		sseq1	$$⊢a=\varnothing \to \left(a\subseteq A\leftrightarrow \varnothing \subseteq A\right)$$
13	12	anbi2d	$$⊢a=\varnothing \to \left(\left(\phi \wedge a\subseteq A\right)\leftrightarrow \left(\phi \wedge \varnothing \subseteq A\right)\right)$$
14		mpteq1	$$⊢a=\varnothing \to \left(k\in a⟼P\underset{\dot{}}{·}Q\right)=\left(k\in \varnothing ⟼P\underset{\dot{}}{·}Q\right)$$
15	14	oveq2d	$$⊢a=\varnothing \to \underset{k\in a}{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=\underset{k\in \varnothing }{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)$$
16		mpteq1	$$⊢a=\varnothing \to \left(k\in a⟼P\right)=\left(k\in \varnothing ⟼P\right)$$
17	16	oveq2d	$$⊢a=\varnothing \to \underset{k\in a}{{\sum }_G}P=\underset{k\in \varnothing }{{\sum }_G}P$$
18	17	oveq1d	$$⊢a=\varnothing \to \left(\underset{k\in a}{{\sum }_G},P\right)\underset{\dot{}}{·}Q=\left(\underset{k\in \varnothing }{{\sum }_G},P\right)\underset{\dot{}}{·}Q$$
19	15 18	eqeq12d	$$⊢a=\varnothing \to \left(\underset{k\in a}{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=\left(\underset{k\in a}{{\sum }_G},P\right)\underset{\dot{}}{·}Q\leftrightarrow \underset{k\in \varnothing }{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=\left(\underset{k\in \varnothing }{{\sum }_G},P\right)\underset{\dot{}}{·}Q\right)$$
20	13 19	imbi12d	$$⊢a=\varnothing \to \left(\left(\left(\phi \wedge a\subseteq A\right)\to \underset{k\in a}{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=\left(\underset{k\in a}{{\sum }_G},P\right)\underset{\dot{}}{·}Q\right)\leftrightarrow \left(\left(\phi \wedge \varnothing \subseteq A\right)\to \underset{k\in \varnothing }{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=\left(\underset{k\in \varnothing }{{\sum }_G},P\right)\underset{\dot{}}{·}Q\right)\right)$$
21		sseq1	$$⊢a=e\to \left(a\subseteq A\leftrightarrow e\subseteq A\right)$$
22	21	anbi2d	$$⊢a=e\to \left(\left(\phi \wedge a\subseteq A\right)\leftrightarrow \left(\phi \wedge e\subseteq A\right)\right)$$
23		mpteq1	$$⊢a=e\to \left(k\in a⟼P\underset{\dot{}}{·}Q\right)=\left(k\in e⟼P\underset{\dot{}}{·}Q\right)$$
24	23	oveq2d	$$⊢a=e\to \underset{k\in a}{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=\underset{k\in e}{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)$$
25		mpteq1	$$⊢a=e\to \left(k\in a⟼P\right)=\left(k\in e⟼P\right)$$
26	25	oveq2d	$$⊢a=e\to \underset{k\in a}{{\sum }_G}P=\underset{k\in e}{{\sum }_G}P$$
27	26	oveq1d	$$⊢a=e\to \left(\underset{k\in a}{{\sum }_G},P\right)\underset{\dot{}}{·}Q=\left(\underset{k\in e}{{\sum }_G},P\right)\underset{\dot{}}{·}Q$$
28	24 27	eqeq12d	$$⊢a=e\to \left(\underset{k\in a}{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=\left(\underset{k\in a}{{\sum }_G},P\right)\underset{\dot{}}{·}Q\leftrightarrow \underset{k\in e}{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=\left(\underset{k\in e}{{\sum }_G},P\right)\underset{\dot{}}{·}Q\right)$$
29	22 28	imbi12d	$$⊢a=e\to \left(\left(\left(\phi \wedge a\subseteq A\right)\to \underset{k\in a}{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=\left(\underset{k\in a}{{\sum }_G},P\right)\underset{\dot{}}{·}Q\right)\leftrightarrow \left(\left(\phi \wedge e\subseteq A\right)\to \underset{k\in e}{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=\left(\underset{k\in e}{{\sum }_G},P\right)\underset{\dot{}}{·}Q\right)\right)$$
30		sseq1	$$⊢a=e\cup \left\{z\right\}\to \left(a\subseteq A\leftrightarrow e\cup \left\{z\right\}\subseteq A\right)$$
31	30	anbi2d	$$⊢a=e\cup \left\{z\right\}\to \left(\left(\phi \wedge a\subseteq A\right)\leftrightarrow \left(\phi \wedge e\cup \left\{z\right\}\subseteq A\right)\right)$$
32		mpteq1	$$⊢a=e\cup \left\{z\right\}\to \left(k\in a⟼P\underset{\dot{}}{·}Q\right)=\left(k\in \left(e\cup \left\{z\right\}\right)⟼P\underset{\dot{}}{·}Q\right)$$
33	32	oveq2d	$$⊢a=e\cup \left\{z\right\}\to \underset{k\in a}{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=\underset{k\in e\cup \left\{z\right\}}{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)$$
34		mpteq1	$$⊢a=e\cup \left\{z\right\}\to \left(k\in a⟼P\right)=\left(k\in \left(e\cup \left\{z\right\}\right)⟼P\right)$$
35	34	oveq2d	$$⊢a=e\cup \left\{z\right\}\to \underset{k\in a}{{\sum }_G}P=\underset{k\in e\cup \left\{z\right\}}{{\sum }_G}P$$
36	35	oveq1d	$$⊢a=e\cup \left\{z\right\}\to \left(\underset{k\in a}{{\sum }_G},P\right)\underset{\dot{}}{·}Q=\left(\underset{k\in e\cup \left\{z\right\}}{{\sum }_G},P\right)\underset{\dot{}}{·}Q$$
37	33 36	eqeq12d	$$⊢a=e\cup \left\{z\right\}\to \left(\underset{k\in a}{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=\left(\underset{k\in a}{{\sum }_G},P\right)\underset{\dot{}}{·}Q\leftrightarrow \underset{k\in e\cup \left\{z\right\}}{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=\left(\underset{k\in e\cup \left\{z\right\}}{{\sum }_G},P\right)\underset{\dot{}}{·}Q\right)$$
38	31 37	imbi12d	$$⊢a=e\cup \left\{z\right\}\to \left(\left(\left(\phi \wedge a\subseteq A\right)\to \underset{k\in a}{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=\left(\underset{k\in a}{{\sum }_G},P\right)\underset{\dot{}}{·}Q\right)\leftrightarrow \left(\left(\phi \wedge e\cup \left\{z\right\}\subseteq A\right)\to \underset{k\in e\cup \left\{z\right\}}{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=\left(\underset{k\in e\cup \left\{z\right\}}{{\sum }_G},P\right)\underset{\dot{}}{·}Q\right)\right)$$
39		sseq1	$$⊢a=A\to \left(a\subseteq A\leftrightarrow A\subseteq A\right)$$
40	39	anbi2d	$$⊢a=A\to \left(\left(\phi \wedge a\subseteq A\right)\leftrightarrow \left(\phi \wedge A\subseteq A\right)\right)$$
41		mpteq1	$$⊢a=A\to \left(k\in a⟼P\underset{\dot{}}{·}Q\right)=\left(k\in A⟼P\underset{\dot{}}{·}Q\right)$$
42	41	oveq2d	$$⊢a=A\to \underset{k\in a}{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=\underset{k\in A}{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)$$
43		mpteq1	$$⊢a=A\to \left(k\in a⟼P\right)=\left(k\in A⟼P\right)$$
44	43	oveq2d	$$⊢a=A\to \underset{k\in a}{{\sum }_G}P=\underset{k\in A}{{\sum }_G}P$$
45	44	oveq1d	$$⊢a=A\to \left(\underset{k\in a}{{\sum }_G},P\right)\underset{\dot{}}{·}Q=\left(\underset{k\in A}{{\sum }_G},P\right)\underset{\dot{}}{·}Q$$
46	42 45	eqeq12d	$$⊢a=A\to \left(\underset{k\in a}{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=\left(\underset{k\in a}{{\sum }_G},P\right)\underset{\dot{}}{·}Q\leftrightarrow \underset{k\in A}{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=\left(\underset{k\in A}{{\sum }_G},P\right)\underset{\dot{}}{·}Q\right)$$
47	40 46	imbi12d	$$⊢a=A\to \left(\left(\left(\phi \wedge a\subseteq A\right)\to \underset{k\in a}{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=\left(\underset{k\in a}{{\sum }_G},P\right)\underset{\dot{}}{·}Q\right)\leftrightarrow \left(\left(\phi \wedge A\subseteq A\right)\to \underset{k\in A}{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=\left(\underset{k\in A}{{\sum }_G},P\right)\underset{\dot{}}{·}Q\right)\right)$$
48		eqid	$$⊢0_G=0_G$$
49	1 2 4 48 3	slmd0vs	$$⊢\left(W\in \mathrm{SLMod}\wedge Q\in B\right)\to 0_G\underset{\dot{}}{·}Q=\underset{\dot{}}{0}$$
50	8 9 49	syl2anc	$$⊢\phi \to 0_G\underset{\dot{}}{·}Q=\underset{\dot{}}{0}$$
51	50	eqcomd	$$⊢\phi \to \underset{\dot{}}{0}=0_G\underset{\dot{}}{·}Q$$
52		mpt0	$$⊢\left(k\in \varnothing ⟼P\underset{\dot{}}{·}Q\right)=\varnothing$$
53	52	oveq2i	$$⊢\underset{k\in \varnothing }{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)={\sum }_W\varnothing$$
54	3	gsum0	$$⊢{\sum }_W\varnothing =\underset{\dot{}}{0}$$
55	53 54	eqtri	$$⊢\underset{k\in \varnothing }{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=\underset{\dot{}}{0}$$
56		mpt0	$$⊢\left(k\in \varnothing ⟼P\right)=\varnothing$$
57	56	oveq2i	$$⊢\underset{k\in \varnothing }{{\sum }_G}P={\sum }_G\varnothing$$
58	48	gsum0	$$⊢{\sum }_G\varnothing =0_G$$
59	57 58	eqtri	$$⊢\underset{k\in \varnothing }{{\sum }_G}P=0_G$$
60	59	oveq1i	$$⊢\left(\underset{k\in \varnothing }{{\sum }_G},P\right)\underset{\dot{}}{·}Q=0_G\underset{\dot{}}{·}Q$$
61	51 55 60	3eqtr4g	$$⊢\phi \to \underset{k\in \varnothing }{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=\left(\underset{k\in \varnothing }{{\sum }_G},P\right)\underset{\dot{}}{·}Q$$
62	61	adantr	$$⊢\left(\phi \wedge \varnothing \subseteq A\right)\to \underset{k\in \varnothing }{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=\left(\underset{k\in \varnothing }{{\sum }_G},P\right)\underset{\dot{}}{·}Q$$
63		ssun1	$$⊢e\subseteq e\cup \left\{z\right\}$$
64		sstr2	$$⊢e\subseteq e\cup \left\{z\right\}\to \left(e\cup \left\{z\right\}\subseteq A\to e\subseteq A\right)$$
65	63 64	ax-mp	$$⊢e\cup \left\{z\right\}\subseteq A\to e\subseteq A$$
66	65	anim2i	$$⊢\left(\phi \wedge e\cup \left\{z\right\}\subseteq A\right)\to \left(\phi \wedge e\subseteq A\right)$$
67	66	imim1i	$$⊢\left(\left(\phi \wedge e\subseteq A\right)\to \underset{k\in e}{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=\left(\underset{k\in e}{{\sum }_G},P\right)\underset{\dot{}}{·}Q\right)\to \left(\left(\phi \wedge e\cup \left\{z\right\}\subseteq A\right)\to \underset{k\in e}{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=\left(\underset{k\in e}{{\sum }_G},P\right)\underset{\dot{}}{·}Q\right)$$
68	8	ad2antrl	$$⊢\left(\left(e\in \mathrm{Fin}\wedge \neg z\in e\right)\wedge \left(\phi \wedge e\cup \left\{z\right\}\subseteq A\right)\right)\to W\in \mathrm{SLMod}$$
69		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
70	2	slmdsrg	$$⊢W\in \mathrm{SLMod}\to G\in \mathrm{SRing}$$
71		srgcmn	$$⊢G\in \mathrm{SRing}\to G\in \mathrm{CMnd}$$
72	68 70 71	3syl	$$⊢\left(\left(e\in \mathrm{Fin}\wedge \neg z\in e\right)\wedge \left(\phi \wedge e\cup \left\{z\right\}\subseteq A\right)\right)\to G\in \mathrm{CMnd}$$
73		vex	$$⊢e\in \mathrm{V}$$
74	73	a1i	$$⊢\left(\left(e\in \mathrm{Fin}\wedge \neg z\in e\right)\wedge \left(\phi \wedge e\cup \left\{z\right\}\subseteq A\right)\right)\to e\in \mathrm{V}$$
75		simplrl	$$⊢\left(\left(\left(e\in \mathrm{Fin}\wedge \neg z\in e\right)\wedge \left(\phi \wedge e\cup \left\{z\right\}\subseteq A\right)\right)\wedge k\in e\right)\to \phi$$
76		simprr	$$⊢\left(\left(e\in \mathrm{Fin}\wedge \neg z\in e\right)\wedge \left(\phi \wedge e\cup \left\{z\right\}\subseteq A\right)\right)\to e\cup \left\{z\right\}\subseteq A$$
77	76	unssad	$$⊢\left(\left(e\in \mathrm{Fin}\wedge \neg z\in e\right)\wedge \left(\phi \wedge e\cup \left\{z\right\}\subseteq A\right)\right)\to e\subseteq A$$
78	77	sselda	$$⊢\left(\left(\left(e\in \mathrm{Fin}\wedge \neg z\in e\right)\wedge \left(\phi \wedge e\cup \left\{z\right\}\subseteq A\right)\right)\wedge k\in e\right)\to k\in A$$
79	6	adantr	$$⊢\left(\phi \wedge k\in A\right)\to K\subseteq {\mathrm{Base}}_G$$
80	79 10	sseldd	$$⊢\left(\phi \wedge k\in A\right)\to P\in {\mathrm{Base}}_G$$
81	75 78 80	syl2anc	$$⊢\left(\left(\left(e\in \mathrm{Fin}\wedge \neg z\in e\right)\wedge \left(\phi \wedge e\cup \left\{z\right\}\subseteq A\right)\right)\wedge k\in e\right)\to P\in {\mathrm{Base}}_G$$
82	81	fmpttd	$$⊢\left(\left(e\in \mathrm{Fin}\wedge \neg z\in e\right)\wedge \left(\phi \wedge e\cup \left\{z\right\}\subseteq A\right)\right)\to \left(k\in e⟼P\right):e⟶{\mathrm{Base}}_G$$
83		eqid	$$⊢\left(k\in e⟼P\right)=\left(k\in e⟼P\right)$$
84		simpll	$$⊢\left(\left(e\in \mathrm{Fin}\wedge \neg z\in e\right)\wedge \left(\phi \wedge e\cup \left\{z\right\}\subseteq A\right)\right)\to e\in \mathrm{Fin}$$
85	75 78 10	syl2anc	$$⊢\left(\left(\left(e\in \mathrm{Fin}\wedge \neg z\in e\right)\wedge \left(\phi \wedge e\cup \left\{z\right\}\subseteq A\right)\right)\wedge k\in e\right)\to P\in K$$
86		fvexd	$$⊢\left(\left(e\in \mathrm{Fin}\wedge \neg z\in e\right)\wedge \left(\phi \wedge e\cup \left\{z\right\}\subseteq A\right)\right)\to 0_G\in \mathrm{V}$$
87	83 84 85 86	fsuppmptdm	$$⊢\left(\left(e\in \mathrm{Fin}\wedge \neg z\in e\right)\wedge \left(\phi \wedge e\cup \left\{z\right\}\subseteq A\right)\right)\to {finSupp}_{0_G}\left(\left(k\in e⟼P\right)\right)$$
88	69 48 72 74 82 87	gsumcl	$$⊢\left(\left(e\in \mathrm{Fin}\wedge \neg z\in e\right)\wedge \left(\phi \wedge e\cup \left\{z\right\}\subseteq A\right)\right)\to \underset{k\in e}{{\sum }_G}P\in {\mathrm{Base}}_G$$
89	76	unssbd	$$⊢\left(\left(e\in \mathrm{Fin}\wedge \neg z\in e\right)\wedge \left(\phi \wedge e\cup \left\{z\right\}\subseteq A\right)\right)\to \left\{z\right\}\subseteq A$$
90		vex	$$⊢z\in \mathrm{V}$$
91	90	snss	$$⊢z\in A\leftrightarrow \left\{z\right\}\subseteq A$$
92	89 91	sylibr	$$⊢\left(\left(e\in \mathrm{Fin}\wedge \neg z\in e\right)\wedge \left(\phi \wedge e\cup \left\{z\right\}\subseteq A\right)\right)\to z\in A$$
93	80	ralrimiva	$$⊢\phi \to \forall k\in AP\in {\mathrm{Base}}_G$$
94	93	ad2antrl	$$⊢\left(\left(e\in \mathrm{Fin}\wedge \neg z\in e\right)\wedge \left(\phi \wedge e\cup \left\{z\right\}\subseteq A\right)\right)\to \forall k\in AP\in {\mathrm{Base}}_G$$
95		rspcsbela	$$⊢\left(z\in A\wedge \forall k\in AP\in {\mathrm{Base}}_G\right)\to ⦋z/k⦌P\in {\mathrm{Base}}_G$$
96	92 94 95	syl2anc	$$⊢\left(\left(e\in \mathrm{Fin}\wedge \neg z\in e\right)\wedge \left(\phi \wedge e\cup \left\{z\right\}\subseteq A\right)\right)\to ⦋z/k⦌P\in {\mathrm{Base}}_G$$
97	9	ad2antrl	$$⊢\left(\left(e\in \mathrm{Fin}\wedge \neg z\in e\right)\wedge \left(\phi \wedge e\cup \left\{z\right\}\subseteq A\right)\right)\to Q\in B$$
98		eqid	$$⊢{+}_G={+}_G$$
99	1 5 2 4 69 98	slmdvsdir	$$⊢\left(W\in \mathrm{SLMod}\wedge \left(\underset{k\in e}{{\sum }_G}P\in {\mathrm{Base}}_G\wedge ⦋z/k⦌P\in {\mathrm{Base}}_G\wedge Q\in B\right)\right)\to \left(\left(\underset{k\in e}{{\sum }_G},P\right){+}_G⦋z/k⦌P\right)\underset{\dot{}}{·}Q=\left(\left(\underset{k\in e}{{\sum }_G},P\right)\underset{\dot{}}{·}Q\right)\underset{\dot{}}{+}\left(⦋z/k⦌P\underset{\dot{}}{·}Q\right)$$
100	68 88 96 97 99	syl13anc	$$⊢\left(\left(e\in \mathrm{Fin}\wedge \neg z\in e\right)\wedge \left(\phi \wedge e\cup \left\{z\right\}\subseteq A\right)\right)\to \left(\left(\underset{k\in e}{{\sum }_G},P\right){+}_G⦋z/k⦌P\right)\underset{\dot{}}{·}Q=\left(\left(\underset{k\in e}{{\sum }_G},P\right)\underset{\dot{}}{·}Q\right)\underset{\dot{}}{+}\left(⦋z/k⦌P\underset{\dot{}}{·}Q\right)$$
101	100	adantr	$$⊢\left(\left(\left(e\in \mathrm{Fin}\wedge \neg z\in e\right)\wedge \left(\phi \wedge e\cup \left\{z\right\}\subseteq A\right)\right)\wedge \underset{k\in e}{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=\left(\underset{k\in e}{{\sum }_G},P\right)\underset{\dot{}}{·}Q\right)\to \left(\left(\underset{k\in e}{{\sum }_G},P\right){+}_G⦋z/k⦌P\right)\underset{\dot{}}{·}Q=\left(\left(\underset{k\in e}{{\sum }_G},P\right)\underset{\dot{}}{·}Q\right)\underset{\dot{}}{+}\left(⦋z/k⦌P\underset{\dot{}}{·}Q\right)$$
102		nfcsb1v	$$⊢\underset{\_}{Ⅎ}k⦋z/k⦌P$$
103	90	a1i	$$⊢\left(\left(e\in \mathrm{Fin}\wedge \neg z\in e\right)\wedge \left(\phi \wedge e\cup \left\{z\right\}\subseteq A\right)\right)\to z\in \mathrm{V}$$
104		simplr	$$⊢\left(\left(e\in \mathrm{Fin}\wedge \neg z\in e\right)\wedge \left(\phi \wedge e\cup \left\{z\right\}\subseteq A\right)\right)\to \neg z\in e$$
105		csbeq1a	$$⊢k=z\to P=⦋z/k⦌P$$
106	102 69 98 72 84 81 103 104 96 105	gsumunsnf	$$⊢\left(\left(e\in \mathrm{Fin}\wedge \neg z\in e\right)\wedge \left(\phi \wedge e\cup \left\{z\right\}\subseteq A\right)\right)\to \underset{k\in e\cup \left\{z\right\}}{{\sum }_G}P=\left(\underset{k\in e}{{\sum }_G},P\right){+}_G⦋z/k⦌P$$
107	106	oveq1d	$$⊢\left(\left(e\in \mathrm{Fin}\wedge \neg z\in e\right)\wedge \left(\phi \wedge e\cup \left\{z\right\}\subseteq A\right)\right)\to \left(\underset{k\in e\cup \left\{z\right\}}{{\sum }_G},P\right)\underset{\dot{}}{·}Q=\left(\left(\underset{k\in e}{{\sum }_G},P\right){+}_G⦋z/k⦌P\right)\underset{\dot{}}{·}Q$$
108	107	adantr	$$⊢\left(\left(\left(e\in \mathrm{Fin}\wedge \neg z\in e\right)\wedge \left(\phi \wedge e\cup \left\{z\right\}\subseteq A\right)\right)\wedge \underset{k\in e}{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=\left(\underset{k\in e}{{\sum }_G},P\right)\underset{\dot{}}{·}Q\right)\to \left(\underset{k\in e\cup \left\{z\right\}}{{\sum }_G},P\right)\underset{\dot{}}{·}Q=\left(\left(\underset{k\in e}{{\sum }_G},P\right){+}_G⦋z/k⦌P\right)\underset{\dot{}}{·}Q$$
109		nfcv	$$⊢\underset{\_}{Ⅎ}k\underset{\dot{}}{·}$$
110		nfcv	$$⊢\underset{\_}{Ⅎ}kQ$$
111	102 109 110	nfov	$$⊢\underset{\_}{Ⅎ}k\left(⦋z/k⦌P\underset{\dot{}}{·}Q\right)$$
112		slmdcmn	$$⊢W\in \mathrm{SLMod}\to W\in \mathrm{CMnd}$$
113	68 112	syl	$$⊢\left(\left(e\in \mathrm{Fin}\wedge \neg z\in e\right)\wedge \left(\phi \wedge e\cup \left\{z\right\}\subseteq A\right)\right)\to W\in \mathrm{CMnd}$$
114	75 8	syl	$$⊢\left(\left(\left(e\in \mathrm{Fin}\wedge \neg z\in e\right)\wedge \left(\phi \wedge e\cup \left\{z\right\}\subseteq A\right)\right)\wedge k\in e\right)\to W\in \mathrm{SLMod}$$
115	75 9	syl	$$⊢\left(\left(\left(e\in \mathrm{Fin}\wedge \neg z\in e\right)\wedge \left(\phi \wedge e\cup \left\{z\right\}\subseteq A\right)\right)\wedge k\in e\right)\to Q\in B$$
116	1 2 4 69	slmdvscl	$$⊢\left(W\in \mathrm{SLMod}\wedge P\in {\mathrm{Base}}_G\wedge Q\in B\right)\to P\underset{\dot{}}{·}Q\in B$$
117	114 81 115 116	syl3anc	$$⊢\left(\left(\left(e\in \mathrm{Fin}\wedge \neg z\in e\right)\wedge \left(\phi \wedge e\cup \left\{z\right\}\subseteq A\right)\right)\wedge k\in e\right)\to P\underset{\dot{}}{·}Q\in B$$
118	1 2 4 69	slmdvscl	$$⊢\left(W\in \mathrm{SLMod}\wedge ⦋z/k⦌P\in {\mathrm{Base}}_G\wedge Q\in B\right)\to ⦋z/k⦌P\underset{\dot{}}{·}Q\in B$$
119	68 96 97 118	syl3anc	$$⊢\left(\left(e\in \mathrm{Fin}\wedge \neg z\in e\right)\wedge \left(\phi \wedge e\cup \left\{z\right\}\subseteq A\right)\right)\to ⦋z/k⦌P\underset{\dot{}}{·}Q\in B$$
120	105	oveq1d	$$⊢k=z\to P\underset{\dot{}}{·}Q=⦋z/k⦌P\underset{\dot{}}{·}Q$$
121	111 1 5 113 84 117 103 104 119 120	gsumunsnf	$$⊢\left(\left(e\in \mathrm{Fin}\wedge \neg z\in e\right)\wedge \left(\phi \wedge e\cup \left\{z\right\}\subseteq A\right)\right)\to \underset{k\in e\cup \left\{z\right\}}{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=\left(\underset{k\in e}{{\sum }_W},\left(P\underset{\dot{}}{·}Q\right)\right)\underset{\dot{}}{+}\left(⦋z/k⦌P\underset{\dot{}}{·}Q\right)$$
122	121	adantr	$$⊢\left(\left(\left(e\in \mathrm{Fin}\wedge \neg z\in e\right)\wedge \left(\phi \wedge e\cup \left\{z\right\}\subseteq A\right)\right)\wedge \underset{k\in e}{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=\left(\underset{k\in e}{{\sum }_G},P\right)\underset{\dot{}}{·}Q\right)\to \underset{k\in e\cup \left\{z\right\}}{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=\left(\underset{k\in e}{{\sum }_W},\left(P\underset{\dot{}}{·}Q\right)\right)\underset{\dot{}}{+}\left(⦋z/k⦌P\underset{\dot{}}{·}Q\right)$$
123		simpr	$$⊢\left(\left(\left(e\in \mathrm{Fin}\wedge \neg z\in e\right)\wedge \left(\phi \wedge e\cup \left\{z\right\}\subseteq A\right)\right)\wedge \underset{k\in e}{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=\left(\underset{k\in e}{{\sum }_G},P\right)\underset{\dot{}}{·}Q\right)\to \underset{k\in e}{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=\left(\underset{k\in e}{{\sum }_G},P\right)\underset{\dot{}}{·}Q$$
124	123	oveq1d	$$⊢\left(\left(\left(e\in \mathrm{Fin}\wedge \neg z\in e\right)\wedge \left(\phi \wedge e\cup \left\{z\right\}\subseteq A\right)\right)\wedge \underset{k\in e}{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=\left(\underset{k\in e}{{\sum }_G},P\right)\underset{\dot{}}{·}Q\right)\to \left(\underset{k\in e}{{\sum }_W},\left(P\underset{\dot{}}{·}Q\right)\right)\underset{\dot{}}{+}\left(⦋z/k⦌P\underset{\dot{}}{·}Q\right)=\left(\left(\underset{k\in e}{{\sum }_G},P\right)\underset{\dot{}}{·}Q\right)\underset{\dot{}}{+}\left(⦋z/k⦌P\underset{\dot{}}{·}Q\right)$$
125	122 124	eqtrd	$$⊢\left(\left(\left(e\in \mathrm{Fin}\wedge \neg z\in e\right)\wedge \left(\phi \wedge e\cup \left\{z\right\}\subseteq A\right)\right)\wedge \underset{k\in e}{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=\left(\underset{k\in e}{{\sum }_G},P\right)\underset{\dot{}}{·}Q\right)\to \underset{k\in e\cup \left\{z\right\}}{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=\left(\left(\underset{k\in e}{{\sum }_G},P\right)\underset{\dot{}}{·}Q\right)\underset{\dot{}}{+}\left(⦋z/k⦌P\underset{\dot{}}{·}Q\right)$$
126	101 108 125	3eqtr4rd	$$⊢\left(\left(\left(e\in \mathrm{Fin}\wedge \neg z\in e\right)\wedge \left(\phi \wedge e\cup \left\{z\right\}\subseteq A\right)\right)\wedge \underset{k\in e}{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=\left(\underset{k\in e}{{\sum }_G},P\right)\underset{\dot{}}{·}Q\right)\to \underset{k\in e\cup \left\{z\right\}}{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=\left(\underset{k\in e\cup \left\{z\right\}}{{\sum }_G},P\right)\underset{\dot{}}{·}Q$$
127	126	exp31	$$⊢\left(e\in \mathrm{Fin}\wedge \neg z\in e\right)\to \left(\left(\phi \wedge e\cup \left\{z\right\}\subseteq A\right)\to \left(\underset{k\in e}{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=\left(\underset{k\in e}{{\sum }_G},P\right)\underset{\dot{}}{·}Q\to \underset{k\in e\cup \left\{z\right\}}{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=\left(\underset{k\in e\cup \left\{z\right\}}{{\sum }_G},P\right)\underset{\dot{}}{·}Q\right)\right)$$
128	127	a2d	$$⊢\left(e\in \mathrm{Fin}\wedge \neg z\in e\right)\to \left(\left(\left(\phi \wedge e\cup \left\{z\right\}\subseteq A\right)\to \underset{k\in e}{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=\left(\underset{k\in e}{{\sum }_G},P\right)\underset{\dot{}}{·}Q\right)\to \left(\left(\phi \wedge e\cup \left\{z\right\}\subseteq A\right)\to \underset{k\in e\cup \left\{z\right\}}{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=\left(\underset{k\in e\cup \left\{z\right\}}{{\sum }_G},P\right)\underset{\dot{}}{·}Q\right)\right)$$
129	67 128	syl5	$$⊢\left(e\in \mathrm{Fin}\wedge \neg z\in e\right)\to \left(\left(\left(\phi \wedge e\subseteq A\right)\to \underset{k\in e}{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=\left(\underset{k\in e}{{\sum }_G},P\right)\underset{\dot{}}{·}Q\right)\to \left(\left(\phi \wedge e\cup \left\{z\right\}\subseteq A\right)\to \underset{k\in e\cup \left\{z\right\}}{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=\left(\underset{k\in e\cup \left\{z\right\}}{{\sum }_G},P\right)\underset{\dot{}}{·}Q\right)\right)$$
130	20 29 38 47 62 129	findcard2s	$$⊢A\in \mathrm{Fin}\to \left(\left(\phi \wedge A\subseteq A\right)\to \underset{k\in A}{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=\left(\underset{k\in A}{{\sum }_G},P\right)\underset{\dot{}}{·}Q\right)$$
131	130	imp	$$⊢\left(A\in \mathrm{Fin}\wedge \left(\phi \wedge A\subseteq A\right)\right)\to \underset{k\in A}{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=\left(\underset{k\in A}{{\sum }_G},P\right)\underset{\dot{}}{·}Q$$
132	11 131	mpanr2	$$⊢\left(A\in \mathrm{Fin}\wedge \phi \right)\to \underset{k\in A}{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=\left(\underset{k\in A}{{\sum }_G},P\right)\underset{\dot{}}{·}Q$$
133	7 132	mpancom	$$⊢\phi \to \underset{k\in A}{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=\left(\underset{k\in A}{{\sum }_G},P\right)\underset{\dot{}}{·}Q$$