Step | Hyp | Ref
| Expression |
1 | | cmat 21907 |
. 2
class
Mat |
2 | | vn |
. . 3
setvar π |
3 | | vr |
. . 3
setvar π |
4 | | cfn 8939 |
. . 3
class
Fin |
5 | | cvv 3475 |
. . 3
class
V |
6 | 3 | cv 1541 |
. . . . 5
class π |
7 | 2 | cv 1541 |
. . . . . 6
class π |
8 | 7, 7 | cxp 5675 |
. . . . 5
class (π Γ π) |
9 | | cfrlm 21301 |
. . . . 5
class
freeLMod |
10 | 6, 8, 9 | co 7409 |
. . . 4
class (π freeLMod (π Γ π)) |
11 | | cnx 17126 |
. . . . . 6
class
ndx |
12 | | cmulr 17198 |
. . . . . 6
class
.r |
13 | 11, 12 | cfv 6544 |
. . . . 5
class
(.rβndx) |
14 | 7, 7, 7 | cotp 4637 |
. . . . . 6
class
β¨π, π, πβ© |
15 | | cmmul 21885 |
. . . . . 6
class
maMul |
16 | 6, 14, 15 | co 7409 |
. . . . 5
class (π maMul β¨π, π, πβ©) |
17 | 13, 16 | cop 4635 |
. . . 4
class
β¨(.rβndx), (π maMul β¨π, π, πβ©)β© |
18 | | csts 17096 |
. . . 4
class
sSet |
19 | 10, 17, 18 | co 7409 |
. . 3
class ((π freeLMod (π Γ π)) sSet β¨(.rβndx),
(π maMul β¨π, π, πβ©)β©) |
20 | 2, 3, 4, 5, 19 | cmpo 7411 |
. 2
class (π β Fin, π β V β¦ ((π freeLMod (π Γ π)) sSet β¨(.rβndx),
(π maMul β¨π, π, πβ©)β©)) |
21 | 1, 20 | wceq 1542 |
1
wff Mat =
(π β Fin, π β V β¦ ((π freeLMod (π Γ π)) sSet β¨(.rβndx),
(π maMul β¨π, π, πβ©)β©)) |