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 ) )`
` |-  ( ( 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 )`
` |-  ( ( M e. B /\ C e. V /\ K e. N ) -> N e. Fin )`
` |-  ( ( 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. ) ) )`