Step | Hyp | Ref
| Expression |
1 | | pm2mpval.p |
. . . . 5
β’ π = (Poly1βπ
) |
2 | | pm2mpval.c |
. . . . 5
β’ πΆ = (π Mat π) |
3 | 1, 2 | pmatring 22057 |
. . . 4
β’ ((π β Fin β§ π
β Ring) β πΆ β Ring) |
4 | | pm2mpval.b |
. . . . 5
β’ π΅ = (BaseβπΆ) |
5 | | eqid 2733 |
. . . . 5
β’
(1rβπΆ) = (1rβπΆ) |
6 | 4, 5 | ringidcl 19994 |
. . . 4
β’ (πΆ β Ring β
(1rβπΆ)
β π΅) |
7 | 3, 6 | syl 17 |
. . 3
β’ ((π β Fin β§ π
β Ring) β
(1rβπΆ)
β π΅) |
8 | | pm2mpval.m |
. . . 4
β’ β = (
Β·π βπ) |
9 | | pm2mpval.e |
. . . 4
β’ β =
(.gβ(mulGrpβπ)) |
10 | | pm2mpval.x |
. . . 4
β’ π = (var1βπ΄) |
11 | | pm2mpval.a |
. . . 4
β’ π΄ = (π Mat π
) |
12 | | pm2mpval.q |
. . . 4
β’ π = (Poly1βπ΄) |
13 | | pm2mpval.t |
. . . 4
β’ π = (π pMatToMatPoly π
) |
14 | 1, 2, 4, 8, 9, 10,
11, 12, 13 | pm2mpfval 22161 |
. . 3
β’ ((π β Fin β§ π
β Ring β§
(1rβπΆ)
β π΅) β (πβ(1rβπΆ)) = (π Ξ£g (π β β0
β¦ (((1rβπΆ) decompPMat π) β (π β π))))) |
15 | 7, 14 | mpd3an3 1463 |
. 2
β’ ((π β Fin β§ π
β Ring) β (πβ(1rβπΆ)) = (π Ξ£g (π β β0
β¦ (((1rβπΆ) decompPMat π) β (π β π))))) |
16 | | eqid 2733 |
. . . . . . 7
β’
(0gβπ΄) = (0gβπ΄) |
17 | | eqid 2733 |
. . . . . . 7
β’
(1rβπ΄) = (1rβπ΄) |
18 | 1, 2, 5, 11, 16, 17 | decpmatid 22135 |
. . . . . 6
β’ ((π β Fin β§ π
β Ring β§ π β β0)
β ((1rβπΆ) decompPMat π) = if(π = 0, (1rβπ΄), (0gβπ΄))) |
19 | 18 | 3expa 1119 |
. . . . 5
β’ (((π β Fin β§ π
β Ring) β§ π β β0)
β ((1rβπΆ) decompPMat π) = if(π = 0, (1rβπ΄), (0gβπ΄))) |
20 | 19 | oveq1d 7373 |
. . . 4
β’ (((π β Fin β§ π
β Ring) β§ π β β0)
β (((1rβπΆ) decompPMat π) β (π β π)) = (if(π = 0, (1rβπ΄), (0gβπ΄)) β (π β π))) |
21 | 20 | mpteq2dva 5206 |
. . 3
β’ ((π β Fin β§ π
β Ring) β (π β β0
β¦ (((1rβπΆ) decompPMat π) β (π β π))) = (π β β0 β¦ (if(π = 0, (1rβπ΄), (0gβπ΄)) β (π β π)))) |
22 | 21 | oveq2d 7374 |
. 2
β’ ((π β Fin β§ π
β Ring) β (π Ξ£g
(π β
β0 β¦ (((1rβπΆ) decompPMat π) β (π β π)))) = (π Ξ£g (π β β0
β¦ (if(π = 0,
(1rβπ΄),
(0gβπ΄))
β
(π β π))))) |
23 | | ovif 7455 |
. . . . . 6
β’ (if(π = 0, (1rβπ΄), (0gβπ΄)) β (π β π)) = if(π = 0, ((1rβπ΄) β (π β π)), ((0gβπ΄) β (π β π))) |
24 | 11 | matring 21808 |
. . . . . . . . . . . 12
β’ ((π β Fin β§ π
β Ring) β π΄ β Ring) |
25 | 12 | ply1sca 21640 |
. . . . . . . . . . . 12
β’ (π΄ β Ring β π΄ = (Scalarβπ)) |
26 | 24, 25 | syl 17 |
. . . . . . . . . . 11
β’ ((π β Fin β§ π
β Ring) β π΄ = (Scalarβπ)) |
27 | 26 | adantr 482 |
. . . . . . . . . 10
β’ (((π β Fin β§ π
β Ring) β§ π β β0)
β π΄ =
(Scalarβπ)) |
28 | 27 | fveq2d 6847 |
. . . . . . . . 9
β’ (((π β Fin β§ π
β Ring) β§ π β β0)
β (1rβπ΄) = (1rβ(Scalarβπ))) |
29 | 28 | oveq1d 7373 |
. . . . . . . 8
β’ (((π β Fin β§ π
β Ring) β§ π β β0)
β ((1rβπ΄) β (π β π)) =
((1rβ(Scalarβπ)) β (π β π))) |
30 | 12 | ply1lmod 21639 |
. . . . . . . . . 10
β’ (π΄ β Ring β π β LMod) |
31 | 24, 30 | syl 17 |
. . . . . . . . 9
β’ ((π β Fin β§ π
β Ring) β π β LMod) |
32 | | eqid 2733 |
. . . . . . . . . . 11
β’
(mulGrpβπ) =
(mulGrpβπ) |
33 | | eqid 2733 |
. . . . . . . . . . 11
β’
(Baseβπ) =
(Baseβπ) |
34 | 12, 10, 32, 9, 33 | ply1moncl 21658 |
. . . . . . . . . 10
β’ ((π΄ β Ring β§ π β β0)
β (π β π) β (Baseβπ)) |
35 | 24, 34 | sylan 581 |
. . . . . . . . 9
β’ (((π β Fin β§ π
β Ring) β§ π β β0)
β (π β π) β (Baseβπ)) |
36 | | eqid 2733 |
. . . . . . . . . 10
β’
(Scalarβπ) =
(Scalarβπ) |
37 | | eqid 2733 |
. . . . . . . . . 10
β’
(1rβ(Scalarβπ)) =
(1rβ(Scalarβπ)) |
38 | 33, 36, 8, 37 | lmodvs1 20365 |
. . . . . . . . 9
β’ ((π β LMod β§ (π β π) β (Baseβπ)) β
((1rβ(Scalarβπ)) β (π β π)) = (π β π)) |
39 | 31, 35, 38 | syl2an2r 684 |
. . . . . . . 8
β’ (((π β Fin β§ π
β Ring) β§ π β β0)
β ((1rβ(Scalarβπ)) β (π β π)) = (π β π)) |
40 | 29, 39 | eqtrd 2773 |
. . . . . . 7
β’ (((π β Fin β§ π
β Ring) β§ π β β0)
β ((1rβπ΄) β (π β π)) = (π β π)) |
41 | 27 | fveq2d 6847 |
. . . . . . . . 9
β’ (((π β Fin β§ π
β Ring) β§ π β β0)
β (0gβπ΄) = (0gβ(Scalarβπ))) |
42 | 41 | oveq1d 7373 |
. . . . . . . 8
β’ (((π β Fin β§ π
β Ring) β§ π β β0)
β ((0gβπ΄) β (π β π)) =
((0gβ(Scalarβπ)) β (π β π))) |
43 | | eqid 2733 |
. . . . . . . . . 10
β’
(0gβ(Scalarβπ)) =
(0gβ(Scalarβπ)) |
44 | | eqid 2733 |
. . . . . . . . . 10
β’
(0gβπ) = (0gβπ) |
45 | 33, 36, 8, 43, 44 | lmod0vs 20370 |
. . . . . . . . 9
β’ ((π β LMod β§ (π β π) β (Baseβπ)) β
((0gβ(Scalarβπ)) β (π β π)) = (0gβπ)) |
46 | 31, 35, 45 | syl2an2r 684 |
. . . . . . . 8
β’ (((π β Fin β§ π
β Ring) β§ π β β0)
β ((0gβ(Scalarβπ)) β (π β π)) = (0gβπ)) |
47 | 42, 46 | eqtrd 2773 |
. . . . . . 7
β’ (((π β Fin β§ π
β Ring) β§ π β β0)
β ((0gβπ΄) β (π β π)) = (0gβπ)) |
48 | 40, 47 | ifeq12d 4508 |
. . . . . 6
β’ (((π β Fin β§ π
β Ring) β§ π β β0)
β if(π = 0,
((1rβπ΄)
β
(π β π)), ((0gβπ΄) β (π β π))) = if(π = 0, (π β π), (0gβπ))) |
49 | 23, 48 | eqtrid 2785 |
. . . . 5
β’ (((π β Fin β§ π
β Ring) β§ π β β0)
β (if(π = 0,
(1rβπ΄),
(0gβπ΄))
β
(π β π)) = if(π = 0, (π β π), (0gβπ))) |
50 | 49 | mpteq2dva 5206 |
. . . 4
β’ ((π β Fin β§ π
β Ring) β (π β β0
β¦ (if(π = 0,
(1rβπ΄),
(0gβπ΄))
β
(π β π))) = (π β β0 β¦ if(π = 0, (π β π), (0gβπ)))) |
51 | 50 | oveq2d 7374 |
. . 3
β’ ((π β Fin β§ π
β Ring) β (π Ξ£g
(π β
β0 β¦ (if(π = 0, (1rβπ΄), (0gβπ΄)) β (π β π)))) = (π Ξ£g (π β β0
β¦ if(π = 0, (π β π), (0gβπ))))) |
52 | 12 | ply1ring 21635 |
. . . . 5
β’ (π΄ β Ring β π β Ring) |
53 | | ringmnd 19979 |
. . . . 5
β’ (π β Ring β π β Mnd) |
54 | 24, 52, 53 | 3syl 18 |
. . . 4
β’ ((π β Fin β§ π
β Ring) β π β Mnd) |
55 | | nn0ex 12424 |
. . . . 5
β’
β0 β V |
56 | 55 | a1i 11 |
. . . 4
β’ ((π β Fin β§ π
β Ring) β
β0 β V) |
57 | | 0nn0 12433 |
. . . . 5
β’ 0 β
β0 |
58 | 57 | a1i 11 |
. . . 4
β’ ((π β Fin β§ π
β Ring) β 0 β
β0) |
59 | | eqid 2733 |
. . . 4
β’ (π β β0
β¦ if(π = 0, (π β π), (0gβπ))) = (π β β0 β¦ if(π = 0, (π β π), (0gβπ))) |
60 | 35 | ralrimiva 3140 |
. . . 4
β’ ((π β Fin β§ π
β Ring) β
βπ β
β0 (π
β
π) β (Baseβπ)) |
61 | 44, 54, 56, 58, 59, 60 | gsummpt1n0 19747 |
. . 3
β’ ((π β Fin β§ π
β Ring) β (π Ξ£g
(π β
β0 β¦ if(π = 0, (π β π), (0gβπ)))) = β¦0 / πβ¦(π β π)) |
62 | | c0ex 11154 |
. . . . 5
β’ 0 β
V |
63 | | csbov1g 7403 |
. . . . 5
β’ (0 β
V β β¦0 / πβ¦(π β π) = (β¦0 / πβ¦π β π)) |
64 | 62, 63 | mp1i 13 |
. . . 4
β’ ((π β Fin β§ π
β Ring) β
β¦0 / πβ¦(π β π) = (β¦0 / πβ¦π β π)) |
65 | | csbvarg 4392 |
. . . . . 6
β’ (0 β
V β β¦0 / πβ¦π = 0) |
66 | 62, 65 | mp1i 13 |
. . . . 5
β’ ((π β Fin β§ π
β Ring) β
β¦0 / πβ¦π = 0) |
67 | 66 | oveq1d 7373 |
. . . 4
β’ ((π β Fin β§ π
β Ring) β
(β¦0 / πβ¦π β π) = (0 β π)) |
68 | 12, 10, 32, 9 | ply1idvr1 21680 |
. . . . 5
β’ (π΄ β Ring β (0 β π) = (1rβπ)) |
69 | 24, 68 | syl 17 |
. . . 4
β’ ((π β Fin β§ π
β Ring) β (0 β π) = (1rβπ)) |
70 | 64, 67, 69 | 3eqtrd 2777 |
. . 3
β’ ((π β Fin β§ π
β Ring) β
β¦0 / πβ¦(π β π) = (1rβπ)) |
71 | 51, 61, 70 | 3eqtrd 2777 |
. 2
β’ ((π β Fin β§ π
β Ring) β (π Ξ£g
(π β
β0 β¦ (if(π = 0, (1rβπ΄), (0gβπ΄)) β (π β π)))) = (1rβπ)) |
72 | 15, 22, 71 | 3eqtrd 2777 |
1
β’ ((π β Fin β§ π
β Ring) β (πβ(1rβπΆ)) = (1rβπ)) |