This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem madetsumid

Description: The identity summand in the Leibniz' formula of a determinant for a square matrix over a commutative ring. (Contributed by AV, 29-Dec-2018)

Ref Expression
Hypotheses madetsumid.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
madetsumid.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
madetsumid.u ⊢ 𝑈 = ( mulGrp ‘ 𝑅 )
madetsumid.y ⊢ 𝑌 = ( ℤRHom ‘ 𝑅 )
madetsumid.s ⊢ 𝑆 = ( pmSgn ‘ 𝑁 )
madetsumid.t ⊢ · = ( .r ‘ 𝑅 )
Assertion madetsumid ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ 𝑃 = ( I ↾ 𝑁 ) ) → ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑃 ) · ( 𝑈 Σg ( 𝑟 ∈ 𝑁 ↦ ( ( 𝑃 ‘ 𝑟 ) 𝑀 𝑟 ) ) ) ) = ( 𝑈 Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑀 𝑟 ) ) ) )

Proof

Step Hyp Ref Expression
1 madetsumid.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 madetsumid.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
3 madetsumid.u ⊢ 𝑈 = ( mulGrp ‘ 𝑅 )
4 madetsumid.y ⊢ 𝑌 = ( ℤRHom ‘ 𝑅 )
5 madetsumid.s ⊢ 𝑆 = ( pmSgn ‘ 𝑁 )
6 madetsumid.t ⊢ · = ( .r ‘ 𝑅 )
7 fveq2 ⊢ ( 𝑃 = ( I ↾ 𝑁 ) → ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑃 ) = ( ( 𝑌 ∘ 𝑆 ) ‘ ( I ↾ 𝑁 ) ) )
8 fveq1 ⊢ ( 𝑃 = ( I ↾ 𝑁 ) → ( 𝑃 ‘ 𝑟 ) = ( ( I ↾ 𝑁 ) ‘ 𝑟 ) )
9 8 oveq1d ⊢ ( 𝑃 = ( I ↾ 𝑁 ) → ( ( 𝑃 ‘ 𝑟 ) 𝑀 𝑟 ) = ( ( ( I ↾ 𝑁 ) ‘ 𝑟 ) 𝑀 𝑟 ) )
10 9 mpteq2dv ⊢ ( 𝑃 = ( I ↾ 𝑁 ) → ( 𝑟 ∈ 𝑁 ↦ ( ( 𝑃 ‘ 𝑟 ) 𝑀 𝑟 ) ) = ( 𝑟 ∈ 𝑁 ↦ ( ( ( I ↾ 𝑁 ) ‘ 𝑟 ) 𝑀 𝑟 ) ) )
11 10 oveq2d ⊢ ( 𝑃 = ( I ↾ 𝑁 ) → ( 𝑈 Σg ( 𝑟 ∈ 𝑁 ↦ ( ( 𝑃 ‘ 𝑟 ) 𝑀 𝑟 ) ) ) = ( 𝑈 Σg ( 𝑟 ∈ 𝑁 ↦ ( ( ( I ↾ 𝑁 ) ‘ 𝑟 ) 𝑀 𝑟 ) ) ) )
12 7 11 oveq12d ⊢ ( 𝑃 = ( I ↾ 𝑁 ) → ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑃 ) · ( 𝑈 Σg ( 𝑟 ∈ 𝑁 ↦ ( ( 𝑃 ‘ 𝑟 ) 𝑀 𝑟 ) ) ) ) = ( ( ( 𝑌 ∘ 𝑆 ) ‘ ( I ↾ 𝑁 ) ) · ( 𝑈 Σg ( 𝑟 ∈ 𝑁 ↦ ( ( ( I ↾ 𝑁 ) ‘ 𝑟 ) 𝑀 𝑟 ) ) ) ) )
13 12 3ad2ant3 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ 𝑃 = ( I ↾ 𝑁 ) ) → ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑃 ) · ( 𝑈 Σg ( 𝑟 ∈ 𝑁 ↦ ( ( 𝑃 ‘ 𝑟 ) 𝑀 𝑟 ) ) ) ) = ( ( ( 𝑌 ∘ 𝑆 ) ‘ ( I ↾ 𝑁 ) ) · ( 𝑈 Σg ( 𝑟 ∈ 𝑁 ↦ ( ( ( I ↾ 𝑁 ) ‘ 𝑟 ) 𝑀 𝑟 ) ) ) ) )
14 1 2 matrcl ⊢ ( 𝑀 ∈ 𝐵 → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
15 14 simpld ⊢ ( 𝑀 ∈ 𝐵 → 𝑁 ∈ Fin )
16 4 5 coeq12i ⊢ ( 𝑌 ∘ 𝑆 ) = ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) )
17 16 a1i ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) → ( 𝑌 ∘ 𝑆 ) = ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) )
18 eqid ⊢ ( SymGrp ‘ 𝑁 ) = ( SymGrp ‘ 𝑁 )
19 18 symgid ⊢ ( 𝑁 ∈ Fin → ( I ↾ 𝑁 ) = ( 0g ‘ ( SymGrp ‘ 𝑁 ) ) )
20 19 adantl ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) → ( I ↾ 𝑁 ) = ( 0g ‘ ( SymGrp ‘ 𝑁 ) ) )
21 17 20 fveq12d ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) → ( ( 𝑌 ∘ 𝑆 ) ‘ ( I ↾ 𝑁 ) ) = ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ ( 0g ‘ ( SymGrp ‘ 𝑁 ) ) ) )
22 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
23 zrhpsgnmhm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) → ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ∈ ( ( SymGrp ‘ 𝑁 ) MndHom ( mulGrp ‘ 𝑅 ) ) )
24 3 oveq2i ⊢ ( ( SymGrp ‘ 𝑁 ) MndHom 𝑈 ) = ( ( SymGrp ‘ 𝑁 ) MndHom ( mulGrp ‘ 𝑅 ) )
25 23 24 eleqtrrdi ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) → ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ∈ ( ( SymGrp ‘ 𝑁 ) MndHom 𝑈 ) )
26 22 25 sylan ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) → ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ∈ ( ( SymGrp ‘ 𝑁 ) MndHom 𝑈 ) )
27 eqid ⊢ ( 0g ‘ ( SymGrp ‘ 𝑁 ) ) = ( 0g ‘ ( SymGrp ‘ 𝑁 ) )
28 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
29 3 28 ringidval ⊢ ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑈 )
30 27 29 mhm0 ⊢ ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ∈ ( ( SymGrp ‘ 𝑁 ) MndHom 𝑈 ) → ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ ( 0g ‘ ( SymGrp ‘ 𝑁 ) ) ) = ( 1r ‘ 𝑅 ) )
31 26 30 syl ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) → ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ ( 0g ‘ ( SymGrp ‘ 𝑁 ) ) ) = ( 1r ‘ 𝑅 ) )
32 21 31 eqtrd ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) → ( ( 𝑌 ∘ 𝑆 ) ‘ ( I ↾ 𝑁 ) ) = ( 1r ‘ 𝑅 ) )
33 fvresi ⊢ ( 𝑟 ∈ 𝑁 → ( ( I ↾ 𝑁 ) ‘ 𝑟 ) = 𝑟 )
34 33 adantl ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ 𝑟 ∈ 𝑁 ) → ( ( I ↾ 𝑁 ) ‘ 𝑟 ) = 𝑟 )
35 34 oveq1d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ 𝑟 ∈ 𝑁 ) → ( ( ( I ↾ 𝑁 ) ‘ 𝑟 ) 𝑀 𝑟 ) = ( 𝑟 𝑀 𝑟 ) )
36 35 mpteq2dva ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) → ( 𝑟 ∈ 𝑁 ↦ ( ( ( I ↾ 𝑁 ) ‘ 𝑟 ) 𝑀 𝑟 ) ) = ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑀 𝑟 ) ) )
37 36 oveq2d ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) → ( 𝑈 Σg ( 𝑟 ∈ 𝑁 ↦ ( ( ( I ↾ 𝑁 ) ‘ 𝑟 ) 𝑀 𝑟 ) ) ) = ( 𝑈 Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑀 𝑟 ) ) ) )
38 32 37 oveq12d ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) → ( ( ( 𝑌 ∘ 𝑆 ) ‘ ( I ↾ 𝑁 ) ) · ( 𝑈 Σg ( 𝑟 ∈ 𝑁 ↦ ( ( ( I ↾ 𝑁 ) ‘ 𝑟 ) 𝑀 𝑟 ) ) ) ) = ( ( 1r ‘ 𝑅 ) · ( 𝑈 Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑀 𝑟 ) ) ) ) )
39 15 38 sylan2 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( ( ( 𝑌 ∘ 𝑆 ) ‘ ( I ↾ 𝑁 ) ) · ( 𝑈 Σg ( 𝑟 ∈ 𝑁 ↦ ( ( ( I ↾ 𝑁 ) ‘ 𝑟 ) 𝑀 𝑟 ) ) ) ) = ( ( 1r ‘ 𝑅 ) · ( 𝑈 Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑀 𝑟 ) ) ) ) )
40 1 2 3 matgsumcl ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑈 Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑀 𝑟 ) ) ) ∈ ( Base ‘ 𝑅 ) )
41 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
42 41 6 28 ringlidm ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑈 Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑀 𝑟 ) ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 1r ‘ 𝑅 ) · ( 𝑈 Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑀 𝑟 ) ) ) ) = ( 𝑈 Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑀 𝑟 ) ) ) )
43 22 40 42 syl2an2r ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( ( 1r ‘ 𝑅 ) · ( 𝑈 Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑀 𝑟 ) ) ) ) = ( 𝑈 Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑀 𝑟 ) ) ) )
44 39 43 eqtrd ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( ( ( 𝑌 ∘ 𝑆 ) ‘ ( I ↾ 𝑁 ) ) · ( 𝑈 Σg ( 𝑟 ∈ 𝑁 ↦ ( ( ( I ↾ 𝑁 ) ‘ 𝑟 ) 𝑀 𝑟 ) ) ) ) = ( 𝑈 Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑀 𝑟 ) ) ) )
45 44 3adant3 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ 𝑃 = ( I ↾ 𝑁 ) ) → ( ( ( 𝑌 ∘ 𝑆 ) ‘ ( I ↾ 𝑁 ) ) · ( 𝑈 Σg ( 𝑟 ∈ 𝑁 ↦ ( ( ( I ↾ 𝑁 ) ‘ 𝑟 ) 𝑀 𝑟 ) ) ) ) = ( 𝑈 Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑀 𝑟 ) ) ) )
46 13 45 eqtrd ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ 𝑃 = ( I ↾ 𝑁 ) ) → ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑃 ) · ( 𝑈 Σg ( 𝑟 ∈ 𝑁 ↦ ( ( 𝑃 ‘ 𝑟 ) 𝑀 𝑟 ) ) ) ) = ( 𝑈 Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑀 𝑟 ) ) ) )