Metamath Proof Explorer

Theorem mdetdiag

Description: The determinant of a diagonal matrix is the product of the entries in the diagonal. (Contributed by AV, 17-Aug-2019)

Ref Expression
Hypotheses mdetdiag.d ⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
mdetdiag.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
mdetdiag.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
mdetdiag.g ⊢ 𝐺 = ( mulGrp ‘ 𝑅 )
mdetdiag.0 ⊢ 0 = ( 0g ‘ 𝑅 )
Assertion mdetdiag ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) → ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) → ( 𝐷 ‘ 𝑀 ) = ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( 𝑘 𝑀 𝑘 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 mdetdiag.d ⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
2 mdetdiag.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
3 mdetdiag.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
4 mdetdiag.g ⊢ 𝐺 = ( mulGrp ‘ 𝑅 )
5 mdetdiag.0 ⊢ 0 = ( 0g ‘ 𝑅 )
6 simpl3 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) → 𝑀 ∈ 𝐵 )
7 eqid ⊢ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
8 eqid ⊢ ( ℤRHom ‘ 𝑅 ) = ( ℤRHom ‘ 𝑅 )
9 eqid ⊢ ( pmSgn ‘ 𝑁 ) = ( pmSgn ‘ 𝑁 )
10 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
11 1 2 3 7 8 9 10 4 mdetleib ⊢ ( 𝑀 ∈ 𝐵 → ( 𝐷 ‘ 𝑀 ) = ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑘 ) 𝑀 𝑘 ) ) ) ) ) ) )
12 6 11 syl ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) → ( 𝐷 ‘ 𝑀 ) = ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑘 ) 𝑀 𝑘 ) ) ) ) ) ) )
13 simpl1 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) → 𝑅 ∈ CRing )
14 13 ad2antrr ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) ∧ 𝑝 = ( I ↾ 𝑁 ) ) → 𝑅 ∈ CRing )
15 6 ad2antrr ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) ∧ 𝑝 = ( I ↾ 𝑁 ) ) → 𝑀 ∈ 𝐵 )
16 simpr ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) ∧ 𝑝 = ( I ↾ 𝑁 ) ) → 𝑝 = ( I ↾ 𝑁 ) )
17 2 3 4 8 9 10 madetsumid ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ 𝑝 = ( I ↾ 𝑁 ) ) → ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑘 ) 𝑀 𝑘 ) ) ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( 𝑘 𝑀 𝑘 ) ) ) )
18 14 15 16 17 syl3anc ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) ∧ 𝑝 = ( I ↾ 𝑁 ) ) → ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑘 ) 𝑀 𝑘 ) ) ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( 𝑘 𝑀 𝑘 ) ) ) )
19 iftrue ⊢ ( 𝑝 = ( I ↾ 𝑁 ) → if ( 𝑝 = ( I ↾ 𝑁 ) , ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( 𝑘 𝑀 𝑘 ) ) ) , 0 ) = ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( 𝑘 𝑀 𝑘 ) ) ) )
20 19 eqcomd ⊢ ( 𝑝 = ( I ↾ 𝑁 ) → ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( 𝑘 𝑀 𝑘 ) ) ) = if ( 𝑝 = ( I ↾ 𝑁 ) , ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( 𝑘 𝑀 𝑘 ) ) ) , 0 ) )
21 20 adantl ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) ∧ 𝑝 = ( I ↾ 𝑁 ) ) → ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( 𝑘 𝑀 𝑘 ) ) ) = if ( 𝑝 = ( I ↾ 𝑁 ) , ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( 𝑘 𝑀 𝑘 ) ) ) , 0 ) )
22 18 21 eqtrd ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) ∧ 𝑝 = ( I ↾ 𝑁 ) ) → ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑘 ) 𝑀 𝑘 ) ) ) ) = if ( 𝑝 = ( I ↾ 𝑁 ) , ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( 𝑘 𝑀 𝑘 ) ) ) , 0 ) )
23 simplll ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) ∧ ¬ 𝑝 = ( I ↾ 𝑁 ) ) → ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) )
24 simpr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) )
25 24 ad2antrr ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) ∧ ¬ 𝑝 = ( I ↾ 𝑁 ) ) → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) )
26 simpr ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) )
27 neqne ⊢ ( ¬ 𝑝 = ( I ↾ 𝑁 ) → 𝑝 ≠ ( I ↾ 𝑁 ) )
28 26 27 anim12i ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) ∧ ¬ 𝑝 = ( I ↾ 𝑁 ) ) → ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑝 ≠ ( I ↾ 𝑁 ) ) )
29 1 2 3 4 5 7 8 9 10 mdetdiaglem ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ∧ ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑝 ≠ ( I ↾ 𝑁 ) ) ) → ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑘 ) 𝑀 𝑘 ) ) ) ) = 0 )
30 23 25 28 29 syl3anc ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) ∧ ¬ 𝑝 = ( I ↾ 𝑁 ) ) → ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑘 ) 𝑀 𝑘 ) ) ) ) = 0 )
31 iffalse ⊢ ( ¬ 𝑝 = ( I ↾ 𝑁 ) → if ( 𝑝 = ( I ↾ 𝑁 ) , ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( 𝑘 𝑀 𝑘 ) ) ) , 0 ) = 0 )
32 31 adantl ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) ∧ ¬ 𝑝 = ( I ↾ 𝑁 ) ) → if ( 𝑝 = ( I ↾ 𝑁 ) , ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( 𝑘 𝑀 𝑘 ) ) ) , 0 ) = 0 )
33 32 eqcomd ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) ∧ ¬ 𝑝 = ( I ↾ 𝑁 ) ) → 0 = if ( 𝑝 = ( I ↾ 𝑁 ) , ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( 𝑘 𝑀 𝑘 ) ) ) , 0 ) )
34 30 33 eqtrd ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) ∧ ¬ 𝑝 = ( I ↾ 𝑁 ) ) → ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑘 ) 𝑀 𝑘 ) ) ) ) = if ( 𝑝 = ( I ↾ 𝑁 ) , ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( 𝑘 𝑀 𝑘 ) ) ) , 0 ) )
35 22 34 pm2.61dan ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑘 ) 𝑀 𝑘 ) ) ) ) = if ( 𝑝 = ( I ↾ 𝑁 ) , ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( 𝑘 𝑀 𝑘 ) ) ) , 0 ) )
36 35 mpteq2dva ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) → ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑘 ) 𝑀 𝑘 ) ) ) ) ) = ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ if ( 𝑝 = ( I ↾ 𝑁 ) , ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( 𝑘 𝑀 𝑘 ) ) ) , 0 ) ) )
37 36 oveq2d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) → ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑘 ) 𝑀 𝑘 ) ) ) ) ) ) = ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ if ( 𝑝 = ( I ↾ 𝑁 ) , ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( 𝑘 𝑀 𝑘 ) ) ) , 0 ) ) ) )
38 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
39 ringmnd ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Mnd )
40 38 39 syl ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Mnd )
41 40 3ad2ant1 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) → 𝑅 ∈ Mnd )
42 41 adantr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) → 𝑅 ∈ Mnd )
43 fvexd ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) → ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∈ V )
44 eqid ⊢ ( SymGrp ‘ 𝑁 ) = ( SymGrp ‘ 𝑁 )
45 44 symgid ⊢ ( 𝑁 ∈ Fin → ( I ↾ 𝑁 ) = ( 0g ‘ ( SymGrp ‘ 𝑁 ) ) )
46 45 3ad2ant2 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) → ( I ↾ 𝑁 ) = ( 0g ‘ ( SymGrp ‘ 𝑁 ) ) )
47 44 symggrp ⊢ ( 𝑁 ∈ Fin → ( SymGrp ‘ 𝑁 ) ∈ Grp )
48 47 3ad2ant2 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) → ( SymGrp ‘ 𝑁 ) ∈ Grp )
49 eqid ⊢ ( 0g ‘ ( SymGrp ‘ 𝑁 ) ) = ( 0g ‘ ( SymGrp ‘ 𝑁 ) )
50 7 49 grpidcl ⊢ ( ( SymGrp ‘ 𝑁 ) ∈ Grp → ( 0g ‘ ( SymGrp ‘ 𝑁 ) ) ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) )
51 48 50 syl ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) → ( 0g ‘ ( SymGrp ‘ 𝑁 ) ) ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) )
52 46 51 eqeltrd ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) → ( I ↾ 𝑁 ) ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) )
53 52 adantr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) → ( I ↾ 𝑁 ) ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) )
54 eqid ⊢ ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ if ( 𝑝 = ( I ↾ 𝑁 ) , ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( 𝑘 𝑀 𝑘 ) ) ) , 0 ) ) = ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ if ( 𝑝 = ( I ↾ 𝑁 ) , ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( 𝑘 𝑀 𝑘 ) ) ) , 0 ) )
55 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
56 4 55 mgpbas ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝐺 )
57 4 crngmgp ⊢ ( 𝑅 ∈ CRing → 𝐺 ∈ CMnd )
58 57 3ad2ant1 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) → 𝐺 ∈ CMnd )
59 58 adantr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) → 𝐺 ∈ CMnd )
60 simpl2 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) → 𝑁 ∈ Fin )
61 simpr ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) ∧ 𝑘 ∈ 𝑁 ) → 𝑘 ∈ 𝑁 )
62 3 eleq2i ⊢ ( 𝑀 ∈ 𝐵 ↔ 𝑀 ∈ ( Base ‘ 𝐴 ) )
63 62 biimpi ⊢ ( 𝑀 ∈ 𝐵 → 𝑀 ∈ ( Base ‘ 𝐴 ) )
64 63 3ad2ant3 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) → 𝑀 ∈ ( Base ‘ 𝐴 ) )
65 64 ad2antrr ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) ∧ 𝑘 ∈ 𝑁 ) → 𝑀 ∈ ( Base ‘ 𝐴 ) )
66 2 55 matecl ⊢ ( ( 𝑘 ∈ 𝑁 ∧ 𝑘 ∈ 𝑁 ∧ 𝑀 ∈ ( Base ‘ 𝐴 ) ) → ( 𝑘 𝑀 𝑘 ) ∈ ( Base ‘ 𝑅 ) )
67 61 61 65 66 syl3anc ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) ∧ 𝑘 ∈ 𝑁 ) → ( 𝑘 𝑀 𝑘 ) ∈ ( Base ‘ 𝑅 ) )
68 67 ralrimiva ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) → ∀ 𝑘 ∈ 𝑁 ( 𝑘 𝑀 𝑘 ) ∈ ( Base ‘ 𝑅 ) )
69 56 59 60 68 gsummptcl ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) → ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( 𝑘 𝑀 𝑘 ) ) ) ∈ ( Base ‘ 𝑅 ) )
70 5 42 43 53 54 69 gsummptif1n0 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) → ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ if ( 𝑝 = ( I ↾ 𝑁 ) , ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( 𝑘 𝑀 𝑘 ) ) ) , 0 ) ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( 𝑘 𝑀 𝑘 ) ) ) )
71 12 37 70 3eqtrd ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) → ( 𝐷 ‘ 𝑀 ) = ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( 𝑘 𝑀 𝑘 ) ) ) )
72 71 ex ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) → ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) → ( 𝐷 ‘ 𝑀 ) = ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( 𝑘 𝑀 𝑘 ) ) ) ) )