Metamath Proof Explorer

Theorem mdetrlin2

Description: The determinant function is additive for each row (matrices are given explicitly by their entries). (Contributed by SO, 16-Jul-2018)

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

Proof

Step Hyp Ref Expression
1 mdetrlin2.d 
 |-  D = ( N maDet R )
2 mdetrlin2.k 
 |-  K = ( Base ` R )
3 mdetrlin2.p 
 |-  .+ = ( +g ` R )
4 mdetrlin2.r 
 |-  ( ph -> R e. CRing )
5 mdetrlin2.n 
 |-  ( ph -> N e. Fin )
6 mdetrlin2.x 
 |-  ( ( ph /\ i e. N /\ j e. N ) -> X e. K )
7 mdetrlin2.y 
 |-  ( ( ph /\ i e. N /\ j e. N ) -> Y e. K )
8 mdetrlin2.z 
 |-  ( ( ph /\ i e. N /\ j e. N ) -> Z e. K )
9 mdetrlin2.i 
 |-  ( ph -> I e. N )
10 eqid 
 |-  ( N Mat R ) = ( N Mat R )
11 eqid 
 |-  ( Base ` ( N Mat R ) ) = ( Base ` ( N Mat R ) )
12 crngring 
 |-  ( R e. CRing -> R e. Ring )
13 4 12 syl 
 |-  ( ph -> R e. Ring )
14 13 3ad2ant1 
 |-  ( ( ph /\ i e. N /\ j e. N ) -> R e. Ring )
15 2 3 ringacl 
 |-  ( ( R e. Ring /\ X e. K /\ Y e. K ) -> ( X .+ Y ) e. K )
16 14 6 7 15 syl3anc 
 |-  ( ( ph /\ i e. N /\ j e. N ) -> ( X .+ Y ) e. K )
17 16 8 ifcld 
 |-  ( ( ph /\ i e. N /\ j e. N ) -> if ( i = I , ( X .+ Y ) , Z ) e. K )
18 10 2 11 5 4 17 matbas2d 
 |-  ( ph -> ( i e. N , j e. N |-> if ( i = I , ( X .+ Y ) , Z ) ) e. ( Base ` ( N Mat R ) ) )
19 6 8 ifcld 
 |-  ( ( ph /\ i e. N /\ j e. N ) -> if ( i = I , X , Z ) e. K )
20 10 2 11 5 4 19 matbas2d 
 |-  ( ph -> ( i e. N , j e. N |-> if ( i = I , X , Z ) ) e. ( Base ` ( N Mat R ) ) )
21 7 8 ifcld 
 |-  ( ( ph /\ i e. N /\ j e. N ) -> if ( i = I , Y , Z ) e. K )
22 10 2 11 5 4 21 matbas2d 
 |-  ( ph -> ( i e. N , j e. N |-> if ( i = I , Y , Z ) ) e. ( Base ` ( N Mat R ) ) )
23 snex 
 |-  { I } e. _V
24 23 a1i 
 |-  ( ph -> { I } e. _V )
25 9 snssd 
 |-  ( ph -> { I } C_ N )
26 25 3ad2ant1 
 |-  ( ( ph /\ i e. { I } /\ j e. N ) -> { I } C_ N )
27 simp2 
 |-  ( ( ph /\ i e. { I } /\ j e. N ) -> i e. { I } )
28 26 27 sseldd 
 |-  ( ( ph /\ i e. { I } /\ j e. N ) -> i e. N )
29 28 6 syld3an2 
 |-  ( ( ph /\ i e. { I } /\ j e. N ) -> X e. K )
30 28 7 syld3an2 
 |-  ( ( ph /\ i e. { I } /\ j e. N ) -> Y e. K )
31 eqidd 
 |-  ( ph -> ( i e. { I } , j e. N |-> X ) = ( i e. { I } , j e. N |-> X ) )
32 eqidd 
 |-  ( ph -> ( i e. { I } , j e. N |-> Y ) = ( i e. { I } , j e. N |-> Y ) )
33 24 5 29 30 31 32 offval22 
 |-  ( ph -> ( ( i e. { I } , j e. N |-> X ) oF .+ ( i e. { I } , j e. N |-> Y ) ) = ( i e. { I } , j e. N |-> ( X .+ Y ) ) )
34 33 eqcomd 
 |-  ( ph -> ( i e. { I } , j e. N |-> ( X .+ Y ) ) = ( ( i e. { I } , j e. N |-> X ) oF .+ ( i e. { I } , j e. N |-> Y ) ) )
35 mposnif 
 |-  ( i e. { I } , j e. N |-> if ( i = I , ( X .+ Y ) , Z ) ) = ( i e. { I } , j e. N |-> ( X .+ Y ) )
36 mposnif 
 |-  ( i e. { I } , j e. N |-> if ( i = I , X , Z ) ) = ( i e. { I } , j e. N |-> X )
37 mposnif 
 |-  ( i e. { I } , j e. N |-> if ( i = I , Y , Z ) ) = ( i e. { I } , j e. N |-> Y )
38 36 37 oveq12i 
 |-  ( ( i e. { I } , j e. N |-> if ( i = I , X , Z ) ) oF .+ ( i e. { I } , j e. N |-> if ( i = I , Y , Z ) ) ) = ( ( i e. { I } , j e. N |-> X ) oF .+ ( i e. { I } , j e. N |-> Y ) )
39 34 35 38 3eqtr4g 
 |-  ( ph -> ( i e. { I } , j e. N |-> if ( i = I , ( X .+ Y ) , Z ) ) = ( ( i e. { I } , j e. N |-> if ( i = I , X , Z ) ) oF .+ ( i e. { I } , j e. N |-> if ( i = I , Y , Z ) ) ) )
40 ssid 
 |-  N C_ N
41 resmpo 
 |-  ( ( { I } C_ N /\ N C_ N ) -> ( ( i e. N , j e. N |-> if ( i = I , ( X .+ Y ) , Z ) ) |` ( { I } X. N ) ) = ( i e. { I } , j e. N |-> if ( i = I , ( X .+ Y ) , Z ) ) )
