gsummatr01lem4

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

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		eqidd	$⊢ (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))$
6		eqeq1	$⊢ i = n \to (i = K \leftrightarrow n = K)$
7	6	adantr	$⊢ (i = n \land j = Q (n)) \to (i = K \leftrightarrow n = K)$
8		eqeq1	$⊢ j = Q (n) \to (j = L \leftrightarrow Q (n) = L)$
9	8	adantl	$⊢ (i = n \land j = Q (n)) \to (j = L \leftrightarrow Q (n) = L)$
10	9	ifbid	$⊢ (i = n \land j = Q (n)) \to if (j = L, \underset{˙}{0}, B) = if (Q (n) = L, \underset{˙}{0}, B)$
11		oveq12	$⊢ (i = n \land j = Q (n)) \to i A j = n A Q (n)$
12	7 10 11	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))$
13		eldifsni	$⊢ n \in (N ∖ \{K\}) \to n \neq K$
14	13	neneqd	$⊢ n \in (N ∖ \{K\}) \to \neg n = K$
15	14	iffalsed	$⊢ n \in (N ∖ \{K\}) \to if (n = K, if (Q (n) = L, \underset{˙}{0}, B), n A Q (n)) = n A Q (n)$
16	15	adantl	$⊢ (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)$
17	12 16	sylan9eqr	$⊢ ((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)$
18		eldifi	$⊢ n \in (N ∖ \{K\}) \to n \in N$
19	18	adantl	$⊢ (Q \in R \land n \in (N ∖ \{K\})) \to n \in N$
20	1 2	gsummatr01lem1	$⊢ (Q \in R \land n \in N) \to Q (n) \in N$
21	18 20	sylan2	$⊢ (Q \in R \land n \in (N ∖ \{K\})) \to Q (n) \in N$
22		ovexd	$⊢ (Q \in R \land n \in (N ∖ \{K\})) \to n A Q (n) \in V$
23	5 17 19 21 22	ovmpod	$⊢ (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)$
24	23	ex	$⊢ Q \in R \to (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))$
25	24	3ad2ant3	$⊢ (K \in N \land L \in N \land Q \in R) \to (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))$
26	25	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 \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))$
27	26	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 (i \in N, j \in N ⟼ if (i = K, if (j = L, \underset{˙}{0}, B), i A j)) Q (n) = n A Q (n)$
28		eqidd	$⊢ (((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 (i \in (N ∖ \{K\}), j \in (N ∖ \{L\}) ⟼ i A j) = (i \in (N ∖ \{K\}), j \in (N ∖ \{L\}) ⟼ i A j)$
29	11	adantl	$⊢ ((((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\})) \land (i = n \land j = Q (n))) \to i A j = n A Q (n)$
30		eqidd	$⊢ ((((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\})) \land i = n) \to N ∖ \{L\} = N ∖ \{L\}$
31		simpr	$⊢ (((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 \in (N ∖ \{K\})$
32		fveq1	$⊢ r = Q \to r (K) = Q (K)$
33	32	eqeq1d	$⊢ r = Q \to (r (K) = L \leftrightarrow Q (K) = L)$
34	33 2	elrab2	$⊢ Q \in R \leftrightarrow (Q \in P \land Q (K) = L)$
35		simpll	$⊢ ((Q \in P \land Q (K) = L) \land (L \in N \land K \in N)) \to Q \in P$
36		eqid	$⊢ SymGrp (N) = SymGrp (N)$
37	36 1	symgfv	$⊢ (Q \in P \land n \in N) \to Q (n) \in N$
38	35 18 37	syl2an	$⊢ (((Q \in P \land Q (K) = L) \land (L \in N \land K \in N)) \land n \in (N ∖ \{K\})) \to Q (n) \in N$
39	35	adantr	$⊢ (((Q \in P \land Q (K) = L) \land (L \in N \land K \in N)) \land n \in (N ∖ \{K\})) \to Q \in P$
40		simplrr	$⊢ (((Q \in P \land Q (K) = L) \land (L \in N \land K \in N)) \land n \in (N ∖ \{K\})) \to K \in N$
41	18	adantl	$⊢ (((Q \in P \land Q (K) = L) \land (L \in N \land K \in N)) \land n \in (N ∖ \{K\})) \to n \in N$
42	39 40 41	3jca	$⊢ (((Q \in P \land Q (K) = L) \land (L \in N \land K \in N)) \land n \in (N ∖ \{K\})) \to (Q \in P \land K \in N \land n \in N)$
43		simpllr	$⊢ (((Q \in P \land Q (K) = L) \land (L \in N \land K \in N)) \land n \in (N ∖ \{K\})) \to Q (K) = L$
44	13	adantl	$⊢ (((Q \in P \land Q (K) = L) \land (L \in N \land K \in N)) \land n \in (N ∖ \{K\})) \to n \neq K$
45	36 1	symgfvne	$⊢ (Q \in P \land K \in N \land n \in N) \to (Q (K) = L \to (n \neq K \to Q (n) \neq L))$
46	42 43 44 45	syl3c	$⊢ (((Q \in P \land Q (K) = L) \land (L \in N \land K \in N)) \land n \in (N ∖ \{K\})) \to Q (n) \neq L$
47	38 46	jca	$⊢ (((Q \in P \land Q (K) = L) \land (L \in N \land K \in N)) \land n \in (N ∖ \{K\})) \to (Q (n) \in N \land Q (n) \neq L)$
48	47	exp42	$⊢ (Q \in P \land Q (K) = L) \to (L \in N \to (K \in N \to (n \in (N ∖ \{K\}) \to (Q (n) \in N \land Q (n) \neq L))))$
49	34 48	sylbi	$⊢ Q \in R \to (L \in N \to (K \in N \to (n \in (N ∖ \{K\}) \to (Q (n) \in N \land Q (n) \neq L))))$
50	49	3imp31	$⊢ (K \in N \land L \in N \land Q \in R) \to (n \in (N ∖ \{K\}) \to (Q (n) \in N \land Q (n) \neq L))$
51	50	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 \in (N ∖ \{K\}) \to (Q (n) \in N \land Q (n) \neq L))$
52	51	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 (Q (n) \in N \land Q (n) \neq L)$
53		eldifsn	$⊢ Q (n) \in (N ∖ \{L\}) \leftrightarrow (Q (n) \in N \land Q (n) \neq L)$
54	52 53	sylibr	$⊢ (((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 Q (n) \in (N ∖ \{L\})$
55		ovexd	$⊢ (((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 V$
56		nfv	$⊢ Ⅎ i (G \in CMnd \land N \in Fin)$
57		nfra1	$⊢ Ⅎ i \forall i \in N \forall j \in N i A j \in S$
58		nfcv	$⊢ \underline{Ⅎ} i S$
59	58	nfel2	$⊢ Ⅎ i B \in S$
60	57 59	nfan	$⊢ Ⅎ i (\forall i \in N \forall j \in N i A j \in S \land B \in S)$
61		nfv	$⊢ Ⅎ i (K \in N \land L \in N \land Q \in R)$
62	56 60 61	nf3an	$⊢ Ⅎ i ((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))$
63		nfcv	$⊢ \underline{Ⅎ} i (N ∖ \{K\})$
64	63	nfel2	$⊢ Ⅎ i n \in (N ∖ \{K\})$
65	62 64	nfan	$⊢ Ⅎ i (((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\}))$
66		nfv	$⊢ Ⅎ j (G \in CMnd \land N \in Fin)$
67		nfra2w	$⊢ Ⅎ j \forall i \in N \forall j \in N i A j \in S$
68		nfcv	$⊢ \underline{Ⅎ} j S$
69	68	nfel2	$⊢ Ⅎ j B \in S$
70	67 69	nfan	$⊢ Ⅎ j (\forall i \in N \forall j \in N i A j \in S \land B \in S)$
71		nfv	$⊢ Ⅎ j (K \in N \land L \in N \land Q \in R)$
72	66 70 71	nf3an	$⊢ Ⅎ j ((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))$
73		nfcv	$⊢ \underline{Ⅎ} j (N ∖ \{K\})$
74	73	nfel2	$⊢ Ⅎ j n \in (N ∖ \{K\})$
75	72 74	nfan	$⊢ Ⅎ j (((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\}))$
76		nfcv	$⊢ \underline{Ⅎ} j n$
77		nfcv	$⊢ \underline{Ⅎ} i Q (n)$
78		nfcv	$⊢ \underline{Ⅎ} i (n A Q (n))$
79		nfcv	$⊢ \underline{Ⅎ} j (n A Q (n))$
80	28 29 30 31 54 55 65 75 76 77 78 79	ovmpodxf	$⊢ (((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 ∖ \{K\}), j \in (N ∖ \{L\}) ⟼ i A j) Q (n) = n A Q (n)$
81	27 80	eqtr4d	$⊢ (((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)$

Metamath Proof Explorer

Theorem gsummatr01lem4

Proof