Metamath Proof Explorer

Theorem mdetero

Description: The determinant function is multilinear (additive and homogeneous for each row (matrices are given explicitly by their entries). Corollary 4.9 in Lang p. 515. (Contributed by SO, 16-Jul-2018)

Ref Expression
Hypotheses mdetero.d 
|- D = ( N maDet R )
mdetero.k 
|- K = ( Base ` R )
mdetero.p 
|- .+ = ( +g ` R )
mdetero.t 
|- .x. = ( .r ` R )
mdetero.r 
|- ( ph -> R e. CRing )
mdetero.n 
|- ( ph -> N e. Fin )
mdetero.x 
|- ( ( ph /\ j e. N ) -> X e. K )
mdetero.y 
|- ( ( ph /\ j e. N ) -> Y e. K )
mdetero.z 
|- ( ( ph /\ i e. N /\ j e. N ) -> Z e. K )
mdetero.w 
|- ( ph -> W e. K )
mdetero.i 
|- ( ph -> I e. N )
mdetero.j 
|- ( ph -> J e. N )
mdetero.ij 
|- ( ph -> I =/= J )
Assertion mdetero 
|- ( ph -> ( D ` ( i e. N , j e. N |-> if ( i = I , ( X .+ ( W .x. Y ) ) , if ( i = J , Y , Z ) ) ) ) = ( D ` ( i e. N , j e. N |-> if ( i = I , X , if ( i = J , Y , Z ) ) ) ) )

Proof

Step Hyp Ref Expression
1 mdetero.d 
 |-  D = ( N maDet R )
2 mdetero.k 
 |-  K = ( Base ` R )
3 mdetero.p 
 |-  .+ = ( +g ` R )
4 mdetero.t 
 |-  .x. = ( .r ` R )
5 mdetero.r 
 |-  ( ph -> R e. CRing )
6 mdetero.n 
 |-  ( ph -> N e. Fin )
7 mdetero.x 
 |-  ( ( ph /\ j e. N ) -> X e. K )
8 mdetero.y 
 |-  ( ( ph /\ j e. N ) -> Y e. K )
9 mdetero.z 
 |-  ( ( ph /\ i e. N /\ j e. N ) -> Z e. K )
10 mdetero.w 
 |-  ( ph -> W e. K )
11 mdetero.i 
 |-  ( ph -> I e. N )
12 mdetero.j 
 |-  ( ph -> J e. N )
13 mdetero.ij 
 |-  ( ph -> I =/= J )
14 7 3adant2 
 |-  ( ( ph /\ i e. N /\ j e. N ) -> X e. K )
15 crngring 
 |-  ( R e. CRing -> R e. Ring )
16 5 15 syl 
 |-  ( ph -> R e. Ring )
17 16 3ad2ant1 
 |-  ( ( ph /\ i e. N /\ j e. N ) -> R e. Ring )
18 10 3ad2ant1 
 |-  ( ( ph /\ i e. N /\ j e. N ) -> W e. K )
19 8 3adant2 
 |-  ( ( ph /\ i e. N /\ j e. N ) -> Y e. K )
20 2 4 ringcl 
 |-  ( ( R e. Ring /\ W e. K /\ Y e. K ) -> ( W .x. Y ) e. K )
21 17 18 19 20 syl3anc 
 |-  ( ( ph /\ i e. N /\ j e. N ) -> ( W .x. Y ) e. K )
22 19 9 ifcld 
 |-  ( ( ph /\ i e. N /\ j e. N ) -> if ( i = J , Y , Z ) e. K )
23 1 2 3 5 6 14 21 22 11 mdetrlin2 
 |-  ( ph -> ( D ` ( i e. N , j e. N |-> if ( i = I , ( X .+ ( W .x. Y ) ) , if ( i = J , Y , Z ) ) ) ) = ( ( D ` ( i e. N , j e. N |-> if ( i = I , X , if ( i = J , Y , Z ) ) ) ) .+ ( D ` ( i e. N , j e. N |-> if ( i = I , ( W .x. Y ) , if ( i = J , Y , Z ) ) ) ) ) )
24 1 2 4 5 6 19 22 10 11 mdetrsca2 
 |-  ( ph -> ( D ` ( i e. N , j e. N |-> if ( i = I , ( W .x. Y ) , if ( i = J , Y , Z ) ) ) ) = ( W .x. ( D ` ( i e. N , j e. N |-> if ( i = I , Y , if ( i = J , Y , Z ) ) ) ) ) )
25 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
26 1 2 25 5 6 8 9 11 12 13 mdetralt2 
 |-  ( ph -> ( D ` ( i e. N , j e. N |-> if ( i = I , Y , if ( i = J , Y , Z ) ) ) ) = ( 0g ` R ) )
27 26 oveq2d 
 |-  ( ph -> ( W .x. ( D ` ( i e. N , j e. N |-> if ( i = I , Y , if ( i = J , Y , Z ) ) ) ) ) = ( W .x. ( 0g ` R ) ) )
28 2 4 25 ringrz 
 |-  ( ( R e. Ring /\ W e. K ) -> ( W .x. ( 0g ` R ) ) = ( 0g ` R ) )
29 16 10 28 syl2anc 
 |-  ( ph -> ( W .x. ( 0g ` R ) ) = ( 0g ` R ) )
30 24 27 29 3eqtrd 
 |-  ( ph -> ( D ` ( i e. N , j e. N |-> if ( i = I , ( W .x. Y ) , if ( i = J , Y , Z ) ) ) ) = ( 0g ` R ) )
31 30 oveq2d 
 |-  ( ph -> ( ( D ` ( i e. N , j e. N |-> if ( i = I , X , if ( i = J , Y , Z ) ) ) ) .+ ( D ` ( i e. N , j e. N |-> if ( i = I , ( W .x. Y ) , if ( i = J , Y , Z ) ) ) ) ) = ( ( D ` ( i e. N , j e. N |-> if ( i = I , X , if ( i = J , Y , Z ) ) ) ) .+ ( 0g ` R ) ) )
32 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
33 16 32 syl 
 |-  ( ph -> R e. Grp )
34 eqid 
 |-  ( N Mat R ) = ( N Mat R )
35 eqid 
 |-  ( Base ` ( N Mat R ) ) = ( Base ` ( N Mat R ) )
36 1 34 35 2 mdetf 
 |-  ( R e. CRing -> D : ( Base ` ( N Mat R ) ) --> K )
