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 ) ) ) ) )