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

Metamath Proof Explorer

Theorem mdetfval1

Description: First substitution of an alternative determinant definition. (Contributed by Stefan O'Rear, 9-Sep-2015) (Revised by AV, 27-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 mdetfval1 𝐷 = ( 𝑚 ∈ 𝐵 ↦ ( 𝑅 Σ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 1 2 3 4 5 6 7 8 mdetfval ⊢ 𝐷 = ( 𝑚 ∈ 𝐵 ↦ ( 𝑅 Σg ( 𝑝 ∈ 𝑃 ↦ ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑝 ) · ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) ) )
10 4 6 cofipsgn ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑝 ) = ( 𝑌 ‘ ( 𝑆 ‘ 𝑝 ) ) )
11 10 oveq1d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑝 ∈ 𝑃 ) → ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑝 ) · ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) = ( ( 𝑌 ‘ ( 𝑆 ‘ 𝑝 ) ) · ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) )
12 11 mpteq2dva ⊢ ( 𝑁 ∈ Fin → ( 𝑝 ∈ 𝑃 ↦ ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑝 ) · ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) = ( 𝑝 ∈ 𝑃 ↦ ( ( 𝑌 ‘ ( 𝑆 ‘ 𝑝 ) ) · ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) )
13 12 oveq2d ⊢ ( 𝑁 ∈ Fin → ( 𝑅 Σg ( 𝑝 ∈ 𝑃 ↦ ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑝 ) · ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) ) = ( 𝑅 Σg ( 𝑝 ∈ 𝑃 ↦ ( ( 𝑌 ‘ ( 𝑆 ‘ 𝑝 ) ) · ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) ) )
14 13 mpteq2dv ⊢ ( 𝑁 ∈ Fin → ( 𝑚 ∈ 𝐵 ↦ ( 𝑅 Σg ( 𝑝 ∈ 𝑃 ↦ ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑝 ) · ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) ) ) = ( 𝑚 ∈ 𝐵 ↦ ( 𝑅 Σg ( 𝑝 ∈ 𝑃 ↦ ( ( 𝑌 ‘ ( 𝑆 ‘ 𝑝 ) ) · ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) ) ) )
15 9 14 eqtrid ⊢ ( 𝑁 ∈ Fin → 𝐷 = ( 𝑚 ∈ 𝐵 ↦ ( 𝑅 Σg ( 𝑝 ∈ 𝑃 ↦ ( ( 𝑌 ‘ ( 𝑆 ‘ 𝑝 ) ) · ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) ) ) )
16 df-nel ⊢ ( 𝑁 ∉ Fin ↔ ¬ 𝑁 ∈ Fin )
17 1 nfimdetndef ⊢ ( 𝑁 ∉ Fin → 𝐷 = ∅ )
18 2 fveq2i ⊢ ( Base ‘ 𝐴 ) = ( Base ‘ ( 𝑁 Mat 𝑅 ) )
19 3 18 eqtri ⊢ 𝐵 = ( Base ‘ ( 𝑁 Mat 𝑅 ) )
20 16 biimpi ⊢ ( 𝑁 ∉ Fin → ¬ 𝑁 ∈ Fin )
21 20 intnanrd ⊢ ( 𝑁 ∉ Fin → ¬ ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
22 matbas0 ⊢ ( ¬ ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) → ( Base ‘ ( 𝑁 Mat 𝑅 ) ) = ∅ )
23 21 22 syl ⊢ ( 𝑁 ∉ Fin → ( Base ‘ ( 𝑁 Mat 𝑅 ) ) = ∅ )
24 19 23 eqtrid ⊢ ( 𝑁 ∉ Fin → 𝐵 = ∅ )
25 24 mpteq1d ⊢ ( 𝑁 ∉ Fin → ( 𝑚 ∈ 𝐵 ↦ ( 𝑅 Σg ( 𝑝 ∈ 𝑃 ↦ ( ( 𝑌 ‘ ( 𝑆 ‘ 𝑝 ) ) · ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) ) ) = ( 𝑚 ∈ ∅ ↦ ( 𝑅 Σg ( 𝑝 ∈ 𝑃 ↦ ( ( 𝑌 ‘ ( 𝑆 ‘ 𝑝 ) ) · ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) ) ) )
26 mpt0 ⊢ ( 𝑚 ∈ ∅ ↦ ( 𝑅 Σg ( 𝑝 ∈ 𝑃 ↦ ( ( 𝑌 ‘ ( 𝑆 ‘ 𝑝 ) ) · ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) ) ) = ∅
27 25 26 eqtrdi ⊢ ( 𝑁 ∉ Fin → ( 𝑚 ∈ 𝐵 ↦ ( 𝑅 Σg ( 𝑝 ∈ 𝑃 ↦ ( ( 𝑌 ‘ ( 𝑆 ‘ 𝑝 ) ) · ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) ) ) = ∅ )
28 17 27 eqtr4d ⊢ ( 𝑁 ∉ Fin → 𝐷 = ( 𝑚 ∈ 𝐵 ↦ ( 𝑅 Σg ( 𝑝 ∈ 𝑃 ↦ ( ( 𝑌 ‘ ( 𝑆 ‘ 𝑝 ) ) · ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) ) ) )
29 16 28 sylbir ⊢ ( ¬ 𝑁 ∈ Fin → 𝐷 = ( 𝑚 ∈ 𝐵 ↦ ( 𝑅 Σg ( 𝑝 ∈ 𝑃 ↦ ( ( 𝑌 ‘ ( 𝑆 ‘ 𝑝 ) ) · ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) ) ) )
30 15 29 pm2.61i ⊢ 𝐷 = ( 𝑚 ∈ 𝐵 ↦ ( 𝑅 Σg ( 𝑝 ∈ 𝑃 ↦ ( ( 𝑌 ‘ ( 𝑆 ‘ 𝑝 ) ) · ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) ) )