Metamath Proof Explorer

Theorem 1marepvmarrepid

Description: Replacing the ith row by 0's and the ith component of a (column) vector at the diagonal position for the identity matrix with the ith column replaced by the vector results in the matrix itself. (Contributed by AV, 14-Feb-2019) (Revised by AV, 27-Feb-2019)

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

Proof

Step Hyp Ref Expression
1 marepvmarrep1.v 
 |-  V = ( ( Base ` R ) ^m N )
2 marepvmarrep1.o 
 |-  .1. = ( 1r ` ( N Mat R ) )
3 marepvmarrep1.x 
 |-  X = ( ( .1. ( N matRepV R ) Z ) ` I )
4 eqid 
 |-  ( N Mat R ) = ( N Mat R )
5 eqid 
 |-  ( Base ` ( N Mat R ) ) = ( Base ` ( N Mat R ) )
6 4 5 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 ) ) )
7 6 ancom2s 
 |-  ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) -> ( ( .1. ( N matRepV R ) Z ) ` I ) e. ( Base ` ( N Mat R ) ) )
8 3 7 eqeltrid 
 |-  ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) -> X e. ( Base ` ( N Mat R ) ) )
9 elmapi 
 |-  ( Z e. ( ( Base ` R ) ^m N ) -> Z : N --> ( Base ` R ) )
10 ffvelrn 
 |-  ( ( Z : N --> ( Base ` R ) /\ I e. N ) -> ( Z ` I ) e. ( Base ` R ) )
11 10 ex 
 |-  ( Z : N --> ( Base ` R ) -> ( I e. N -> ( Z ` I ) e. ( Base ` R ) ) )
12 9 11 syl 
 |-  ( Z e. ( ( Base ` R ) ^m N ) -> ( I e. N -> ( Z ` I ) e. ( Base ` R ) ) )
13 12 1 eleq2s 
 |-  ( Z e. V -> ( I e. N -> ( Z ` I ) e. ( Base ` R ) ) )
14 13 impcom 
 |-  ( ( I e. N /\ Z e. V ) -> ( Z ` I ) e. ( Base ` R ) )
15 14 adantl 
 |-  ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) -> ( Z ` I ) e. ( Base ` R ) )
16 simpl 
 |-  ( ( I e. N /\ Z e. V ) -> I e. N )
17 16 adantl 
 |-  ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) -> I e. N )
18 eqid 
 |-  ( N matRRep R ) = ( N matRRep R )
19 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
20 4 5 18 19 marrepval 
 |-  ( ( ( X e. ( Base ` ( N Mat R ) ) /\ ( Z ` I ) e. ( Base ` R ) ) /\ ( I e. N /\ I e. N ) ) -> ( I ( X ( N matRRep R ) ( Z ` I ) ) I ) = ( i e. N , j e. N |-> if ( i = I , if ( j = I , ( Z ` I ) , ( 0g ` R ) ) , ( i X j ) ) ) )
21 8 15 17 17 20 syl22anc 
 |-  ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) -> ( I ( X ( N matRRep R ) ( Z ` I ) ) I ) = ( i e. N , j e. N |-> if ( i = I , if ( j = I , ( Z ` I ) , ( 0g ` R ) ) , ( i X j ) ) ) )
22 iftrue 
 |-  ( i = I -> if ( i = I , if ( j = I , ( Z ` I ) , ( 0g ` R ) ) , ( i X j ) ) = if ( j = I , ( Z ` I ) , ( 0g ` R ) ) )
23 22 adantr 
 |-  ( ( i = I /\ ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) /\ i e. N /\ j e. N ) ) -> if ( i = I , if ( j = I , ( Z ` I ) , ( 0g ` R ) ) , ( i X j ) ) = if ( j = I , ( Z ` I ) , ( 0g ` R ) ) )
24 iftrue 
 |-  ( j = I -> if ( j = I , ( Z ` I ) , ( 0g ` R ) ) = ( Z ` I ) )
25 24 adantr 
 |-  ( ( j = I /\ ( i = I /\ ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) /\ i e. N /\ j e. N ) ) ) -> if ( j = I , ( Z ` I ) , ( 0g ` R ) ) = ( Z ` I ) )