42 25 40 41 sylancl 
 |-  ( ph -> ( ( i e. N , j e. N |-> if ( i = I , ( X .+ Y ) , Z ) ) |` ( { I } X. N ) ) = ( i e. { I } , j e. N |-> if ( i = I , ( X .+ Y ) , Z ) ) )
43 resmpo 
 |-  ( ( { I } C_ N /\ N C_ N ) -> ( ( i e. N , j e. N |-> if ( i = I , X , Z ) ) |` ( { I } X. N ) ) = ( i e. { I } , j e. N |-> if ( i = I , X , Z ) ) )
44 25 40 43 sylancl 
 |-  ( ph -> ( ( i e. N , j e. N |-> if ( i = I , X , Z ) ) |` ( { I } X. N ) ) = ( i e. { I } , j e. N |-> if ( i = I , X , Z ) ) )
45 resmpo 
 |-  ( ( { I } C_ N /\ N C_ N ) -> ( ( i e. N , j e. N |-> if ( i = I , Y , Z ) ) |` ( { I } X. N ) ) = ( i e. { I } , j e. N |-> if ( i = I , Y , Z ) ) )
46 25 40 45 sylancl 
 |-  ( ph -> ( ( i e. N , j e. N |-> if ( i = I , Y , Z ) ) |` ( { I } X. N ) ) = ( i e. { I } , j e. N |-> if ( i = I , Y , Z ) ) )
47 44 46 oveq12d 
 |-  ( ph -> ( ( ( i e. N , j e. N |-> if ( i = I , X , Z ) ) |` ( { I } X. N ) ) oF .+ ( ( i e. N , j e. N |-> if ( i = I , Y , Z ) ) |` ( { I } X. N ) ) ) = ( ( i e. { I } , j e. N |-> if ( i = I , X , Z ) ) oF .+ ( i e. { I } , j e. N |-> if ( i = I , Y , Z ) ) ) )
48 39 42 47 3eqtr4d 
 |-  ( ph -> ( ( i e. N , j e. N |-> if ( i = I , ( X .+ Y ) , Z ) ) |` ( { I } X. N ) ) = ( ( ( i e. N , j e. N |-> if ( i = I , X , Z ) ) |` ( { I } X. N ) ) oF .+ ( ( i e. N , j e. N |-> if ( i = I , Y , Z ) ) |` ( { I } X. N ) ) ) )
49 eldifsni 
 |-  ( i e. ( N \ { I } ) -> i =/= I )
50 49 neneqd 
 |-  ( i e. ( N \ { I } ) -> -. i = I )
51 iffalse 
 |-  ( -. i = I -> if ( i = I , ( X .+ Y ) , Z ) = Z )
52 iffalse 
 |-  ( -. i = I -> if ( i = I , X , Z ) = Z )
53 51 52 eqtr4d 
 |-  ( -. i = I -> if ( i = I , ( X .+ Y ) , Z ) = if ( i = I , X , Z ) )
54 50 53 syl 
 |-  ( i e. ( N \ { I } ) -> if ( i = I , ( X .+ Y ) , Z ) = if ( i = I , X , Z ) )
