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 ⊢ D = N maDet R
mdetfval1.a ⊢ A = N Mat R
mdetfval1.b ⊢ B = Base A
mdetfval1.p ⊢ P = Base SymGrp ⁡ N
mdetfval1.y ⊢ Y = ℤRHom ⁡ R
mdetfval1.s ⊢ S = pmSgn ⁡ N
mdetfval1.t ⊢ · ˙ = ⋅ R
mdetfval1.u ⊢ U = mulGrp R
Assertion mdetfval1 ⊢ D = m ∈ B ⟼ ∑ R p ∈ P Y ⁡ S ⁡ p · ˙ ∑ U x ∈ N p ⁡ x m x

Proof

Step Hyp Ref Expression
1 mdetfval1.d ⊢ D = N maDet R
2 mdetfval1.a ⊢ A = N Mat R
3 mdetfval1.b ⊢ B = Base A
4 mdetfval1.p ⊢ P = Base SymGrp ⁡ N
5 mdetfval1.y ⊢ Y = ℤRHom ⁡ R
6 mdetfval1.s ⊢ S = pmSgn ⁡ N
7 mdetfval1.t ⊢ · ˙ = ⋅ R
8 mdetfval1.u ⊢ U = mulGrp R
9 1 2 3 4 5 6 7 8 mdetfval ⊢ D = m ∈ B ⟼ ∑ R p ∈ P Y ∘ S ⁡ p · ˙ ∑ U x ∈ N p ⁡ x m x
10 4 6 cofipsgn ⊢ N ∈ Fin ∧ p ∈ P → Y ∘ S ⁡ p = Y ⁡ S ⁡ p
11 10 oveq1d ⊢ N ∈ Fin ∧ p ∈ P → Y ∘ S ⁡ p · ˙ ∑ U x ∈ N p ⁡ x m x = Y ⁡ S ⁡ p · ˙ ∑ U x ∈ N p ⁡ x m x
12 11 mpteq2dva ⊢ N ∈ Fin → p ∈ P ⟼ Y ∘ S ⁡ p · ˙ ∑ U x ∈ N p ⁡ x m x = p ∈ P ⟼ Y ⁡ S ⁡ p · ˙ ∑ U x ∈ N p ⁡ x m x
13 12 oveq2d ⊢ N ∈ Fin → ∑ R p ∈ P Y ∘ S ⁡ p · ˙ ∑ U x ∈ N p ⁡ x m x = ∑ R p ∈ P Y ⁡ S ⁡ p · ˙ ∑ U x ∈ N p ⁡ x m x
14 13 mpteq2dv ⊢ N ∈ Fin → m ∈ B ⟼ ∑ R p ∈ P Y ∘ S ⁡ p · ˙ ∑ U x ∈ N p ⁡ x m x = m ∈ B ⟼ ∑ R p ∈ P Y ⁡ S ⁡ p · ˙ ∑ U x ∈ N p ⁡ x m x
15 9 14 eqtrid ⊢ N ∈ Fin → D = m ∈ B ⟼ ∑ R p ∈ P Y ⁡ S ⁡ p · ˙ ∑ U x ∈ N p ⁡ x m x
16 df-nel ⊢ N ∉ Fin ↔ ¬ N ∈ Fin
17 1 nfimdetndef ⊢ N ∉ Fin → D = ∅
18 2 fveq2i ⊢ Base A = Base N Mat R
19 3 18 eqtri ⊢ B = Base N Mat R
20 16 biimpi ⊢ N ∉ Fin → ¬ N ∈ Fin
21 20 intnanrd ⊢ N ∉ Fin → ¬ N ∈ Fin ∧ R ∈ V
22 matbas0 ⊢ ¬ N ∈ Fin ∧ R ∈ V → Base N Mat R = ∅
23 21 22 syl ⊢ N ∉ Fin → Base N Mat R = ∅
24 19 23 eqtrid ⊢ N ∉ Fin → B = ∅
25 24 mpteq1d ⊢ N ∉ Fin → m ∈ B ⟼ ∑ R p ∈ P Y ⁡ S ⁡ p · ˙ ∑ U x ∈ N p ⁡ x m x = m ∈ ∅ ⟼ ∑ R p ∈ P Y ⁡ S ⁡ p · ˙ ∑ U x ∈ N p ⁡ x m x
26 mpt0 ⊢ m ∈ ∅ ⟼ ∑ R p ∈ P Y ⁡ S ⁡ p · ˙ ∑ U x ∈ N p ⁡ x m x = ∅
27 25 26 eqtrdi ⊢ N ∉ Fin → m ∈ B ⟼ ∑ R p ∈ P Y ⁡ S ⁡ p · ˙ ∑ U x ∈ N p ⁡ x m x = ∅
28 17 27 eqtr4d ⊢ N ∉ Fin → D = m ∈ B ⟼ ∑ R p ∈ P Y ⁡ S ⁡ p · ˙ ∑ U x ∈ N p ⁡ x m x
29 16 28 sylbir ⊢ ¬ N ∈ Fin → D = m ∈ B ⟼ ∑ R p ∈ P Y ⁡ S ⁡ p · ˙ ∑ U x ∈ N p ⁡ x m x
30 15 29 pm2.61i ⊢ D = m ∈ B ⟼ ∑ R p ∈ P Y ⁡ S ⁡ p · ˙ ∑ U x ∈ N p ⁡ x m x