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

Proof

Step	Hyp	Ref	Expression
1		mdetfval1.d	⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
2		mdetfval1.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
3		mdetfval1.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
4		mdetfval1.p	⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
5		mdetfval1.y	⊢ 𝑌 = ( ℤRHom ‘ 𝑅 )
6		mdetfval1.s	⊢ 𝑆 = ( pmSgn ‘ 𝑁 )
7		mdetfval1.t	⊢ · = ( .r ‘ 𝑅 )
8		mdetfval1.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	mdetfval1	⊢ 𝐷 = ( 𝑚 ∈ 𝐵 ↦ ( 𝑅 Σg ( 𝑝 ∈ 𝑃 ↦ ( ( 𝑌 ‘ ( 𝑆 ‘ 𝑝 ) ) · ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) ) )
16		ovex	⊢ ( 𝑅 Σg ( 𝑝 ∈ 𝑃 ↦ ( ( 𝑌 ‘ ( 𝑆 ‘ 𝑝 ) ) · ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑀 𝑥 ) ) ) ) ) ) ∈ V
17	14 15 16	fvmpt	⊢ ( 𝑀 ∈ 𝐵 → ( 𝐷 ‘ 𝑀 ) = ( 𝑅 Σg ( 𝑝 ∈ 𝑃 ↦ ( ( 𝑌 ‘ ( 𝑆 ‘ 𝑝 ) ) · ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑀 𝑥 ) ) ) ) ) ) )