55 54 3ad2ant2 
 |-  ( ( ph /\ i e. ( N \ { I } ) /\ j e. N ) -> if ( i = I , ( X .+ Y ) , Z ) = if ( i = I , X , Z ) )
56 55 mpoeq3dva 
 |-  ( ph -> ( i e. ( N \ { I } ) , j e. N |-> if ( i = I , ( X .+ Y ) , Z ) ) = ( i e. ( N \ { I } ) , j e. N |-> if ( i = I , X , Z ) ) )
57 difss 
 |-  ( N \ { I } ) C_ N
58 resmpo 
 |-  ( ( ( N \ { I } ) C_ N /\ N C_ N ) -> ( ( i e. N , j e. N |-> if ( i = I , ( X .+ Y ) , Z ) ) |` ( ( N \ { I } ) X. N ) ) = ( i e. ( N \ { I } ) , j e. N |-> if ( i = I , ( X .+ Y ) , Z ) ) )
59 57 40 58 mp2an 
 |-  ( ( i e. N , j e. N |-> if ( i = I , ( X .+ Y ) , Z ) ) |` ( ( N \ { I } ) X. N ) ) = ( i e. ( N \ { I } ) , j e. N |-> if ( i = I , ( X .+ Y ) , Z ) )
60 resmpo 
 |-  ( ( ( N \ { I } ) C_ N /\ N C_ N ) -> ( ( i e. N , j e. N |-> if ( i = I , X , Z ) ) |` ( ( N \ { I } ) X. N ) ) = ( i e. ( N \ { I } ) , j e. N |-> if ( i = I , X , Z ) ) )
61 57 40 60 mp2an 
 |-  ( ( i e. N , j e. N |-> if ( i = I , X , Z ) ) |` ( ( N \ { I } ) X. N ) ) = ( i e. ( N \ { I } ) , j e. N |-> if ( i = I , X , Z ) )
62 56 59 61 3eqtr4g 
 |-  ( ph -> ( ( i e. N , j e. N |-> if ( i = I , ( X .+ Y ) , Z ) ) |` ( ( N \ { I } ) X. N ) ) = ( ( i e. N , j e. N |-> if ( i = I , X , Z ) ) |` ( ( N \ { I } ) X. N ) ) )
63 iffalse 
 |-  ( -. i = I -> if ( i = I , Y , Z ) = Z )
64 51 63 eqtr4d 
 |-  ( -. i = I -> if ( i = I , ( X .+ Y ) , Z ) = if ( i = I , Y , Z ) )
65 50 64 syl 
 |-  ( i e. ( N \ { I } ) -> if ( i = I , ( X .+ Y ) , Z ) = if ( i = I , Y , Z ) )
66 65 3ad2ant2 
 |-  ( ( ph /\ i e. ( N \ { I } ) /\ j e. N ) -> if ( i = I , ( X .+ Y ) , Z ) = if ( i = I , Y , Z ) )
67 66 mpoeq3dva 
 |-  ( ph -> ( i e. ( N \ { I } ) , j e. N |-> if ( i = I , ( X .+ Y ) , Z ) ) = ( i e. ( N \ { I } ) , j e. N |-> if ( i = I , Y , Z ) ) )
68 resmpo 
 |-  ( ( ( N \ { I } ) C_ N /\ N C_ N ) -> ( ( i e. N , j e. N |-> if ( i = I , Y , Z ) ) |` ( ( N \ { I } ) X. N ) ) = ( i e. ( N \ { I } ) , j e. N |-> if ( i = I , Y , Z ) ) )
69 57 40 68 mp2an 
 |-  ( ( i e. N , j e. N |-> if ( i = I , Y , Z ) ) |` ( ( N \ { I } ) X. N ) ) = ( i e. ( N \ { I } ) , j e. N |-> if ( i = I , Y , Z ) )
70 67 59 69 3eqtr4g 
 |-  ( ph -> ( ( i e. N , j e. N |-> if ( i = I , ( X .+ Y ) , Z ) ) |` ( ( N \ { I } ) X. N ) ) = ( ( i e. N , j e. N |-> if ( i = I , Y , Z ) ) |` ( ( N \ { I } ) X. N ) ) )
71 1 10 11 3 4 18 20 22 9 48 62 70 mdetrlin 
 |-  ( ph -> ( D ` ( i e. N , j e. N |-> if ( i = I , ( X .+ Y ) , Z ) ) ) = ( ( D ` ( i e. N , j e. N |-> if ( i = I , X , Z ) ) ) .+ ( D ` ( i e. N , j e. N |-> if ( i = I , Y , Z ) ) ) ) )