gsummatr01

	Ref	Expression
Hypotheses	gsummatr01.p	$⊢ P = {Base}_{SymGrp (N)}$
	gsummatr01.r	$⊢ R = \{r \in P \| r (K) = L\}$
	gsummatr01.0	$⊢ \underset{˙}{0} = 0_{G}$
	gsummatr01.s	$⊢ S = {Base}_{G}$
Assertion	gsummatr01	$⊢ ((G \in CMnd \land N \in Fin) \land (\forall i \in N \forall j \in N i A j \in S \land B \in S) \land (K \in N \land L \in N \land Q \in R)) \to \underset{n \in N}{\sum_{G}} (n (i \in N, j \in N ⟼ if (i = K, if (j = L, \underset{˙}{0}, B), i A j)) Q (n)) = \underset{n \in N ∖ \{K\}}{\sum_{G}} (n (i \in (N ∖ \{K\}), j \in (N ∖ \{L\}) ⟼ i A j) Q (n))$

Proof

Step	Hyp	Ref	Expression
1		gsummatr01.p	$⊢ P = {Base}_{SymGrp (N)}$
2		gsummatr01.r	$⊢ R = \{r \in P \| r (K) = L\}$
3		gsummatr01.0	$⊢ \underset{˙}{0} = 0_{G}$
4		gsummatr01.s	$⊢ S = {Base}_{G}$
5		difsnid	$⊢ K \in N \to (N ∖ \{K\}) \cup \{K\} = N$
6	5	eqcomd	$⊢ K \in N \to N = (N ∖ \{K\}) \cup \{K\}$
7	6	3ad2ant1	$⊢ (K \in N \land L \in N \land Q \in R) \to N = (N ∖ \{K\}) \cup \{K\}$
8	7	3ad2ant3	$⊢ ((G \in CMnd \land N \in Fin) \land (\forall i \in N \forall j \in N i A j \in S \land B \in S) \land (K \in N \land L \in N \land Q \in R)) \to N = (N ∖ \{K\}) \cup \{K\}$
9	8	mpteq1d	$⊢ ((G \in CMnd \land N \in Fin) \land (\forall i \in N \forall j \in N i A j \in S \land B \in S) \land (K \in N \land L \in N \land Q \in R)) \to (n \in N ⟼ n (i \in N, j \in N ⟼ if (i = K, if (j = L, \underset{˙}{0}, B), i A j)) Q (n)) = (n \in ((N ∖ \{K\}) \cup \{K\}) ⟼ n (i \in N, j \in N ⟼ if (i = K, if (j = L, \underset{˙}{0}, B), i A j)) Q (n))$
10	9	oveq2d	$⊢ ((G \in CMnd \land N \in Fin) \land (\forall i \in N \forall j \in N i A j \in S \land B \in S) \land (K \in N \land L \in N \land Q \in R)) \to \underset{n \in N}{\sum_{G}} (n (i \in N, j \in N ⟼ if (i = K, if (j = L, \underset{˙}{0}, B), i A j)) Q (n)) = \underset{n \in (N ∖ \{K\}) \cup \{K\}}{\sum_{G}} (n (i \in N, j \in N ⟼ if (i = K, if (j = L, \underset{˙}{0}, B), i A j)) Q (n))$
11	1 2 3 4	gsummatr01lem3	$⊢ ((G \in CMnd \land N \in Fin) \land (\forall i \in N \forall j \in N i A j \in S \land B \in S) \land (K \in N \land L \in N \land Q \in R)) \to \underset{n \in (N ∖ \{K\}) \cup \{K\}}{\sum_{G}} (n (i \in N, j \in N ⟼ if (i = K, if (j = L, \underset{˙}{0}, B), i A j)) Q (n)) = (\underset{n \in N ∖ \{K\}}{\sum_{G}}, (n (i \in N, j \in N ⟼ if (i = K, if (j = L, \underset{˙}{0}, B), i A j)) Q (n))) +_{G} (K (i \in N, j \in N ⟼ if (i = K, if (j = L, \underset{˙}{0}, B), i A j)) Q (K))$
12		eqidd	$⊢ (K \in N \land L \in N \land Q \in R) \to (i \in N, j \in N ⟼ if (i = K, if (j = L, \underset{˙}{0}, B), i A j)) = (i \in N, j \in N ⟼ if (i = K, if (j = L, \underset{˙}{0}, B), i A j))$
13		fveq1	$⊢ r = Q \to r (K) = Q (K)$
14	13	eqeq1d	$⊢ r = Q \to (r (K) = L \leftrightarrow Q (K) = L)$
15	14 2	elrab2	$⊢ Q \in R \leftrightarrow (Q \in P \land Q (K) = L)$
16		eqeq2	$⊢ Q (K) = L \to (j = Q (K) \leftrightarrow j = L)$
17	16	adantl	$⊢ (Q \in P \land Q (K) = L) \to (j = Q (K) \leftrightarrow j = L)$
18	17	anbi2d	$⊢ (Q \in P \land Q (K) = L) \to ((i = K \land j = Q (K)) \leftrightarrow (i = K \land j = L))$
19	15 18	sylbi	$⊢ Q \in R \to ((i = K \land j = Q (K)) \leftrightarrow (i = K \land j = L))$
20	19	3ad2ant3	$⊢ (K \in N \land L \in N \land Q \in R) \to ((i = K \land j = Q (K)) \leftrightarrow (i = K \land j = L))$
21		iftrue	$⊢ i = K \to if (i = K, if (j = L, \underset{˙}{0}, B), i A j) = if (j = L, \underset{˙}{0}, B)$
22		iftrue	$⊢ j = L \to if (j = L, \underset{˙}{0}, B) = \underset{˙}{0}$
23	21 22	sylan9eq	$⊢ (i = K \land j = L) \to if (i = K, if (j = L, \underset{˙}{0}, B), i A j) = \underset{˙}{0}$
24	20 23	syl6bi	$⊢ (K \in N \land L \in N \land Q \in R) \to ((i = K \land j = Q (K)) \to if (i = K, if (j = L, \underset{˙}{0}, B), i A j) = \underset{˙}{0})$
25	24	imp	$⊢ ((K \in N \land L \in N \land Q \in R) \land (i = K \land j = Q (K))) \to if (i = K, if (j = L, \underset{˙}{0}, B), i A j) = \underset{˙}{0}$
26		simp1	$⊢ (K \in N \land L \in N \land Q \in R) \to K \in N$
27	1 2	gsummatr01lem1	$⊢ (Q \in R \land K \in N) \to Q (K) \in N$
28	27	ancoms	$⊢ (K \in N \land Q \in R) \to Q (K) \in N$
29	28	3adant2	$⊢ (K \in N \land L \in N \land Q \in R) \to Q (K) \in N$
30	3	fvexi	$⊢ \underset{˙}{0} \in V$
31	30	a1i	$⊢ (K \in N \land L \in N \land Q \in R) \to \underset{˙}{0} \in V$
32	12 25 26 29 31	ovmpod	$⊢ (K \in N \land L \in N \land Q \in R) \to K (i \in N, j \in N ⟼ if (i = K, if (j = L, \underset{˙}{0}, B), i A j)) Q (K) = \underset{˙}{0}$
33	32	3ad2ant3	$⊢ ((G \in CMnd \land N \in Fin) \land (\forall i \in N \forall j \in N i A j \in S \land B \in S) \land (K \in N \land L \in N \land Q \in R)) \to K (i \in N, j \in N ⟼ if (i = K, if (j = L, \underset{˙}{0}, B), i A j)) Q (K) = \underset{˙}{0}$
34	33	oveq2d	$⊢ ((G \in CMnd \land N \in Fin) \land (\forall i \in N \forall j \in N i A j \in S \land B \in S) \land (K \in N \land L \in N \land Q \in R)) \to (\underset{n \in N ∖ \{K\}}{\sum_{G}}, (n (i \in N, j \in N ⟼ if (i = K, if (j = L, \underset{˙}{0}, B), i A j)) Q (n))) +_{G} (K (i \in N, j \in N ⟼ if (i = K, if (j = L, \underset{˙}{0}, B), i A j)) Q (K)) = (\underset{n \in N ∖ \{K\}}{\sum_{G}}, (n (i \in N, j \in N ⟼ if (i = K, if (j = L, \underset{˙}{0}, B), i A j)) Q (n))) +_{G} \underset{˙}{0}$
35		cmnmnd	$⊢ G \in CMnd \to G \in Mnd$
36	35	adantr	$⊢ (G \in CMnd \land N \in Fin) \to G \in Mnd$
37	36	3ad2ant1	$⊢ ((G \in CMnd \land N \in Fin) \land (\forall i \in N \forall j \in N i A j \in S \land B \in S) \land (K \in N \land L \in N \land Q \in R)) \to G \in Mnd$
38		eqid	$⊢ {Base}_{G} = {Base}_{G}$
39		simp1l	$⊢ ((G \in CMnd \land N \in Fin) \land (\forall i \in N \forall j \in N i A j \in S \land B \in S) \land (K \in N \land L \in N \land Q \in R)) \to G \in CMnd$
40		diffi	$⊢ N \in Fin \to N ∖ \{K\} \in Fin$
41	40	adantl	$⊢ (G \in CMnd \land N \in Fin) \to N ∖ \{K\} \in Fin$
42	41	3ad2ant1	$⊢ ((G \in CMnd \land N \in Fin) \land (\forall i \in N \forall j \in N i A j \in S \land B \in S) \land (K \in N \land L \in N \land Q \in R)) \to N ∖ \{K\} \in Fin$
43		eqidd	$⊢ ((K \in N \land L \in N \land Q \in R) \land n \in (N ∖ \{K\})) \to (i \in N, j \in N ⟼ if (i = K, if (j = L, \underset{˙}{0}, B), i A j)) = (i \in N, j \in N ⟼ if (i = K, if (j = L, \underset{˙}{0}, B), i A j))$
44		eqeq1	$⊢ i = n \to (i = K \leftrightarrow n = K)$
45	44	adantr	$⊢ (i = n \land j = Q (n)) \to (i = K \leftrightarrow n = K)$
46		eqeq1	$⊢ j = Q (n) \to (j = L \leftrightarrow Q (n) = L)$
47	46	ifbid	$⊢ j = Q (n) \to if (j = L, \underset{˙}{0}, B) = if (Q (n) = L, \underset{˙}{0}, B)$
48	47	adantl	$⊢ (i = n \land j = Q (n)) \to if (j = L, \underset{˙}{0}, B) = if (Q (n) = L, \underset{˙}{0}, B)$
49		oveq12	$⊢ (i = n \land j = Q (n)) \to i A j = n A Q (n)$
50	45 48 49	ifbieq12d	$⊢ (i = n \land j = Q (n)) \to if (i = K, if (j = L, \underset{˙}{0}, B), i A j) = if (n = K, if (Q (n) = L, \underset{˙}{0}, B), n A Q (n))$
51		eldifsni	$⊢ n \in (N ∖ \{K\}) \to n \neq K$
52	51	neneqd	$⊢ n \in (N ∖ \{K\}) \to \neg n = K$
53	52	iffalsed	$⊢ n \in (N ∖ \{K\}) \to if (n = K, if (Q (n) = L, \underset{˙}{0}, B), n A Q (n)) = n A Q (n)$
54	53	adantl	$⊢ ((K \in N \land L \in N \land Q \in R) \land n \in (N ∖ \{K\})) \to if (n = K, if (Q (n) = L, \underset{˙}{0}, B), n A Q (n)) = n A Q (n)$
55	50 54	sylan9eqr	$⊢ (((K \in N \land L \in N \land Q \in R) \land n \in (N ∖ \{K\})) \land (i = n \land j = Q (n))) \to if (i = K, if (j = L, \underset{˙}{0}, B), i A j) = n A Q (n)$
56		eldifi	$⊢ n \in (N ∖ \{K\}) \to n \in N$
57	56	adantl	$⊢ ((K \in N \land L \in N \land Q \in R) \land n \in (N ∖ \{K\})) \to n \in N$
58		simp3	$⊢ (K \in N \land L \in N \land Q \in R) \to Q \in R$
59	1 2	gsummatr01lem1	$⊢ (Q \in R \land n \in N) \to Q (n) \in N$
60	58 56 59	syl2an	$⊢ ((K \in N \land L \in N \land Q \in R) \land n \in (N ∖ \{K\})) \to Q (n) \in N$
61		ovexd	$⊢ ((K \in N \land L \in N \land Q \in R) \land n \in (N ∖ \{K\})) \to n A Q (n) \in V$
62	43 55 57 60 61	ovmpod	$⊢ ((K \in N \land L \in N \land Q \in R) \land n \in (N ∖ \{K\})) \to n (i \in N, j \in N ⟼ if (i = K, if (j = L, \underset{˙}{0}, B), i A j)) Q (n) = n A Q (n)$
63	62	3ad2antl3	$⊢ (((G \in CMnd \land N \in Fin) \land (\forall i \in N \forall j \in N i A j \in S \land B \in S) \land (K \in N \land L \in N \land Q \in R)) \land n \in (N ∖ \{K\})) \to n (i \in N, j \in N ⟼ if (i = K, if (j = L, \underset{˙}{0}, B), i A j)) Q (n) = n A Q (n)$
64	4	eleq2i	$⊢ i A j \in S \leftrightarrow i A j \in {Base}_{G}$
65	64	2ralbii	$⊢ \forall i \in N \forall j \in N i A j \in S \leftrightarrow \forall i \in N \forall j \in N i A j \in {Base}_{G}$
66	1 2	gsummatr01lem2	$⊢ (Q \in R \land n \in N) \to (\forall i \in N \forall j \in N i A j \in {Base}_{G} \to n A Q (n) \in {Base}_{G})$
67	65 66	syl5bi	$⊢ (Q \in R \land n \in N) \to (\forall i \in N \forall j \in N i A j \in S \to n A Q (n) \in {Base}_{G})$
68	58 56 67	syl2anr	$⊢ (n \in (N ∖ \{K\}) \land (K \in N \land L \in N \land Q \in R)) \to (\forall i \in N \forall j \in N i A j \in S \to n A Q (n) \in {Base}_{G})$
69	68	ex	$⊢ n \in (N ∖ \{K\}) \to ((K \in N \land L \in N \land Q \in R) \to (\forall i \in N \forall j \in N i A j \in S \to n A Q (n) \in {Base}_{G}))$
70	69	com13	$⊢ \forall i \in N \forall j \in N i A j \in S \to ((K \in N \land L \in N \land Q \in R) \to (n \in (N ∖ \{K\}) \to n A Q (n) \in {Base}_{G}))$
71	70	adantr	$⊢ (\forall i \in N \forall j \in N i A j \in S \land B \in S) \to ((K \in N \land L \in N \land Q \in R) \to (n \in (N ∖ \{K\}) \to n A Q (n) \in {Base}_{G}))$
72	71	imp	$⊢ ((\forall i \in N \forall j \in N i A j \in S \land B \in S) \land (K \in N \land L \in N \land Q \in R)) \to (n \in (N ∖ \{K\}) \to n A Q (n) \in {Base}_{G})$
73	72	3adant1	$⊢ ((G \in CMnd \land N \in Fin) \land (\forall i \in N \forall j \in N i A j \in S \land B \in S) \land (K \in N \land L \in N \land Q \in R)) \to (n \in (N ∖ \{K\}) \to n A Q (n) \in {Base}_{G})$
74	73	imp	$⊢ (((G \in CMnd \land N \in Fin) \land (\forall i \in N \forall j \in N i A j \in S \land B \in S) \land (K \in N \land L \in N \land Q \in R)) \land n \in (N ∖ \{K\})) \to n A Q (n) \in {Base}_{G}$
75	63 74	eqeltrd	$⊢ (((G \in CMnd \land N \in Fin) \land (\forall i \in N \forall j \in N i A j \in S \land B \in S) \land (K \in N \land L \in N \land Q \in R)) \land n \in (N ∖ \{K\})) \to n (i \in N, j \in N ⟼ if (i = K, if (j = L, \underset{˙}{0}, B), i A j)) Q (n) \in {Base}_{G}$
76	75	ralrimiva	$⊢ ((G \in CMnd \land N \in Fin) \land (\forall i \in N \forall j \in N i A j \in S \land B \in S) \land (K \in N \land L \in N \land Q \in R)) \to \forall n \in (N ∖ \{K\}) n (i \in N, j \in N ⟼ if (i = K, if (j = L, \underset{˙}{0}, B), i A j)) Q (n) \in {Base}_{G}$
77	38 39 42 76	gsummptcl	$⊢ ((G \in CMnd \land N \in Fin) \land (\forall i \in N \forall j \in N i A j \in S \land B \in S) \land (K \in N \land L \in N \land Q \in R)) \to \underset{n \in N ∖ \{K\}}{\sum_{G}} (n (i \in N, j \in N ⟼ if (i = K, if (j = L, \underset{˙}{0}, B), i A j)) Q (n)) \in {Base}_{G}$
78		eqid	$⊢ +_{G} = +_{G}$
79	38 78 3	mndrid	$⊢ (G \in Mnd \land \underset{n \in N ∖ \{K\}}{\sum_{G}} (n (i \in N, j \in N ⟼ if (i = K, if (j = L, \underset{˙}{0}, B), i A j)) Q (n)) \in {Base}_{G}) \to (\underset{n \in N ∖ \{K\}}{\sum_{G}}, (n (i \in N, j \in N ⟼ if (i = K, if (j = L, \underset{˙}{0}, B), i A j)) Q (n))) +_{G} \underset{˙}{0} = \underset{n \in N ∖ \{K\}}{\sum_{G}} (n (i \in N, j \in N ⟼ if (i = K, if (j = L, \underset{˙}{0}, B), i A j)) Q (n))$
80	37 77 79	syl2anc	$⊢ ((G \in CMnd \land N \in Fin) \land (\forall i \in N \forall j \in N i A j \in S \land B \in S) \land (K \in N \land L \in N \land Q \in R)) \to (\underset{n \in N ∖ \{K\}}{\sum_{G}}, (n (i \in N, j \in N ⟼ if (i = K, if (j = L, \underset{˙}{0}, B), i A j)) Q (n))) +_{G} \underset{˙}{0} = \underset{n \in N ∖ \{K\}}{\sum_{G}} (n (i \in N, j \in N ⟼ if (i = K, if (j = L, \underset{˙}{0}, B), i A j)) Q (n))$
81	1 2 3 4	gsummatr01lem4	$⊢ (((G \in CMnd \land N \in Fin) \land (\forall i \in N \forall j \in N i A j \in S \land B \in S) \land (K \in N \land L \in N \land Q \in R)) \land n \in (N ∖ \{K\})) \to n (i \in N, j \in N ⟼ if (i = K, if (j = L, \underset{˙}{0}, B), i A j)) Q (n) = n (i \in (N ∖ \{K\}), j \in (N ∖ \{L\}) ⟼ i A j) Q (n)$
82	81	mpteq2dva	$⊢ ((G \in CMnd \land N \in Fin) \land (\forall i \in N \forall j \in N i A j \in S \land B \in S) \land (K \in N \land L \in N \land Q \in R)) \to (n \in (N ∖ \{K\}) ⟼ n (i \in N, j \in N ⟼ if (i = K, if (j = L, \underset{˙}{0}, B), i A j)) Q (n)) = (n \in (N ∖ \{K\}) ⟼ n (i \in (N ∖ \{K\}), j \in (N ∖ \{L\}) ⟼ i A j) Q (n))$
83	82	oveq2d	$⊢ ((G \in CMnd \land N \in Fin) \land (\forall i \in N \forall j \in N i A j \in S \land B \in S) \land (K \in N \land L \in N \land Q \in R)) \to \underset{n \in N ∖ \{K\}}{\sum_{G}} (n (i \in N, j \in N ⟼ if (i = K, if (j = L, \underset{˙}{0}, B), i A j)) Q (n)) = \underset{n \in N ∖ \{K\}}{\sum_{G}} (n (i \in (N ∖ \{K\}), j \in (N ∖ \{L\}) ⟼ i A j) Q (n))$
84	34 80 83	3eqtrd	$⊢ ((G \in CMnd \land N \in Fin) \land (\forall i \in N \forall j \in N i A j \in S \land B \in S) \land (K \in N \land L \in N \land Q \in R)) \to (\underset{n \in N ∖ \{K\}}{\sum_{G}}, (n (i \in N, j \in N ⟼ if (i = K, if (j = L, \underset{˙}{0}, B), i A j)) Q (n))) +_{G} (K (i \in N, j \in N ⟼ if (i = K, if (j = L, \underset{˙}{0}, B), i A j)) Q (K)) = \underset{n \in N ∖ \{K\}}{\sum_{G}} (n (i \in (N ∖ \{K\}), j \in (N ∖ \{L\}) ⟼ i A j) Q (n))$
85	10 11 84	3eqtrd	$⊢ ((G \in CMnd \land N \in Fin) \land (\forall i \in N \forall j \in N i A j \in S \land B \in S) \land (K \in N \land L \in N \land Q \in R)) \to \underset{n \in N}{\sum_{G}} (n (i \in N, j \in N ⟼ if (i = K, if (j = L, \underset{˙}{0}, B), i A j)) Q (n)) = \underset{n \in N ∖ \{K\}}{\sum_{G}} (n (i \in (N ∖ \{K\}), j \in (N ∖ \{L\}) ⟼ i A j) Q (n))$

Metamath Proof Explorer

Theorem gsummatr01

Proof