Theorem smadiadetlem1

Description: Lemma 1 for smadiadet : A summand of the determinant of a matrix belongs to the underlying ring. (Contributed by AV, 1-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$$
	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	smadiadetlem1	$$⊢\left(\left(M\in B\wedge K\in N\right)\wedge p\in P\right)\to \left(Y\circ S\right)\left(p\right){\cdot }_R\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)\in {\mathrm{Base}}_R$$

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	marep01ma	$$⊢M\in B\to \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)\in B$$
12	11	ad2antrr	$$⊢\left(\left(M\in B\wedge K\in N\right)\wedge p\in P\right)\to \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)\in B$$
13		simpr	$$⊢\left(\left(M\in B\wedge K\in N\right)\wedge p\in P\right)\to p\in P$$
14	6 9 8 1 2 7	madetsmelbas2	$$⊢\left(R\in \mathrm{CRing}\wedge \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)\in B\wedge p\in P\right)\to \left(Y\circ S\right)\left(p\right){\cdot }_R\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)\in {\mathrm{Base}}_R$$
15	3 12 13 14	mp3an2i	$$⊢\left(\left(M\in B\wedge K\in N\right)\wedge p\in P\right)\to \left(Y\circ S\right)\left(p\right){\cdot }_R\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)\in {\mathrm{Base}}_R$$