Metamath Proof Explorer

Theorem mdetpmtr2

Description: The determinant of a matrix with permuted columns is the determinant of the original matrix multiplied by the sign of the permutation. (Contributed by Thierry Arnoux, 22-Aug-2020)

Ref Expression
Hypotheses mdetpmtr.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
mdetpmtr.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
mdetpmtr.d ⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
mdetpmtr.g ⊢ 𝐺 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
mdetpmtr.s ⊢ 𝑆 = ( pmSgn ‘ 𝑁 )
mdetpmtr.z ⊢ 𝑍 = ( ℤRHom ‘ 𝑅 )
mdetpmtr.t ⊢ · = ( .r ‘ 𝑅 )
mdetpmtr2.e ⊢ 𝐸 = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑖 𝑀 ( 𝑃 ‘ 𝑗 ) ) )
Assertion mdetpmtr2 ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) → ( 𝐷 ‘ 𝑀 ) = ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑃 ) · ( 𝐷 ‘ 𝐸 ) ) )

Proof

Step Hyp Ref Expression
1 mdetpmtr.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 mdetpmtr.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
3 mdetpmtr.d ⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
4 mdetpmtr.g ⊢ 𝐺 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
5 mdetpmtr.s ⊢ 𝑆 = ( pmSgn ‘ 𝑁 )
6 mdetpmtr.z ⊢ 𝑍 = ( ℤRHom ‘ 𝑅 )
7 mdetpmtr.t ⊢ · = ( .r ‘ 𝑅 )
8 mdetpmtr2.e ⊢ 𝐸 = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑖 𝑀 ( 𝑃 ‘ 𝑗 ) ) )
9 simpll ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) → 𝑅 ∈ CRing )
10 simplr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) → 𝑁 ∈ Fin )
11 1 2 mattposcl ⊢ ( 𝑀 ∈ 𝐵 → tpos 𝑀 ∈ 𝐵 )
12 11 ad2antrl ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) → tpos 𝑀 ∈ 𝐵 )
13 simprr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) → 𝑃 ∈ 𝐺 )
14 ovtpos ⊢ ( ( 𝑃 ‘ 𝑗 ) tpos 𝑀 𝑖 ) = ( 𝑖 𝑀 ( 𝑃 ‘ 𝑗 ) )
15 14 eqcomi ⊢ ( 𝑖 𝑀 ( 𝑃 ‘ 𝑗 ) ) = ( ( 𝑃 ‘ 𝑗 ) tpos 𝑀 𝑖 )
16 15 a1i ⊢ ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑖 𝑀 ( 𝑃 ‘ 𝑗 ) ) = ( ( 𝑃 ‘ 𝑗 ) tpos 𝑀 𝑖 ) )
17 16 mpoeq3ia ⊢ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑖 𝑀 ( 𝑃 ‘ 𝑗 ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑃 ‘ 𝑗 ) tpos 𝑀 𝑖 ) )
18 8 17 eqtri ⊢ 𝐸 = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑃 ‘ 𝑗 ) tpos 𝑀 𝑖 ) )
19 18 tposmpo ⊢ tpos 𝐸 = ( 𝑗 ∈ 𝑁 , 𝑖 ∈ 𝑁 ↦ ( ( 𝑃 ‘ 𝑗 ) tpos 𝑀 𝑖 ) )
20 1 2 3 4 5 6 7 19 mdetpmtr1 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( tpos 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) → ( 𝐷 ‘ tpos 𝑀 ) = ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑃 ) · ( 𝐷 ‘ tpos 𝐸 ) ) )
21 9 10 12 13 20 syl22anc ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) → ( 𝐷 ‘ tpos 𝑀 ) = ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑃 ) · ( 𝐷 ‘ tpos 𝐸 ) ) )
22 3 1 2 mdettpos ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝐷 ‘ tpos 𝑀 ) = ( 𝐷 ‘ 𝑀 ) )
23 22 ad2ant2r ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) → ( 𝐷 ‘ tpos 𝑀 ) = ( 𝐷 ‘ 𝑀 ) )
24 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
25 simp2 ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑖 ∈ 𝑁 )
26 13 3ad2ant1 ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑃 ∈ 𝐺 )
27 simp3 ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑗 ∈ 𝑁 )
28 eqid ⊢ ( SymGrp ‘ 𝑁 ) = ( SymGrp ‘ 𝑁 )
29 28 4 symgfv ⊢ ( ( 𝑃 ∈ 𝐺 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑃 ‘ 𝑗 ) ∈ 𝑁 )
30 26 27 29 syl2anc ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑃 ‘ 𝑗 ) ∈ 𝑁 )
31 simp1rl ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑀 ∈ 𝐵 )
32 1 24 2 25 30 31 matecld ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑖 𝑀 ( 𝑃 ‘ 𝑗 ) ) ∈ ( Base ‘ 𝑅 ) )
33 1 24 2 10 9 32 matbas2d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑖 𝑀 ( 𝑃 ‘ 𝑗 ) ) ) ∈ 𝐵 )
34 8 33 eqeltrid ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) → 𝐸 ∈ 𝐵 )
35 3 1 2 mdettpos ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐸 ∈ 𝐵 ) → ( 𝐷 ‘ tpos 𝐸 ) = ( 𝐷 ‘ 𝐸 ) )
36 9 34 35 syl2anc ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) → ( 𝐷 ‘ tpos 𝐸 ) = ( 𝐷 ‘ 𝐸 ) )
37 36 oveq2d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) → ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑃 ) · ( 𝐷 ‘ tpos 𝐸 ) ) = ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑃 ) · ( 𝐷 ‘ 𝐸 ) ) )
38 21 23 37 3eqtr3d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) → ( 𝐷 ‘ 𝑀 ) = ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑃 ) · ( 𝐷 ‘ 𝐸 ) ) )