26 iftrue 
 |-  ( j = I -> if ( j = I , ( Z ` i ) , ( i .1. j ) ) = ( Z ` i ) )
27 fveq2 
 |-  ( i = I -> ( Z ` i ) = ( Z ` I ) )
28 27 adantr 
 |-  ( ( i = I /\ ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) /\ i e. N /\ j e. N ) ) -> ( Z ` i ) = ( Z ` I ) )
29 26 28 sylan9eq 
 |-  ( ( j = I /\ ( i = I /\ ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) /\ i e. N /\ j e. N ) ) ) -> if ( j = I , ( Z ` i ) , ( i .1. j ) ) = ( Z ` I ) )
30 25 29 eqtr4d 
 |-  ( ( j = I /\ ( i = I /\ ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) /\ i e. N /\ j e. N ) ) ) -> if ( j = I , ( Z ` I ) , ( 0g ` R ) ) = if ( j = I , ( Z ` i ) , ( i .1. j ) ) )
31 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
32 simpr 
 |-  ( ( R e. Ring /\ N e. Fin ) -> N e. Fin )
33 32 adantr 
 |-  ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) -> N e. Fin )
34 33 3ad2ant1 
 |-  ( ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) /\ i e. N /\ j e. N ) -> N e. Fin )
35 simpl 
 |-  ( ( R e. Ring /\ N e. Fin ) -> R e. Ring )
36 35 adantr 
 |-  ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) -> R e. Ring )
37 36 3ad2ant1 
 |-  ( ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) /\ i e. N /\ j e. N ) -> R e. Ring )
38 simp2 
 |-  ( ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) /\ i e. N /\ j e. N ) -> i e. N )
39 simp3 
 |-  ( ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) /\ i e. N /\ j e. N ) -> j e. N )
40 4 31 19 34 37 38 39 2 mat1ov 
 |-  ( ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) /\ i e. N /\ j e. N ) -> ( i .1. j ) = if ( i = j , ( 1r ` R ) , ( 0g ` R ) ) )
41 40 adantl 
 |-  ( ( i = I /\ ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) /\ i e. N /\ j e. N ) ) -> ( i .1. j ) = if ( i = j , ( 1r ` R ) , ( 0g ` R ) ) )
42 41 adantl 
 |-  ( ( -. j = I /\ ( i = I /\ ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) /\ i e. N /\ j e. N ) ) ) -> ( i .1. j ) = if ( i = j , ( 1r ` R ) , ( 0g ` R ) ) )
43 eqtr2 
 |-  ( ( i = I /\ i = j ) -> I = j )
44 43 eqcomd 
 |-  ( ( i = I /\ i = j ) -> j = I )
45 44 ex 
 |-  ( i = I -> ( i = j -> j = I ) )
46 45 con3d 
 |-  ( i = I -> ( -. j = I -> -. i = j ) )
47 46 adantr 
 |-  ( ( i = I /\ ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) /\ i e. N /\ j e. N ) ) -> ( -. j = I -> -. i = j ) )
48 47 impcom 
 |-  ( ( -. j = I /\ ( i = I /\ ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) /\ i e. N /\ j e. N ) ) ) -> -. i = j )
49 iffalse 
 |-  ( -. i = j -> if ( i = j , ( 1r ` R ) , ( 0g ` R ) ) = ( 0g ` R ) )
50 48 49 syl 
 |-  ( ( -. j = I /\ ( i = I /\ ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) /\ i e. N /\ j e. N ) ) ) -> if ( i = j , ( 1r ` R ) , ( 0g ` R ) ) = ( 0g ` R ) )
51 42 50 eqtrd 
 |-  ( ( -. j = I /\ ( i = I /\ ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) /\ i e. N /\ j e. N ) ) ) -> ( i .1. j ) = ( 0g ` R ) )