37 5 36 syl 
 |-  ( ph -> D : ( Base ` ( N Mat R ) ) --> K )
38 14 22 ifcld 
 |-  ( ( ph /\ i e. N /\ j e. N ) -> if ( i = I , X , if ( i = J , Y , Z ) ) e. K )
39 34 2 35 6 5 38 matbas2d 
 |-  ( ph -> ( i e. N , j e. N |-> if ( i = I , X , if ( i = J , Y , Z ) ) ) e. ( Base ` ( N Mat R ) ) )
40 37 39 ffvelrnd 
 |-  ( ph -> ( D ` ( i e. N , j e. N |-> if ( i = I , X , if ( i = J , Y , Z ) ) ) ) e. K )
41 2 3 25 grprid 
 |-  ( ( R e. Grp /\ ( D ` ( i e. N , j e. N |-> if ( i = I , X , if ( i = J , Y , Z ) ) ) ) e. K ) -> ( ( D ` ( i e. N , j e. N |-> if ( i = I , X , if ( i = J , Y , Z ) ) ) ) .+ ( 0g ` R ) ) = ( D ` ( i e. N , j e. N |-> if ( i = I , X , if ( i = J , Y , Z ) ) ) ) )
42 33 40 41 syl2anc 
 |-  ( ph -> ( ( D ` ( i e. N , j e. N |-> if ( i = I , X , if ( i = J , Y , Z ) ) ) ) .+ ( 0g ` R ) ) = ( D ` ( i e. N , j e. N |-> if ( i = I , X , if ( i = J , Y , Z ) ) ) ) )
43 23 31 42 3eqtrd 
 |-  ( ph -> ( D ` ( i e. N , j e. N |-> if ( i = I , ( X .+ ( W .x. Y ) ) , if ( i = J , Y , Z ) ) ) ) = ( D ` ( i e. N , j e. N |-> if ( i = I , X , if ( i = J , Y , Z ) ) ) ) )