Metamath Proof Explorer

Theorem ma1repveval

Description: An entry of an identity matrix with a replaced column. (Contributed by AV, 16-Feb-2019) (Revised by AV, 26-Feb-2019)

Ref Expression
Hypotheses marepvcl.a 
|- A = ( N Mat R )
marepvcl.b 
|- B = ( Base ` A )
marepvcl.v 
|- V = ( ( Base ` R ) ^m N )
ma1repvcl.1 
|- .1. = ( 1r ` A )
mulmarep1el.0 
|- .0. = ( 0g ` R )
mulmarep1el.e 
|- E = ( ( .1. ( N matRepV R ) C ) ` K )
Assertion ma1repveval 
|- ( ( R e. Ring /\ ( M e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N ) ) -> ( I E J ) = if ( J = K , ( C ` I ) , if ( J = I , ( 1r ` R ) , .0. ) ) )

Proof

Step Hyp Ref Expression
1 marepvcl.a 
 |-  A = ( N Mat R )
2 marepvcl.b 
 |-  B = ( Base ` A )
3 marepvcl.v 
 |-  V = ( ( Base ` R ) ^m N )
4 ma1repvcl.1 
 |-  .1. = ( 1r ` A )
5 mulmarep1el.0 
 |-  .0. = ( 0g ` R )
6 mulmarep1el.e 
 |-  E = ( ( .1. ( N matRepV R ) C ) ` K )
7 1 2 matrcl 
 |-  ( M e. B -> ( N e. Fin /\ R e. _V ) )
8 7 simpld 
 |-  ( M e. B -> N e. Fin )
9 1 fveq2i 
 |-  ( 1r ` A ) = ( 1r ` ( N Mat R ) )
10 4 9 eqtri 
 |-  .1. = ( 1r ` ( N Mat R ) )
11 1 2 10 mat1bas 
 |-  ( ( R e. Ring /\ N e. Fin ) -> .1. e. B )
12 11 expcom 
 |-  ( N e. Fin -> ( R e. Ring -> .1. e. B ) )
13 8 12 syl 
 |-  ( M e. B -> ( R e. Ring -> .1. e. B ) )
14 13 3ad2ant1 
 |-  ( ( M e. B /\ C e. V /\ K e. N ) -> ( R e. Ring -> .1. e. B ) )
15 14 impcom 
 |-  ( ( R e. Ring /\ ( M e. B /\ C e. V /\ K e. N ) ) -> .1. e. B )
16 simpr2 
 |-  ( ( R e. Ring /\ ( M e. B /\ C e. V /\ K e. N ) ) -> C e. V )
17 simpr3 
 |-  ( ( R e. Ring /\ ( M e. B /\ C e. V /\ K e. N ) ) -> K e. N )
18 15 16 17 3jca 
 |-  ( ( R e. Ring /\ ( M e. B /\ C e. V /\ K e. N ) ) -> ( .1. e. B /\ C e. V /\ K e. N ) )
19 6 a1i 
 |-  ( ( ( .1. e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N ) ) -> E = ( ( .1. ( N matRepV R ) C ) ` K ) )
20 19 oveqd 
 |-  ( ( ( .1. e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N ) ) -> ( I E J ) = ( I ( ( .1. ( N matRepV R ) C ) ` K ) J ) )
21 eqid 
 |-  ( N matRepV R ) = ( N matRepV R )
22 1 2 21 3 marepveval 
 |-  ( ( ( .1. e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N ) ) -> ( I ( ( .1. ( N matRepV R ) C ) ` K ) J ) = if ( J = K , ( C ` I ) , ( I .1. J ) ) )
23 20 22 eqtrd 
 |-  ( ( ( .1. e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N ) ) -> ( I E J ) = if ( J = K , ( C ` I ) , ( I .1. J ) ) )
24 18 23 stoic3 
 |-  ( ( R e. Ring /\ ( M e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N ) ) -> ( I E J ) = if ( J = K , ( C ` I ) , ( I .1. J ) ) )
25 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
26 8 3ad2ant1 
 |-  ( ( M e. B /\ C e. V /\ K e. N ) -> N e. Fin )
27 26 3ad2ant2 
 |-  ( ( R e. Ring /\ ( M e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N ) ) -> N e. Fin )
28 simp1 
 |-  ( ( R e. Ring /\ ( M e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N ) ) -> R e. Ring )
29 simp3l 
 |-  ( ( R e. Ring /\ ( M e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N ) ) -> I e. N )
30 simp3r 
 |-  ( ( R e. Ring /\ ( M e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N ) ) -> J e. N )
31 1 25 5 27 28 29 30 4 mat1ov 
 |-  ( ( R e. Ring /\ ( M e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N ) ) -> ( I .1. J ) = if ( I = J , ( 1r ` R ) , .0. ) )
32 eqcom 
 |-  ( I = J <-> J = I )
33 32 a1i 
 |-  ( ( R e. Ring /\ ( M e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N ) ) -> ( I = J <-> J = I ) )
34 33 ifbid 
 |-  ( ( R e. Ring /\ ( M e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N ) ) -> if ( I = J , ( 1r ` R ) , .0. ) = if ( J = I , ( 1r ` R ) , .0. ) )
35 31 34 eqtrd 
 |-  ( ( R e. Ring /\ ( M e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N ) ) -> ( I .1. J ) = if ( J = I , ( 1r ` R ) , .0. ) )
36 35 ifeq2d 
 |-  ( ( R e. Ring /\ ( M e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N ) ) -> if ( J = K , ( C ` I ) , ( I .1. J ) ) = if ( J = K , ( C ` I ) , if ( J = I , ( 1r ` R ) , .0. ) ) )
37 24 36 eqtrd 
 |-  ( ( R e. Ring /\ ( M e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N ) ) -> ( I E J ) = if ( J = K , ( C ` I ) , if ( J = I , ( 1r ` R ) , .0. ) ) )