52 iffalse 
 |-  ( -. j = I -> if ( j = I , ( Z ` i ) , ( i .1. j ) ) = ( i .1. j ) )
53 52 adantr 
 |-  ( ( -. j = I /\ ( i = I /\ ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) /\ i e. N /\ j e. N ) ) ) -> if ( j = I , ( Z ` i ) , ( i .1. j ) ) = ( i .1. j ) )
54 iffalse 
 |-  ( -. j = I -> if ( j = I , ( Z ` I ) , ( 0g ` R ) ) = ( 0g ` R ) )
55 54 adantr 
 |-  ( ( -. j = I /\ ( i = I /\ ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) /\ i e. N /\ j e. N ) ) ) -> if ( j = I , ( Z ` I ) , ( 0g ` R ) ) = ( 0g ` R ) )
56 51 53 55 3eqtr4rd 
 |-  ( ( -. j = I /\ ( i = I /\ ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) /\ i e. N /\ j e. N ) ) ) -> if ( j = I , ( Z ` I ) , ( 0g ` R ) ) = if ( j = I , ( Z ` i ) , ( i .1. j ) ) )
57 30 56 pm2.61ian 
 |-  ( ( i = I /\ ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) /\ i e. N /\ j e. N ) ) -> if ( j = I , ( Z ` I ) , ( 0g ` R ) ) = if ( j = I , ( Z ` i ) , ( i .1. j ) ) )
58 23 57 eqtrd 
 |-  ( ( i = I /\ ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) /\ i e. N /\ j e. N ) ) -> if ( i = I , if ( j = I , ( Z ` I ) , ( 0g ` R ) ) , ( i X j ) ) = if ( j = I , ( Z ` i ) , ( i .1. j ) ) )
59 iffalse 
 |-  ( -. i = I -> if ( i = I , if ( j = I , ( Z ` I ) , ( 0g ` R ) ) , ( i X j ) ) = ( i X j ) )
60 59 adantr 
 |-  ( ( -. i = I /\ ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) /\ i e. N /\ j e. N ) ) -> if ( i = I , if ( j = I , ( Z ` I ) , ( 0g ` R ) ) , ( i X j ) ) = ( i X j ) )
61 4 5 2 mat1bas 
 |-  ( ( R e. Ring /\ N e. Fin ) -> .1. e. ( Base ` ( N Mat R ) ) )
62 61 adantr 
 |-  ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) -> .1. e. ( Base ` ( N Mat R ) ) )
63 simpr 
 |-  ( ( I e. N /\ Z e. V ) -> Z e. V )
64 63 adantl 
 |-  ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) -> Z e. V )
65 62 64 17 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 ) )
66 65 3ad2ant1 
 |-  ( ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) /\ i e. N /\ j e. N ) -> ( .1. e. ( Base ` ( N Mat R ) ) /\ Z e. V /\ I e. N ) )
67 3simpc 
 |-  ( ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) /\ i e. N /\ j e. N ) -> ( i e. N /\ j e. N ) )
68 37 66 67 3jca 
 |-  ( ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) /\ i e. N /\ j e. N ) -> ( R e. Ring /\ ( .1. e. ( Base ` ( N Mat R ) ) /\ Z e. V /\ I e. N ) /\ ( i e. N /\ j e. N ) ) )
69 68 adantl 
 |-  ( ( -. i = I /\ ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) /\ i e. N /\ j e. N ) ) -> ( R e. Ring /\ ( .1. e. ( Base ` ( N Mat R ) ) /\ Z e. V /\ I e. N ) /\ ( i e. N /\ j e. N ) ) )
