Metamath Proof Explorer

Theorem mdet0

Description: The determinant of the zero matrix (of dimension greater 0!) is 0. (Contributed by AV, 17-Aug-2019) (Revised by AV, 3-Jul-2022)

Ref Expression
Hypotheses mdet0.d 
|- D = ( N maDet R )
mdet0.a 
|- A = ( N Mat R )
mdet0.z 
|- Z = ( 0g ` A )
mdet0.0 
|- .0. = ( 0g ` R )
Assertion mdet0 
|- ( ( R e. CRing /\ N e. Fin /\ N =/= (/) ) -> ( D ` Z ) = .0. )

Proof

Step Hyp Ref Expression
1 mdet0.d 
 |-  D = ( N maDet R )
2 mdet0.a 
 |-  A = ( N Mat R )
3 mdet0.z 
 |-  Z = ( 0g ` A )
4 mdet0.0 
 |-  .0. = ( 0g ` R )
5 n0 
 |-  ( N =/= (/) <-> E. i i e. N )
6 crngring 
 |-  ( R e. CRing -> R e. Ring )
7 6 anim1ci 
 |-  ( ( R e. CRing /\ N e. Fin ) -> ( N e. Fin /\ R e. Ring ) )
8 7 adantr 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ i e. N ) -> ( N e. Fin /\ R e. Ring ) )
9 2 4 mat0op 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( 0g ` A ) = ( x e. N , y e. N |-> .0. ) )
10 3 9 eqtrid 
 |-  ( ( N e. Fin /\ R e. Ring ) -> Z = ( x e. N , y e. N |-> .0. ) )
11 8 10 syl 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ i e. N ) -> Z = ( x e. N , y e. N |-> .0. ) )
12 11 fveq2d 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ i e. N ) -> ( D ` Z ) = ( D ` ( x e. N , y e. N |-> .0. ) ) )
13 ifid 
 |-  if ( x = i , .0. , .0. ) = .0.
14 13 eqcomi 
 |-  .0. = if ( x = i , .0. , .0. )
15 14 a1i 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ i e. N ) -> .0. = if ( x = i , .0. , .0. ) )
16 15 mpoeq3dv 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ i e. N ) -> ( x e. N , y e. N |-> .0. ) = ( x e. N , y e. N |-> if ( x = i , .0. , .0. ) ) )
17 16 fveq2d 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ i e. N ) -> ( D ` ( x e. N , y e. N |-> .0. ) ) = ( D ` ( x e. N , y e. N |-> if ( x = i , .0. , .0. ) ) ) )
18 eqid 
 |-  ( Base ` R ) = ( Base ` R )
19 simpll 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ i e. N ) -> R e. CRing )
20 simpr 
 |-  ( ( R e. CRing /\ N e. Fin ) -> N e. Fin )
21 20 adantr 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ i e. N ) -> N e. Fin )
22 ringmnd 
 |-  ( R e. Ring -> R e. Mnd )
23 6 22 syl 
 |-  ( R e. CRing -> R e. Mnd )
24 23 adantr 
 |-  ( ( R e. CRing /\ N e. Fin ) -> R e. Mnd )
25 18 4 mndidcl 
 |-  ( R e. Mnd -> .0. e. ( Base ` R ) )
26 24 25 syl 
 |-  ( ( R e. CRing /\ N e. Fin ) -> .0. e. ( Base ` R ) )
27 26 adantr 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ i e. N ) -> .0. e. ( Base ` R ) )
28 27 3ad2ant1 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ i e. N ) /\ x e. N /\ y e. N ) -> .0. e. ( Base ` R ) )
29 simpr 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ i e. N ) -> i e. N )
30 1 18 4 19 21 28 29 mdetr0 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ i e. N ) -> ( D ` ( x e. N , y e. N |-> if ( x = i , .0. , .0. ) ) ) = .0. )
31 12 17 30 3eqtrd 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ i e. N ) -> ( D ` Z ) = .0. )
32 31 ex 
 |-  ( ( R e. CRing /\ N e. Fin ) -> ( i e. N -> ( D ` Z ) = .0. ) )
33 32 exlimdv 
 |-  ( ( R e. CRing /\ N e. Fin ) -> ( E. i i e. N -> ( D ` Z ) = .0. ) )
34 5 33 biimtrid 
 |-  ( ( R e. CRing /\ N e. Fin ) -> ( N =/= (/) -> ( D ` Z ) = .0. ) )
35 34 3impia 
 |-  ( ( R e. CRing /\ N e. Fin /\ N =/= (/) ) -> ( D ` Z ) = .0. )