Theorem mdetleib1

Description: Full substitution of an alternative determinant definition (also known as Leibniz' Formula). (Contributed by Stefan O'Rear, 3-Oct-2015) (Revised by AV, 26-Dec-2018)

	Ref	Expression
Hypotheses	mdetfval1.d	$$⊢D=N\mathrm{maDet}R$$
	mdetfval1.a	$$⊢A=N\mathrm{Mat}R$$
	mdetfval1.b	$$⊢B={\mathrm{Base}}_A$$
	mdetfval1.p	$$⊢P={\mathrm{Base}}_{\mathrm{SymGrp}\left(N\right)}$$
	mdetfval1.y	$$⊢Y=\mathrm{\mathbb{Z}RHom}\left(R\right)$$
	mdetfval1.s	$$⊢S=\mathrm{pmSgn}\left(N\right)$$
	mdetfval1.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	mdetfval1.u	$$⊢U={\mathrm{mulGrp}}_R$$
Assertion	mdetleib1	$$⊢M\in B\to D\left(M\right)=\underset{p\in P}{{\sum }_R}\left(Y\left(S\left(p\right)\right)\underset{\dot{}}{·}\left(\underset{x\in N}{{\sum }_U},\left(p\left(x\right)Mx\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		mdetfval1.d	$$⊢D=N\mathrm{maDet}R$$
2		mdetfval1.a	$$⊢A=N\mathrm{Mat}R$$
3		mdetfval1.b	$$⊢B={\mathrm{Base}}_A$$
4		mdetfval1.p	$$⊢P={\mathrm{Base}}_{\mathrm{SymGrp}\left(N\right)}$$
5		mdetfval1.y	$$⊢Y=\mathrm{\mathbb{Z}RHom}\left(R\right)$$
6		mdetfval1.s	$$⊢S=\mathrm{pmSgn}\left(N\right)$$
7		mdetfval1.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
8		mdetfval1.u	$$⊢U={\mathrm{mulGrp}}_R$$
9		oveq	$$⊢m=M\to p\left(x\right)mx=p\left(x\right)Mx$$
10	9	mpteq2dv	$$⊢m=M\to \left(x\in N⟼p\left(x\right)mx\right)=\left(x\in N⟼p\left(x\right)Mx\right)$$
11	10	oveq2d	$$⊢m=M\to \underset{x\in N}{{\sum }_U}\left(p\left(x\right)mx\right)=\underset{x\in N}{{\sum }_U}\left(p\left(x\right)Mx\right)$$
12	11	oveq2d	$$⊢m=M\to Y\left(S\left(p\right)\right)\underset{\dot{}}{·}\left(\underset{x\in N}{{\sum }_U},\left(p\left(x\right)mx\right)\right)=Y\left(S\left(p\right)\right)\underset{\dot{}}{·}\left(\underset{x\in N}{{\sum }_U},\left(p\left(x\right)Mx\right)\right)$$
13	12	mpteq2dv	$$⊢m=M\to \left(p\in P⟼Y\left(S\left(p\right)\right)\underset{\dot{}}{·}\left(\underset{x\in N}{{\sum }_U},\left(p\left(x\right)mx\right)\right)\right)=\left(p\in P⟼Y\left(S\left(p\right)\right)\underset{\dot{}}{·}\left(\underset{x\in N}{{\sum }_U},\left(p\left(x\right)Mx\right)\right)\right)$$
14	13	oveq2d	$$⊢m=M\to \underset{p\in P}{{\sum }_R}\left(Y\left(S\left(p\right)\right)\underset{\dot{}}{·}\left(\underset{x\in N}{{\sum }_U},\left(p\left(x\right)mx\right)\right)\right)=\underset{p\in P}{{\sum }_R}\left(Y\left(S\left(p\right)\right)\underset{\dot{}}{·}\left(\underset{x\in N}{{\sum }_U},\left(p\left(x\right)Mx\right)\right)\right)$$
15	1 2 3 4 5 6 7 8	mdetfval1	$$⊢D=\left(m\in B⟼\underset{p\in P}{{\sum }_R}\left(Y\left(S\left(p\right)\right)\underset{\dot{}}{·}\left(\underset{x\in N}{{\sum }_U},\left(p\left(x\right)mx\right)\right)\right)\right)$$
16		ovex	$$⊢\underset{p\in P}{{\sum }_R}\left(Y\left(S\left(p\right)\right)\underset{\dot{}}{·}\left(\underset{x\in N}{{\sum }_U},\left(p\left(x\right)Mx\right)\right)\right)\in \mathrm{V}$$
17	14 15 16	fvmpt	$$⊢M\in B\to D\left(M\right)=\underset{p\in P}{{\sum }_R}\left(Y\left(S\left(p\right)\right)\underset{\dot{}}{·}\left(\underset{x\in N}{{\sum }_U},\left(p\left(x\right)Mx\right)\right)\right)$$