Step | Hyp | Ref
| Expression |
1 | | pm2mpval.t |
. 2
โข ๐ = (๐ pMatToMatPoly ๐
) |
2 | | df-pm2mp 22158 |
. . . 4
โข
pMatToMatPoly = (๐ โ
Fin, ๐ โ V โฆ
(๐ โ
(Baseโ(๐ Mat
(Poly1โ๐))) โฆ โฆ(๐ Mat ๐) / ๐โฆโฆ(Poly1โ๐) / ๐โฆ(๐ ฮฃg (๐ โ โ0 โฆ ((๐ decompPMat ๐)( ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐))))))) |
3 | 2 | a1i 11 |
. . 3
โข ((๐ โ Fin โง ๐
โ ๐) โ pMatToMatPoly = (๐ โ Fin, ๐ โ V โฆ (๐ โ (Baseโ(๐ Mat (Poly1โ๐))) โฆ
โฆ(๐ Mat ๐) / ๐โฆโฆ(Poly1โ๐) / ๐โฆ(๐ ฮฃg (๐ โ โ0 โฆ ((๐ decompPMat ๐)( ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐)))))))) |
4 | | simpl 484 |
. . . . . . . 8
โข ((๐ = ๐ โง ๐ = ๐
) โ ๐ = ๐) |
5 | | fveq2 6843 |
. . . . . . . . 9
โข (๐ = ๐
โ (Poly1โ๐) =
(Poly1โ๐
)) |
6 | 5 | adantl 483 |
. . . . . . . 8
โข ((๐ = ๐ โง ๐ = ๐
) โ (Poly1โ๐) =
(Poly1โ๐
)) |
7 | 4, 6 | oveq12d 7376 |
. . . . . . 7
โข ((๐ = ๐ โง ๐ = ๐
) โ (๐ Mat (Poly1โ๐)) = (๐ Mat (Poly1โ๐
))) |
8 | 7 | fveq2d 6847 |
. . . . . 6
โข ((๐ = ๐ โง ๐ = ๐
) โ (Baseโ(๐ Mat (Poly1โ๐))) = (Baseโ(๐ Mat
(Poly1โ๐
)))) |
9 | | pm2mpval.b |
. . . . . . 7
โข ๐ต = (Baseโ๐ถ) |
10 | | pm2mpval.c |
. . . . . . . . 9
โข ๐ถ = (๐ Mat ๐) |
11 | | pm2mpval.p |
. . . . . . . . . 10
โข ๐ = (Poly1โ๐
) |
12 | 11 | oveq2i 7369 |
. . . . . . . . 9
โข (๐ Mat ๐) = (๐ Mat (Poly1โ๐
)) |
13 | 10, 12 | eqtri 2761 |
. . . . . . . 8
โข ๐ถ = (๐ Mat (Poly1โ๐
)) |
14 | 13 | fveq2i 6846 |
. . . . . . 7
โข
(Baseโ๐ถ) =
(Baseโ(๐ Mat
(Poly1โ๐
))) |
15 | 9, 14 | eqtri 2761 |
. . . . . 6
โข ๐ต = (Baseโ(๐ Mat
(Poly1โ๐
))) |
16 | 8, 15 | eqtr4di 2791 |
. . . . 5
โข ((๐ = ๐ โง ๐ = ๐
) โ (Baseโ(๐ Mat (Poly1โ๐))) = ๐ต) |
17 | 16 | adantl 483 |
. . . 4
โข (((๐ โ Fin โง ๐
โ ๐) โง (๐ = ๐ โง ๐ = ๐
)) โ (Baseโ(๐ Mat (Poly1โ๐))) = ๐ต) |
18 | | ovex 7391 |
. . . . . 6
โข (๐ Mat ๐) โ V |
19 | | fvexd 6858 |
. . . . . . 7
โข (๐ = (๐ Mat ๐) โ (Poly1โ๐) โ V) |
20 | | simpr 486 |
. . . . . . . . 9
โข ((๐ = (๐ Mat ๐) โง ๐ = (Poly1โ๐)) โ ๐ = (Poly1โ๐)) |
21 | | fveq2 6843 |
. . . . . . . . . 10
โข (๐ = (๐ Mat ๐) โ (Poly1โ๐) =
(Poly1โ(๐
Mat ๐))) |
22 | 21 | adantr 482 |
. . . . . . . . 9
โข ((๐ = (๐ Mat ๐) โง ๐ = (Poly1โ๐)) โ (Poly1โ๐) =
(Poly1โ(๐
Mat ๐))) |
23 | 20, 22 | eqtrd 2773 |
. . . . . . . 8
โข ((๐ = (๐ Mat ๐) โง ๐ = (Poly1โ๐)) โ ๐ = (Poly1โ(๐ Mat ๐))) |
24 | 23 | fveq2d 6847 |
. . . . . . . . . 10
โข ((๐ = (๐ Mat ๐) โง ๐ = (Poly1โ๐)) โ (
ยท๐ โ๐) = ( ยท๐
โ(Poly1โ(๐ Mat ๐)))) |
25 | | eqidd 2734 |
. . . . . . . . . 10
โข ((๐ = (๐ Mat ๐) โง ๐ = (Poly1โ๐)) โ (๐ decompPMat ๐) = (๐ decompPMat ๐)) |
26 | 23 | fveq2d 6847 |
. . . . . . . . . . . 12
โข ((๐ = (๐ Mat ๐) โง ๐ = (Poly1โ๐)) โ (mulGrpโ๐) =
(mulGrpโ(Poly1โ(๐ Mat ๐)))) |
27 | 26 | fveq2d 6847 |
. . . . . . . . . . 11
โข ((๐ = (๐ Mat ๐) โง ๐ = (Poly1โ๐)) โ
(.gโ(mulGrpโ๐)) =
(.gโ(mulGrpโ(Poly1โ(๐ Mat ๐))))) |
28 | | eqidd 2734 |
. . . . . . . . . . 11
โข ((๐ = (๐ Mat ๐) โง ๐ = (Poly1โ๐)) โ ๐ = ๐) |
29 | | fveq2 6843 |
. . . . . . . . . . . 12
โข (๐ = (๐ Mat ๐) โ (var1โ๐) =
(var1โ(๐
Mat ๐))) |
30 | 29 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ = (๐ Mat ๐) โง ๐ = (Poly1โ๐)) โ (var1โ๐) =
(var1โ(๐
Mat ๐))) |
31 | 27, 28, 30 | oveq123d 7379 |
. . . . . . . . . 10
โข ((๐ = (๐ Mat ๐) โง ๐ = (Poly1โ๐)) โ (๐(.gโ(mulGrpโ๐))(var1โ๐)) = (๐(.gโ(mulGrpโ(Poly1โ(๐ Mat ๐))))(var1โ(๐ Mat ๐)))) |
32 | 24, 25, 31 | oveq123d 7379 |
. . . . . . . . 9
โข ((๐ = (๐ Mat ๐) โง ๐ = (Poly1โ๐)) โ ((๐ decompPMat ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐))) = ((๐ decompPMat ๐)( ยท๐
โ(Poly1โ(๐ Mat ๐)))(๐(.gโ(mulGrpโ(Poly1โ(๐ Mat ๐))))(var1โ(๐ Mat ๐))))) |
33 | 32 | mpteq2dv 5208 |
. . . . . . . 8
โข ((๐ = (๐ Mat ๐) โง ๐ = (Poly1โ๐)) โ (๐ โ โ0 โฆ ((๐ decompPMat ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐)))) = (๐ โ โ0 โฆ ((๐ decompPMat ๐)( ยท๐
โ(Poly1โ(๐ Mat ๐)))(๐(.gโ(mulGrpโ(Poly1โ(๐ Mat ๐))))(var1โ(๐ Mat ๐)))))) |
34 | 23, 33 | oveq12d 7376 |
. . . . . . 7
โข ((๐ = (๐ Mat ๐) โง ๐ = (Poly1โ๐)) โ (๐ ฮฃg (๐ โ โ0
โฆ ((๐ decompPMat
๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐))))) =
((Poly1โ(๐
Mat ๐))
ฮฃg (๐ โ โ0 โฆ ((๐ decompPMat ๐)( ยท๐
โ(Poly1โ(๐ Mat ๐)))(๐(.gโ(mulGrpโ(Poly1โ(๐ Mat ๐))))(var1โ(๐ Mat ๐))))))) |
35 | 19, 34 | csbied 3894 |
. . . . . 6
โข (๐ = (๐ Mat ๐) โ
โฆ(Poly1โ๐) / ๐โฆ(๐ ฮฃg (๐ โ โ0
โฆ ((๐ decompPMat
๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐))))) =
((Poly1โ(๐
Mat ๐))
ฮฃg (๐ โ โ0 โฆ ((๐ decompPMat ๐)( ยท๐
โ(Poly1โ(๐ Mat ๐)))(๐(.gโ(mulGrpโ(Poly1โ(๐ Mat ๐))))(var1โ(๐ Mat ๐))))))) |
36 | 18, 35 | csbie 3892 |
. . . . 5
โข
โฆ(๐
Mat ๐) / ๐โฆโฆ(Poly1โ๐) / ๐โฆ(๐ ฮฃg (๐ โ โ0 โฆ ((๐ decompPMat ๐)( ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐))))) = ((Poly1โ(๐ Mat ๐)) ฮฃg (๐ โ โ0 โฆ ((๐ decompPMat ๐)( ยท๐
โ(Poly1โ(๐ Mat
๐)))(๐(.gโ(mulGrpโ(Poly1โ(๐ Mat ๐))))(var1โ(๐ Mat ๐)))))) |
37 | | oveq12 7367 |
. . . . . . . . 9
โข ((๐ = ๐ โง ๐ = ๐
) โ (๐ Mat ๐) = (๐ Mat ๐
)) |
38 | 37 | fveq2d 6847 |
. . . . . . . 8
โข ((๐ = ๐ โง ๐ = ๐
) โ (Poly1โ(๐ Mat ๐)) = (Poly1โ(๐ Mat ๐
))) |
39 | | pm2mpval.q |
. . . . . . . . 9
โข ๐ = (Poly1โ๐ด) |
40 | | pm2mpval.a |
. . . . . . . . . 10
โข ๐ด = (๐ Mat ๐
) |
41 | 40 | fveq2i 6846 |
. . . . . . . . 9
โข
(Poly1โ๐ด) = (Poly1โ(๐ Mat ๐
)) |
42 | 39, 41 | eqtri 2761 |
. . . . . . . 8
โข ๐ =
(Poly1โ(๐
Mat ๐
)) |
43 | 38, 42 | eqtr4di 2791 |
. . . . . . 7
โข ((๐ = ๐ โง ๐ = ๐
) โ (Poly1โ(๐ Mat ๐)) = ๐) |
44 | 38 | fveq2d 6847 |
. . . . . . . . . 10
โข ((๐ = ๐ โง ๐ = ๐
) โ (
ยท๐ โ(Poly1โ(๐ Mat ๐))) = ( ยท๐
โ(Poly1โ(๐ Mat ๐
)))) |
45 | | pm2mpval.m |
. . . . . . . . . . 11
โข โ = (
ยท๐ โ๐) |
46 | 42 | fveq2i 6846 |
. . . . . . . . . . 11
โข (
ยท๐ โ๐) = ( ยท๐
โ(Poly1โ(๐ Mat ๐
))) |
47 | 45, 46 | eqtri 2761 |
. . . . . . . . . 10
โข โ = (
ยท๐ โ(Poly1โ(๐ Mat ๐
))) |
48 | 44, 47 | eqtr4di 2791 |
. . . . . . . . 9
โข ((๐ = ๐ โง ๐ = ๐
) โ (
ยท๐ โ(Poly1โ(๐ Mat ๐))) = โ ) |
49 | | eqidd 2734 |
. . . . . . . . 9
โข ((๐ = ๐ โง ๐ = ๐
) โ (๐ decompPMat ๐) = (๐ decompPMat ๐)) |
50 | 38 | fveq2d 6847 |
. . . . . . . . . . . 12
โข ((๐ = ๐ โง ๐ = ๐
) โ
(mulGrpโ(Poly1โ(๐ Mat ๐))) =
(mulGrpโ(Poly1โ(๐ Mat ๐
)))) |
51 | 50 | fveq2d 6847 |
. . . . . . . . . . 11
โข ((๐ = ๐ โง ๐ = ๐
) โ
(.gโ(mulGrpโ(Poly1โ(๐ Mat ๐)))) =
(.gโ(mulGrpโ(Poly1โ(๐ Mat ๐
))))) |
52 | | pm2mpval.e |
. . . . . . . . . . . 12
โข โ =
(.gโ(mulGrpโ๐)) |
53 | 42 | fveq2i 6846 |
. . . . . . . . . . . . 13
โข
(mulGrpโ๐) =
(mulGrpโ(Poly1โ(๐ Mat ๐
))) |
54 | 53 | fveq2i 6846 |
. . . . . . . . . . . 12
โข
(.gโ(mulGrpโ๐)) =
(.gโ(mulGrpโ(Poly1โ(๐ Mat ๐
)))) |
55 | 52, 54 | eqtri 2761 |
. . . . . . . . . . 11
โข โ =
(.gโ(mulGrpโ(Poly1โ(๐ Mat ๐
)))) |
56 | 51, 55 | eqtr4di 2791 |
. . . . . . . . . 10
โข ((๐ = ๐ โง ๐ = ๐
) โ
(.gโ(mulGrpโ(Poly1โ(๐ Mat ๐)))) = โ ) |
57 | | eqidd 2734 |
. . . . . . . . . 10
โข ((๐ = ๐ โง ๐ = ๐
) โ ๐ = ๐) |
58 | 37 | fveq2d 6847 |
. . . . . . . . . . 11
โข ((๐ = ๐ โง ๐ = ๐
) โ (var1โ(๐ Mat ๐)) = (var1โ(๐ Mat ๐
))) |
59 | | pm2mpval.x |
. . . . . . . . . . . 12
โข ๐ = (var1โ๐ด) |
60 | 40 | fveq2i 6846 |
. . . . . . . . . . . 12
โข
(var1โ๐ด) = (var1โ(๐ Mat ๐
)) |
61 | 59, 60 | eqtri 2761 |
. . . . . . . . . . 11
โข ๐ = (var1โ(๐ Mat ๐
)) |
62 | 58, 61 | eqtr4di 2791 |
. . . . . . . . . 10
โข ((๐ = ๐ โง ๐ = ๐
) โ (var1โ(๐ Mat ๐)) = ๐) |
63 | 56, 57, 62 | oveq123d 7379 |
. . . . . . . . 9
โข ((๐ = ๐ โง ๐ = ๐
) โ (๐(.gโ(mulGrpโ(Poly1โ(๐ Mat ๐))))(var1โ(๐ Mat ๐))) =
(๐ โ ๐)) |
64 | 48, 49, 63 | oveq123d 7379 |
. . . . . . . 8
โข ((๐ = ๐ โง ๐ = ๐
) โ ((๐ decompPMat ๐)( ยท๐
โ(Poly1โ(๐ Mat ๐)))(๐(.gโ(mulGrpโ(Poly1โ(๐ Mat ๐))))(var1โ(๐ Mat ๐)))) =
((๐ decompPMat ๐) โ (๐ โ ๐))) |
65 | 64 | mpteq2dv 5208 |
. . . . . . 7
โข ((๐ = ๐ โง ๐ = ๐
) โ (๐ โ โ0 โฆ ((๐ decompPMat ๐)( ยท๐
โ(Poly1โ(๐ Mat ๐)))(๐(.gโ(mulGrpโ(Poly1โ(๐ Mat ๐))))(var1โ(๐ Mat ๐))))) =
(๐ โ โ0 โฆ ((๐ decompPMat ๐) โ (๐ โ ๐)))) |
66 | 43, 65 | oveq12d 7376 |
. . . . . 6
โข ((๐ = ๐ โง ๐ = ๐
) โ ((Poly1โ(๐ Mat ๐)) ฮฃg (๐ โ โ0
โฆ ((๐ decompPMat
๐)(
ยท๐ โ(Poly1โ(๐ Mat ๐)))(๐(.gโ(mulGrpโ(Poly1โ(๐ Mat ๐))))(var1โ(๐ Mat ๐))))))
= (๐ ฮฃg (๐ โ โ0 โฆ ((๐ decompPMat ๐) โ (๐ โ ๐))))) |
67 | 66 | adantl 483 |
. . . . 5
โข (((๐ โ Fin โง ๐
โ ๐) โง (๐ = ๐ โง ๐ = ๐
)) โ ((Poly1โ(๐ Mat ๐)) ฮฃg (๐ โ โ0
โฆ ((๐ decompPMat
๐)(
ยท๐ โ(Poly1โ(๐ Mat ๐)))(๐(.gโ(mulGrpโ(Poly1โ(๐ Mat ๐))))(var1โ(๐ Mat ๐))))))
= (๐ ฮฃg (๐ โ โ0 โฆ ((๐ decompPMat ๐) โ (๐ โ ๐))))) |
68 | 36, 67 | eqtrid 2785 |
. . . 4
โข (((๐ โ Fin โง ๐
โ ๐) โง (๐ = ๐ โง ๐ = ๐
)) โ โฆ(๐ Mat ๐) / ๐โฆโฆ(Poly1โ๐) / ๐โฆ(๐ ฮฃg (๐ โ โ0 โฆ ((๐ decompPMat ๐)( ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐))))) = (๐ ฮฃg (๐ โ โ0 โฆ ((๐ decompPMat ๐) โ (๐ โ ๐))))) |
69 | 17, 68 | mpteq12dv 5197 |
. . 3
โข (((๐ โ Fin โง ๐
โ ๐) โง (๐ = ๐ โง ๐ = ๐
)) โ (๐ โ (Baseโ(๐ Mat (Poly1โ๐))) โฆ
โฆ(๐ Mat ๐) / ๐โฆโฆ(Poly1โ๐) / ๐โฆ(๐ ฮฃg (๐ โ โ0 โฆ ((๐ decompPMat ๐)( ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐)))))) = (๐ โ ๐ต โฆ (๐ ฮฃg (๐ โ โ0 โฆ ((๐ decompPMat ๐) โ (๐ โ ๐)))))) |
70 | | simpl 484 |
. . 3
โข ((๐ โ Fin โง ๐
โ ๐) โ ๐ โ Fin) |
71 | | elex 3462 |
. . . 4
โข (๐
โ ๐ โ ๐
โ V) |
72 | 71 | adantl 483 |
. . 3
โข ((๐ โ Fin โง ๐
โ ๐) โ ๐
โ V) |
73 | 9 | fvexi 6857 |
. . . . 5
โข ๐ต โ V |
74 | 73 | mptex 7174 |
. . . 4
โข (๐ โ ๐ต โฆ (๐ ฮฃg (๐ โ โ0
โฆ ((๐ decompPMat
๐) โ (๐ โ ๐))))) โ V |
75 | 74 | a1i 11 |
. . 3
โข ((๐ โ Fin โง ๐
โ ๐) โ (๐ โ ๐ต โฆ (๐ ฮฃg (๐ โ โ0
โฆ ((๐ decompPMat
๐) โ (๐ โ ๐))))) โ V) |
76 | 3, 69, 70, 72, 75 | ovmpod 7508 |
. 2
โข ((๐ โ Fin โง ๐
โ ๐) โ (๐ pMatToMatPoly ๐
) = (๐ โ ๐ต โฆ (๐ ฮฃg (๐ โ โ0
โฆ ((๐ decompPMat
๐) โ (๐ โ ๐)))))) |
77 | 1, 76 | eqtrid 2785 |
1
โข ((๐ โ Fin โง ๐
โ ๐) โ ๐ = (๐ โ ๐ต โฆ (๐ ฮฃg (๐ โ โ0
โฆ ((๐ decompPMat
๐) โ (๐ โ ๐)))))) |