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	⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
	mdetfval.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	mdetfval.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	mdetfval.p	⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
	mdetfval.y	⊢ 𝑌 = ( ℤRHom ‘ 𝑅 )
	mdetfval.s	⊢ 𝑆 = ( pmSgn ‘ 𝑁 )
	mdetfval.t	⊢ · = ( .r ‘ 𝑅 )
	mdetfval.u	⊢ 𝑈 = ( mulGrp ‘ 𝑅 )
Assertion	mdetleib	⊢ ( 𝑀 ∈ 𝐵 → ( 𝐷 ‘ 𝑀 ) = ( 𝑅 Σg ( 𝑝 ∈ 𝑃 ↦ ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑝 ) · ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑀 𝑥 ) ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		mdetfval.d	⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
2		mdetfval.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
3		mdetfval.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
4		mdetfval.p	⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
5		mdetfval.y	⊢ 𝑌 = ( ℤRHom ‘ 𝑅 )
6		mdetfval.s	⊢ 𝑆 = ( pmSgn ‘ 𝑁 )
7		mdetfval.t	⊢ · = ( .r ‘ 𝑅 )
8		mdetfval.u	⊢ 𝑈 = ( mulGrp ‘ 𝑅 )
9		oveq	⊢ ( 𝑚 = 𝑀 → ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) = ( ( 𝑝 ‘ 𝑥 ) 𝑀 𝑥 ) )
10	9	mpteq2dv	⊢ ( 𝑚 = 𝑀 → ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) = ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑀 𝑥 ) ) )
11	10	oveq2d	⊢ ( 𝑚 = 𝑀 → ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) = ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑀 𝑥 ) ) ) )
12	11	oveq2d	⊢ ( 𝑚 = 𝑀 → ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑝 ) · ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) = ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑝 ) · ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑀 𝑥 ) ) ) ) )
13	12	mpteq2dv	⊢ ( 𝑚 = 𝑀 → ( 𝑝 ∈ 𝑃 ↦ ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑝 ) · ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) = ( 𝑝 ∈ 𝑃 ↦ ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑝 ) · ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑀 𝑥 ) ) ) ) ) )
14	13	oveq2d	⊢ ( 𝑚 = 𝑀 → ( 𝑅 Σg ( 𝑝 ∈ 𝑃 ↦ ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑝 ) · ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) ) = ( 𝑅 Σg ( 𝑝 ∈ 𝑃 ↦ ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑝 ) · ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑀 𝑥 ) ) ) ) ) ) )
15	1 2 3 4 5 6 7 8	mdetfval	⊢ 𝐷 = ( 𝑚 ∈ 𝐵 ↦ ( 𝑅 Σg ( 𝑝 ∈ 𝑃 ↦ ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑝 ) · ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) ) )
16		ovex	⊢ ( 𝑅 Σg ( 𝑝 ∈ 𝑃 ↦ ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑝 ) · ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑀 𝑥 ) ) ) ) ) ) ∈ V
17	14 15 16	fvmpt	⊢ ( 𝑀 ∈ 𝐵 → ( 𝐷 ‘ 𝑀 ) = ( 𝑅 Σg ( 𝑝 ∈ 𝑃 ↦ ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑝 ) · ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑀 𝑥 ) ) ) ) ) ) )