Step | Hyp | Ref
| Expression |
1 | | ply1degltlss.2 |
. . 3
⊢ (𝜑 → 𝑅 ∈ Ring) |
2 | | ply1degltlss.p |
. . . 4
⊢ 𝑃 = (Poly1‘𝑅) |
3 | 2 | ply1sca 22178 |
. . 3
⊢ (𝑅 ∈ Ring → 𝑅 = (Scalar‘𝑃)) |
4 | 1, 3 | syl 17 |
. 2
⊢ (𝜑 → 𝑅 = (Scalar‘𝑃)) |
5 | | eqidd 2729 |
. 2
⊢ (𝜑 → (Base‘𝑅) = (Base‘𝑅)) |
6 | | eqidd 2729 |
. 2
⊢ (𝜑 → (Base‘𝑃) = (Base‘𝑃)) |
7 | | eqidd 2729 |
. 2
⊢ (𝜑 → (+g‘𝑃) = (+g‘𝑃)) |
8 | | eqidd 2729 |
. 2
⊢ (𝜑 → (
·𝑠 ‘𝑃) = ( ·𝑠
‘𝑃)) |
9 | | eqidd 2729 |
. 2
⊢ (𝜑 → (LSubSp‘𝑃) = (LSubSp‘𝑃)) |
10 | | ply1degltlss.1 |
. . . . 5
⊢ 𝑆 = (◡𝐷 “ (-∞[,)𝑁)) |
11 | | cnvimass 6090 |
. . . . 5
⊢ (◡𝐷 “ (-∞[,)𝑁)) ⊆ dom 𝐷 |
12 | 10, 11 | eqsstri 4016 |
. . . 4
⊢ 𝑆 ⊆ dom 𝐷 |
13 | | ply1degltlss.d |
. . . . . 6
⊢ 𝐷 = ( deg1
‘𝑅) |
14 | | eqid 2728 |
. . . . . 6
⊢
(Base‘𝑃) =
(Base‘𝑃) |
15 | 13, 2, 14 | deg1xrf 26037 |
. . . . 5
⊢ 𝐷:(Base‘𝑃)⟶ℝ* |
16 | 15 | fdmi 6739 |
. . . 4
⊢ dom 𝐷 = (Base‘𝑃) |
17 | 12, 16 | sseqtri 4018 |
. . 3
⊢ 𝑆 ⊆ (Base‘𝑃) |
18 | 17 | a1i 11 |
. 2
⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑃)) |
19 | 15 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 𝐷:(Base‘𝑃)⟶ℝ*) |
20 | 19 | ffnd 6728 |
. . . . 5
⊢ (𝜑 → 𝐷 Fn (Base‘𝑃)) |
21 | 2 | ply1ring 22173 |
. . . . . 6
⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring) |
22 | | eqid 2728 |
. . . . . . 7
⊢
(0g‘𝑃) = (0g‘𝑃) |
23 | 14, 22 | ring0cl 20210 |
. . . . . 6
⊢ (𝑃 ∈ Ring →
(0g‘𝑃)
∈ (Base‘𝑃)) |
24 | 1, 21, 23 | 3syl 18 |
. . . . 5
⊢ (𝜑 → (0g‘𝑃) ∈ (Base‘𝑃)) |
25 | 13, 2, 22 | deg1z 26043 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → (𝐷‘(0g‘𝑃)) = -∞) |
26 | 1, 25 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝐷‘(0g‘𝑃)) = -∞) |
27 | | mnfxr 11309 |
. . . . . . . 8
⊢ -∞
∈ ℝ* |
28 | 27 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → -∞ ∈
ℝ*) |
29 | | ply1degltlss.3 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
30 | 29 | nn0red 12571 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ℝ) |
31 | 30 | rexrd 11302 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈
ℝ*) |
32 | 28 | xrleidd 13171 |
. . . . . . 7
⊢ (𝜑 → -∞ ≤
-∞) |
33 | 30 | mnfltd 13144 |
. . . . . . 7
⊢ (𝜑 → -∞ < 𝑁) |
34 | 28, 31, 28, 32, 33 | elicod 13414 |
. . . . . 6
⊢ (𝜑 → -∞ ∈
(-∞[,)𝑁)) |
35 | 26, 34 | eqeltrd 2829 |
. . . . 5
⊢ (𝜑 → (𝐷‘(0g‘𝑃)) ∈ (-∞[,)𝑁)) |
36 | 20, 24, 35 | elpreimad 7073 |
. . . 4
⊢ (𝜑 → (0g‘𝑃) ∈ (◡𝐷 “ (-∞[,)𝑁))) |
37 | 36, 10 | eleqtrrdi 2840 |
. . 3
⊢ (𝜑 → (0g‘𝑃) ∈ 𝑆) |
38 | 37 | ne0d 4339 |
. 2
⊢ (𝜑 → 𝑆 ≠ ∅) |
39 | | simpl 481 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆)) → 𝜑) |
40 | | eqid 2728 |
. . . 4
⊢
(+g‘𝑃) = (+g‘𝑃) |
41 | 2 | ply1lmod 22177 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → 𝑃 ∈ LMod) |
42 | 1, 41 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑃 ∈ LMod) |
43 | 42 | adantr 479 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆)) → 𝑃 ∈ LMod) |
44 | 43 | lmodgrpd 20760 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆)) → 𝑃 ∈ Grp) |
45 | | simpr1 1191 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆)) → 𝑥 ∈ (Base‘𝑅)) |
46 | 4 | fveq2d 6906 |
. . . . . . 7
⊢ (𝜑 → (Base‘𝑅) =
(Base‘(Scalar‘𝑃))) |
47 | 46 | adantr 479 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆)) → (Base‘𝑅) = (Base‘(Scalar‘𝑃))) |
48 | 45, 47 | eleqtrd 2831 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆)) → 𝑥 ∈ (Base‘(Scalar‘𝑃))) |
49 | | simpr2 1192 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆)) → 𝑎 ∈ 𝑆) |
50 | 17, 49 | sselid 3980 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆)) → 𝑎 ∈ (Base‘𝑃)) |
51 | | eqid 2728 |
. . . . . 6
⊢
(Scalar‘𝑃) =
(Scalar‘𝑃) |
52 | | eqid 2728 |
. . . . . 6
⊢ (
·𝑠 ‘𝑃) = ( ·𝑠
‘𝑃) |
53 | | eqid 2728 |
. . . . . 6
⊢
(Base‘(Scalar‘𝑃)) = (Base‘(Scalar‘𝑃)) |
54 | 14, 51, 52, 53 | lmodvscl 20768 |
. . . . 5
⊢ ((𝑃 ∈ LMod ∧ 𝑥 ∈
(Base‘(Scalar‘𝑃)) ∧ 𝑎 ∈ (Base‘𝑃)) → (𝑥( ·𝑠
‘𝑃)𝑎) ∈ (Base‘𝑃)) |
55 | 43, 48, 50, 54 | syl3anc 1368 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆)) → (𝑥( ·𝑠
‘𝑃)𝑎) ∈ (Base‘𝑃)) |
56 | | simpr3 1193 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆)) → 𝑏 ∈ 𝑆) |
57 | 17, 56 | sselid 3980 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆)) → 𝑏 ∈ (Base‘𝑃)) |
58 | 14, 40, 44, 55, 57 | grpcld 18911 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆)) → ((𝑥( ·𝑠
‘𝑃)𝑎)(+g‘𝑃)𝑏) ∈ (Base‘𝑃)) |
59 | 1 | adantr 479 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆)) → 𝑅 ∈ Ring) |
60 | | 1red 11253 |
. . . . . . 7
⊢ (𝜑 → 1 ∈
ℝ) |
61 | 30, 60 | resubcld 11680 |
. . . . . 6
⊢ (𝜑 → (𝑁 − 1) ∈ ℝ) |
62 | 61 | rexrd 11302 |
. . . . 5
⊢ (𝜑 → (𝑁 − 1) ∈
ℝ*) |
63 | 62 | adantr 479 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆)) → (𝑁 − 1) ∈
ℝ*) |
64 | 15 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆)) → 𝐷:(Base‘𝑃)⟶ℝ*) |
65 | 64, 55 | ffvelcdmd 7100 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆)) → (𝐷‘(𝑥( ·𝑠
‘𝑃)𝑎)) ∈
ℝ*) |
66 | 64, 50 | ffvelcdmd 7100 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆)) → (𝐷‘𝑎) ∈
ℝ*) |
67 | | eqid 2728 |
. . . . . 6
⊢
(Base‘𝑅) =
(Base‘𝑅) |
68 | 2, 13, 59, 14, 67, 52, 45, 50 | deg1vscale 26060 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆)) → (𝐷‘(𝑥( ·𝑠
‘𝑃)𝑎)) ≤ (𝐷‘𝑎)) |
69 | 2, 13, 10, 29, 1, 14 | ply1degltel 33298 |
. . . . . . 7
⊢ (𝜑 → (𝑎 ∈ 𝑆 ↔ (𝑎 ∈ (Base‘𝑃) ∧ (𝐷‘𝑎) ≤ (𝑁 − 1)))) |
70 | 69 | simplbda 498 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝐷‘𝑎) ≤ (𝑁 − 1)) |
71 | 49, 70 | syldan 589 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆)) → (𝐷‘𝑎) ≤ (𝑁 − 1)) |
72 | 65, 66, 63, 68, 71 | xrletrd 13181 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆)) → (𝐷‘(𝑥( ·𝑠
‘𝑃)𝑎)) ≤ (𝑁 − 1)) |
73 | 2, 13, 10, 29, 1, 14 | ply1degltel 33298 |
. . . . . 6
⊢ (𝜑 → (𝑏 ∈ 𝑆 ↔ (𝑏 ∈ (Base‘𝑃) ∧ (𝐷‘𝑏) ≤ (𝑁 − 1)))) |
74 | 73 | simplbda 498 |
. . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ 𝑆) → (𝐷‘𝑏) ≤ (𝑁 − 1)) |
75 | 56, 74 | syldan 589 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆)) → (𝐷‘𝑏) ≤ (𝑁 − 1)) |
76 | 2, 13, 59, 14, 40, 55, 57, 63, 72, 75 | deg1addle2 26058 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆)) → (𝐷‘((𝑥( ·𝑠
‘𝑃)𝑎)(+g‘𝑃)𝑏)) ≤ (𝑁 − 1)) |
77 | 2, 13, 10, 29, 1, 14 | ply1degltel 33298 |
. . . 4
⊢ (𝜑 → (((𝑥( ·𝑠
‘𝑃)𝑎)(+g‘𝑃)𝑏) ∈ 𝑆 ↔ (((𝑥( ·𝑠
‘𝑃)𝑎)(+g‘𝑃)𝑏) ∈ (Base‘𝑃) ∧ (𝐷‘((𝑥( ·𝑠
‘𝑃)𝑎)(+g‘𝑃)𝑏)) ≤ (𝑁 − 1)))) |
78 | 77 | biimpar 476 |
. . 3
⊢ ((𝜑 ∧ (((𝑥( ·𝑠
‘𝑃)𝑎)(+g‘𝑃)𝑏) ∈ (Base‘𝑃) ∧ (𝐷‘((𝑥( ·𝑠
‘𝑃)𝑎)(+g‘𝑃)𝑏)) ≤ (𝑁 − 1))) → ((𝑥( ·𝑠
‘𝑃)𝑎)(+g‘𝑃)𝑏) ∈ 𝑆) |
79 | 39, 58, 76, 78 | syl12anc 835 |
. 2
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆)) → ((𝑥( ·𝑠
‘𝑃)𝑎)(+g‘𝑃)𝑏) ∈ 𝑆) |
80 | 4, 5, 6, 7, 8, 9, 18, 38, 79 | islssd 20826 |
1
⊢ (𝜑 → 𝑆 ∈ (LSubSp‘𝑃)) |