# 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}\mathrm{maDet}{R}$
mdettpos.a ${⊢}{A}={N}\mathrm{Mat}{R}$
mdettpos.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
Assertion mdettpos ${⊢}\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\to {D}\left(tpos{M}\right)={D}\left({M}\right)$

### Proof

Step Hyp Ref Expression
1 mdettpos.d ${⊢}{D}={N}\mathrm{maDet}{R}$
2 mdettpos.a ${⊢}{A}={N}\mathrm{Mat}{R}$
3 mdettpos.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
4 ovtpos ${⊢}{p}\left({x}\right)tpos{M}{x}={x}{M}{p}\left({x}\right)$
5 4 mpteq2i ${⊢}\left({x}\in {N}⟼{p}\left({x}\right)tpos{M}{x}\right)=\left({x}\in {N}⟼{x}{M}{p}\left({x}\right)\right)$
6 5 oveq2i ${⊢}\underset{{x}\in {N}}{{\sum }_{{\mathrm{mulGrp}}_{{R}}}}\left({p}\left({x}\right)tpos{M}{x}\right)=\underset{{x}\in {N}}{{\sum }_{{\mathrm{mulGrp}}_{{R}}}}\left({x}{M}{p}\left({x}\right)\right)$
7 6 oveq2i ${⊢}\left(\mathrm{ℤRHom}\left({R}\right)\circ \mathrm{pmSgn}\left({N}\right)\right)\left({p}\right){\cdot }_{{R}}\left(\underset{{x}\in {N}}{{\sum }_{{\mathrm{mulGrp}}_{{R}}}},\left({p}\left({x}\right)tpos{M}{x}\right)\right)=\left(\mathrm{ℤRHom}\left({R}\right)\circ \mathrm{pmSgn}\left({N}\right)\right)\left({p}\right){\cdot }_{{R}}\left(\underset{{x}\in {N}}{{\sum }_{{\mathrm{mulGrp}}_{{R}}}},\left({x}{M}{p}\left({x}\right)\right)\right)$
8 7 mpteq2i ${⊢}\left({p}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}⟼\left(\mathrm{ℤRHom}\left({R}\right)\circ \mathrm{pmSgn}\left({N}\right)\right)\left({p}\right){\cdot }_{{R}}\left(\underset{{x}\in {N}}{{\sum }_{{\mathrm{mulGrp}}_{{R}}}},\left({p}\left({x}\right)tpos{M}{x}\right)\right)\right)=\left({p}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}⟼\left(\mathrm{ℤRHom}\left({R}\right)\circ \mathrm{pmSgn}\left({N}\right)\right)\left({p}\right){\cdot }_{{R}}\left(\underset{{x}\in {N}}{{\sum }_{{\mathrm{mulGrp}}_{{R}}}},\left({x}{M}{p}\left({x}\right)\right)\right)\right)$
9 8 oveq2i ${⊢}\underset{{p}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}}{{\sum }_{{R}}}\left(\left(\mathrm{ℤRHom}\left({R}\right)\circ \mathrm{pmSgn}\left({N}\right)\right)\left({p}\right){\cdot }_{{R}}\left(\underset{{x}\in {N}}{{\sum }_{{\mathrm{mulGrp}}_{{R}}}},\left({p}\left({x}\right)tpos{M}{x}\right)\right)\right)=\underset{{p}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}}{{\sum }_{{R}}}\left(\left(\mathrm{ℤRHom}\left({R}\right)\circ \mathrm{pmSgn}\left({N}\right)\right)\left({p}\right){\cdot }_{{R}}\left(\underset{{x}\in {N}}{{\sum }_{{\mathrm{mulGrp}}_{{R}}}},\left({x}{M}{p}\left({x}\right)\right)\right)\right)$
10 2 3 mattposcl ${⊢}{M}\in {B}\to tpos{M}\in {B}$
11 10 adantl ${⊢}\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\to tpos{M}\in {B}$
12 eqid ${⊢}{\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}={\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}$
13 eqid ${⊢}\mathrm{ℤRHom}\left({R}\right)=\mathrm{ℤRHom}\left({R}\right)$
14 eqid ${⊢}\mathrm{pmSgn}\left({N}\right)=\mathrm{pmSgn}\left({N}\right)$
15 eqid ${⊢}{\cdot }_{{R}}={\cdot }_{{R}}$
16 eqid ${⊢}{\mathrm{mulGrp}}_{{R}}={\mathrm{mulGrp}}_{{R}}$
17 1 2 3 12 13 14 15 16 mdetleib ${⊢}tpos{M}\in {B}\to {D}\left(tpos{M}\right)=\underset{{p}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}}{{\sum }_{{R}}}\left(\left(\mathrm{ℤRHom}\left({R}\right)\circ \mathrm{pmSgn}\left({N}\right)\right)\left({p}\right){\cdot }_{{R}}\left(\underset{{x}\in {N}}{{\sum }_{{\mathrm{mulGrp}}_{{R}}}},\left({p}\left({x}\right)tpos{M}{x}\right)\right)\right)$
18 11 17 syl ${⊢}\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\to {D}\left(tpos{M}\right)=\underset{{p}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}}{{\sum }_{{R}}}\left(\left(\mathrm{ℤRHom}\left({R}\right)\circ \mathrm{pmSgn}\left({N}\right)\right)\left({p}\right){\cdot }_{{R}}\left(\underset{{x}\in {N}}{{\sum }_{{\mathrm{mulGrp}}_{{R}}}},\left({p}\left({x}\right)tpos{M}{x}\right)\right)\right)$
19 1 2 3 12 13 14 15 16 mdetleib2 ${⊢}\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\to {D}\left({M}\right)=\underset{{p}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}}{{\sum }_{{R}}}\left(\left(\mathrm{ℤRHom}\left({R}\right)\circ \mathrm{pmSgn}\left({N}\right)\right)\left({p}\right){\cdot }_{{R}}\left(\underset{{x}\in {N}}{{\sum }_{{\mathrm{mulGrp}}_{{R}}}},\left({x}{M}{p}\left({x}\right)\right)\right)\right)$
20 9 18 19 3eqtr4a ${⊢}\left({R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\to {D}\left(tpos{M}\right)={D}\left({M}\right)$