Step | Hyp | Ref
| Expression |
1 | | cpm2mp 22157 |
. 2
class
pMatToMatPoly |
2 | | vn |
. . 3
setvar ๐ |
3 | | vr |
. . 3
setvar ๐ |
4 | | cfn 8886 |
. . 3
class
Fin |
5 | | cvv 3444 |
. . 3
class
V |
6 | | vm |
. . . 4
setvar ๐ |
7 | 2 | cv 1541 |
. . . . . 6
class ๐ |
8 | 3 | cv 1541 |
. . . . . . 7
class ๐ |
9 | | cpl1 21564 |
. . . . . . 7
class
Poly1 |
10 | 8, 9 | cfv 6497 |
. . . . . 6
class
(Poly1โ๐) |
11 | | cmat 21770 |
. . . . . 6
class
Mat |
12 | 7, 10, 11 | co 7358 |
. . . . 5
class (๐ Mat
(Poly1โ๐)) |
13 | | cbs 17088 |
. . . . 5
class
Base |
14 | 12, 13 | cfv 6497 |
. . . 4
class
(Baseโ(๐ Mat
(Poly1โ๐))) |
15 | | va |
. . . . 5
setvar ๐ |
16 | 7, 8, 11 | co 7358 |
. . . . 5
class (๐ Mat ๐) |
17 | | vq |
. . . . . 6
setvar ๐ |
18 | 15 | cv 1541 |
. . . . . . 7
class ๐ |
19 | 18, 9 | cfv 6497 |
. . . . . 6
class
(Poly1โ๐) |
20 | 17 | cv 1541 |
. . . . . . 7
class ๐ |
21 | | vk |
. . . . . . . 8
setvar ๐ |
22 | | cn0 12418 |
. . . . . . . 8
class
โ0 |
23 | 6 | cv 1541 |
. . . . . . . . . 10
class ๐ |
24 | 21 | cv 1541 |
. . . . . . . . . 10
class ๐ |
25 | | cdecpmat 22127 |
. . . . . . . . . 10
class
decompPMat |
26 | 23, 24, 25 | co 7358 |
. . . . . . . . 9
class (๐ decompPMat ๐) |
27 | | cv1 21563 |
. . . . . . . . . . 11
class
var1 |
28 | 18, 27 | cfv 6497 |
. . . . . . . . . 10
class
(var1โ๐) |
29 | | cmgp 19901 |
. . . . . . . . . . . 12
class
mulGrp |
30 | 20, 29 | cfv 6497 |
. . . . . . . . . . 11
class
(mulGrpโ๐) |
31 | | cmg 18877 |
. . . . . . . . . . 11
class
.g |
32 | 30, 31 | cfv 6497 |
. . . . . . . . . 10
class
(.gโ(mulGrpโ๐)) |
33 | 24, 28, 32 | co 7358 |
. . . . . . . . 9
class (๐(.gโ(mulGrpโ๐))(var1โ๐)) |
34 | | cvsca 17142 |
. . . . . . . . . 10
class
ยท๐ |
35 | 20, 34 | cfv 6497 |
. . . . . . . . 9
class (
ยท๐ โ๐) |
36 | 26, 33, 35 | co 7358 |
. . . . . . . 8
class ((๐ decompPMat ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐))) |
37 | 21, 22, 36 | cmpt 5189 |
. . . . . . 7
class (๐ โ โ0
โฆ ((๐ decompPMat
๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐)))) |
38 | | cgsu 17327 |
. . . . . . 7
class
ฮฃg |
39 | 20, 37, 38 | co 7358 |
. . . . . 6
class (๐ ฮฃg
(๐ โ
โ0 โฆ ((๐ decompPMat ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐))))) |
40 | 17, 19, 39 | csb 3856 |
. . . . 5
class
โฆ(Poly1โ๐) / ๐โฆ(๐ ฮฃg (๐ โ โ0
โฆ ((๐ decompPMat
๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐))))) |
41 | 15, 16, 40 | csb 3856 |
. . . 4
class
โฆ(๐
Mat ๐) / ๐โฆโฆ(Poly1โ๐) / ๐โฆ(๐ ฮฃg (๐ โ โ0 โฆ ((๐ decompPMat ๐)( ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐))))) |
42 | 6, 14, 41 | cmpt 5189 |
. . 3
class (๐ โ (Baseโ(๐ Mat
(Poly1โ๐))) โฆ โฆ(๐ Mat ๐) / ๐โฆโฆ(Poly1โ๐) / ๐โฆ(๐ ฮฃg (๐ โ โ0 โฆ ((๐ decompPMat ๐)( ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐)))))) |
43 | 2, 3, 4, 5, 42 | cmpo 7360 |
. 2
class (๐ โ Fin, ๐ โ V โฆ (๐ โ (Baseโ(๐ Mat (Poly1โ๐))) โฆ
โฆ(๐ Mat ๐) / ๐โฆโฆ(Poly1โ๐) / ๐โฆ(๐ ฮฃg (๐ โ โ0 โฆ ((๐ decompPMat ๐)( ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐))))))) |
44 | 1, 43 | wceq 1542 |
1
wff
pMatToMatPoly = (๐ โ
Fin, ๐ โ V โฆ
(๐ โ
(Baseโ(๐ Mat
(Poly1โ๐))) โฆ โฆ(๐ Mat ๐) / ๐โฆโฆ(Poly1โ๐) / ๐โฆ(๐ ฮฃg (๐ โ โ0 โฆ ((๐ decompPMat ๐)( ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐))))))) |