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 unit of that ring. (Contributed by AV, 28-Feb-2019)

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

Proof

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