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 e. Ring -> ( (/) maDet R ) = { <. (/) , ( 1r ` 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 
 |-  ( ZRHom ` R ) = ( ZRHom ` R )
6 eqid 
 |-  ( pmSgn ` (/) ) = ( pmSgn ` (/) )
7 eqid 
 |-  ( .r ` R ) = ( .r ` R )
8 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
9 1 2 3 4 5 6 7 8 mdetfval 
 |-  ( (/) maDet R ) = ( m e. ( Base ` ( (/) Mat R ) ) |-> ( R gsum ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( x e. (/) |-> ( ( p ` x ) m x ) ) ) ) ) ) )
10 9 a1i 
 |-  ( R e. Ring -> ( (/) maDet R ) = ( m e. ( Base ` ( (/) Mat R ) ) |-> ( R gsum ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( x e. (/) |-> ( ( p ` x ) m x ) ) ) ) ) ) ) )
11 mat0dimbas0 
 |-  ( R e. Ring -> ( Base ` ( (/) Mat R ) ) = { (/) } )
12 11 mpteq1d 
 |-  ( R e. Ring -> ( m e. ( Base ` ( (/) Mat R ) ) |-> ( R gsum ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( x e. (/) |-> ( ( p ` x ) m x ) ) ) ) ) ) ) = ( m e. { (/) } |-> ( R gsum ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( x e. (/) |-> ( ( p ` x ) m x ) ) ) ) ) ) ) )
13 0ex 
 |-  (/) e. _V
14 13 a1i 
 |-  ( R e. Ring -> (/) e. _V )
15 ovex 
 |-  ( R gsum ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( x e. (/) |-> ( ( p ` x ) (/) x ) ) ) ) ) ) e. _V
16 oveq 
 |-  ( m = (/) -> ( ( p ` x ) m x ) = ( ( p ` x ) (/) x ) )
17 16 mpteq2dv 
 |-  ( m = (/) -> ( x e. (/) |-> ( ( p ` x ) m x ) ) = ( x e. (/) |-> ( ( p ` x ) (/) x ) ) )
18 17 oveq2d 
 |-  ( m = (/) -> ( ( mulGrp ` R ) gsum ( x e. (/) |-> ( ( p ` x ) m x ) ) ) = ( ( mulGrp ` R ) gsum ( x e. (/) |-> ( ( p ` x ) (/) x ) ) ) )
19 18 oveq2d 
 |-  ( m = (/) -> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( x e. (/) |-> ( ( p ` x ) m x ) ) ) ) = ( ( ( ( ZRHom ` R ) o. ( pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( x e. (/) |-> ( ( p ` x ) (/) x ) ) ) ) )
20 19 mpteq2dv 
 |-  ( m = (/) -> ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( x e. (/) |-> ( ( p ` x ) m x ) ) ) ) ) = ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( x e. (/) |-> ( ( p ` x ) (/) x ) ) ) ) ) )
21 20 oveq2d 
 |-  ( m = (/) -> ( R gsum ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( x e. (/) |-> ( ( p ` x ) m x ) ) ) ) ) ) = ( R gsum ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( x e. (/) |-> ( ( p ` x ) (/) x ) ) ) ) ) ) )
22 21 fmptsng 
 |-  ( ( (/) e. _V /\ ( R gsum ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( x e. (/) |-> ( ( p ` x ) (/) x ) ) ) ) ) ) e. _V ) -> { <. (/) , ( R gsum ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( x e. (/) |-> ( ( p ` x ) (/) x ) ) ) ) ) ) >. } = ( m e. { (/) } |-> ( R gsum ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( x e. (/) |-> ( ( p ` x ) m x ) ) ) ) ) ) ) )
23 14 15 22 sylancl 
 |-  ( R e. Ring -> { <. (/) , ( R gsum ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( x e. (/) |-> ( ( p ` x ) (/) x ) ) ) ) ) ) >. } = ( m e. { (/) } |-> ( R gsum ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( x e. (/) |-> ( ( p ` x ) m x ) ) ) ) ) ) ) )
24 mpt0 
 |-  ( x e. (/) |-> ( ( p ` x ) (/) x ) ) = (/)
25 24 a1i 
 |-  ( R e. Ring -> ( x e. (/) |-> ( ( p ` x ) (/) x ) ) = (/) )
26 25 oveq2d 
 |-  ( R e. Ring -> ( ( mulGrp ` R ) gsum ( x e. (/) |-> ( ( p ` x ) (/) x ) ) ) = ( ( mulGrp ` R ) gsum (/) ) )
27 eqid 
 |-  ( 0g ` ( mulGrp ` R ) ) = ( 0g ` ( mulGrp ` R ) )
28 27 gsum0 
 |-  ( ( mulGrp ` R ) gsum (/) ) = ( 0g ` ( mulGrp ` R ) )
29 26 28 eqtrdi 
 |-  ( R e. Ring -> ( ( mulGrp ` R ) gsum ( x e. (/) |-> ( ( p ` x ) (/) x ) ) ) = ( 0g ` ( mulGrp ` R ) ) )
