Theorem gsumvsca1

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

	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}$$
	gsumvsca1.n	$$⊢\phi \to P\in K$$
	gsumvsca1.c	$$⊢\left(\phi \wedge k\in A\right)\to Q\in B$$
Assertion	gsumvsca1	$$⊢\phi \to \underset{k\in A}{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=P\underset{\dot{}}{·}\left(\underset{k\in A}{{\sum }_W},Q\right)$$

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		gsumvsca1.n	$$⊢\phi \to P\in K$$
10		gsumvsca1.c	$$⊢\left(\phi \wedge k\in A\right)\to Q\in B$$
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⟼Q\right)=\left(k\in \varnothing ⟼Q\right)$$
17	16	oveq2d	$$⊢a=\varnothing \to \underset{k\in a}{{\sum }_W}Q=\underset{k\in \varnothing }{{\sum }_W}Q$$
18	17	oveq2d	$$⊢a=\varnothing \to P\underset{\dot{}}{·}\left(\underset{k\in a}{{\sum }_W},Q\right)=P\underset{\dot{}}{·}\left(\underset{k\in \varnothing }{{\sum }_W},Q\right)$$
19	15 18	eqeq12d	$$⊢a=\varnothing \to \left(\underset{k\in a}{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=P\underset{\dot{}}{·}\left(\underset{k\in a}{{\sum }_W},Q\right)\leftrightarrow \underset{k\in \varnothing }{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=P\underset{\dot{}}{·}\left(\underset{k\in \varnothing }{{\sum }_W},Q\right)\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)=P\underset{\dot{}}{·}\left(\underset{k\in a}{{\sum }_W},Q\right)\right)\leftrightarrow \left(\left(\phi \wedge \varnothing \subseteq A\right)\to \underset{k\in \varnothing }{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=P\underset{\dot{}}{·}\left(\underset{k\in \varnothing }{{\sum }_W},Q\right)\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⟼Q\right)=\left(k\in e⟼Q\right)$$
26	25	oveq2d	$$⊢a=e\to \underset{k\in a}{{\sum }_W}Q=\underset{k\in e}{{\sum }_W}Q$$
27	26	oveq2d	$$⊢a=e\to P\underset{\dot{}}{·}\left(\underset{k\in a}{{\sum }_W},Q\right)=P\underset{\dot{}}{·}\left(\underset{k\in e}{{\sum }_W},Q\right)$$
28	24 27	eqeq12d	$$⊢a=e\to \left(\underset{k\in a}{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=P\underset{\dot{}}{·}\left(\underset{k\in a}{{\sum }_W},Q\right)\leftrightarrow \underset{k\in e}{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=P\underset{\dot{}}{·}\left(\underset{k\in e}{{\sum }_W},Q\right)\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)=P\underset{\dot{}}{·}\left(\underset{k\in a}{{\sum }_W},Q\right)\right)\leftrightarrow \left(\left(\phi \wedge e\subseteq A\right)\to \underset{k\in e}{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=P\underset{\dot{}}{·}\left(\underset{k\in e}{{\sum }_W},Q\right)\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⟼Q\right)=\left(k\in \left(e\cup \left\{z\right\}\right)⟼Q\right)$$
35	34	oveq2d	$$⊢a=e\cup \left\{z\right\}\to \underset{k\in a}{{\sum }_W}Q=\underset{k\in e\cup \left\{z\right\}}{{\sum }_W}Q$$
36	35	oveq2d	$$⊢a=e\cup \left\{z\right\}\to P\underset{\dot{}}{·}\left(\underset{k\in a}{{\sum }_W},Q\right)=P\underset{\dot{}}{·}\left(\underset{k\in e\cup \left\{z\right\}}{{\sum }_W},Q\right)$$
37	33 36	eqeq12d	$$⊢a=e\cup \left\{z\right\}\to \left(\underset{k\in a}{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=P\underset{\dot{}}{·}\left(\underset{k\in a}{{\sum }_W},Q\right)\leftrightarrow \underset{k\in e\cup \left\{z\right\}}{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=P\underset{\dot{}}{·}\left(\underset{k\in e\cup \left\{z\right\}}{{\sum }_W},Q\right)\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)=P\underset{\dot{}}{·}\left(\underset{k\in a}{{\sum }_W},Q\right)\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)=P\underset{\dot{}}{·}\left(\underset{k\in e\cup \left\{z\right\}}{{\sum }_W},Q\right)\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⟼Q\right)=\left(k\in A⟼Q\right)$$
44	43	oveq2d	$$⊢a=A\to \underset{k\in a}{{\sum }_W}Q=\underset{k\in A}{{\sum }_W}Q$$
45	44	oveq2d	$$⊢a=A\to P\underset{\dot{}}{·}\left(\underset{k\in a}{{\sum }_W},Q\right)=P\underset{\dot{}}{·}\left(\underset{k\in A}{{\sum }_W},Q\right)$$
46	42 45	eqeq12d	$$⊢a=A\to \left(\underset{k\in a}{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=P\underset{\dot{}}{·}\left(\underset{k\in a}{{\sum }_W},Q\right)\leftrightarrow \underset{k\in A}{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=P\underset{\dot{}}{·}\left(\underset{k\in A}{{\sum }_W},Q\right)\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)=P\underset{\dot{}}{·}\left(\underset{k\in a}{{\sum }_W},Q\right)\right)\leftrightarrow \left(\left(\phi \wedge A\subseteq A\right)\to \underset{k\in A}{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=P\underset{\dot{}}{·}\left(\underset{k\in A}{{\sum }_W},Q\right)\right)\right)$$
48	6 9	sseldd	$$⊢\phi \to P\in {\mathrm{Base}}_G$$
49		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
50	2 4 49 3	slmdvs0	$$⊢\left(W\in \mathrm{SLMod}\wedge P\in {\mathrm{Base}}_G\right)\to P\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
51	8 48 50	syl2anc	$$⊢\phi \to P\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
52	51	eqcomd	$$⊢\phi \to \underset{\dot{}}{0}=P\underset{\dot{}}{·}\underset{\dot{}}{0}$$
53		mpt0	$$⊢\left(k\in \varnothing ⟼P\underset{\dot{}}{·}Q\right)=\varnothing$$
54	53	oveq2i	$$⊢\underset{k\in \varnothing }{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)={\sum }_W\varnothing$$
55	3	gsum0	$$⊢{\sum }_W\varnothing =\underset{\dot{}}{0}$$
56	54 55	eqtri	$$⊢\underset{k\in \varnothing }{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=\underset{\dot{}}{0}$$
57		mpt0	$$⊢\left(k\in \varnothing ⟼Q\right)=\varnothing$$
58	57	oveq2i	$$⊢\underset{k\in \varnothing }{{\sum }_W}Q={\sum }_W\varnothing$$
59	58 55	eqtri	$$⊢\underset{k\in \varnothing }{{\sum }_W}Q=\underset{\dot{}}{0}$$
60	59	oveq2i	$$⊢P\underset{\dot{}}{·}\left(\underset{k\in \varnothing }{{\sum }_W},Q\right)=P\underset{\dot{}}{·}\underset{\dot{}}{0}$$
61	52 56 60	3eqtr4g	$$⊢\phi \to \underset{k\in \varnothing }{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=P\underset{\dot{}}{·}\left(\underset{k\in \varnothing }{{\sum }_W},Q\right)$$
62	61	adantr	$$⊢\left(\phi \wedge \varnothing \subseteq A\right)\to \underset{k\in \varnothing }{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=P\underset{\dot{}}{·}\left(\underset{k\in \varnothing }{{\sum }_W},Q\right)$$
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)=P\underset{\dot{}}{·}\left(\underset{k\in e}{{\sum }_W},Q\right)\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)=P\underset{\dot{}}{·}\left(\underset{k\in e}{{\sum }_W},Q\right)\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	48	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 P\in {\mathrm{Base}}_G$$
70		slmdcmn	$$⊢W\in \mathrm{SLMod}\to W\in \mathrm{CMnd}$$
71	68 70	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}$$
72		vex	$$⊢e\in \mathrm{V}$$
73	72	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}$$
74		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$$
75		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$$
76	75	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$$
77	76	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$$
78	74 77 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 Q\in B$$
79	78	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⟼Q\right):e⟶B$$
80		eqid	$$⊢\left(k\in e⟼Q\right)=\left(k\in e⟼Q\right)$$
81		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}$$
82	3	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
83	82	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 \underset{\dot{}}{0}\in \mathrm{V}$$
84	80 81 78 83	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}_{\underset{\dot{}}{0}}\left(\left(k\in e⟼Q\right)\right)$$
85	1 3 71 73 79 84	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 }_W}Q\in B$$
86	75	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$$
87		vex	$$⊢z\in \mathrm{V}$$
88	87	snss	$$⊢z\in A\leftrightarrow \left\{z\right\}\subseteq A$$
89	86 88	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$$
90	10	ralrimiva	$$⊢\phi \to \forall k\in AQ\in B$$
91	90	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 AQ\in B$$
92		rspcsbela	$$⊢\left(z\in A\wedge \forall k\in AQ\in B\right)\to ⦋z/k⦌Q\in B$$
93	89 91 92	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⦌Q\in B$$
94	1 5 2 4 49	slmdvsdi	$$⊢\left(W\in \mathrm{SLMod}\wedge \left(P\in {\mathrm{Base}}_G\wedge \underset{k\in e}{{\sum }_W}Q\in B\wedge ⦋z/k⦌Q\in B\right)\right)\to P\underset{\dot{}}{·}\left(\left(\underset{k\in e}{{\sum }_W},Q\right)\underset{\dot{}}{+}⦋z/k⦌Q\right)=\left(P\underset{\dot{}}{·}\left(\underset{k\in e}{{\sum }_W},Q\right)\right)\underset{\dot{}}{+}\left(P\underset{\dot{}}{·}⦋z/k⦌Q\right)$$
95	68 69 85 93 94	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 P\underset{\dot{}}{·}\left(\left(\underset{k\in e}{{\sum }_W},Q\right)\underset{\dot{}}{+}⦋z/k⦌Q\right)=\left(P\underset{\dot{}}{·}\left(\underset{k\in e}{{\sum }_W},Q\right)\right)\underset{\dot{}}{+}\left(P\underset{\dot{}}{·}⦋z/k⦌Q\right)$$
96	95	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)=P\underset{\dot{}}{·}\left(\underset{k\in e}{{\sum }_W},Q\right)\right)\to P\underset{\dot{}}{·}\left(\left(\underset{k\in e}{{\sum }_W},Q\right)\underset{\dot{}}{+}⦋z/k⦌Q\right)=\left(P\underset{\dot{}}{·}\left(\underset{k\in e}{{\sum }_W},Q\right)\right)\underset{\dot{}}{+}\left(P\underset{\dot{}}{·}⦋z/k⦌Q\right)$$
97		nfcsb1v	$$⊢\underset{\_}{Ⅎ}k⦋z/k⦌Q$$
98	87	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}$$
99		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$$
100		csbeq1a	$$⊢k=z\to Q=⦋z/k⦌Q$$
101	97 1 5 71 81 78 98 99 93 100	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}Q=\left(\underset{k\in e}{{\sum }_W},Q\right)\underset{\dot{}}{+}⦋z/k⦌Q$$
102	101	oveq2d	$$⊢\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 P\underset{\dot{}}{·}\left(\underset{k\in e\cup \left\{z\right\}}{{\sum }_W},Q\right)=P\underset{\dot{}}{·}\left(\left(\underset{k\in e}{{\sum }_W},Q\right)\underset{\dot{}}{+}⦋z/k⦌Q\right)$$
103	102	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)=P\underset{\dot{}}{·}\left(\underset{k\in e}{{\sum }_W},Q\right)\right)\to P\underset{\dot{}}{·}\left(\underset{k\in e\cup \left\{z\right\}}{{\sum }_W},Q\right)=P\underset{\dot{}}{·}\left(\left(\underset{k\in e}{{\sum }_W},Q\right)\underset{\dot{}}{+}⦋z/k⦌Q\right)$$
104		nfcv	$$⊢\underset{\_}{Ⅎ}kP$$
105		nfcv	$$⊢\underset{\_}{Ⅎ}k\underset{\dot{}}{·}$$
106	104 105 97	nfov	$$⊢\underset{\_}{Ⅎ}k\left(P\underset{\dot{}}{·}⦋z/k⦌Q\right)$$
107	74 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}$$
108	74 48	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 P\in {\mathrm{Base}}_G$$
109	1 2 4 49	slmdvscl	$$⊢\left(W\in \mathrm{SLMod}\wedge P\in {\mathrm{Base}}_G\wedge Q\in B\right)\to P\underset{\dot{}}{·}Q\in B$$
110	107 108 78 109	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$$
111	1 2 4 49	slmdvscl	$$⊢\left(W\in \mathrm{SLMod}\wedge P\in {\mathrm{Base}}_G\wedge ⦋z/k⦌Q\in B\right)\to P\underset{\dot{}}{·}⦋z/k⦌Q\in B$$
112	68 69 93 111	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 P\underset{\dot{}}{·}⦋z/k⦌Q\in B$$
113	100	oveq2d	$$⊢k=z\to P\underset{\dot{}}{·}Q=P\underset{\dot{}}{·}⦋z/k⦌Q$$
114	106 1 5 71 81 110 98 99 112 113	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(P\underset{\dot{}}{·}⦋z/k⦌Q\right)$$
115	114	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)=P\underset{\dot{}}{·}\left(\underset{k\in e}{{\sum }_W},Q\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(P\underset{\dot{}}{·}⦋z/k⦌Q\right)$$
116		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)=P\underset{\dot{}}{·}\left(\underset{k\in e}{{\sum }_W},Q\right)\right)\to \underset{k\in e}{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=P\underset{\dot{}}{·}\left(\underset{k\in e}{{\sum }_W},Q\right)$$
117	116	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)=P\underset{\dot{}}{·}\left(\underset{k\in e}{{\sum }_W},Q\right)\right)\to \left(\underset{k\in e}{{\sum }_W},\left(P\underset{\dot{}}{·}Q\right)\right)\underset{\dot{}}{+}\left(P\underset{\dot{}}{·}⦋z/k⦌Q\right)=\left(P\underset{\dot{}}{·}\left(\underset{k\in e}{{\sum }_W},Q\right)\right)\underset{\dot{}}{+}\left(P\underset{\dot{}}{·}⦋z/k⦌Q\right)$$
118	115 117	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)=P\underset{\dot{}}{·}\left(\underset{k\in e}{{\sum }_W},Q\right)\right)\to \underset{k\in e\cup \left\{z\right\}}{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=\left(P\underset{\dot{}}{·}\left(\underset{k\in e}{{\sum }_W},Q\right)\right)\underset{\dot{}}{+}\left(P\underset{\dot{}}{·}⦋z/k⦌Q\right)$$
119	96 103 118	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)=P\underset{\dot{}}{·}\left(\underset{k\in e}{{\sum }_W},Q\right)\right)\to \underset{k\in e\cup \left\{z\right\}}{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=P\underset{\dot{}}{·}\left(\underset{k\in e\cup \left\{z\right\}}{{\sum }_W},Q\right)$$
120	119	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)=P\underset{\dot{}}{·}\left(\underset{k\in e}{{\sum }_W},Q\right)\to \underset{k\in e\cup \left\{z\right\}}{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=P\underset{\dot{}}{·}\left(\underset{k\in e\cup \left\{z\right\}}{{\sum }_W},Q\right)\right)\right)$$
121	120	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)=P\underset{\dot{}}{·}\left(\underset{k\in e}{{\sum }_W},Q\right)\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)=P\underset{\dot{}}{·}\left(\underset{k\in e\cup \left\{z\right\}}{{\sum }_W},Q\right)\right)\right)$$
122	67 121	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)=P\underset{\dot{}}{·}\left(\underset{k\in e}{{\sum }_W},Q\right)\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)=P\underset{\dot{}}{·}\left(\underset{k\in e\cup \left\{z\right\}}{{\sum }_W},Q\right)\right)\right)$$
123	20 29 38 47 62 122	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)=P\underset{\dot{}}{·}\left(\underset{k\in A}{{\sum }_W},Q\right)\right)$$
124	123	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)=P\underset{\dot{}}{·}\left(\underset{k\in A}{{\sum }_W},Q\right)$$
125	11 124	mpanr2	$$⊢\left(A\in \mathrm{Fin}\wedge \phi \right)\to \underset{k\in A}{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=P\underset{\dot{}}{·}\left(\underset{k\in A}{{\sum }_W},Q\right)$$
126	7 125	mpancom	$$⊢\phi \to \underset{k\in A}{{\sum }_W}\left(P\underset{\dot{}}{·}Q\right)=P\underset{\dot{}}{·}\left(\underset{k\in A}{{\sum }_W},Q\right)$$