Step |
Hyp |
Ref |
Expression |
0 |
|
cmat |
|- Mat |
1 |
|
vn |
|- n |
2 |
|
cfn |
|- Fin |
3 |
|
vr |
|- r |
4 |
|
cvv |
|- _V |
5 |
3
|
cv |
|- r |
6 |
|
cfrlm |
|- freeLMod |
7 |
1
|
cv |
|- n |
8 |
7 7
|
cxp |
|- ( n X. n ) |
9 |
5 8 6
|
co |
|- ( r freeLMod ( n X. n ) ) |
10 |
|
csts |
|- sSet |
11 |
|
cmulr |
|- .r |
12 |
|
cnx |
|- ndx |
13 |
12 11
|
cfv |
|- ( .r ` ndx ) |
14 |
|
cmmul |
|- maMul |
15 |
7 7 7
|
cotp |
|- <. n , n , n >. |
16 |
5 15 14
|
co |
|- ( r maMul <. n , n , n >. ) |
17 |
13 16
|
cop |
|- <. ( .r ` ndx ) , ( r maMul <. n , n , n >. ) >. |
18 |
9 17 10
|
co |
|- ( ( r freeLMod ( n X. n ) ) sSet <. ( .r ` ndx ) , ( r maMul <. n , n , n >. ) >. ) |
19 |
1 3 2 4 18
|
cmpo |
|- ( n e. Fin , r e. _V |-> ( ( r freeLMod ( n X. n ) ) sSet <. ( .r ` ndx ) , ( r maMul <. n , n , n >. ) >. ) ) |
20 |
0 19
|
wceq |
|- Mat = ( n e. Fin , r e. _V |-> ( ( r freeLMod ( n X. n ) ) sSet <. ( .r ` ndx ) , ( r maMul <. n , n , n >. ) >. ) ) |