30 29 oveq2d 
 |-  ( R e. Ring -> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( x e. (/) |-> ( ( p ` x ) (/) x ) ) ) ) = ( ( ( ( ZRHom ` R ) o. ( pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( 0g ` ( mulGrp ` R ) ) ) )
31 30 mpteq2dv 
 |-  ( R e. Ring -> ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( x e. (/) |-> ( ( p ` x ) (/) x ) ) ) ) ) = ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( 0g ` ( mulGrp ` R ) ) ) ) )
32 31 oveq2d 
 |-  ( R e. Ring -> ( R gsum ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( x e. (/) |-> ( ( p ` x ) (/) x ) ) ) ) ) ) = ( R gsum ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( 0g ` ( mulGrp ` R ) ) ) ) ) )
33 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
34 8 33 ringidval 
 |-  ( 1r ` R ) = ( 0g ` ( mulGrp ` R ) )
35 34 eqcomi 
 |-  ( 0g ` ( mulGrp ` R ) ) = ( 1r ` R )
36 35 a1i 
 |-  ( ( R e. Ring /\ p e. ( Base ` ( SymGrp ` (/) ) ) ) -> ( 0g ` ( mulGrp ` R ) ) = ( 1r ` R ) )
37 36 oveq2d 
 |-  ( ( R e. Ring /\ p e. ( Base ` ( SymGrp ` (/) ) ) ) -> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( 0g ` ( mulGrp ` R ) ) ) = ( ( ( ( ZRHom ` R ) o. ( pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( 1r ` R ) ) )
38 0fin 
 |-  (/) e. Fin
39 4 6 5 zrhcopsgnelbas 
 |-  ( ( R e. Ring /\ (/) e. Fin /\ p e. ( Base ` ( SymGrp ` (/) ) ) ) -> ( ( ( ZRHom ` R ) o. ( pmSgn ` (/) ) ) ` p ) e. ( Base ` R ) )
40 38 39 mp3an2 
 |-  ( ( R e. Ring /\ p e. ( Base ` ( SymGrp ` (/) ) ) ) -> ( ( ( ZRHom ` R ) o. ( pmSgn ` (/) ) ) ` p ) e. ( Base ` R ) )
41 eqid 
 |-  ( Base ` R ) = ( Base ` R )
42 41 7 33 ringridm 
 |-  ( ( R e. Ring /\ ( ( ( ZRHom ` R ) o. ( pmSgn ` (/) ) ) ` p ) e. ( Base ` R ) ) -> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( 1r ` R ) ) = ( ( ( ZRHom ` R ) o. ( pmSgn ` (/) ) ) ` p ) )
43 40 42 syldan 
 |-  ( ( R e. Ring /\ p e. ( Base ` ( SymGrp ` (/) ) ) ) -> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( 1r ` R ) ) = ( ( ( ZRHom ` R ) o. ( pmSgn ` (/) ) ) ` p ) )
44 37 43 eqtrd 
 |-  ( ( R e. Ring /\ p e. ( Base ` ( SymGrp ` (/) ) ) ) -> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( 0g ` ( mulGrp ` R ) ) ) = ( ( ( ZRHom ` R ) o. ( pmSgn ` (/) ) ) ` p ) )
45 44 mpteq2dva 
 |-  ( R e. Ring -> ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( 0g ` ( mulGrp ` R ) ) ) ) = ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( ( ( ZRHom ` R ) o. ( pmSgn ` (/) ) ) ` p ) ) )
46 45 oveq2d 
 |-  ( R e. Ring -> ( R gsum ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( 0g ` ( mulGrp ` R ) ) ) ) ) = ( R gsum ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( ( ( ZRHom ` R ) o. ( pmSgn ` (/) ) ) ` p ) ) ) )
47 simpl 
 |-  ( ( R e. Ring /\ p e. ( Base ` ( SymGrp ` (/) ) ) ) -> R e. Ring )
48 38 a1i 
 |-  ( ( R e. Ring /\ p e. ( Base ` ( SymGrp ` (/) ) ) ) -> (/) e. Fin )
49 simpr 
 |-  ( ( R e. Ring /\ p e. ( Base ` ( SymGrp ` (/) ) ) ) -> p e. ( Base ` ( SymGrp ` (/) ) ) )
50 elsni 
 |-  ( p e. { (/) } -> p = (/) )
