Step |
Hyp |
Ref |
Expression |
0 |
|
cscmat |
|- ScMat |
1 |
|
vn |
|- n |
2 |
|
cfn |
|- Fin |
3 |
|
vr |
|- r |
4 |
|
cvv |
|- _V |
5 |
1
|
cv |
|- n |
6 |
|
cmat |
|- Mat |
7 |
3
|
cv |
|- r |
8 |
5 7 6
|
co |
|- ( n Mat r ) |
9 |
|
va |
|- a |
10 |
|
vm |
|- m |
11 |
|
cbs |
|- Base |
12 |
9
|
cv |
|- a |
13 |
12 11
|
cfv |
|- ( Base ` a ) |
14 |
|
vc |
|- c |
15 |
7 11
|
cfv |
|- ( Base ` r ) |
16 |
10
|
cv |
|- m |
17 |
14
|
cv |
|- c |
18 |
|
cvsca |
|- .s |
19 |
12 18
|
cfv |
|- ( .s ` a ) |
20 |
|
cur |
|- 1r |
21 |
12 20
|
cfv |
|- ( 1r ` a ) |
22 |
17 21 19
|
co |
|- ( c ( .s ` a ) ( 1r ` a ) ) |
23 |
16 22
|
wceq |
|- m = ( c ( .s ` a ) ( 1r ` a ) ) |
24 |
23 14 15
|
wrex |
|- E. c e. ( Base ` r ) m = ( c ( .s ` a ) ( 1r ` a ) ) |
25 |
24 10 13
|
crab |
|- { m e. ( Base ` a ) | E. c e. ( Base ` r ) m = ( c ( .s ` a ) ( 1r ` a ) ) } |
26 |
9 8 25
|
csb |
|- [_ ( n Mat r ) / a ]_ { m e. ( Base ` a ) | E. c e. ( Base ` r ) m = ( c ( .s ` a ) ( 1r ` a ) ) } |
27 |
1 3 2 4 26
|
cmpo |
|- ( n e. Fin , r e. _V |-> [_ ( n Mat r ) / a ]_ { m e. ( Base ` a ) | E. c e. ( Base ` r ) m = ( c ( .s ` a ) ( 1r ` a ) ) } ) |
28 |
0 27
|
wceq |
|- ScMat = ( n e. Fin , r e. _V |-> [_ ( n Mat r ) / a ]_ { m e. ( Base ` a ) | E. c e. ( Base ` r ) m = ( c ( .s ` a ) ( 1r ` a ) ) } ) |