smadiadetlem1a

Description: Lemma 1a for smadiadet : The summands of the Leibniz' formula vanish for all permutations fixing the index of the row containing the 0's and the 1 to the column with the 1. (Contributed by AV, 3-Jan-2019)

	Ref	Expression
Hypotheses	marep01ma.a	$⊢ A = N Mat R$
	marep01ma.b	$⊢ B = {Base}_{A}$
	marep01ma.r	$⊢ R \in CRing$
	marep01ma.0	$⊢ \underset{˙}{0} = 0_{R}$
	marep01ma.1	$⊢ \underset{˙}{1} = 1_{R}$
	smadiadetlem.p	$⊢ P = {Base}_{SymGrp (N)}$
	smadiadetlem.g	$⊢ G = {mulGrp}_{R}$
	madetminlem.y	$⊢ Y = ℤRHom (R)$
	madetminlem.s	$⊢ S = pmSgn (N)$
	madetminlem.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
Assertion	smadiadetlem1a	$⊢ (M \in B \land K \in N \land L \in N) \to \underset{p \in P ∖ \{q \in P \| q (K) = L\}}{\sum_{R}} ((Y \circ S) (p) \underset{˙}{\cdot} (\underset{n \in N}{\sum_{G}}, (n (i \in N, j \in N ⟼ if (i = K, if (j = L, \underset{˙}{1}, \underset{˙}{0}), i M j)) p (n)))) = \underset{˙}{0}$

Proof

