Theorem smadiadetlem2

Description: Lemma 2 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 itself. (Contributed by AV, 31-Dec-2018)

	Ref	Expression
Hypotheses	marep01ma.a	$$⊢A=N\mathrm{Mat}R$$
	marep01ma.b	$$⊢B={\mathrm{Base}}_A$$
	marep01ma.r	$$⊢R\in \mathrm{CRing}$$
	marep01ma.0	$$⊢\underset{\dot{}}{0}=0_R$$
	marep01ma.1	$$⊢\underset{\dot{}}{1}=1_R$$
	smadiadetlem.p	$$⊢P={\mathrm{Base}}_{\mathrm{SymGrp}\left(N\right)}$$
	smadiadetlem.g	$$⊢G={\mathrm{mulGrp}}_R$$
	madetminlem.y	$$⊢Y=\mathrm{\mathbb{Z}RHom}\left(R\right)$$
	madetminlem.s	$$⊢S=\mathrm{pmSgn}\left(N\right)$$
	madetminlem.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
Assertion	smadiadetlem2	$$⊢\left(M\in B\wedge K\in N\right)\to \underset{p\in P\setminus \left\{q\in P|q\left(K\right)=K\right\}}{{\sum }_R}\left(\left(Y\circ S\right)\left(p\right)\underset{\dot{}}{·}\left(\underset{n\in N}{{\sum }_G},\left(n\left(i\in N,j\in N⟼if\left(i=K,if\left(j=K,\underset{\dot{}}{1},\underset{\dot{}}{0}\right),iMj\right)\right)p\left(n\right)\right)\right)\right)=\underset{\dot{}}{0}$$

Proof

Step	Hyp	Ref	Expression
1		marep01ma.a	$$⊢A=N\mathrm{Mat}R$$
2		marep01ma.b	$$⊢B={\mathrm{Base}}_A$$
3		marep01ma.r	$$⊢R\in \mathrm{CRing}$$
4		marep01ma.0	$$⊢\underset{\dot{}}{0}=0_R$$
5		marep01ma.1	$$⊢\underset{\dot{}}{1}=1_R$$
6		smadiadetlem.p	$$⊢P={\mathrm{Base}}_{\mathrm{SymGrp}\left(N\right)}$$
7		smadiadetlem.g	$$⊢G={\mathrm{mulGrp}}_R$$
8		madetminlem.y	$$⊢Y=\mathrm{\mathbb{Z}RHom}\left(R\right)$$
9		madetminlem.s	$$⊢S=\mathrm{pmSgn}\left(N\right)$$
10		madetminlem.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
11	1 2 3 4 5 6 7 8 9 10	smadiadetlem1a	$$⊢\left(M\in B\wedge K\in N\wedge K\in N\right)\to \underset{p\in P\setminus \left\{q\in P|q\left(K\right)=K\right\}}{{\sum }_R}\left(\left(Y\circ S\right)\left(p\right)\underset{\dot{}}{·}\left(\underset{n\in N}{{\sum }_G},\left(n\left(i\in N,j\in N⟼if\left(i=K,if\left(j=K,\underset{\dot{}}{1},\underset{\dot{}}{0}\right),iMj\right)\right)p\left(n\right)\right)\right)\right)=\underset{\dot{}}{0}$$
12	11	3anidm23	$$⊢\left(M\in B\wedge K\in N\right)\to \underset{p\in P\setminus \left\{q\in P|q\left(K\right)=K\right\}}{{\sum }_R}\left(\left(Y\circ S\right)\left(p\right)\underset{\dot{}}{·}\left(\underset{n\in N}{{\sum }_G},\left(n\left(i\in N,j\in N⟼if\left(i=K,if\left(j=K,\underset{\dot{}}{1},\underset{\dot{}}{0}\right),iMj\right)\right)p\left(n\right)\right)\right)\right)=\underset{\dot{}}{0}$$