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