Metamath Proof Explorer

Theorem 1marepvsma1

Description: The submatrix of the identity matrix with the ith column replaced by the vector obtained by removing the ith row and the ith column is an identity matrix. (Contributed by AV, 14-Feb-2019) (Revised by AV, 27-Feb-2019)

Ref Expression
Hypotheses 1marepvsma1.v 
|- V = ( ( Base ` R ) ^m N )
1marepvsma1.1 
|- .1. = ( 1r ` ( N Mat R ) )
1marepvsma1.x 
|- X = ( ( .1. ( N matRepV R ) Z ) ` I )
Assertion 1marepvsma1 
|- ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) -> ( I ( ( N subMat R ) ` X ) I ) = ( 1r ` ( ( N \ { I } ) Mat R ) ) )

Proof

Step Hyp Ref Expression
1 1marepvsma1.v 
 |-  V = ( ( Base ` R ) ^m N )
2 1marepvsma1.1 
 |-  .1. = ( 1r ` ( N Mat R ) )
3 1marepvsma1.x 
 |-  X = ( ( .1. ( N matRepV R ) Z ) ` I )
4 3 oveqi 
 |-  ( i X j ) = ( i ( ( .1. ( N matRepV R ) Z ) ` I ) j )
5 4 a1i 
 |-  ( ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) /\ i e. ( N \ { I } ) /\ j e. ( N \ { I } ) ) -> ( i X j ) = ( i ( ( .1. ( N matRepV R ) Z ) ` I ) j ) )
6 eqid 
 |-  ( N Mat R ) = ( N Mat R )
7 eqid 
 |-  ( Base ` ( N Mat R ) ) = ( Base ` ( N Mat R ) )
8 6 7 2 mat1bas 
 |-  ( ( R e. Ring /\ N e. Fin ) -> .1. e. ( Base ` ( N Mat R ) ) )
9 8 adantr 
 |-  ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) -> .1. e. ( Base ` ( N Mat R ) ) )
10 simprr 
 |-  ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) -> Z e. V )
11 simprl 
 |-  ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) -> I e. N )
12 9 10 11 3jca 
 |-  ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) -> ( .1. e. ( Base ` ( N Mat R ) ) /\ Z e. V /\ I e. N ) )
13 12 3ad2ant1 
 |-  ( ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) /\ i e. ( N \ { I } ) /\ j e. ( N \ { I } ) ) -> ( .1. e. ( Base ` ( N Mat R ) ) /\ Z e. V /\ I e. N ) )
14 eldifi 
 |-  ( i e. ( N \ { I } ) -> i e. N )
15 eldifi 
 |-  ( j e. ( N \ { I } ) -> j e. N )
16 14 15 anim12i 
 |-  ( ( i e. ( N \ { I } ) /\ j e. ( N \ { I } ) ) -> ( i e. N /\ j e. N ) )
17 16 3adant1 
 |-  ( ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) /\ i e. ( N \ { I } ) /\ j e. ( N \ { I } ) ) -> ( i e. N /\ j e. N ) )
18 eqid 
 |-  ( N matRepV R ) = ( N matRepV R )
19 6 7 18 1 marepveval 
 |-  ( ( ( .1. e. ( Base ` ( N Mat R ) ) /\ Z e. V /\ I e. N ) /\ ( i e. N /\ j e. N ) ) -> ( i ( ( .1. ( N matRepV R ) Z ) ` I ) j ) = if ( j = I , ( Z ` i ) , ( i .1. j ) ) )
20 13 17 19 syl2anc 
 |-  ( ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) /\ i e. ( N \ { I } ) /\ j e. ( N \ { I } ) ) -> ( i ( ( .1. ( N matRepV R ) Z ) ` I ) j ) = if ( j = I , ( Z ` i ) , ( i .1. j ) ) )
21 eldifsni 
 |-  ( j e. ( N \ { I } ) -> j =/= I )
22 21 neneqd 
 |-  ( j e. ( N \ { I } ) -> -. j = I )
23 22 3ad2ant3 
 |-  ( ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) /\ i e. ( N \ { I } ) /\ j e. ( N \ { I } ) ) -> -. j = I )
24 23 iffalsed 
 |-  ( ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) /\ i e. ( N \ { I } ) /\ j e. ( N \ { I } ) ) -> if ( j = I , ( Z ` i ) , ( i .1. j ) ) = ( i .1. j ) )
25 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
26 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
27 simp1lr 
 |-  ( ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) /\ i e. ( N \ { I } ) /\ j e. ( N \ { I } ) ) -> N e. Fin )
