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 = {Base}_{W}$
	gsumvsca.g	$⊢ G = Scalar (W)$
	gsumvsca.z	$⊢ \underset{˙}{0} = 0_{W}$
	gsumvsca.t	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	gsumvsca.p	$⊢ \underset{˙}{+} = +_{W}$
	gsumvsca.k	$⊢ φ \to K \subseteq {Base}_{G}$
	gsumvsca.a	$⊢ φ \to A \in Fin$
	gsumvsca.w	$⊢ φ \to W \in SLMod$
	gsumvsca2.n	$⊢ φ \to Q \in B$
	gsumvsca2.c	$⊢ (φ \land k \in A) \to P \in K$
Assertion	gsumvsca2	$⊢ φ \to \underset{k \in A}{\sum_{W}} (P \underset{˙}{\cdot} Q) = (\underset{k \in A}{\sum_{G}}, P) \underset{˙}{\cdot} Q$

Proof

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

Metamath Proof Explorer

Theorem gsumvsca2

Proof