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 ) → ( 𝐷𝑀 ) = ( ( ♯ ‘ 𝑁 ) · 𝑋 ) ) )