Metamath Proof Explorer

Theorem mdettpos

Description: Determinant is invariant under transposition. Proposition 4.8 in Lang p. 514. (Contributed by Stefan O'Rear, 9-Jul-2018)

Ref Expression
Hypotheses mdettpos.d ⊢ D = N maDet R
mdettpos.a ⊢ A = N Mat R
mdettpos.b ⊢ B = Base A
Assertion mdettpos ⊢ R ∈ CRing ∧ M ∈ B → D ⁡ tpos M = D ⁡ M

Proof

Step Hyp Ref Expression
1 mdettpos.d ⊢ D = N maDet R
2 mdettpos.a ⊢ A = N Mat R
3 mdettpos.b ⊢ B = Base A
4 ovtpos ⊢ p ⁡ x tpos M x = x M p ⁡ x
5 4 mpteq2i ⊢ x ∈ N ⟼ p ⁡ x tpos M x = x ∈ N ⟼ x M p ⁡ x
6 5 oveq2i ⊢ ∑ mulGrp R x ∈ N p ⁡ x tpos M x = ∑ mulGrp R x ∈ N x M p ⁡ x
7 6 oveq2i ⊢ ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ p ⋅ R ∑ mulGrp R x ∈ N p ⁡ x tpos M x = ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ p ⋅ R ∑ mulGrp R x ∈ N x M p ⁡ x
8 7 mpteq2i ⊢ p ∈ Base SymGrp ⁡ N ⟼ ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ p ⋅ R ∑ mulGrp R x ∈ N p ⁡ x tpos M x = p ∈ Base SymGrp ⁡ N ⟼ ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ p ⋅ R ∑ mulGrp R x ∈ N x M p ⁡ x
9 8 oveq2i ⊢ ∑ R p ∈ Base SymGrp ⁡ N ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ p ⋅ R ∑ mulGrp R x ∈ N p ⁡ x tpos M x = ∑ R p ∈ Base SymGrp ⁡ N ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ p ⋅ R ∑ mulGrp R x ∈ N x M p ⁡ x
10 2 3 mattposcl ⊢ M ∈ B → tpos M ∈ B
11 10 adantl ⊢ R ∈ CRing ∧ M ∈ B → tpos M ∈ B
12 eqid ⊢ Base SymGrp ⁡ N = Base SymGrp ⁡ N
13 eqid ⊢ ℤRHom ⁡ R = ℤRHom ⁡ R
14 eqid ⊢ pmSgn ⁡ N = pmSgn ⁡ N
15 eqid ⊢ ⋅ R = ⋅ R
16 eqid ⊢ mulGrp R = mulGrp R
17 1 2 3 12 13 14 15 16 mdetleib ⊢ tpos M ∈ B → D ⁡ tpos M = ∑ R p ∈ Base SymGrp ⁡ N ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ p ⋅ R ∑ mulGrp R x ∈ N p ⁡ x tpos M x
18 11 17 syl ⊢ R ∈ CRing ∧ M ∈ B → D ⁡ tpos M = ∑ R p ∈ Base SymGrp ⁡ N ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ p ⋅ R ∑ mulGrp R x ∈ N p ⁡ x tpos M x
19 1 2 3 12 13 14 15 16 mdetleib2 ⊢ R ∈ CRing ∧ M ∈ B → D ⁡ M = ∑ R p ∈ Base SymGrp ⁡ N ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ p ⋅ R ∑ mulGrp R x ∈ N x M p ⁡ x
20 9 18 19 3eqtr4a ⊢ R ∈ CRing ∧ M ∈ B → D ⁡ tpos M = D ⁡ M