This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑀 𝑥 ) ) ) ) ) ) )