Description: Value of an identity matrix, see also the statement in Lang p. 504: "The unit element of the ring of n x n matrices is the matrix I_n ... whose components are equal to 0 except on the diagonal, in which case they are equal to 1.". (Contributed by Stefan O'Rear, 7-Sep-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | mat1.a | |
|
mat1.o | |
||
mat1.z | |
||
Assertion | mat1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mat1.a | |
|
2 | mat1.o | |
|
3 | mat1.z | |
|
4 | eqid | |
|
5 | simpr | |
|
6 | eqid | |
|
7 | simpl | |
|
8 | 4 5 2 3 6 7 | mamumat1cl | |
9 | 1 4 | matbas2 | |
10 | 8 9 | eleqtrd | |
11 | eqid | |
|
12 | 1 11 | matmulr | |
13 | 12 | adantr | |
14 | 13 | oveqd | |
15 | simplr | |
|
16 | simpll | |
|
17 | 9 | eleq2d | |
18 | 17 | biimpar | |
19 | 4 15 2 3 6 16 16 11 18 | mamulid | |
20 | 14 19 | eqtr3d | |
21 | 13 | oveqd | |
22 | 4 15 2 3 6 16 16 11 18 | mamurid | |
23 | 21 22 | eqtr3d | |
24 | 20 23 | jca | |
25 | 24 | ralrimiva | |
26 | 1 | matring | |
27 | eqid | |
|
28 | eqid | |
|
29 | eqid | |
|
30 | 27 28 29 | isringid | |
31 | 26 30 | syl | |
32 | 10 25 31 | mpbi2and | |