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=NmaDetR
mdettpos.a ⊢A=NMatR
mdettpos.b ⊢B=BaseA
Assertion mdettpos ⊢R∈CRing∧M∈B→D⁡tposM=D⁡M

Proof

Step Hyp Ref Expression
1 mdettpos.d ⊢D=NmaDetR
2 mdettpos.a ⊢A=NMatR
3 mdettpos.b ⊢B=BaseA
4 ovtpos ⊢p⁡xtposMx=xMp⁡x
5 4 mpteq2i ⊢x∈N⟼p⁡xtposMx=x∈N⟼xMp⁡x
6 5 oveq2i ⊢∑mulGrpRx∈Np⁡xtposMx=∑mulGrpRx∈NxMp⁡x
7 6 oveq2i ⊢ℤRHom⁡R∘pmSgn⁡N⁡p⋅R∑mulGrpRx∈Np⁡xtposMx=ℤRHom⁡R∘pmSgn⁡N⁡p⋅R∑mulGrpRx∈NxMp⁡x
8 7 mpteq2i ⊢p∈BaseSymGrp⁡N⟼ℤRHom⁡R∘pmSgn⁡N⁡p⋅R∑mulGrpRx∈Np⁡xtposMx=p∈BaseSymGrp⁡N⟼ℤRHom⁡R∘pmSgn⁡N⁡p⋅R∑mulGrpRx∈NxMp⁡x
9 8 oveq2i ⊢∑Rp∈BaseSymGrp⁡NℤRHom⁡R∘pmSgn⁡N⁡p⋅R∑mulGrpRx∈Np⁡xtposMx=∑Rp∈BaseSymGrp⁡NℤRHom⁡R∘pmSgn⁡N⁡p⋅R∑mulGrpRx∈NxMp⁡x
10 2 3 mattposcl ⊢M∈B→tposM∈B
11 10 adantl ⊢R∈CRing∧M∈B→tposM∈B
12 eqid ⊢BaseSymGrp⁡N=BaseSymGrp⁡N
13 eqid ⊢ℤRHom⁡R=ℤRHom⁡R
14 eqid ⊢pmSgn⁡N=pmSgn⁡N
15 eqid ⊢⋅R=⋅R
16 eqid ⊢mulGrpR=mulGrpR
17 1 2 3 12 13 14 15 16 mdetleib ⊢tposM∈B→D⁡tposM=∑Rp∈BaseSymGrp⁡NℤRHom⁡R∘pmSgn⁡N⁡p⋅R∑mulGrpRx∈Np⁡xtposMx
18 11 17 syl ⊢R∈CRing∧M∈B→D⁡tposM=∑Rp∈BaseSymGrp⁡NℤRHom⁡R∘pmSgn⁡N⁡p⋅R∑mulGrpRx∈Np⁡xtposMx
19 1 2 3 12 13 14 15 16 mdetleib2 ⊢R∈CRing∧M∈B→D⁡M=∑Rp∈BaseSymGrp⁡NℤRHom⁡R∘pmSgn⁡N⁡p⋅R∑mulGrpRx∈NxMp⁡x
20 9 18 19 3eqtr4a ⊢R∈CRing∧M∈B→D⁡tposM=D⁡M