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