Theorem mdetleib

Description: Full substitution of our determinant definition (also known as Leibniz' Formula, expanding by columns). Proposition 4.6 in Lang p. 514. (Contributed by Stefan O'Rear, 3-Oct-2015) (Revised by SO, 9-Jul-2018)

	Ref	Expression
Hypotheses	mdetfval.d	$$⊢D=N\mathrm{maDet}R$$
	mdetfval.a	$$⊢A=N\mathrm{Mat}R$$
	mdetfval.b	$$⊢B={\mathrm{Base}}_A$$
	mdetfval.p	$$⊢P={\mathrm{Base}}_{\mathrm{SymGrp}\left(N\right)}$$
	mdetfval.y	$$⊢Y=\mathrm{\mathbb{Z}RHom}\left(R\right)$$
	mdetfval.s	$$⊢S=\mathrm{pmSgn}\left(N\right)$$
	mdetfval.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	mdetfval.u	$$⊢U={\mathrm{mulGrp}}_R$$
Assertion	mdetleib	$$⊢M\in B\to D\left(M\right)=\underset{p\in P}{{\sum }_R}\left(\left(Y\circ S\right)\left(p\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		mdetfval.d	$$⊢D=N\mathrm{maDet}R$$
2		mdetfval.a	$$⊢A=N\mathrm{Mat}R$$
3		mdetfval.b	$$⊢B={\mathrm{Base}}_A$$
4		mdetfval.p	$$⊢P={\mathrm{Base}}_{\mathrm{SymGrp}\left(N\right)}$$
5		mdetfval.y	$$⊢Y=\mathrm{\mathbb{Z}RHom}\left(R\right)$$
6		mdetfval.s	$$⊢S=\mathrm{pmSgn}\left(N\right)$$
7		mdetfval.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
8		mdetfval.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 \left(Y\circ S\right)\left(p\right)\underset{\dot{}}{·}\left(\underset{x\in N}{{\sum }_U},\left(p\left(x\right)mx\right)\right)=\left(Y\circ S\right)\left(p\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⟼\left(Y\circ S\right)\left(p\right)\underset{\dot{}}{·}\left(\underset{x\in N}{{\sum }_U},\left(p\left(x\right)mx\right)\right)\right)=\left(p\in P⟼\left(Y\circ S\right)\left(p\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(\left(Y\circ S\right)\left(p\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(\left(Y\circ S\right)\left(p\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	mdetfval	$$⊢D=\left(m\in B⟼\underset{p\in P}{{\sum }_R}\left(\left(Y\circ S\right)\left(p\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(\left(Y\circ S\right)\left(p\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(\left(Y\circ S\right)\left(p\right)\underset{\dot{}}{·}\left(\underset{x\in N}{{\sum }_U},\left(p\left(x\right)Mx\right)\right)\right)$$