Theorem smadiadetlem3lem1

Description: Lemma 1 for smadiadetlem3 . (Contributed by AV, 12-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$$
	smadiadetlem.w	$$⊢W={\mathrm{Base}}_{\mathrm{SymGrp}\left(N\setminus \left\{K\right\}\right)}$$
	smadiadetlem.z	$$⊢Z=\mathrm{pmSgn}\left(N\setminus \left\{K\right\}\right)$$
Assertion	smadiadetlem3lem1	$$⊢\left(M\in B\wedge K\in N\right)\to \left(p\in W⟼\left(Y\circ Z\right)\left(p\right){\cdot }_R\left(\underset{n\in N\setminus \left\{K\right\}}{{\sum }_G},\left(n\left(i\in \left(N\setminus \left\{K\right\}\right),j\in \left(N\setminus \left\{K\right\}\right)⟼iMj\right)p\left(n\right)\right)\right)\right):W⟶{\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		smadiadetlem.w	$$⊢W={\mathrm{Base}}_{\mathrm{SymGrp}\left(N\setminus \left\{K\right\}\right)}$$
12		smadiadetlem.z	$$⊢Z=\mathrm{pmSgn}\left(N\setminus \left\{K\right\}\right)$$
13	1 2 3 4 5 6 7 8 9 10 11 12	smadiadetlem3lem0	$$⊢\left(\left(M\in B\wedge K\in N\right)\wedge p\in W\right)\to \left(Y\circ Z\right)\left(p\right){\cdot }_R\left(\underset{n\in N\setminus \left\{K\right\}}{{\sum }_G},\left(n\left(i\in \left(N\setminus \left\{K\right\}\right),j\in \left(N\setminus \left\{K\right\}\right)⟼iMj\right)p\left(n\right)\right)\right)\in {\mathrm{Base}}_R$$
14	13	fmpttd	$$⊢\left(M\in B\wedge K\in N\right)\to \left(p\in W⟼\left(Y\circ Z\right)\left(p\right){\cdot }_R\left(\underset{n\in N\setminus \left\{K\right\}}{{\sum }_G},\left(n\left(i\in \left(N\setminus \left\{K\right\}\right),j\in \left(N\setminus \left\{K\right\}\right)⟼iMj\right)p\left(n\right)\right)\right)\right):W⟶{\mathrm{Base}}_R$$