gsumpr

Description: Group sum of a pair. (Contributed by AV, 6-Dec-2018) (Proof shortened by AV, 28-Jul-2019)

	Ref	Expression
Hypotheses	gsumpr.b	$⊢ B = {Base}_{G}$
	gsumpr.p	$⊢ \underset{˙}{+} = +_{G}$
	gsumpr.s	$⊢ k = M \to A = C$
	gsumpr.t	$⊢ k = N \to A = D$
Assertion	gsumpr	$⊢ (G \in CMnd \land (M \in V \land N \in W \land M \neq N) \land (C \in B \land D \in B)) \to \underset{k \in \{M, N\}}{\sum_{G}} A = C \underset{˙}{+} D$

Proof

Step	Hyp	Ref	Expression
1		gsumpr.b	$⊢ B = {Base}_{G}$
2		gsumpr.p	$⊢ \underset{˙}{+} = +_{G}$
3		gsumpr.s	$⊢ k = M \to A = C$
4		gsumpr.t	$⊢ k = N \to A = D$
5		simp1	$⊢ (G \in CMnd \land (M \in V \land N \in W \land M \neq N) \land (C \in B \land D \in B)) \to G \in CMnd$
6		prfi	$⊢ \{M, N\} \in Fin$
7	6	a1i	$⊢ (G \in CMnd \land (M \in V \land N \in W \land M \neq N) \land (C \in B \land D \in B)) \to \{M, N\} \in Fin$
8		vex	$⊢ k \in V$
9	8	elpr	$⊢ k \in \{M, N\} \leftrightarrow (k = M \lor k = N)$
10		eleq1a	$⊢ C \in B \to (A = C \to A \in B)$
11	10	adantr	$⊢ (C \in B \land D \in B) \to (A = C \to A \in B)$
12	11	3ad2ant3	$⊢ (G \in CMnd \land (M \in V \land N \in W \land M \neq N) \land (C \in B \land D \in B)) \to (A = C \to A \in B)$
13	3 12	syl5com	$⊢ k = M \to ((G \in CMnd \land (M \in V \land N \in W \land M \neq N) \land (C \in B \land D \in B)) \to A \in B)$
14		eleq1a	$⊢ D \in B \to (A = D \to A \in B)$
15	14	adantl	$⊢ (C \in B \land D \in B) \to (A = D \to A \in B)$
16	15	3ad2ant3	$⊢ (G \in CMnd \land (M \in V \land N \in W \land M \neq N) \land (C \in B \land D \in B)) \to (A = D \to A \in B)$
17	4 16	syl5com	$⊢ k = N \to ((G \in CMnd \land (M \in V \land N \in W \land M \neq N) \land (C \in B \land D \in B)) \to A \in B)$
18	13 17	jaoi	$⊢ (k = M \lor k = N) \to ((G \in CMnd \land (M \in V \land N \in W \land M \neq N) \land (C \in B \land D \in B)) \to A \in B)$
19	9 18	sylbi	$⊢ k \in \{M, N\} \to ((G \in CMnd \land (M \in V \land N \in W \land M \neq N) \land (C \in B \land D \in B)) \to A \in B)$
20	19	impcom	$⊢ ((G \in CMnd \land (M \in V \land N \in W \land M \neq N) \land (C \in B \land D \in B)) \land k \in \{M, N\}) \to A \in B$
21		disjsn2	$⊢ M \neq N \to \{M\} \cap \{N\} = \emptyset$
22	21	3ad2ant3	$⊢ (M \in V \land N \in W \land M \neq N) \to \{M\} \cap \{N\} = \emptyset$
23	22	3ad2ant2	$⊢ (G \in CMnd \land (M \in V \land N \in W \land M \neq N) \land (C \in B \land D \in B)) \to \{M\} \cap \{N\} = \emptyset$
24		df-pr	$⊢ \{M, N\} = \{M\} \cup \{N\}$
25	24	a1i	$⊢ (G \in CMnd \land (M \in V \land N \in W \land M \neq N) \land (C \in B \land D \in B)) \to \{M, N\} = \{M\} \cup \{N\}$
26		eqid	$⊢ (k \in \{M, N\} ⟼ A) = (k \in \{M, N\} ⟼ A)$
27	1 2 5 7 20 23 25 26	gsummptfidmsplitres	$⊢ (G \in CMnd \land (M \in V \land N \in W \land M \neq N) \land (C \in B \land D \in B)) \to \underset{k \in \{M, N\}}{\sum_{G}} A = (\sum_{G}, ({(k \in \{M, N\} ⟼ A) ↾}_{\{M\}})) \underset{˙}{+} (\sum_{G}, ({(k \in \{M, N\} ⟼ A) ↾}_{\{N\}}))$
28		snsspr1	$⊢ \{M\} \subseteq \{M, N\}$
29		resmpt	$⊢ \{M\} \subseteq \{M, N\} \to {(k \in \{M, N\} ⟼ A) ↾}_{\{M\}} = (k \in \{M\} ⟼ A)$
30	28 29	mp1i	$⊢ (G \in CMnd \land (M \in V \land N \in W \land M \neq N) \land (C \in B \land D \in B)) \to {(k \in \{M, N\} ⟼ A) ↾}_{\{M\}} = (k \in \{M\} ⟼ A)$
31	30	oveq2d	$⊢ (G \in CMnd \land (M \in V \land N \in W \land M \neq N) \land (C \in B \land D \in B)) \to \sum_{G} ({(k \in \{M, N\} ⟼ A) ↾}_{\{M\}}) = \underset{k \in \{M\}}{\sum_{G}} A$
32		cmnmnd	$⊢ G \in CMnd \to G \in Mnd$
33		simp1	$⊢ (M \in V \land N \in W \land M \neq N) \to M \in V$
34		simpl	$⊢ (C \in B \land D \in B) \to C \in B$
35	1 3	gsumsn	$⊢ (G \in Mnd \land M \in V \land C \in B) \to \underset{k \in \{M\}}{\sum_{G}} A = C$
36	32 33 34 35	syl3an	$⊢ (G \in CMnd \land (M \in V \land N \in W \land M \neq N) \land (C \in B \land D \in B)) \to \underset{k \in \{M\}}{\sum_{G}} A = C$
37	31 36	eqtrd	$⊢ (G \in CMnd \land (M \in V \land N \in W \land M \neq N) \land (C \in B \land D \in B)) \to \sum_{G} ({(k \in \{M, N\} ⟼ A) ↾}_{\{M\}}) = C$
38		snsspr2	$⊢ \{N\} \subseteq \{M, N\}$
39		resmpt	$⊢ \{N\} \subseteq \{M, N\} \to {(k \in \{M, N\} ⟼ A) ↾}_{\{N\}} = (k \in \{N\} ⟼ A)$
40	38 39	mp1i	$⊢ (G \in CMnd \land (M \in V \land N \in W \land M \neq N) \land (C \in B \land D \in B)) \to {(k \in \{M, N\} ⟼ A) ↾}_{\{N\}} = (k \in \{N\} ⟼ A)$
41	40	oveq2d	$⊢ (G \in CMnd \land (M \in V \land N \in W \land M \neq N) \land (C \in B \land D \in B)) \to \sum_{G} ({(k \in \{M, N\} ⟼ A) ↾}_{\{N\}}) = \underset{k \in \{N\}}{\sum_{G}} A$
42		simp2	$⊢ (M \in V \land N \in W \land M \neq N) \to N \in W$
43		simpr	$⊢ (C \in B \land D \in B) \to D \in B$
44	1 4	gsumsn	$⊢ (G \in Mnd \land N \in W \land D \in B) \to \underset{k \in \{N\}}{\sum_{G}} A = D$
45	32 42 43 44	syl3an	$⊢ (G \in CMnd \land (M \in V \land N \in W \land M \neq N) \land (C \in B \land D \in B)) \to \underset{k \in \{N\}}{\sum_{G}} A = D$
46	41 45	eqtrd	$⊢ (G \in CMnd \land (M \in V \land N \in W \land M \neq N) \land (C \in B \land D \in B)) \to \sum_{G} ({(k \in \{M, N\} ⟼ A) ↾}_{\{N\}}) = D$
47	37 46	oveq12d	$⊢ (G \in CMnd \land (M \in V \land N \in W \land M \neq N) \land (C \in B \land D \in B)) \to (\sum_{G}, ({(k \in \{M, N\} ⟼ A) ↾}_{\{M\}})) \underset{˙}{+} (\sum_{G}, ({(k \in \{M, N\} ⟼ A) ↾}_{\{N\}})) = C \underset{˙}{+} D$
48	27 47	eqtrd	$⊢ (G \in CMnd \land (M \in V \land N \in W \land M \neq N) \land (C \in B \land D \in B)) \to \underset{k \in \{M, N\}}{\sum_{G}} A = C \underset{˙}{+} D$

Metamath Proof Explorer

Theorem gsumpr

Proof