Theorem smadiadetlem0

Description: Lemma 0 for smadiadet : The products 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\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$$
Assertion	smadiadetlem0	$$⊢\left(M\in B\wedge K\in N\wedge L\in N\right)\to \left(Q\in \left(P\setminus \left\{q\in P|q\left(K\right)=L\right\}\right)\to \underset{n\in N}{{\sum }_G}\left(n\left(i\in N,j\in N⟼if\left(i=K,if\left(j=L,\underset{\dot{}}{1},\underset{\dot{}}{0}\right),iMj\right)\right)Q\left(n\right)\right)=\underset{\dot{}}{0}\right)$$

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	3	a1i	$$⊢\left(\left(M\in B\wedge K\in N\wedge L\in N\right)\wedge Q\in \left(P\setminus \left\{q\in P|q\left(K\right)=L\right\}\right)\right)\to R\in \mathrm{CRing}$$
9	1 2	matrcl	$$⊢M\in B\to \left(N\in \mathrm{Fin}\wedge R\in \mathrm{V}\right)$$
10	9	simpld	$$⊢M\in B\to N\in \mathrm{Fin}$$
11	10	3ad2ant1	$$⊢\left(M\in B\wedge K\in N\wedge L\in N\right)\to N\in \mathrm{Fin}$$
12	11	adantr	$$⊢\left(\left(M\in B\wedge K\in N\wedge L\in N\right)\wedge Q\in \left(P\setminus \left\{q\in P|q\left(K\right)=L\right\}\right)\right)\to N\in \mathrm{Fin}$$
13		crngring	$$⊢R\in \mathrm{CRing}\to R\in \mathrm{Ring}$$
14	3 13	mp1i	$$⊢\left(\left(M\in B\wedge K\in N\wedge L\in N\right)\wedge Q\in \left(P\setminus \left\{q\in P|q\left(K\right)=L\right\}\right)\right)\to R\in \mathrm{Ring}$$
15		eldifi	$$⊢Q\in \left(P\setminus \left\{q\in P|q\left(K\right)=L\right\}\right)\to Q\in P$$
16	15	adantl	$$⊢\left(\left(M\in B\wedge K\in N\wedge L\in N\right)\wedge Q\in \left(P\setminus \left\{q\in P|q\left(K\right)=L\right\}\right)\right)\to Q\in P$$
17	1 2 3 4 5	marep01ma	$$⊢M\in B\to \left(i\in N,j\in N⟼if\left(i=K,if\left(j=L,\underset{\dot{}}{1},\underset{\dot{}}{0}\right),iMj\right)\right)\in B$$
18	17	3ad2ant1	$$⊢\left(M\in B\wedge K\in N\wedge L\in N\right)\to \left(i\in N,j\in N⟼if\left(i=K,if\left(j=L,\underset{\dot{}}{1},\underset{\dot{}}{0}\right),iMj\right)\right)\in B$$
19	18	adantr	$$⊢\left(\left(M\in B\wedge K\in N\wedge L\in N\right)\wedge Q\in \left(P\setminus \left\{q\in P|q\left(K\right)=L\right\}\right)\right)\to \left(i\in N,j\in N⟼if\left(i=K,if\left(j=L,\underset{\dot{}}{1},\underset{\dot{}}{0}\right),iMj\right)\right)\in B$$
20	1 2 6	matepm2cl	$$⊢\left(R\in \mathrm{Ring}\wedge Q\in P\wedge \left(i\in N,j\in N⟼if\left(i=K,if\left(j=L,\underset{\dot{}}{1},\underset{\dot{}}{0}\right),iMj\right)\right)\in B\right)\to \forall m\in Nm\left(i\in N,j\in N⟼if\left(i=K,if\left(j=L,\underset{\dot{}}{1},\underset{\dot{}}{0}\right),iMj\right)\right)Q\left(m\right)\in {\mathrm{Base}}_R$$
21	14 16 19 20	syl3anc	$$⊢\left(\left(M\in B\wedge K\in N\wedge L\in N\right)\wedge Q\in \left(P\setminus \left\{q\in P|q\left(K\right)=L\right\}\right)\right)\to \forall m\in Nm\left(i\in N,j\in N⟼if\left(i=K,if\left(j=L,\underset{\dot{}}{1},\underset{\dot{}}{0}\right),iMj\right)\right)Q\left(m\right)\in {\mathrm{Base}}_R$$
22		id	$$⊢m=n\to m=n$$
23		fveq2	$$⊢m=n\to Q\left(m\right)=Q\left(n\right)$$
24	22 23	oveq12d	$$⊢m=n\to m\left(i\in N,j\in N⟼if\left(i=K,if\left(j=L,\underset{\dot{}}{1},\underset{\dot{}}{0}\right),iMj\right)\right)Q\left(m\right)=n\left(i\in N,j\in N⟼if\left(i=K,if\left(j=L,\underset{\dot{}}{1},\underset{\dot{}}{0}\right),iMj\right)\right)Q\left(n\right)$$
25	24	eleq1d	$$⊢m=n\to \left(m\left(i\in N,j\in N⟼if\left(i=K,if\left(j=L,\underset{\dot{}}{1},\underset{\dot{}}{0}\right),iMj\right)\right)Q\left(m\right)\in {\mathrm{Base}}_R\leftrightarrow n\left(i\in N,j\in N⟼if\left(i=K,if\left(j=L,\underset{\dot{}}{1},\underset{\dot{}}{0}\right),iMj\right)\right)Q\left(n\right)\in {\mathrm{Base}}_R\right)$$
26	25	rspccv	$$⊢\forall m\in Nm\left(i\in N,j\in N⟼if\left(i=K,if\left(j=L,\underset{\dot{}}{1},\underset{\dot{}}{0}\right),iMj\right)\right)Q\left(m\right)\in {\mathrm{Base}}_R\to \left(n\in N\to n\left(i\in N,j\in N⟼if\left(i=K,if\left(j=L,\underset{\dot{}}{1},\underset{\dot{}}{0}\right),iMj\right)\right)Q\left(n\right)\in {\mathrm{Base}}_R\right)$$
27	21 26	syl	$$⊢\left(\left(M\in B\wedge K\in N\wedge L\in N\right)\wedge Q\in \left(P\setminus \left\{q\in P|q\left(K\right)=L\right\}\right)\right)\to \left(n\in N\to n\left(i\in N,j\in N⟼if\left(i=K,if\left(j=L,\underset{\dot{}}{1},\underset{\dot{}}{0}\right),iMj\right)\right)Q\left(n\right)\in {\mathrm{Base}}_R\right)$$
28	27	imp	$$⊢\left(\left(\left(M\in B\wedge K\in N\wedge L\in N\right)\wedge Q\in \left(P\setminus \left\{q\in P|q\left(K\right)=L\right\}\right)\right)\wedge n\in N\right)\to n\left(i\in N,j\in N⟼if\left(i=K,if\left(j=L,\underset{\dot{}}{1},\underset{\dot{}}{0}\right),iMj\right)\right)Q\left(n\right)\in {\mathrm{Base}}_R$$
29		id	$$⊢n=m\to n=m$$
30		fveq2	$$⊢n=m\to Q\left(n\right)=Q\left(m\right)$$
31	29 30	oveq12d	$$⊢n=m\to n\left(i\in N,j\in N⟼if\left(i=K,if\left(j=L,\underset{\dot{}}{1},\underset{\dot{}}{0}\right),iMj\right)\right)Q\left(n\right)=m\left(i\in N,j\in N⟼if\left(i=K,if\left(j=L,\underset{\dot{}}{1},\underset{\dot{}}{0}\right),iMj\right)\right)Q\left(m\right)$$
32	31	adantl	$$⊢\left(\left(\left(M\in B\wedge K\in N\wedge L\in N\right)\wedge Q\in \left(P\setminus \left\{q\in P|q\left(K\right)=L\right\}\right)\right)\wedge n=m\right)\to n\left(i\in N,j\in N⟼if\left(i=K,if\left(j=L,\underset{\dot{}}{1},\underset{\dot{}}{0}\right),iMj\right)\right)Q\left(n\right)=m\left(i\in N,j\in N⟼if\left(i=K,if\left(j=L,\underset{\dot{}}{1},\underset{\dot{}}{0}\right),iMj\right)\right)Q\left(m\right)$$
33	6 4 5	symgmatr01	$$⊢\left(K\in N\wedge L\in N\right)\to \left(Q\in \left(P\setminus \left\{q\in P|q\left(K\right)=L\right\}\right)\to \exists m\in Nm\left(i\in N,j\in N⟼if\left(i=K,if\left(j=L,\underset{\dot{}}{1},\underset{\dot{}}{0}\right),iMj\right)\right)Q\left(m\right)=\underset{\dot{}}{0}\right)$$
34	33	3adant1	$$⊢\left(M\in B\wedge K\in N\wedge L\in N\right)\to \left(Q\in \left(P\setminus \left\{q\in P|q\left(K\right)=L\right\}\right)\to \exists m\in Nm\left(i\in N,j\in N⟼if\left(i=K,if\left(j=L,\underset{\dot{}}{1},\underset{\dot{}}{0}\right),iMj\right)\right)Q\left(m\right)=\underset{\dot{}}{0}\right)$$
35	34	imp	$$⊢\left(\left(M\in B\wedge K\in N\wedge L\in N\right)\wedge Q\in \left(P\setminus \left\{q\in P|q\left(K\right)=L\right\}\right)\right)\to \exists m\in Nm\left(i\in N,j\in N⟼if\left(i=K,if\left(j=L,\underset{\dot{}}{1},\underset{\dot{}}{0}\right),iMj\right)\right)Q\left(m\right)=\underset{\dot{}}{0}$$
36	7 4 8 12 28 32 35	gsummgp0	$$⊢\left(\left(M\in B\wedge K\in N\wedge L\in N\right)\wedge Q\in \left(P\setminus \left\{q\in P|q\left(K\right)=L\right\}\right)\right)\to \underset{n\in N}{{\sum }_G}\left(n\left(i\in N,j\in N⟼if\left(i=K,if\left(j=L,\underset{\dot{}}{1},\underset{\dot{}}{0}\right),iMj\right)\right)Q\left(n\right)\right)=\underset{\dot{}}{0}$$
37	36	ex	$$⊢\left(M\in B\wedge K\in N\wedge L\in N\right)\to \left(Q\in \left(P\setminus \left\{q\in P|q\left(K\right)=L\right\}\right)\to \underset{n\in N}{{\sum }_G}\left(n\left(i\in N,j\in N⟼if\left(i=K,if\left(j=L,\underset{\dot{}}{1},\underset{\dot{}}{0}\right),iMj\right)\right)Q\left(n\right)\right)=\underset{\dot{}}{0}\right)$$