Metamath Proof Explorer

Theorem mdetdiagid

Description: The determinant of a diagonal matrix with identical entries is the power of the entry 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 ‘ 𝑅 )
mdetdiagid.c ⊢ 𝐶 = ( Base ‘ 𝑅 )
mdetdiagid.t ⊢ · = ( .g ‘ 𝐺 )
Assertion mdetdiagid ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑋 ∈ 𝐶 ) ) → ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑀 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑋 , 0 ) → ( 𝐷 ‘ 𝑀 ) = ( ( ♯ ‘ 𝑁 ) · 𝑋 ) ) )

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 mdetdiagid.c ⊢ 𝐶 = ( Base ‘ 𝑅 )
7 mdetdiagid.t ⊢ · = ( .g ‘ 𝐺 )
8 simpl ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) → 𝑅 ∈ CRing )
9 8 adantr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑋 ∈ 𝐶 ) ) → 𝑅 ∈ CRing )
10 simpr ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) → 𝑁 ∈ Fin )
11 10 adantr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑋 ∈ 𝐶 ) ) → 𝑁 ∈ Fin )
12 simpl ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑋 ∈ 𝐶 ) → 𝑀 ∈ 𝐵 )
13 12 adantl ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑋 ∈ 𝐶 ) ) → 𝑀 ∈ 𝐵 )
14 9 11 13 3jca ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑋 ∈ 𝐶 ) ) → ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) )
15 14 adantr ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑋 ∈ 𝐶 ) ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑀 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑋 , 0 ) ) → ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) )
16 id ⊢ ( ( 𝑖 𝑀 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑋 , 0 ) → ( 𝑖 𝑀 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑋 , 0 ) )
17 ifnefalse ⊢ ( 𝑖 ≠ 𝑗 → if ( 𝑖 = 𝑗 , 𝑋 , 0 ) = 0 )
18 17 adantl ⊢ ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑋 ∈ 𝐶 ) ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑖 ≠ 𝑗 ) → if ( 𝑖 = 𝑗 , 𝑋 , 0 ) = 0 )
19 16 18 sylan9eqr ⊢ ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑋 ∈ 𝐶 ) ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑖 ≠ 𝑗 ) ∧ ( 𝑖 𝑀 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑋 , 0 ) ) → ( 𝑖 𝑀 𝑗 ) = 0 )
20 19 exp31 ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑋 ∈ 𝐶 ) ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( 𝑖 ≠ 𝑗 → ( ( 𝑖 𝑀 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑋 , 0 ) → ( 𝑖 𝑀 𝑗 ) = 0 ) ) )
21 20 com23 ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑋 ∈ 𝐶 ) ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( ( 𝑖 𝑀 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑋 , 0 ) → ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) )
22 21 ralimdva ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑋 ∈ 𝐶 ) ) ∧ 𝑖 ∈ 𝑁 ) → ( ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑀 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑋 , 0 ) → ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) )
23 22 ralimdva ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑋 ∈ 𝐶 ) ) → ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑀 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑋 , 0 ) → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) )
24 23 imp ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑋 ∈ 𝐶 ) ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑀 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑋 , 0 ) ) → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) )
25 1 2 3 4 5 mdetdiag ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) → ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) → ( 𝐷 ‘ 𝑀 ) = ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( 𝑘 𝑀 𝑘 ) ) ) ) )
26 15 24 25 sylc ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑋 ∈ 𝐶 ) ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑀 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑋 , 0 ) ) → ( 𝐷 ‘ 𝑀 ) = ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( 𝑘 𝑀 𝑘 ) ) ) )
27 oveq1 ⊢ ( 𝑖 = 𝑘 → ( 𝑖 𝑀 𝑗 ) = ( 𝑘 𝑀 𝑗 ) )
28 equequ1 ⊢ ( 𝑖 = 𝑘 → ( 𝑖 = 𝑗 ↔ 𝑘 = 𝑗 ) )
29 28 ifbid ⊢ ( 𝑖 = 𝑘 → if ( 𝑖 = 𝑗 , 𝑋 , 0 ) = if ( 𝑘 = 𝑗 , 𝑋 , 0 ) )
30 27 29 eqeq12d ⊢ ( 𝑖 = 𝑘 → ( ( 𝑖 𝑀 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑋 , 0 ) ↔ ( 𝑘 𝑀 𝑗 ) = if ( 𝑘 = 𝑗 , 𝑋 , 0 ) ) )
31 oveq2 ⊢ ( 𝑗 = 𝑘 → ( 𝑘 𝑀 𝑗 ) = ( 𝑘 𝑀 𝑘 ) )
32 equequ2 ⊢ ( 𝑗 = 𝑘 → ( 𝑘 = 𝑗 ↔ 𝑘 = 𝑘 ) )
33 32 ifbid ⊢ ( 𝑗 = 𝑘 → if ( 𝑘 = 𝑗 , 𝑋 , 0 ) = if ( 𝑘 = 𝑘 , 𝑋 , 0 ) )
34 31 33 eqeq12d ⊢ ( 𝑗 = 𝑘 → ( ( 𝑘 𝑀 𝑗 ) = if ( 𝑘 = 𝑗 , 𝑋 , 0 ) ↔ ( 𝑘 𝑀 𝑘 ) = if ( 𝑘 = 𝑘 , 𝑋 , 0 ) ) )
35 30 34 rspc2v ⊢ ( ( 𝑘 ∈ 𝑁 ∧ 𝑘 ∈ 𝑁 ) → ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑀 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑋 , 0 ) → ( 𝑘 𝑀 𝑘 ) = if ( 𝑘 = 𝑘 , 𝑋 , 0 ) ) )
36 35 anidms ⊢ ( 𝑘 ∈ 𝑁 → ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑀 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑋 , 0 ) → ( 𝑘 𝑀 𝑘 ) = if ( 𝑘 = 𝑘 , 𝑋 , 0 ) ) )
37 36 adantl ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑋 ∈ 𝐶 ) ) ∧ 𝑘 ∈ 𝑁 ) → ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑀 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑋 , 0 ) → ( 𝑘 𝑀 𝑘 ) = if ( 𝑘 = 𝑘 , 𝑋 , 0 ) ) )
38 37 imp ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑋 ∈ 𝐶 ) ) ∧ 𝑘 ∈ 𝑁 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑀 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑋 , 0 ) ) → ( 𝑘 𝑀 𝑘 ) = if ( 𝑘 = 𝑘 , 𝑋 , 0 ) )
39 equid ⊢ 𝑘 = 𝑘
40 39 iftruei ⊢ if ( 𝑘 = 𝑘 , 𝑋 , 0 ) = 𝑋
41 38 40 eqtrdi ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑋 ∈ 𝐶 ) ) ∧ 𝑘 ∈ 𝑁 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑀 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑋 , 0 ) ) → ( 𝑘 𝑀 𝑘 ) = 𝑋 )
42 41 an32s ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑋 ∈ 𝐶 ) ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑀 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑋 , 0 ) ) ∧ 𝑘 ∈ 𝑁 ) → ( 𝑘 𝑀 𝑘 ) = 𝑋 )
43 42 mpteq2dva ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑋 ∈ 𝐶 ) ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑀 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑋 , 0 ) ) → ( 𝑘 ∈ 𝑁 ↦ ( 𝑘 𝑀 𝑘 ) ) = ( 𝑘 ∈ 𝑁 ↦ 𝑋 ) )
44 43 oveq2d ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑋 ∈ 𝐶 ) ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑀 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑋 , 0 ) ) → ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( 𝑘 𝑀 𝑘 ) ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ 𝑋 ) ) )
45 4 crngmgp ⊢ ( 𝑅 ∈ CRing → 𝐺 ∈ CMnd )
46 cmnmnd ⊢ ( 𝐺 ∈ CMnd → 𝐺 ∈ Mnd )
47 45 46 syl ⊢ ( 𝑅 ∈ CRing → 𝐺 ∈ Mnd )
48 47 adantr ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) → 𝐺 ∈ Mnd )
49 simpr ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑋 ∈ 𝐶 ) → 𝑋 ∈ 𝐶 )
50 4 6 mgpbas ⊢ 𝐶 = ( Base ‘ 𝐺 )
51 50 7 gsumconst ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑁 ∈ Fin ∧ 𝑋 ∈ 𝐶 ) → ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ 𝑋 ) ) = ( ( ♯ ‘ 𝑁 ) · 𝑋 ) )
52 48 10 49 51 syl2an3an ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑋 ∈ 𝐶 ) ) → ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ 𝑋 ) ) = ( ( ♯ ‘ 𝑁 ) · 𝑋 ) )
53 52 adantr ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑋 ∈ 𝐶 ) ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑀 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑋 , 0 ) ) → ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ 𝑋 ) ) = ( ( ♯ ‘ 𝑁 ) · 𝑋 ) )
54 26 44 53 3eqtrd ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑋 ∈ 𝐶 ) ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑀 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑋 , 0 ) ) → ( 𝐷 ‘ 𝑀 ) = ( ( ♯ ‘ 𝑁 ) · 𝑋 ) )
55 54 ex ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑋 ∈ 𝐶 ) ) → ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑀 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑋 , 0 ) → ( 𝐷 ‘ 𝑀 ) = ( ( ♯ ‘ 𝑁 ) · 𝑋 ) ) )