Metamath Proof Explorer

Theorem mdetrsca2

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

Ref Expression
Hypotheses mdetrsca2.d 
|- D = ( N maDet R )
mdetrsca2.k 
|- K = ( Base ` R )
mdetrsca2.t 
|- .x. = ( .r ` R )
mdetrsca2.r 
|- ( ph -> R e. CRing )
mdetrsca2.n 
|- ( ph -> N e. Fin )
mdetrsca2.x 
|- ( ( ph /\ i e. N /\ j e. N ) -> X e. K )
mdetrsca2.y 
|- ( ( ph /\ i e. N /\ j e. N ) -> Y e. K )
mdetrsca2.f 
|- ( ph -> F e. K )
mdetrsca2.i 
|- ( ph -> I e. N )
Assertion mdetrsca2 
|- ( ph -> ( D ` ( i e. N , j e. N |-> if ( i = I , ( F .x. X ) , Y ) ) ) = ( F .x. ( D ` ( i e. N , j e. N |-> if ( i = I , X , Y ) ) ) ) )

Proof

Step Hyp Ref Expression
1 mdetrsca2.d 
 |-  D = ( N maDet R )
2 mdetrsca2.k 
 |-  K = ( Base ` R )
3 mdetrsca2.t 
 |-  .x. = ( .r ` R )
4 mdetrsca2.r 
 |-  ( ph -> R e. CRing )
5 mdetrsca2.n 
 |-  ( ph -> N e. Fin )
6 mdetrsca2.x 
 |-  ( ( ph /\ i e. N /\ j e. N ) -> X e. K )
7 mdetrsca2.y 
 |-  ( ( ph /\ i e. N /\ j e. N ) -> Y e. K )
8 mdetrsca2.f 
 |-  ( ph -> F e. K )
9 mdetrsca2.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 8 3ad2ant1 
 |-  ( ( ph /\ i e. N /\ j e. N ) -> F e. K )
16 2 3 ringcl 
 |-  ( ( R e. Ring /\ F e. K /\ X e. K ) -> ( F .x. X ) e. K )
17 14 15 6 16 syl3anc 
 |-  ( ( ph /\ i e. N /\ j e. N ) -> ( F .x. X ) e. K )
18 17 7 ifcld 
 |-  ( ( ph /\ i e. N /\ j e. N ) -> if ( i = I , ( F .x. X ) , Y ) e. K )
19 10 2 11 5 4 18 matbas2d 
 |-  ( ph -> ( i e. N , j e. N |-> if ( i = I , ( F .x. X ) , Y ) ) e. ( Base ` ( N Mat R ) ) )
20 6 7 ifcld 
 |-  ( ( ph /\ i e. N /\ j e. N ) -> if ( i = I , X , Y ) e. K )
21 10 2 11 5 4 20 matbas2d 
 |-  ( ph -> ( i e. N , j e. N |-> if ( i = I , X , Y ) ) e. ( Base ` ( N Mat R ) ) )
22 snex 
 |-  { I } e. _V
23 22 a1i 
 |-  ( ph -> { I } e. _V )
24 8 3ad2ant1 
 |-  ( ( ph /\ i e. { I } /\ j e. N ) -> F e. K )
25 9 snssd 
 |-  ( ph -> { I } C_ N )
26 25 sselda 
 |-  ( ( ph /\ i e. { I } ) -> i e. N )
27 26 3adant3 
 |-  ( ( ph /\ i e. { I } /\ j e. N ) -> i e. N )
28 27 6 syld3an2 
 |-  ( ( ph /\ i e. { I } /\ j e. N ) -> X e. K )
29 fconstmpo 
 |-  ( ( { I } X. N ) X. { F } ) = ( i e. { I } , j e. N |-> F )
30 29 a1i 
 |-  ( ph -> ( ( { I } X. N ) X. { F } ) = ( i e. { I } , j e. N |-> F ) )
31 eqidd 
 |-  ( ph -> ( i e. { I } , j e. N |-> X ) = ( i e. { I } , j e. N |-> X ) )
32 23 5 24 28 30 31 offval22 
 |-  ( ph -> ( ( ( { I } X. N ) X. { F } ) oF .x. ( i e. { I } , j e. N |-> X ) ) = ( i e. { I } , j e. N |-> ( F .x. X ) ) )
33 mposnif 
 |-  ( i e. { I } , j e. N |-> if ( i = I , X , Y ) ) = ( i e. { I } , j e. N |-> X )
34 33 oveq2i 
 |-  ( ( ( { I } X. N ) X. { F } ) oF .x. ( i e. { I } , j e. N |-> if ( i = I , X , Y ) ) ) = ( ( ( { I } X. N ) X. { F } ) oF .x. ( i e. { I } , j e. N |-> X ) )
35 mposnif 
 |-  ( i e. { I } , j e. N |-> if ( i = I , ( F .x. X ) , Y ) ) = ( i e. { I } , j e. N |-> ( F .x. X ) )
36 32 34 35 3eqtr4g 
 |-  ( ph -> ( ( ( { I } X. N ) X. { F } ) oF .x. ( i e. { I } , j e. N |-> if ( i = I , X , Y ) ) ) = ( i e. { I } , j e. N |-> if ( i = I , ( F .x. X ) , Y ) ) )
