Step | Hyp | Ref
| Expression |
1 | | ply1degltlss.2 |
. . 3
β’ (π β π
β Ring) |
2 | | ply1degltlss.p |
. . . 4
β’ π = (Poly1βπ
) |
3 | 2 | ply1sca 22145 |
. . 3
β’ (π
β Ring β π
= (Scalarβπ)) |
4 | 1, 3 | syl 17 |
. 2
β’ (π β π
= (Scalarβπ)) |
5 | | eqidd 2728 |
. 2
β’ (π β (Baseβπ
) = (Baseβπ
)) |
6 | | eqidd 2728 |
. 2
β’ (π β (Baseβπ) = (Baseβπ)) |
7 | | eqidd 2728 |
. 2
β’ (π β (+gβπ) = (+gβπ)) |
8 | | eqidd 2728 |
. 2
β’ (π β (
Β·π βπ) = ( Β·π
βπ)) |
9 | | eqidd 2728 |
. 2
β’ (π β (LSubSpβπ) = (LSubSpβπ)) |
10 | | ply1degltlss.1 |
. . . . 5
β’ π = (β‘π· β (-β[,)π)) |
11 | | cnvimass 6079 |
. . . . 5
β’ (β‘π· β (-β[,)π)) β dom π· |
12 | 10, 11 | eqsstri 4012 |
. . . 4
β’ π β dom π· |
13 | | ply1degltlss.d |
. . . . . 6
β’ π· = ( deg1
βπ
) |
14 | | eqid 2727 |
. . . . . 6
β’
(Baseβπ) =
(Baseβπ) |
15 | 13, 2, 14 | deg1xrf 25991 |
. . . . 5
β’ π·:(Baseβπ)βΆβ* |
16 | 15 | fdmi 6728 |
. . . 4
β’ dom π· = (Baseβπ) |
17 | 12, 16 | sseqtri 4014 |
. . 3
β’ π β (Baseβπ) |
18 | 17 | a1i 11 |
. 2
β’ (π β π β (Baseβπ)) |
19 | 15 | a1i 11 |
. . . . . 6
β’ (π β π·:(Baseβπ)βΆβ*) |
20 | 19 | ffnd 6717 |
. . . . 5
β’ (π β π· Fn (Baseβπ)) |
21 | 2 | ply1ring 22140 |
. . . . . 6
β’ (π
β Ring β π β Ring) |
22 | | eqid 2727 |
. . . . . . 7
β’
(0gβπ) = (0gβπ) |
23 | 14, 22 | ring0cl 20185 |
. . . . . 6
β’ (π β Ring β
(0gβπ)
β (Baseβπ)) |
24 | 1, 21, 23 | 3syl 18 |
. . . . 5
β’ (π β (0gβπ) β (Baseβπ)) |
25 | 13, 2, 22 | deg1z 25997 |
. . . . . . 7
β’ (π
β Ring β (π·β(0gβπ)) = -β) |
26 | 1, 25 | syl 17 |
. . . . . 6
β’ (π β (π·β(0gβπ)) = -β) |
27 | | mnfxr 11287 |
. . . . . . . 8
β’ -β
β β* |
28 | 27 | a1i 11 |
. . . . . . 7
β’ (π β -β β
β*) |
29 | | ply1degltlss.3 |
. . . . . . . . 9
β’ (π β π β
β0) |
30 | 29 | nn0red 12549 |
. . . . . . . 8
β’ (π β π β β) |
31 | 30 | rexrd 11280 |
. . . . . . 7
β’ (π β π β
β*) |
32 | 28 | xrleidd 13149 |
. . . . . . 7
β’ (π β -β β€
-β) |
33 | 30 | mnfltd 13122 |
. . . . . . 7
β’ (π β -β < π) |
34 | 28, 31, 28, 32, 33 | elicod 13392 |
. . . . . 6
β’ (π β -β β
(-β[,)π)) |
35 | 26, 34 | eqeltrd 2828 |
. . . . 5
β’ (π β (π·β(0gβπ)) β (-β[,)π)) |
36 | 20, 24, 35 | elpreimad 7062 |
. . . 4
β’ (π β (0gβπ) β (β‘π· β (-β[,)π))) |
37 | 36, 10 | eleqtrrdi 2839 |
. . 3
β’ (π β (0gβπ) β π) |
38 | 37 | ne0d 4331 |
. 2
β’ (π β π β β
) |
39 | | simpl 482 |
. . 3
β’ ((π β§ (π₯ β (Baseβπ
) β§ π β π β§ π β π)) β π) |
40 | | eqid 2727 |
. . . 4
β’
(+gβπ) = (+gβπ) |
41 | 2 | ply1lmod 22144 |
. . . . . . 7
β’ (π
β Ring β π β LMod) |
42 | 1, 41 | syl 17 |
. . . . . 6
β’ (π β π β LMod) |
43 | 42 | adantr 480 |
. . . . 5
β’ ((π β§ (π₯ β (Baseβπ
) β§ π β π β§ π β π)) β π β LMod) |
44 | 43 | lmodgrpd 20735 |
. . . 4
β’ ((π β§ (π₯ β (Baseβπ
) β§ π β π β§ π β π)) β π β Grp) |
45 | | simpr1 1192 |
. . . . . 6
β’ ((π β§ (π₯ β (Baseβπ
) β§ π β π β§ π β π)) β π₯ β (Baseβπ
)) |
46 | 4 | fveq2d 6895 |
. . . . . . 7
β’ (π β (Baseβπ
) =
(Baseβ(Scalarβπ))) |
47 | 46 | adantr 480 |
. . . . . 6
β’ ((π β§ (π₯ β (Baseβπ
) β§ π β π β§ π β π)) β (Baseβπ
) = (Baseβ(Scalarβπ))) |
48 | 45, 47 | eleqtrd 2830 |
. . . . 5
β’ ((π β§ (π₯ β (Baseβπ
) β§ π β π β§ π β π)) β π₯ β (Baseβ(Scalarβπ))) |
49 | | simpr2 1193 |
. . . . . 6
β’ ((π β§ (π₯ β (Baseβπ
) β§ π β π β§ π β π)) β π β π) |
50 | 17, 49 | sselid 3976 |
. . . . 5
β’ ((π β§ (π₯ β (Baseβπ
) β§ π β π β§ π β π)) β π β (Baseβπ)) |
51 | | eqid 2727 |
. . . . . 6
β’
(Scalarβπ) =
(Scalarβπ) |
52 | | eqid 2727 |
. . . . . 6
β’ (
Β·π βπ) = ( Β·π
βπ) |
53 | | eqid 2727 |
. . . . . 6
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
54 | 14, 51, 52, 53 | lmodvscl 20743 |
. . . . 5
β’ ((π β LMod β§ π₯ β
(Baseβ(Scalarβπ)) β§ π β (Baseβπ)) β (π₯( Β·π
βπ)π) β (Baseβπ)) |
55 | 43, 48, 50, 54 | syl3anc 1369 |
. . . 4
β’ ((π β§ (π₯ β (Baseβπ
) β§ π β π β§ π β π)) β (π₯( Β·π
βπ)π) β (Baseβπ)) |
56 | | simpr3 1194 |
. . . . 5
β’ ((π β§ (π₯ β (Baseβπ
) β§ π β π β§ π β π)) β π β π) |
57 | 17, 56 | sselid 3976 |
. . . 4
β’ ((π β§ (π₯ β (Baseβπ
) β§ π β π β§ π β π)) β π β (Baseβπ)) |
58 | 14, 40, 44, 55, 57 | grpcld 18889 |
. . 3
β’ ((π β§ (π₯ β (Baseβπ
) β§ π β π β§ π β π)) β ((π₯( Β·π
βπ)π)(+gβπ)π) β (Baseβπ)) |
59 | 1 | adantr 480 |
. . . 4
β’ ((π β§ (π₯ β (Baseβπ
) β§ π β π β§ π β π)) β π
β Ring) |
60 | | 1red 11231 |
. . . . . . 7
β’ (π β 1 β
β) |
61 | 30, 60 | resubcld 11658 |
. . . . . 6
β’ (π β (π β 1) β β) |
62 | 61 | rexrd 11280 |
. . . . 5
β’ (π β (π β 1) β
β*) |
63 | 62 | adantr 480 |
. . . 4
β’ ((π β§ (π₯ β (Baseβπ
) β§ π β π β§ π β π)) β (π β 1) β
β*) |
64 | 15 | a1i 11 |
. . . . . 6
β’ ((π β§ (π₯ β (Baseβπ
) β§ π β π β§ π β π)) β π·:(Baseβπ)βΆβ*) |
65 | 64, 55 | ffvelcdmd 7089 |
. . . . 5
β’ ((π β§ (π₯ β (Baseβπ
) β§ π β π β§ π β π)) β (π·β(π₯( Β·π
βπ)π)) β
β*) |
66 | 64, 50 | ffvelcdmd 7089 |
. . . . 5
β’ ((π β§ (π₯ β (Baseβπ
) β§ π β π β§ π β π)) β (π·βπ) β
β*) |
67 | | eqid 2727 |
. . . . . 6
β’
(Baseβπ
) =
(Baseβπ
) |
68 | 2, 13, 59, 14, 67, 52, 45, 50 | deg1vscale 26014 |
. . . . 5
β’ ((π β§ (π₯ β (Baseβπ
) β§ π β π β§ π β π)) β (π·β(π₯( Β·π
βπ)π)) β€ (π·βπ)) |
69 | 2, 13, 10, 29, 1, 14 | ply1degltel 33184 |
. . . . . . 7
β’ (π β (π β π β (π β (Baseβπ) β§ (π·βπ) β€ (π β 1)))) |
70 | 69 | simplbda 499 |
. . . . . 6
β’ ((π β§ π β π) β (π·βπ) β€ (π β 1)) |
71 | 49, 70 | syldan 590 |
. . . . 5
β’ ((π β§ (π₯ β (Baseβπ
) β§ π β π β§ π β π)) β (π·βπ) β€ (π β 1)) |
72 | 65, 66, 63, 68, 71 | xrletrd 13159 |
. . . 4
β’ ((π β§ (π₯ β (Baseβπ
) β§ π β π β§ π β π)) β (π·β(π₯( Β·π
βπ)π)) β€ (π β 1)) |
73 | 2, 13, 10, 29, 1, 14 | ply1degltel 33184 |
. . . . . 6
β’ (π β (π β π β (π β (Baseβπ) β§ (π·βπ) β€ (π β 1)))) |
74 | 73 | simplbda 499 |
. . . . 5
β’ ((π β§ π β π) β (π·βπ) β€ (π β 1)) |
75 | 56, 74 | syldan 590 |
. . . 4
β’ ((π β§ (π₯ β (Baseβπ
) β§ π β π β§ π β π)) β (π·βπ) β€ (π β 1)) |
76 | 2, 13, 59, 14, 40, 55, 57, 63, 72, 75 | deg1addle2 26012 |
. . 3
β’ ((π β§ (π₯ β (Baseβπ
) β§ π β π β§ π β π)) β (π·β((π₯( Β·π
βπ)π)(+gβπ)π)) β€ (π β 1)) |
77 | 2, 13, 10, 29, 1, 14 | ply1degltel 33184 |
. . . 4
β’ (π β (((π₯( Β·π
βπ)π)(+gβπ)π) β π β (((π₯( Β·π
βπ)π)(+gβπ)π) β (Baseβπ) β§ (π·β((π₯( Β·π
βπ)π)(+gβπ)π)) β€ (π β 1)))) |
78 | 77 | biimpar 477 |
. . 3
β’ ((π β§ (((π₯( Β·π
βπ)π)(+gβπ)π) β (Baseβπ) β§ (π·β((π₯( Β·π
βπ)π)(+gβπ)π)) β€ (π β 1))) β ((π₯( Β·π
βπ)π)(+gβπ)π) β π) |
79 | 39, 58, 76, 78 | syl12anc 836 |
. 2
β’ ((π β§ (π₯ β (Baseβπ
) β§ π β π β§ π β π)) β ((π₯( Β·π
βπ)π)(+gβπ)π) β π) |
80 | 4, 5, 6, 7, 8, 9, 18, 38, 79 | islssd 20801 |
1
β’ (π β π β (LSubSpβπ)) |