51 fveq2 
 |-  ( p = (/) -> ( ( pmSgn ` (/) ) ` p ) = ( ( pmSgn ` (/) ) ` (/) ) )
52 psgn0fv0 
 |-  ( ( pmSgn ` (/) ) ` (/) ) = 1
53 51 52 eqtrdi 
 |-  ( p = (/) -> ( ( pmSgn ` (/) ) ` p ) = 1 )
54 50 53 syl 
 |-  ( p e. { (/) } -> ( ( pmSgn ` (/) ) ` p ) = 1 )
55 symgbas0 
 |-  ( Base ` ( SymGrp ` (/) ) ) = { (/) }
56 54 55 eleq2s 
 |-  ( p e. ( Base ` ( SymGrp ` (/) ) ) -> ( ( pmSgn ` (/) ) ` p ) = 1 )
57 56 adantl 
 |-  ( ( R e. Ring /\ p e. ( Base ` ( SymGrp ` (/) ) ) ) -> ( ( pmSgn ` (/) ) ` p ) = 1 )
58 eqid 
 |-  ( SymGrp ` (/) ) = ( SymGrp ` (/) )
59 58 4 6 psgnevpmb 
 |-  ( (/) e. Fin -> ( p e. ( pmEven ` (/) ) <-> ( p e. ( Base ` ( SymGrp ` (/) ) ) /\ ( ( pmSgn ` (/) ) ` p ) = 1 ) ) )
60 48 59 syl 
 |-  ( ( R e. Ring /\ p e. ( Base ` ( SymGrp ` (/) ) ) ) -> ( p e. ( pmEven ` (/) ) <-> ( p e. ( Base ` ( SymGrp ` (/) ) ) /\ ( ( pmSgn ` (/) ) ` p ) = 1 ) ) )
61 49 57 60 mpbir2and 
 |-  ( ( R e. Ring /\ p e. ( Base ` ( SymGrp ` (/) ) ) ) -> p e. ( pmEven ` (/) ) )
62 5 6 33 zrhpsgnevpm 
 |-  ( ( R e. Ring /\ (/) e. Fin /\ p e. ( pmEven ` (/) ) ) -> ( ( ( ZRHom ` R ) o. ( pmSgn ` (/) ) ) ` p ) = ( 1r ` R ) )
63 47 48 61 62 syl3anc 
 |-  ( ( R e. Ring /\ p e. ( Base ` ( SymGrp ` (/) ) ) ) -> ( ( ( ZRHom ` R ) o. ( pmSgn ` (/) ) ) ` p ) = ( 1r ` R ) )
64 63 mpteq2dva 
 |-  ( R e. Ring -> ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( ( ( ZRHom ` R ) o. ( pmSgn ` (/) ) ) ` p ) ) = ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( 1r ` R ) ) )
65 64 oveq2d 
 |-  ( R e. Ring -> ( R gsum ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( ( ( ZRHom ` R ) o. ( pmSgn ` (/) ) ) ` p ) ) ) = ( R gsum ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( 1r ` R ) ) ) )
66 55 a1i 
 |-  ( R e. Ring -> ( Base ` ( SymGrp ` (/) ) ) = { (/) } )
67 66 mpteq1d 
 |-  ( R e. Ring -> ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( 1r ` R ) ) = ( p e. { (/) } |-> ( 1r ` R ) ) )
68 67 oveq2d 
 |-  ( R e. Ring -> ( R gsum ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( 1r ` R ) ) ) = ( R gsum ( p e. { (/) } |-> ( 1r ` R ) ) ) )
69 ringmnd 
 |-  ( R e. Ring -> R e. Mnd )
70 41 33 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. ( Base ` R ) )
71 eqidd 
 |-  ( p = (/) -> ( 1r ` R ) = ( 1r ` R ) )
72 41 71 gsumsn 
 |-  ( ( R e. Mnd /\ (/) e. _V /\ ( 1r ` R ) e. ( Base ` R ) ) -> ( R gsum ( p e. { (/) } |-> ( 1r ` R ) ) ) = ( 1r ` R ) )
73 69 14 70 72 syl3anc 
 |-  ( R e. Ring -> ( R gsum ( p e. { (/) } |-> ( 1r ` R ) ) ) = ( 1r ` R ) )
74 65 68 73 3eqtrd 
 |-  ( R e. Ring -> ( R gsum ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( ( ( ZRHom ` R ) o. ( pmSgn ` (/) ) ) ` p ) ) ) = ( 1r ` R ) )
75 32 46 74 3eqtrd 
 |-  ( R e. Ring -> ( R gsum ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( x e. (/) |-> ( ( p ` x ) (/) x ) ) ) ) ) ) = ( 1r ` R ) )
76 75 opeq2d 
 |-  ( R e. Ring -> <. (/) , ( R gsum ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( x e. (/) |-> ( ( p ` x ) (/) x ) ) ) ) ) ) >. = <. (/) , ( 1r ` R ) >. )
77 76 sneqd 
 |-  ( R e. Ring -> { <. (/) , ( R gsum ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( x e. (/) |-> ( ( p ` x ) (/) x ) ) ) ) ) ) >. } = { <. (/) , ( 1r ` R ) >. } )
78 23 77 eqtr3d 
 |-  ( R e. Ring -> ( m e. { (/) } |-> ( R gsum ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( x e. (/) |-> ( ( p ` x ) m x ) ) ) ) ) ) ) = { <. (/) , ( 1r ` R ) >. } )
79 10 12 78 3eqtrd 
 |-  ( R e. Ring -> ( (/) maDet R ) = { <. (/) , ( 1r ` R ) >. } )