Metamath Proof Explorer

Theorem mdet0pr

Description: The determinant function for 0-dimensional matrices on a given ring is the function mapping the empty set to the unity element of that ring. (Contributed by AV, 28-Feb-2019)

Ref Expression
Assertion mdet0pr ⊢R∈Ring→∅maDetR=∅1R

Proof

Step Hyp Ref Expression
1 eqid ⊢∅maDetR=∅maDetR
2 eqid ⊢∅MatR=∅MatR
3 eqid ⊢Base∅MatR=Base∅MatR
4 eqid ⊢BaseSymGrp⁡∅=BaseSymGrp⁡∅
5 eqid ⊢ℤRHom⁡R=ℤRHom⁡R
6 eqid ⊢pmSgn⁡∅=pmSgn⁡∅
7 eqid ⊢⋅R=⋅R
8 eqid ⊢mulGrpR=mulGrpR
9 1 2 3 4 5 6 7 8 mdetfval ⊢∅maDetR=m∈Base∅MatR⟼∑Rp∈BaseSymGrp⁡∅ℤRHom⁡R∘pmSgn⁡∅⁡p⋅R∑mulGrpRx∈∅p⁡xmx
10 9 a1i ⊢R∈Ring→∅maDetR=m∈Base∅MatR⟼∑Rp∈BaseSymGrp⁡∅ℤRHom⁡R∘pmSgn⁡∅⁡p⋅R∑mulGrpRx∈∅p⁡xmx
11 mat0dimbas0 ⊢R∈Ring→Base∅MatR=∅
12 11 mpteq1d ⊢R∈Ring→m∈Base∅MatR⟼∑Rp∈BaseSymGrp⁡∅ℤRHom⁡R∘pmSgn⁡∅⁡p⋅R∑mulGrpRx∈∅p⁡xmx=m∈∅⟼∑Rp∈BaseSymGrp⁡∅ℤRHom⁡R∘pmSgn⁡∅⁡p⋅R∑mulGrpRx∈∅p⁡xmx
13 0ex ⊢∅∈V
14 13 a1i ⊢R∈Ring→∅∈V
15 ovex ⊢∑Rp∈BaseSymGrp⁡∅ℤRHom⁡R∘pmSgn⁡∅⁡p⋅R∑mulGrpRx∈∅p⁡x∅x∈V
16 oveq ⊢m=∅→p⁡xmx=p⁡x∅x
17 16 mpteq2dv ⊢m=∅→x∈∅⟼p⁡xmx=x∈∅⟼p⁡x∅x
18 17 oveq2d ⊢m=∅→∑mulGrpRx∈∅p⁡xmx=∑mulGrpRx∈∅p⁡x∅x
19 18 oveq2d ⊢m=∅→ℤRHom⁡R∘pmSgn⁡∅⁡p⋅R∑mulGrpRx∈∅p⁡xmx=ℤRHom⁡R∘pmSgn⁡∅⁡p⋅R∑mulGrpRx∈∅p⁡x∅x
20 19 mpteq2dv ⊢m=∅→p∈BaseSymGrp⁡∅⟼ℤRHom⁡R∘pmSgn⁡∅⁡p⋅R∑mulGrpRx∈∅p⁡xmx=p∈BaseSymGrp⁡∅⟼ℤRHom⁡R∘pmSgn⁡∅⁡p⋅R∑mulGrpRx∈∅p⁡x∅x
21 20 oveq2d ⊢m=∅→∑Rp∈BaseSymGrp⁡∅ℤRHom⁡R∘pmSgn⁡∅⁡p⋅R∑mulGrpRx∈∅p⁡xmx=∑Rp∈BaseSymGrp⁡∅ℤRHom⁡R∘pmSgn⁡∅⁡p⋅R∑mulGrpRx∈∅p⁡x∅x
22 21 fmptsng ⊢∅∈V∧∑Rp∈BaseSymGrp⁡∅ℤRHom⁡R∘pmSgn⁡∅⁡p⋅R∑mulGrpRx∈∅p⁡x∅x∈V→∅∑Rp∈BaseSymGrp⁡∅ℤRHom⁡R∘pmSgn⁡∅⁡p⋅R∑mulGrpRx∈∅p⁡x∅x=m∈∅⟼∑Rp∈BaseSymGrp⁡∅ℤRHom⁡R∘pmSgn⁡∅⁡p⋅R∑mulGrpRx∈∅p⁡xmx
23 14 15 22 sylancl ⊢R∈Ring→∅∑Rp∈BaseSymGrp⁡∅ℤRHom⁡R∘pmSgn⁡∅⁡p⋅R∑mulGrpRx∈∅p⁡x∅x=m∈∅⟼∑Rp∈BaseSymGrp⁡∅ℤRHom⁡R∘pmSgn⁡∅⁡p⋅R∑mulGrpRx∈∅p⁡xmx
24 mpt0 ⊢x∈∅⟼p⁡x∅x=∅
25 24 a1i ⊢R∈Ring→x∈∅⟼p⁡x∅x=∅
26 25 oveq2d ⊢R∈Ring→∑mulGrpRx∈∅p⁡x∅x=∑mulGrpR∅
27 eqid ⊢0mulGrpR=0mulGrpR
28 27 gsum0 ⊢∑mulGrpR∅=0mulGrpR
29 26 28 eqtrdi ⊢R∈Ring→∑mulGrpRx∈∅p⁡x∅x=0mulGrpR
30 29 oveq2d ⊢R∈Ring→ℤRHom⁡R∘pmSgn⁡∅⁡p⋅R∑mulGrpRx∈∅p⁡x∅x=ℤRHom⁡R∘pmSgn⁡∅⁡p⋅R0mulGrpR
31 30 mpteq2dv ⊢R∈Ring→p∈BaseSymGrp⁡∅⟼ℤRHom⁡R∘pmSgn⁡∅⁡p⋅R∑mulGrpRx∈∅p⁡x∅x=p∈BaseSymGrp⁡∅⟼ℤRHom⁡R∘pmSgn⁡∅⁡p⋅R0mulGrpR
32 31 oveq2d ⊢R∈Ring→∑Rp∈BaseSymGrp⁡∅ℤRHom⁡R∘pmSgn⁡∅⁡p⋅R∑mulGrpRx∈∅p⁡x∅x=∑Rp∈BaseSymGrp⁡∅ℤRHom⁡R∘pmSgn⁡∅⁡p⋅R0mulGrpR
33 eqid ⊢1R=1R
34 8 33 ringidval ⊢1R=0mulGrpR
35 34 eqcomi ⊢0mulGrpR=1R
36 35 a1i ⊢R∈Ring∧p∈BaseSymGrp⁡∅→0mulGrpR=1R
37 36 oveq2d ⊢R∈Ring∧p∈BaseSymGrp⁡∅→ℤRHom⁡R∘pmSgn⁡∅⁡p⋅R0mulGrpR=ℤRHom⁡R∘pmSgn⁡∅⁡p⋅R1R
38 0fin ⊢∅∈Fin
39 4 6 5 zrhcopsgnelbas ⊢R∈Ring∧∅∈Fin∧p∈BaseSymGrp⁡∅→ℤRHom⁡R∘pmSgn⁡∅⁡p∈BaseR
40 38 39 mp3an2 ⊢R∈Ring∧p∈BaseSymGrp⁡∅→ℤRHom⁡R∘pmSgn⁡∅⁡p∈BaseR
41 eqid ⊢BaseR=BaseR
42 41 7 33 ringridm ⊢R∈Ring∧ℤRHom⁡R∘pmSgn⁡∅⁡p∈BaseR→ℤRHom⁡R∘pmSgn⁡∅⁡p⋅R1R=ℤRHom⁡R∘pmSgn⁡∅⁡p
43 40 42 syldan ⊢R∈Ring∧p∈BaseSymGrp⁡∅→ℤRHom⁡R∘pmSgn⁡∅⁡p⋅R1R=ℤRHom⁡R∘pmSgn⁡∅⁡p
44 37 43 eqtrd ⊢R∈Ring∧p∈BaseSymGrp⁡∅→ℤRHom⁡R∘pmSgn⁡∅⁡p⋅R0mulGrpR=ℤRHom⁡R∘pmSgn⁡∅⁡p
45 44 mpteq2dva ⊢R∈Ring→p∈BaseSymGrp⁡∅⟼ℤRHom⁡R∘pmSgn⁡∅⁡p⋅R0mulGrpR=p∈BaseSymGrp⁡∅⟼ℤRHom⁡R∘pmSgn⁡∅⁡p
46 45 oveq2d ⊢R∈Ring→∑Rp∈BaseSymGrp⁡∅ℤRHom⁡R∘pmSgn⁡∅⁡p⋅R0mulGrpR=∑Rp∈BaseSymGrp⁡∅ℤRHom⁡R∘pmSgn⁡∅⁡p
47 simpl ⊢R∈Ring∧p∈BaseSymGrp⁡∅→R∈Ring
48 38 a1i ⊢R∈Ring∧p∈BaseSymGrp⁡∅→∅∈Fin
49 simpr ⊢R∈Ring∧p∈BaseSymGrp⁡∅→p∈BaseSymGrp⁡∅
50 elsni ⊢p∈∅→p=∅
51 fveq2 ⊢p=∅→pmSgn⁡∅⁡p=pmSgn⁡∅⁡∅
52 psgn0fv0 ⊢pmSgn⁡∅⁡∅=1
53 51 52 eqtrdi ⊢p=∅→pmSgn⁡∅⁡p=1
54 50 53 syl ⊢p∈∅→pmSgn⁡∅⁡p=1
55 symgbas0 ⊢BaseSymGrp⁡∅=∅
56 54 55 eleq2s ⊢p∈BaseSymGrp⁡∅→pmSgn⁡∅⁡p=1
57 56 adantl ⊢R∈Ring∧p∈BaseSymGrp⁡∅→pmSgn⁡∅⁡p=1
58 eqid ⊢SymGrp⁡∅=SymGrp⁡∅
59 58 4 6 psgnevpmb ⊢∅∈Fin→p∈pmEven⁡∅↔p∈BaseSymGrp⁡∅∧pmSgn⁡∅⁡p=1
60 48 59 syl ⊢R∈Ring∧p∈BaseSymGrp⁡∅→p∈pmEven⁡∅↔p∈BaseSymGrp⁡∅∧pmSgn⁡∅⁡p=1
61 49 57 60 mpbir2and ⊢R∈Ring∧p∈BaseSymGrp⁡∅→p∈pmEven⁡∅
62 5 6 33 zrhpsgnevpm ⊢R∈Ring∧∅∈Fin∧p∈pmEven⁡∅→ℤRHom⁡R∘pmSgn⁡∅⁡p=1R
63 47 48 61 62 syl3anc ⊢R∈Ring∧p∈BaseSymGrp⁡∅→ℤRHom⁡R∘pmSgn⁡∅⁡p=1R
64 63 mpteq2dva ⊢R∈Ring→p∈BaseSymGrp⁡∅⟼ℤRHom⁡R∘pmSgn⁡∅⁡p=p∈BaseSymGrp⁡∅⟼1R
65 64 oveq2d ⊢R∈Ring→∑Rp∈BaseSymGrp⁡∅ℤRHom⁡R∘pmSgn⁡∅⁡p=∑Rp∈BaseSymGrp⁡∅1R
66 55 a1i ⊢R∈Ring→BaseSymGrp⁡∅=∅
67 66 mpteq1d ⊢R∈Ring→p∈BaseSymGrp⁡∅⟼1R=p∈∅⟼1R
68 67 oveq2d ⊢R∈Ring→∑Rp∈BaseSymGrp⁡∅1R=∑Rp∈∅1R
69 ringmnd ⊢R∈Ring→R∈Mnd
70 41 33 ringidcl ⊢R∈Ring→1R∈BaseR
71 eqidd ⊢p=∅→1R=1R
72 41 71 gsumsn ⊢R∈Mnd∧∅∈V∧1R∈BaseR→∑Rp∈∅1R=1R
73 69 14 70 72 syl3anc ⊢R∈Ring→∑Rp∈∅1R=1R
74 65 68 73 3eqtrd ⊢R∈Ring→∑Rp∈BaseSymGrp⁡∅ℤRHom⁡R∘pmSgn⁡∅⁡p=1R
75 32 46 74 3eqtrd ⊢R∈Ring→∑Rp∈BaseSymGrp⁡∅ℤRHom⁡R∘pmSgn⁡∅⁡p⋅R∑mulGrpRx∈∅p⁡x∅x=1R
76 75 opeq2d ⊢R∈Ring→∅∑Rp∈BaseSymGrp⁡∅ℤRHom⁡R∘pmSgn⁡∅⁡p⋅R∑mulGrpRx∈∅p⁡x∅x=∅1R
77 76 sneqd ⊢R∈Ring→∅∑Rp∈BaseSymGrp⁡∅ℤRHom⁡R∘pmSgn⁡∅⁡p⋅R∑mulGrpRx∈∅p⁡x∅x=∅1R
78 23 77 eqtr3d ⊢R∈Ring→m∈∅⟼∑Rp∈BaseSymGrp⁡∅ℤRHom⁡R∘pmSgn⁡∅⁡p⋅R∑mulGrpRx∈∅p⁡xmx=∅1R
79 10 12 78 3eqtrd ⊢R∈Ring→∅maDetR=∅1R