Metamath Proof Explorer

Theorem mdetr0

Description: The determinant of a matrix with a row containing only 0's is 0. (Contributed by SO, 16-Jul-2018)

Ref Expression
Hypotheses mdetr0.d 
|- D = ( N maDet R )
mdetr0.k 
|- K = ( Base ` R )
mdetr0.z 
|- .0. = ( 0g ` R )
mdetr0.r 
|- ( ph -> R e. CRing )
mdetr0.n 
|- ( ph -> N e. Fin )
mdetr0.x 
|- ( ( ph /\ i e. N /\ j e. N ) -> X e. K )
mdetr0.i 
|- ( ph -> I e. N )
Assertion mdetr0 
|- ( ph -> ( D ` ( i e. N , j e. N |-> if ( i = I , .0. , X ) ) ) = .0. )

Proof

Step Hyp Ref Expression
1 mdetr0.d 
 |-  D = ( N maDet R )
2 mdetr0.k 
 |-  K = ( Base ` R )
3 mdetr0.z 
 |-  .0. = ( 0g ` R )
4 mdetr0.r 
 |-  ( ph -> R e. CRing )
5 mdetr0.n 
 |-  ( ph -> N e. Fin )
6 mdetr0.x 
 |-  ( ( ph /\ i e. N /\ j e. N ) -> X e. K )
7 mdetr0.i 
 |-  ( ph -> I e. N )
8 eqid 
 |-  ( .r ` R ) = ( .r ` R )
9 crngring 
 |-  ( R e. CRing -> R e. Ring )
10 4 9 syl 
 |-  ( ph -> R e. Ring )
11 2 3 ring0cl 
 |-  ( R e. Ring -> .0. e. K )
12 10 11 syl 
 |-  ( ph -> .0. e. K )
13 12 3ad2ant1 
 |-  ( ( ph /\ i e. N /\ j e. N ) -> .0. e. K )
14 1 2 8 4 5 13 6 12 7 mdetrsca2 
 |-  ( ph -> ( D ` ( i e. N , j e. N |-> if ( i = I , ( .0. ( .r ` R ) .0. ) , X ) ) ) = ( .0. ( .r ` R ) ( D ` ( i e. N , j e. N |-> if ( i = I , .0. , X ) ) ) ) )
15 2 8 3 ringlz 
 |-  ( ( R e. Ring /\ .0. e. K ) -> ( .0. ( .r ` R ) .0. ) = .0. )
16 10 12 15 syl2anc 
 |-  ( ph -> ( .0. ( .r ` R ) .0. ) = .0. )
17 16 ifeq1d 
 |-  ( ph -> if ( i = I , ( .0. ( .r ` R ) .0. ) , X ) = if ( i = I , .0. , X ) )
18 17 mpoeq3dv 
 |-  ( ph -> ( i e. N , j e. N |-> if ( i = I , ( .0. ( .r ` R ) .0. ) , X ) ) = ( i e. N , j e. N |-> if ( i = I , .0. , X ) ) )
19 18 fveq2d 
 |-  ( ph -> ( D ` ( i e. N , j e. N |-> if ( i = I , ( .0. ( .r ` R ) .0. ) , X ) ) ) = ( D ` ( i e. N , j e. N |-> if ( i = I , .0. , X ) ) ) )
20 eqid 
 |-  ( N Mat R ) = ( N Mat R )
21 eqid 
 |-  ( Base ` ( N Mat R ) ) = ( Base ` ( N Mat R ) )
22 1 20 21 2 mdetf 
 |-  ( R e. CRing -> D : ( Base ` ( N Mat R ) ) --> K )
23 4 22 syl 
 |-  ( ph -> D : ( Base ` ( N Mat R ) ) --> K )
24 13 6 ifcld 
 |-  ( ( ph /\ i e. N /\ j e. N ) -> if ( i = I , .0. , X ) e. K )
25 20 2 21 5 4 24 matbas2d 
 |-  ( ph -> ( i e. N , j e. N |-> if ( i = I , .0. , X ) ) e. ( Base ` ( N Mat R ) ) )
26 23 25 ffvelrnd 
 |-  ( ph -> ( D ` ( i e. N , j e. N |-> if ( i = I , .0. , X ) ) ) e. K )
27 2 8 3 ringlz 
 |-  ( ( R e. Ring /\ ( D ` ( i e. N , j e. N |-> if ( i = I , .0. , X ) ) ) e. K ) -> ( .0. ( .r ` R ) ( D ` ( i e. N , j e. N |-> if ( i = I , .0. , X ) ) ) ) = .0. )
28 10 26 27 syl2anc 
 |-  ( ph -> ( .0. ( .r ` R ) ( D ` ( i e. N , j e. N |-> if ( i = I , .0. , X ) ) ) ) = .0. )
29 14 19 28 3eqtr3d 
 |-  ( ph -> ( D ` ( i e. N , j e. N |-> if ( i = I , .0. , X ) ) ) = .0. )