Description: An N x N scalar matrix over (a ring) R . (Contributed by AV, 18-Dec-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | scmatval.k | |
|
scmatval.a | |
||
scmatval.b | |
||
scmatval.1 | |
||
scmatval.t | |
||
scmatval.s | |
||
Assertion | scmatel | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | scmatval.k | |
|
2 | scmatval.a | |
|
3 | scmatval.b | |
|
4 | scmatval.1 | |
|
5 | scmatval.t | |
|
6 | scmatval.s | |
|
7 | 1 2 3 4 5 6 | scmatval | |
8 | 7 | eleq2d | |
9 | eqeq1 | |
|
10 | 9 | rexbidv | |
11 | 10 | elrab | |
12 | 8 11 | bitrdi | |