37 ssid 
 |-  N C_ N
38 resmpo 
 |-  ( ( { I } C_ N /\ N C_ N ) -> ( ( i e. N , j e. N |-> if ( i = I , X , Y ) ) |` ( { I } X. N ) ) = ( i e. { I } , j e. N |-> if ( i = I , X , Y ) ) )
39 25 37 38 sylancl 
 |-  ( ph -> ( ( i e. N , j e. N |-> if ( i = I , X , Y ) ) |` ( { I } X. N ) ) = ( i e. { I } , j e. N |-> if ( i = I , X , Y ) ) )
40 39 oveq2d 
 |-  ( ph -> ( ( ( { I } X. N ) X. { F } ) oF .x. ( ( i e. N , j e. N |-> if ( i = I , X , Y ) ) |` ( { I } X. N ) ) ) = ( ( ( { I } X. N ) X. { F } ) oF .x. ( i e. { I } , j e. N |-> if ( i = I , X , Y ) ) ) )
41 resmpo 
 |-  ( ( { I } C_ N /\ N C_ N ) -> ( ( i e. N , j e. N |-> if ( i = I , ( F .x. X ) , Y ) ) |` ( { I } X. N ) ) = ( i e. { I } , j e. N |-> if ( i = I , ( F .x. X ) , Y ) ) )
42 25 37 41 sylancl 
 |-  ( ph -> ( ( i e. N , j e. N |-> if ( i = I , ( F .x. X ) , Y ) ) |` ( { I } X. N ) ) = ( i e. { I } , j e. N |-> if ( i = I , ( F .x. X ) , Y ) ) )
43 36 40 42 3eqtr4rd 
 |-  ( ph -> ( ( i e. N , j e. N |-> if ( i = I , ( F .x. X ) , Y ) ) |` ( { I } X. N ) ) = ( ( ( { I } X. N ) X. { F } ) oF .x. ( ( i e. N , j e. N |-> if ( i = I , X , Y ) ) |` ( { I } X. N ) ) ) )
44 eldifsni 
 |-  ( i e. ( N \ { I } ) -> i =/= I )
45 44 3ad2ant2 
 |-  ( ( ph /\ i e. ( N \ { I } ) /\ j e. N ) -> i =/= I )
46 45 neneqd 
 |-  ( ( ph /\ i e. ( N \ { I } ) /\ j e. N ) -> -. i = I )
47 iffalse 
 |-  ( -. i = I -> if ( i = I , ( F .x. X ) , Y ) = Y )
48 iffalse 
 |-  ( -. i = I -> if ( i = I , X , Y ) = Y )
49 47 48 eqtr4d 
 |-  ( -. i = I -> if ( i = I , ( F .x. X ) , Y ) = if ( i = I , X , Y ) )
50 46 49 syl 
 |-  ( ( ph /\ i e. ( N \ { I } ) /\ j e. N ) -> if ( i = I , ( F .x. X ) , Y ) = if ( i = I , X , Y ) )
51 50 mpoeq3dva 
 |-  ( ph -> ( i e. ( N \ { I } ) , j e. N |-> if ( i = I , ( F .x. X ) , Y ) ) = ( i e. ( N \ { I } ) , j e. N |-> if ( i = I , X , Y ) ) )
52 difss 
 |-  ( N \ { I } ) C_ N
53 resmpo 
 |-  ( ( ( N \ { I } ) C_ N /\ N C_ N ) -> ( ( i e. N , j e. N |-> if ( i = I , ( F .x. X ) , Y ) ) |` ( ( N \ { I } ) X. N ) ) = ( i e. ( N \ { I } ) , j e. N |-> if ( i = I , ( F .x. X ) , Y ) ) )
54 52 37 53 mp2an 
 |-  ( ( i e. N , j e. N |-> if ( i = I , ( F .x. X ) , Y ) ) |` ( ( N \ { I } ) X. N ) ) = ( i e. ( N \ { I } ) , j e. N |-> if ( i = I , ( F .x. X ) , Y ) )
55 resmpo 
 |-  ( ( ( N \ { I } ) C_ N /\ N C_ N ) -> ( ( i e. N , j e. N |-> if ( i = I , X , Y ) ) |` ( ( N \ { I } ) X. N ) ) = ( i e. ( N \ { I } ) , j e. N |-> if ( i = I , X , Y ) ) )
56 52 37 55 mp2an 
 |-  ( ( i e. N , j e. N |-> if ( i = I , X , Y ) ) |` ( ( N \ { I } ) X. N ) ) = ( i e. ( N \ { I } ) , j e. N |-> if ( i = I , X , Y ) )
57 51 54 56 3eqtr4g 
 |-  ( ph -> ( ( i e. N , j e. N |-> if ( i = I , ( F .x. X ) , Y ) ) |` ( ( N \ { I } ) X. N ) ) = ( ( i e. N , j e. N |-> if ( i = I , X , Y ) ) |` ( ( N \ { I } ) X. N ) ) )
58 1 10 11 2 3 4 19 8 21 9 43 57 mdetrsca 
 |-  ( ph -> ( D ` ( i e. N , j e. N |-> if ( i = I , ( F .x. X ) , Y ) ) ) = ( F .x. ( D ` ( i e. N , j e. N |-> if ( i = I , X , Y ) ) ) ) )