Metamath Proof Explorer

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 ⊢ 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 mdetleib1 ⊢ M ∈ B → D ⁡ M = ∑ 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 oveq ⊢ m = M → p ⁡ x m x = p ⁡ x M x
10 9 mpteq2dv ⊢ m = M → x ∈ N ⟼ p ⁡ x m x = x ∈ N ⟼ p ⁡ x M x
11 10 oveq2d ⊢ m = M → ∑ U x ∈ N p ⁡ x m x = ∑ U x ∈ N p ⁡ x M x
12 11 oveq2d ⊢ m = M → Y ⁡ S ⁡ p · ˙ ∑ U x ∈ N p ⁡ x m x = Y ⁡ S ⁡ p · ˙ ∑ U x ∈ N p ⁡ x M x
13 12 mpteq2dv ⊢ m = M → p ∈ P ⟼ Y ⁡ S ⁡ p · ˙ ∑ U x ∈ N p ⁡ x m x = p ∈ P ⟼ Y ⁡ S ⁡ p · ˙ ∑ U x ∈ N p ⁡ x M x
14 13 oveq2d ⊢ m = M → ∑ 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
15 1 2 3 4 5 6 7 8 mdetfval1 ⊢ D = m ∈ B ⟼ ∑ R p ∈ P Y ⁡ S ⁡ p · ˙ ∑ U x ∈ N p ⁡ x m x
16 ovex ⊢ ∑ R p ∈ P Y ⁡ S ⁡ p · ˙ ∑ U x ∈ N p ⁡ x M x ∈ V
17 14 15 16 fvmpt ⊢ M ∈ B → D ⁡ M = ∑ R p ∈ P Y ⁡ S ⁡ p · ˙ ∑ U x ∈ N p ⁡ x M x