70 4 5 1 2 19 3 ma1repveval 
 |-  ( ( R e. Ring /\ ( .1. e. ( Base ` ( N Mat R ) ) /\ Z e. V /\ I e. N ) /\ ( i e. N /\ j e. N ) ) -> ( i X j ) = if ( j = I , ( Z ` i ) , if ( j = i , ( 1r ` R ) , ( 0g ` R ) ) ) )
71 69 70 syl 
 |-  ( ( -. i = I /\ ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) /\ i e. N /\ j e. N ) ) -> ( i X j ) = if ( j = I , ( Z ` i ) , if ( j = i , ( 1r ` R ) , ( 0g ` R ) ) ) )
72 34 ad2antlr 
 |-  ( ( ( -. i = I /\ ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) /\ i e. N /\ j e. N ) ) /\ -. j = I ) -> N e. Fin )
73 37 ad2antlr 
 |-  ( ( ( -. i = I /\ ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) /\ i e. N /\ j e. N ) ) /\ -. j = I ) -> R e. Ring )
74 38 ad2antlr 
 |-  ( ( ( -. i = I /\ ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) /\ i e. N /\ j e. N ) ) /\ -. j = I ) -> i e. N )
75 39 ad2antlr 
 |-  ( ( ( -. i = I /\ ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) /\ i e. N /\ j e. N ) ) /\ -. j = I ) -> j e. N )
76 4 31 19 72 73 74 75 2 mat1ov 
 |-  ( ( ( -. i = I /\ ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) /\ i e. N /\ j e. N ) ) /\ -. j = I ) -> ( i .1. j ) = if ( i = j , ( 1r ` R ) , ( 0g ` R ) ) )
77 equcom 
 |-  ( i = j <-> j = i )
78 77 a1i 
 |-  ( ( ( -. i = I /\ ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) /\ i e. N /\ j e. N ) ) /\ -. j = I ) -> ( i = j <-> j = i ) )
79 78 ifbid 
 |-  ( ( ( -. i = I /\ ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) /\ i e. N /\ j e. N ) ) /\ -. j = I ) -> if ( i = j , ( 1r ` R ) , ( 0g ` R ) ) = if ( j = i , ( 1r ` R ) , ( 0g ` R ) ) )
80 76 79 eqtr2d 
 |-  ( ( ( -. i = I /\ ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) /\ i e. N /\ j e. N ) ) /\ -. j = I ) -> if ( j = i , ( 1r ` R ) , ( 0g ` R ) ) = ( i .1. j ) )
81 80 ifeq2da 
 |-  ( ( -. i = I /\ ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) /\ i e. N /\ j e. N ) ) -> if ( j = I , ( Z ` i ) , if ( j = i , ( 1r ` R ) , ( 0g ` R ) ) ) = if ( j = I , ( Z ` i ) , ( i .1. j ) ) )
82 60 71 81 3eqtrd 
 |-  ( ( -. i = I /\ ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) /\ i e. N /\ j e. N ) ) -> if ( i = I , if ( j = I , ( Z ` I ) , ( 0g ` R ) ) , ( i X j ) ) = if ( j = I , ( Z ` i ) , ( i .1. j ) ) )
83 58 82 pm2.61ian 
 |-  ( ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) /\ i e. N /\ j e. N ) -> if ( i = I , if ( j = I , ( Z ` I ) , ( 0g ` R ) ) , ( i X j ) ) = if ( j = I , ( Z ` i ) , ( i .1. j ) ) )
84 83 mpoeq3dva 
 |-  ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) -> ( i e. N , j e. N |-> if ( i = I , if ( j = I , ( Z ` I ) , ( 0g ` R ) ) , ( i X j ) ) ) = ( i e. N , j e. N |-> if ( j = I , ( Z ` i ) , ( i .1. j ) ) ) )
85 eqid 
 |-  ( N matRepV R ) = ( N matRepV R )
86 4 5 85 1 marepvval 
 |-  ( ( .1. e. ( Base ` ( N Mat R ) ) /\ Z e. V /\ I e. N ) -> ( ( .1. ( N matRepV R ) Z ) ` I ) = ( i e. N , j e. N |-> if ( j = I , ( Z ` i ) , ( i .1. j ) ) ) )
87 65 86 syl 
 |-  ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) -> ( ( .1. ( N matRepV R ) Z ) ` I ) = ( i e. N , j e. N |-> if ( j = I , ( Z ` i ) , ( i .1. j ) ) ) )
88 3 87 syl5req 
 |-  ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) -> ( i e. N , j e. N |-> if ( j = I , ( Z ` i ) , ( i .1. j ) ) ) = X )
89 21 84 88 3eqtrd 
 |-  ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) -> ( I ( X ( N matRRep R ) ( Z ` I ) ) I ) = X )