Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  1marepvsma1 Structured version   Unicode version

Theorem 1marepvsma1 19543
 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.)
Hypotheses
Ref Expression
1marepvsma1.v
1marepvsma1.1 Mat
1marepvsma1.x matRepV
Assertion
Ref Expression
1marepvsma1 subMat Mat

Proof of Theorem 1marepvsma1
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 1marepvsma1.x . . . . . 6 matRepV
21oveqi 6318 . . . . 5 matRepV
32a1i 11 . . . 4 matRepV
4 eqid 2429 . . . . . . . . 9 Mat Mat
5 eqid 2429 . . . . . . . . 9 Mat Mat
6 1marepvsma1.1 . . . . . . . . 9 Mat
74, 5, 6mat1bas 19409 . . . . . . . 8 Mat
87adantr 466 . . . . . . 7 Mat
9 simprr 764 . . . . . . 7
10 simprl 762 . . . . . . 7
118, 9, 103jca 1185 . . . . . 6 Mat
12113ad2ant1 1026 . . . . 5 Mat
13 eldifi 3593 . . . . . . 7
14 eldifi 3593 . . . . . . 7
1513, 14anim12i 568 . . . . . 6
16153adant1 1023 . . . . 5
17 eqid 2429 . . . . . 6 matRepV matRepV
18 1marepvsma1.v . . . . . 6
194, 5, 17, 18marepveval 19528 . . . . 5 Mat matRepV
2012, 16, 19syl2anc 665 . . . 4 matRepV
21 eldifsni 4129 . . . . . . . 8
2221neneqd 2632 . . . . . . 7
23223ad2ant3 1028 . . . . . 6
2423iffalsed 3926 . . . . 5
25 eqid 2429 . . . . . 6
26 eqid 2429 . . . . . 6
27 simp1lr 1069 . . . . . 6
28 simp1ll 1068 . . . . . 6
29133ad2ant2 1027 . . . . . 6
30143ad2ant3 1028 . . . . . 6
314, 25, 26, 27, 28, 29, 30, 6mat1ov 19408 . . . . 5
3224, 31eqtrd 2470 . . . 4
333, 20, 323eqtrd 2474 . . 3
3433mpt2eq3dva 6369 . 2
354, 5, 18, 6ma1repvcl 19530 . . . . 5 matRepV Mat
3635ancom2s 809 . . . 4 matRepV Mat
371, 36syl5eqel 2521 . . 3 Mat
38 eqid 2429 . . . 4 subMat subMat
394, 38, 5submaval 19541 . . 3 Mat subMat
4037, 10, 10, 39syl3anc 1264 . 2 subMat
41 diffi 7809 . . . . . 6
4241anim2i 571 . . . . 5
4342ancomd 452 . . . 4