28 simp1ll 
 |-  ( ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) /\ i e. ( N \ { I } ) /\ j e. ( N \ { I } ) ) -> R e. Ring )
29 14 3ad2ant2 
 |-  ( ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) /\ i e. ( N \ { I } ) /\ j e. ( N \ { I } ) ) -> i e. N )
30 15 3ad2ant3 
 |-  ( ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) /\ i e. ( N \ { I } ) /\ j e. ( N \ { I } ) ) -> j e. N )
31 6 25 26 27 28 29 30 2 mat1ov 
 |-  ( ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) /\ i e. ( N \ { I } ) /\ j e. ( N \ { I } ) ) -> ( i .1. j ) = if ( i = j , ( 1r ` R ) , ( 0g ` R ) ) )
32 24 31 eqtrd 
 |-  ( ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) /\ i e. ( N \ { I } ) /\ j e. ( N \ { I } ) ) -> if ( j = I , ( Z ` i ) , ( i .1. j ) ) = if ( i = j , ( 1r ` R ) , ( 0g ` R ) ) )
33 5 20 32 3eqtrd 
 |-  ( ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) /\ i e. ( N \ { I } ) /\ j e. ( N \ { I } ) ) -> ( i X j ) = if ( i = j , ( 1r ` R ) , ( 0g ` R ) ) )
34 33 mpoeq3dva 
 |-  ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) -> ( i e. ( N \ { I } ) , j e. ( N \ { I } ) |-> ( i X j ) ) = ( i e. ( N \ { I } ) , j e. ( N \ { I } ) |-> if ( i = j , ( 1r ` R ) , ( 0g ` R ) ) ) )
35 6 7 1 2 ma1repvcl 
 |-  ( ( ( R e. Ring /\ N e. Fin ) /\ ( Z e. V /\ I e. N ) ) -> ( ( .1. ( N matRepV R ) Z ) ` I ) e. ( Base ` ( N Mat R ) ) )
36 35 ancom2s 
 |-  ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) -> ( ( .1. ( N matRepV R ) Z ) ` I ) e. ( Base ` ( N Mat R ) ) )
37 3 36 eqeltrid 
 |-  ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) -> X e. ( Base ` ( N Mat R ) ) )
38 eqid 
 |-  ( N subMat R ) = ( N subMat R )
39 6 38 7 submaval 
 |-  ( ( X e. ( Base ` ( N Mat R ) ) /\ I e. N /\ I e. N ) -> ( I ( ( N subMat R ) ` X ) I ) = ( i e. ( N \ { I } ) , j e. ( N \ { I } ) |-> ( i X j ) ) )
40 37 11 11 39 syl3anc 
 |-  ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) -> ( I ( ( N subMat R ) ` X ) I ) = ( i e. ( N \ { I } ) , j e. ( N \ { I } ) |-> ( i X j ) ) )
41 diffi 
 |-  ( N e. Fin -> ( N \ { I } ) e. Fin )
42 41 anim2i 
 |-  ( ( R e. Ring /\ N e. Fin ) -> ( R e. Ring /\ ( N \ { I } ) e. Fin ) )
43 42 ancomd 
 |-  ( ( R e. Ring /\ N e. Fin ) -> ( ( N \ { I } ) e. Fin /\ R e. Ring ) )
44 43 adantr 
 |-  ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) -> ( ( N \ { I } ) e. Fin /\ R e. Ring ) )
45 eqid 
 |-  ( ( N \ { I } ) Mat R ) = ( ( N \ { I } ) Mat R )
46 45 25 26 mat1 
 |-  ( ( ( N \ { I } ) e. Fin /\ R e. Ring ) -> ( 1r ` ( ( N \ { I } ) Mat R ) ) = ( i e. ( N \ { I } ) , j e. ( N \ { I } ) |-> if ( i = j , ( 1r ` R ) , ( 0g ` R ) ) ) )
47 44 46 syl 
 |-  ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) -> ( 1r ` ( ( N \ { I } ) Mat R ) ) = ( i e. ( N \ { I } ) , j e. ( N \ { I } ) |-> if ( i = j , ( 1r ` R ) , ( 0g ` R ) ) ) )
48 34 40 47 3eqtr4d 
 |-  ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) -> ( I ( ( N subMat R ) ` X ) I ) = ( 1r ` ( ( N \ { I } ) Mat R ) ) )