Step	Hyp	Ref	Expression
1		marep01ma.a	$⊢ A = N Mat R$
2		marep01ma.b	$⊢ B = {Base}_{A}$
3		marep01ma.r	$⊢ R \in CRing$
4		marep01ma.0	$⊢ \underset{˙}{0} = 0_{R}$
5		marep01ma.1	$⊢ \underset{˙}{1} = 1_{R}$
6		smadiadetlem.p	$⊢ P = {Base}_{SymGrp (N)}$
7		smadiadetlem.g	$⊢ G = {mulGrp}_{R}$
8		madetminlem.y	$⊢ Y = ℤRHom (R)$
9		madetminlem.s	$⊢ S = pmSgn (N)$
10		madetminlem.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
11	1 2 3 4 5 6 7	smadiadetlem0	$⊢ (M \in B \land K \in N \land L \in N) \to (p \in (P ∖ \{q \in P \| q (K) = L\}) \to \underset{n \in N}{\sum_{G}} (n (i \in N, j \in N ⟼ if (i = K, if (j = L, \underset{˙}{1}, \underset{˙}{0}), i M j)) p (n)) = \underset{˙}{0})$
12	11	imp	$⊢ ((M \in B \land K \in N \land L \in N) \land p \in (P ∖ \{q \in P \| q (K) = L\})) \to \underset{n \in N}{\sum_{G}} (n (i \in N, j \in N ⟼ if (i = K, if (j = L, \underset{˙}{1}, \underset{˙}{0}), i M j)) p (n)) = \underset{˙}{0}$
13	12	oveq2d	$⊢ ((M \in B \land K \in N \land L \in N) \land p \in (P ∖ \{q \in P \| q (K) = L\})) \to (Y \circ S) (p) \underset{˙}{\cdot} (\underset{n \in N}{\sum_{G}}, (n (i \in N, j \in N ⟼ if (i = K, if (j = L, \underset{˙}{1}, \underset{˙}{0}), i M j)) p (n))) = (Y \circ S) (p) \underset{˙}{\cdot} \underset{˙}{0}$
14	13	mpteq2dva	$⊢ (M \in B \land K \in N \land L \in N) \to (p \in (P ∖ \{q \in P \| q (K) = L\}) ⟼ (Y \circ S) (p) \underset{˙}{\cdot} (\underset{n \in N}{\sum_{G}}, (n (i \in N, j \in N ⟼ if (i = K, if (j = L, \underset{˙}{1}, \underset{˙}{0}), i M j)) p (n)))) = (p \in (P ∖ \{q \in P \| q (K) = L\}) ⟼ (Y \circ S) (p) \underset{˙}{\cdot} \underset{˙}{0})$
15	14	oveq2d	$⊢ (M \in B \land K \in N \land L \in N) \to \underset{p \in P ∖ \{q \in P \| q (K) = L\}}{\sum_{R}} ((Y \circ S) (p) \underset{˙}{\cdot} (\underset{n \in N}{\sum_{G}}, (n (i \in N, j \in N ⟼ if (i = K, if (j = L, \underset{˙}{1}, \underset{˙}{0}), i M j)) p (n)))) = \underset{p \in P ∖ \{q \in P \| q (K) = L\}}{\sum_{R}} ((Y \circ S) (p) \underset{˙}{\cdot} \underset{˙}{0})$
16		crngring	$⊢ R \in CRing \to R \in Ring$
17	3 16	mp1i	$⊢ ((M \in B \land K \in N \land L \in N) \land p \in (P ∖ \{q \in P \| q (K) = L\})) \to R \in Ring$
18	1 2	matrcl	$⊢ M \in B \to (N \in Fin \land R \in V)$
19	18	simpld	$⊢ M \in B \to N \in Fin$
20	19	3ad2ant1	$⊢ (M \in B \land K \in N \land L \in N) \to N \in Fin$
21	20	adantr	$⊢ ((M \in B \land K \in N \land L \in N) \land p \in (P ∖ \{q \in P \| q (K) = L\})) \to N \in Fin$
22		eldifi	$⊢ p \in (P ∖ \{q \in P \| q (K) = L\}) \to p \in P$
23	22	adantl	$⊢ ((M \in B \land K \in N \land L \in N) \land p \in (P ∖ \{q \in P \| q (K) = L\})) \to p \in P$
24	6 9 8	zrhcopsgnelbas	$⊢ (R \in Ring \land N \in Fin \land p \in P) \to (Y \circ S) (p) \in {Base}_{R}$
25	17 21 23 24	syl3anc	$⊢ ((M \in B \land K \in N \land L \in N) \land p \in (P ∖ \{q \in P \| q (K) = L\})) \to (Y \circ S) (p) \in {Base}_{R}$
26		eqid	$⊢ {Base}_{R} = {Base}_{R}$
27	26 10 4	ringrz	$⊢ (R \in Ring \land (Y \circ S) (p) \in {Base}_{R}) \to (Y \circ S) (p) \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}$
28	17 25 27	syl2anc	$⊢ ((M \in B \land K \in N \land L \in N) \land p \in (P ∖ \{q \in P \| q (K) = L\})) \to (Y \circ S) (p) \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}$
29	28	mpteq2dva	$⊢ (M \in B \land K \in N \land L \in N) \to (p \in (P ∖ \{q \in P \| q (K) = L\}) ⟼ (Y \circ S) (p) \underset{˙}{\cdot} \underset{˙}{0}) = (p \in (P ∖ \{q \in P \| q (K) = L\}) ⟼ \underset{˙}{0})$
30	29	oveq2d	$⊢ (M \in B \land K \in N \land L \in N) \to \underset{p \in P ∖ \{q \in P \| q (K) = L\}}{\sum_{R}} ((Y \circ S) (p) \underset{˙}{\cdot} \underset{˙}{0}) = \underset{p \in P ∖ \{q \in P \| q (K) = L\}}{\sum_{R}} \underset{˙}{0}$
31		ringmnd	$⊢ R \in Ring \to R \in Mnd$
32	3 16 31	mp2b	$⊢ R \in Mnd$
33	6	fvexi	$⊢ P \in V$
34		difexg	$⊢ P \in V \to P ∖ \{q \in P \| q (K) = L\} \in V$
35	33 34	mp1i	$⊢ (M \in B \land K \in N \land L \in N) \to P ∖ \{q \in P \| q (K) = L\} \in V$
36	4	gsumz	$⊢ (R \in Mnd \land P ∖ \{q \in P \| q (K) = L\} \in V) \to \underset{p \in P ∖ \{q \in P \| q (K) = L\}}{\sum_{R}} \underset{˙}{0} = \underset{˙}{0}$
37	32 35 36	sylancr	$⊢ (M \in B \land K \in N \land L \in N) \to \underset{p \in P ∖ \{q \in P \| q (K) = L\}}{\sum_{R}} \underset{˙}{0} = \underset{˙}{0}$
38	15 30 37	3eqtrd	$⊢ (M \in B \land K \in N \land L \in N) \to \underset{p \in P ∖ \{q \in P \| q (K) = L\}}{\sum_{R}} ((Y \circ S) (p) \underset{˙}{\cdot} (\underset{n \in N}{\sum_{G}}, (n (i \in N, j \in N ⟼ if (i = K, if (j = L, \underset{˙}{1}, \underset{˙}{0}), i M j)) p (n)))) = \underset{˙}{0}$

Metamath Proof Explorer

Theorem smadiadetlem1a

Proof