gsummatr01lem3

	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	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))$

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		eqid	$⊢ {Base}_{G} = {Base}_{G}$
6		eqid	$⊢ +_{G} = +_{G}$
7		simpl	$⊢ (G \in CMnd \land N \in Fin) \to G \in CMnd$
8	7	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 CMnd$
9		diffi	$⊢ N \in Fin \to N ∖ \{K\} \in Fin$
10	9	adantl	$⊢ (G \in CMnd \land N \in Fin) \to N ∖ \{K\} \in Fin$
11	10	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$
12		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))$
13		eqeq1	$⊢ i = n \to (i = K \leftrightarrow n = K)$
14	13	adantr	$⊢ (i = n \land j = Q (n)) \to (i = K \leftrightarrow n = K)$
15		eqeq1	$⊢ j = Q (n) \to (j = L \leftrightarrow Q (n) = L)$
16	15	ifbid	$⊢ j = Q (n) \to if (j = L, \underset{˙}{0}, B) = if (Q (n) = L, \underset{˙}{0}, B)$
17	16	adantl	$⊢ (i = n \land j = Q (n)) \to if (j = L, \underset{˙}{0}, B) = if (Q (n) = L, \underset{˙}{0}, B)$
18		oveq12	$⊢ (i = n \land j = Q (n)) \to i A j = n A Q (n)$
19	14 17 18	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))$
20		eldifsni	$⊢ n \in (N ∖ \{K\}) \to n \neq K$
21	20	neneqd	$⊢ n \in (N ∖ \{K\}) \to \neg n = K$
22	21	iffalsed	$⊢ n \in (N ∖ \{K\}) \to if (n = K, if (Q (n) = L, \underset{˙}{0}, B), n A Q (n)) = n A Q (n)$
23	22	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)$
24	19 23	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)$
25		eldifi	$⊢ n \in (N ∖ \{K\}) \to n \in N$
26	25	adantl	$⊢ ((K \in N \land L \in N \land Q \in R) \land n \in (N ∖ \{K\})) \to n \in N$
27	1 2	gsummatr01lem1	$⊢ (Q \in R \land n \in N) \to Q (n) \in N$
28	27	expcom	$⊢ n \in N \to (Q \in R \to Q (n) \in N)$
29	28 25	syl11	$⊢ Q \in R \to (n \in (N ∖ \{K\}) \to Q (n) \in N)$
30	29	3ad2ant3	$⊢ (K \in N \land L \in N \land Q \in R) \to (n \in (N ∖ \{K\}) \to Q (n) \in N)$
31	30	imp	$⊢ ((K \in N \land L \in N \land Q \in R) \land n \in (N ∖ \{K\})) \to Q (n) \in N$
32		ovexd	$⊢ ((K \in N \land L \in N \land Q \in R) \land n \in (N ∖ \{K\})) \to n A Q (n) \in V$
33	12 24 26 31 32	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)$
34	33	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)$
35	4	eleq2i	$⊢ i A j \in S \leftrightarrow i A j \in {Base}_{G}$
36	35	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}$
37	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})$
38	25 37	sylan2	$⊢ (Q \in R \land n \in (N ∖ \{K\})) \to (\forall i \in N \forall j \in N i A j \in {Base}_{G} \to n A Q (n) \in {Base}_{G})$
39	38	ex	$⊢ Q \in R \to (n \in (N ∖ \{K\}) \to (\forall i \in N \forall j \in N i A j \in {Base}_{G} \to n A Q (n) \in {Base}_{G}))$
40	39	3ad2ant3	$⊢ (K \in N \land L \in N \land Q \in R) \to (n \in (N ∖ \{K\}) \to (\forall i \in N \forall j \in N i A j \in {Base}_{G} \to n A Q (n) \in {Base}_{G}))$
41	40	com3r	$⊢ \forall i \in N \forall j \in N i A j \in {Base}_{G} \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}))$
42	36 41	sylbi	$⊢ \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}))$
43	42	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}))$
44	43	imp31	$⊢ (((\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}$
45	44	3adantl1	$⊢ (((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}$
46	34 45	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}$
47		simp31	$⊢ ((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 \in N$
48		neldifsnd	$⊢ ((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 \neg K \in (N ∖ \{K\})$
49		eqidd	$⊢ (B \in S \land (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))$
50		iftrue	$⊢ i = K \to if (i = K, if (j = L, \underset{˙}{0}, B), i A j) = if (j = L, \underset{˙}{0}, B)$
51		eqeq1	$⊢ j = Q (K) \to (j = L \leftrightarrow Q (K) = L)$
52	51	ifbid	$⊢ j = Q (K) \to if (j = L, \underset{˙}{0}, B) = if (Q (K) = L, \underset{˙}{0}, B)$
53	50 52	sylan9eq	$⊢ (i = K \land j = Q (K)) \to if (i = K, if (j = L, \underset{˙}{0}, B), i A j) = if (Q (K) = L, \underset{˙}{0}, B)$
54	53	adantl	$⊢ ((B \in S \land (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) = if (Q (K) = L, \underset{˙}{0}, B)$
55		simpr1	$⊢ (B \in S \land (K \in N \land L \in N \land Q \in R)) \to K \in N$
56	1 2	gsummatr01lem1	$⊢ (Q \in R \land K \in N) \to Q (K) \in N$
57	56	ancoms	$⊢ (K \in N \land Q \in R) \to Q (K) \in N$
58	57	3adant2	$⊢ (K \in N \land L \in N \land Q \in R) \to Q (K) \in N$
59	58	adantl	$⊢ (B \in S \land (K \in N \land L \in N \land Q \in R)) \to Q (K) \in N$
60	3	fvexi	$⊢ \underset{˙}{0} \in V$
61		simpl	$⊢ (B \in S \land (K \in N \land L \in N \land Q \in R)) \to B \in S$
62		ifexg	$⊢ (\underset{˙}{0} \in V \land B \in S) \to if (Q (K) = L, \underset{˙}{0}, B) \in V$
63	60 61 62	sylancr	$⊢ (B \in S \land (K \in N \land L \in N \land Q \in R)) \to if (Q (K) = L, \underset{˙}{0}, B) \in V$
64	49 54 55 59 63	ovmpod	$⊢ (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) = if (Q (K) = L, \underset{˙}{0}, B)$
65	64	adantll	$⊢ ((\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) = if (Q (K) = L, \underset{˙}{0}, B)$
66	65	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 K (i \in N, j \in N ⟼ if (i = K, if (j = L, \underset{˙}{0}, B), i A j)) Q (K) = if (Q (K) = L, \underset{˙}{0}, B)$
67		cmnmnd	$⊢ G \in CMnd \to G \in Mnd$
68	5 3	mndidcl	$⊢ G \in Mnd \to \underset{˙}{0} \in {Base}_{G}$
69	67 68	syl	$⊢ G \in CMnd \to \underset{˙}{0} \in {Base}_{G}$
70	69	adantr	$⊢ (G \in CMnd \land N \in Fin) \to \underset{˙}{0} \in {Base}_{G}$
71	70	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 \underset{˙}{0} \in {Base}_{G}$
72	4	eleq2i	$⊢ B \in S \leftrightarrow B \in {Base}_{G}$
73	72	bilani	$⊢ (\forall i \in N \forall j \in N i A j \in S \land B \in S) \to B \in {Base}_{G}$
74	73	3ad2ant2	$⊢ ((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 B \in {Base}_{G}$
75	71 74	ifcld	$⊢ ((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 if (Q (K) = L, \underset{˙}{0}, B) \in {Base}_{G}$
76	66 75	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)) \to K (i \in N, j \in N ⟼ if (i = K, if (j = L, \underset{˙}{0}, B), i A j)) Q (K) \in {Base}_{G}$
77		id	$⊢ n = K \to n = K$
78		fveq2	$⊢ n = K \to Q (n) = Q (K)$
79	77 78	oveq12d	$⊢ n = K \to n (i \in N, j \in N ⟼ if (i = K, if (j = L, \underset{˙}{0}, B), i A j)) Q (n) = K (i \in N, j \in N ⟼ if (i = K, if (j = L, \underset{˙}{0}, B), i A j)) Q (K)$
80	5 6 8 11 46 47 48 76 79	gsumunsn	$⊢ ((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))$

Metamath Proof Explorer

Theorem gsummatr01lem3

Proof