Step | Hyp | Ref
| Expression |
1 | | ply1degltdim.p |
. . . . 5
⊢ 𝑃 = (Poly1‘𝑅) |
2 | | ply1degltdim.r |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ DivRing) |
3 | 1, 2 | ply1lvec 33072 |
. . . 4
⊢ (𝜑 → 𝑃 ∈ LVec) |
4 | | ply1degltdim.d |
. . . . 5
⊢ 𝐷 = ( deg1
‘𝑅) |
5 | | ply1degltdim.s |
. . . . 5
⊢ 𝑆 = (◡𝐷 “ (-∞[,)𝑁)) |
6 | | ply1degltdim.n |
. . . . 5
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
7 | 2 | drngringd 20584 |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ Ring) |
8 | 1, 4, 5, 6, 7 | ply1degltlss 33099 |
. . . 4
⊢ (𝜑 → 𝑆 ∈ (LSubSp‘𝑃)) |
9 | | ply1degltdim.e |
. . . . 5
⊢ 𝐸 = (𝑃 ↾s 𝑆) |
10 | | eqid 2724 |
. . . . 5
⊢
(LSubSp‘𝑃) =
(LSubSp‘𝑃) |
11 | 9, 10 | lsslvec 20946 |
. . . 4
⊢ ((𝑃 ∈ LVec ∧ 𝑆 ∈ (LSubSp‘𝑃)) → 𝐸 ∈ LVec) |
12 | 3, 8, 11 | syl2anc 583 |
. . 3
⊢ (𝜑 → 𝐸 ∈ LVec) |
13 | | oveq1 7408 |
. . . . 5
⊢ (𝑘 = 𝑛 → (𝑘(.g‘(mulGrp‘𝑃))(var1‘𝑅)) = (𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅))) |
14 | 13 | cbvmptv 5251 |
. . . 4
⊢ (𝑘 ∈ (0..^𝑁) ↦ (𝑘(.g‘(mulGrp‘𝑃))(var1‘𝑅))) = (𝑛 ∈ (0..^𝑁) ↦ (𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅))) |
15 | 1, 4, 5, 6, 2, 9, 14 | ply1degltdimlem 33152 |
. . 3
⊢ (𝜑 → ran (𝑘 ∈ (0..^𝑁) ↦ (𝑘(.g‘(mulGrp‘𝑃))(var1‘𝑅))) ∈ (LBasis‘𝐸)) |
16 | | eqid 2724 |
. . . . . . . . . . . . 13
⊢
(Base‘𝑃) =
(Base‘𝑃) |
17 | 4, 1, 16 | deg1xrf 25938 |
. . . . . . . . . . . 12
⊢ 𝐷:(Base‘𝑃)⟶ℝ* |
18 | | ffn 6707 |
. . . . . . . . . . . 12
⊢ (𝐷:(Base‘𝑃)⟶ℝ* → 𝐷 Fn (Base‘𝑃)) |
19 | 17, 18 | mp1i 13 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → 𝐷 Fn (Base‘𝑃)) |
20 | | eqid 2724 |
. . . . . . . . . . . . 13
⊢
(mulGrp‘𝑃) =
(mulGrp‘𝑃) |
21 | 20, 16 | mgpbas 20034 |
. . . . . . . . . . . 12
⊢
(Base‘𝑃) =
(Base‘(mulGrp‘𝑃)) |
22 | | eqid 2724 |
. . . . . . . . . . . 12
⊢
(.g‘(mulGrp‘𝑃)) =
(.g‘(mulGrp‘𝑃)) |
23 | 1 | ply1ring 22088 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring) |
24 | 20 | ringmgp 20133 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ Ring →
(mulGrp‘𝑃) ∈
Mnd) |
25 | 7, 23, 24 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (mulGrp‘𝑃) ∈ Mnd) |
26 | 25 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (mulGrp‘𝑃) ∈ Mnd) |
27 | | elfzonn0 13673 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ (0..^𝑁) → 𝑛 ∈ ℕ0) |
28 | 27 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → 𝑛 ∈ ℕ0) |
29 | | eqid 2724 |
. . . . . . . . . . . . . . 15
⊢
(var1‘𝑅) = (var1‘𝑅) |
30 | 29, 1, 16 | vr1cl 22058 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ∈ Ring →
(var1‘𝑅)
∈ (Base‘𝑃)) |
31 | 7, 30 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
(var1‘𝑅)
∈ (Base‘𝑃)) |
32 | 31 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (var1‘𝑅) ∈ (Base‘𝑃)) |
33 | 21, 22, 26, 28, 32 | mulgnn0cld 19011 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅)) ∈ (Base‘𝑃)) |
34 | | mnfxr 11267 |
. . . . . . . . . . . . 13
⊢ -∞
∈ ℝ* |
35 | 34 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → -∞ ∈
ℝ*) |
36 | 6 | nn0red 12529 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈ ℝ) |
37 | 36 | rexrd 11260 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈
ℝ*) |
38 | 37 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → 𝑁 ∈
ℝ*) |
39 | 4, 1, 16 | deg1xrcl 25939 |
. . . . . . . . . . . . 13
⊢ ((𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅)) ∈ (Base‘𝑃) → (𝐷‘(𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅))) ∈
ℝ*) |
40 | 33, 39 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (𝐷‘(𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅))) ∈
ℝ*) |
41 | 40 | mnfled 13111 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → -∞ ≤ (𝐷‘(𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) |
42 | 27 | nn0red 12529 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ (0..^𝑁) → 𝑛 ∈ ℝ) |
43 | 42 | rexrd 11260 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ (0..^𝑁) → 𝑛 ∈ ℝ*) |
44 | 43 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → 𝑛 ∈ ℝ*) |
45 | 4, 1, 29, 20, 22 | deg1pwle 25976 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ Ring ∧ 𝑛 ∈ ℕ0)
→ (𝐷‘(𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅))) ≤ 𝑛) |
46 | 7, 27, 45 | syl2an 595 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (𝐷‘(𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅))) ≤ 𝑛) |
47 | | elfzolt2 13637 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ (0..^𝑁) → 𝑛 < 𝑁) |
48 | 47 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → 𝑛 < 𝑁) |
49 | 40, 44, 38, 46, 48 | xrlelttrd 13135 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (𝐷‘(𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅))) < 𝑁) |
50 | 35, 38, 40, 41, 49 | elicod 13370 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (𝐷‘(𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅))) ∈ (-∞[,)𝑁)) |
51 | 19, 33, 50 | elpreimad 7050 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅)) ∈ (◡𝐷 “ (-∞[,)𝑁))) |
52 | 51, 5 | eleqtrrdi 2836 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅)) ∈ 𝑆) |
53 | 16, 10 | lssss 20772 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ (LSubSp‘𝑃) → 𝑆 ⊆ (Base‘𝑃)) |
54 | 9, 16 | ressbas2 17180 |
. . . . . . . . . . 11
⊢ (𝑆 ⊆ (Base‘𝑃) → 𝑆 = (Base‘𝐸)) |
55 | 8, 53, 54 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 = (Base‘𝐸)) |
56 | 55 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → 𝑆 = (Base‘𝐸)) |
57 | 52, 56 | eleqtrd 2827 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅)) ∈ (Base‘𝐸)) |
58 | 57, 14 | fmptd 7105 |
. . . . . . 7
⊢ (𝜑 → (𝑘 ∈ (0..^𝑁) ↦ (𝑘(.g‘(mulGrp‘𝑃))(var1‘𝑅))):(0..^𝑁)⟶(Base‘𝐸)) |
59 | 58 | ffnd 6708 |
. . . . . 6
⊢ (𝜑 → (𝑘 ∈ (0..^𝑁) ↦ (𝑘(.g‘(mulGrp‘𝑃))(var1‘𝑅))) Fn (0..^𝑁)) |
60 | | hashfn 14331 |
. . . . . 6
⊢ ((𝑘 ∈ (0..^𝑁) ↦ (𝑘(.g‘(mulGrp‘𝑃))(var1‘𝑅))) Fn (0..^𝑁) → (♯‘(𝑘 ∈ (0..^𝑁) ↦ (𝑘(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) = (♯‘(0..^𝑁))) |
61 | 59, 60 | syl 17 |
. . . . 5
⊢ (𝜑 → (♯‘(𝑘 ∈ (0..^𝑁) ↦ (𝑘(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) = (♯‘(0..^𝑁))) |
62 | | ovexd 7436 |
. . . . . 6
⊢ (𝜑 → (0..^𝑁) ∈ V) |
63 | 57 | ralrimiva 3138 |
. . . . . . 7
⊢ (𝜑 → ∀𝑛 ∈ (0..^𝑁)(𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅)) ∈ (Base‘𝐸)) |
64 | | drngnzr 20596 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ NzRing) |
65 | 2, 64 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑅 ∈ NzRing) |
66 | 65 | ad2antrr 723 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑅 ∈ NzRing) |
67 | 28 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑛 ∈ ℕ0) |
68 | | elfzonn0 13673 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ (0..^𝑁) → 𝑖 ∈ ℕ0) |
69 | 68 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑖 ∈ ℕ0) |
70 | 1, 29, 22, 66, 67, 69 | ply1moneq 33096 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅)) = (𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅)) ↔ 𝑛 = 𝑖)) |
71 | 70 | biimpd 228 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅)) = (𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅)) → 𝑛 = 𝑖)) |
72 | 71 | anasss 466 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ (0..^𝑁) ∧ 𝑖 ∈ (0..^𝑁))) → ((𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅)) = (𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅)) → 𝑛 = 𝑖)) |
73 | 72 | ralrimivva 3192 |
. . . . . . 7
⊢ (𝜑 → ∀𝑛 ∈ (0..^𝑁)∀𝑖 ∈ (0..^𝑁)((𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅)) = (𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅)) → 𝑛 = 𝑖)) |
74 | | oveq1 7408 |
. . . . . . . 8
⊢ (𝑛 = 𝑖 → (𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅)) = (𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅))) |
75 | 14, 74 | f1mpt 7252 |
. . . . . . 7
⊢ ((𝑘 ∈ (0..^𝑁) ↦ (𝑘(.g‘(mulGrp‘𝑃))(var1‘𝑅))):(0..^𝑁)–1-1→(Base‘𝐸) ↔ (∀𝑛 ∈ (0..^𝑁)(𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅)) ∈ (Base‘𝐸) ∧ ∀𝑛 ∈ (0..^𝑁)∀𝑖 ∈ (0..^𝑁)((𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅)) = (𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅)) → 𝑛 = 𝑖))) |
76 | 63, 73, 75 | sylanbrc 582 |
. . . . . 6
⊢ (𝜑 → (𝑘 ∈ (0..^𝑁) ↦ (𝑘(.g‘(mulGrp‘𝑃))(var1‘𝑅))):(0..^𝑁)–1-1→(Base‘𝐸)) |
77 | | hashf1rn 14308 |
. . . . . 6
⊢
(((0..^𝑁) ∈ V
∧ (𝑘 ∈ (0..^𝑁) ↦ (𝑘(.g‘(mulGrp‘𝑃))(var1‘𝑅))):(0..^𝑁)–1-1→(Base‘𝐸)) → (♯‘(𝑘 ∈ (0..^𝑁) ↦ (𝑘(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) = (♯‘ran (𝑘 ∈ (0..^𝑁) ↦ (𝑘(.g‘(mulGrp‘𝑃))(var1‘𝑅))))) |
78 | 62, 76, 77 | syl2anc 583 |
. . . . 5
⊢ (𝜑 → (♯‘(𝑘 ∈ (0..^𝑁) ↦ (𝑘(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) = (♯‘ran (𝑘 ∈ (0..^𝑁) ↦ (𝑘(.g‘(mulGrp‘𝑃))(var1‘𝑅))))) |
79 | | hashfzo0 14386 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ (♯‘(0..^𝑁)) = 𝑁) |
80 | 6, 79 | syl 17 |
. . . . 5
⊢ (𝜑 → (♯‘(0..^𝑁)) = 𝑁) |
81 | 61, 78, 80 | 3eqtr3d 2772 |
. . . 4
⊢ (𝜑 → (♯‘ran (𝑘 ∈ (0..^𝑁) ↦ (𝑘(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) = 𝑁) |
82 | | hashvnfin 14316 |
. . . . 5
⊢ ((ran
(𝑘 ∈ (0..^𝑁) ↦ (𝑘(.g‘(mulGrp‘𝑃))(var1‘𝑅))) ∈ (LBasis‘𝐸) ∧ 𝑁 ∈ ℕ0) →
((♯‘ran (𝑘
∈ (0..^𝑁) ↦
(𝑘(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) = 𝑁 → ran (𝑘 ∈ (0..^𝑁) ↦ (𝑘(.g‘(mulGrp‘𝑃))(var1‘𝑅))) ∈
Fin)) |
83 | 82 | imp 406 |
. . . 4
⊢ (((ran
(𝑘 ∈ (0..^𝑁) ↦ (𝑘(.g‘(mulGrp‘𝑃))(var1‘𝑅))) ∈ (LBasis‘𝐸) ∧ 𝑁 ∈ ℕ0) ∧
(♯‘ran (𝑘
∈ (0..^𝑁) ↦
(𝑘(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) = 𝑁) → ran (𝑘 ∈ (0..^𝑁) ↦ (𝑘(.g‘(mulGrp‘𝑃))(var1‘𝑅))) ∈ Fin) |
84 | 15, 6, 81, 83 | syl21anc 835 |
. . 3
⊢ (𝜑 → ran (𝑘 ∈ (0..^𝑁) ↦ (𝑘(.g‘(mulGrp‘𝑃))(var1‘𝑅))) ∈ Fin) |
85 | | eqid 2724 |
. . . 4
⊢
(LBasis‘𝐸) =
(LBasis‘𝐸) |
86 | 85 | dimvalfi 33131 |
. . 3
⊢ ((𝐸 ∈ LVec ∧ ran (𝑘 ∈ (0..^𝑁) ↦ (𝑘(.g‘(mulGrp‘𝑃))(var1‘𝑅))) ∈ (LBasis‘𝐸) ∧ ran (𝑘 ∈ (0..^𝑁) ↦ (𝑘(.g‘(mulGrp‘𝑃))(var1‘𝑅))) ∈ Fin) →
(dim‘𝐸) =
(♯‘ran (𝑘
∈ (0..^𝑁) ↦
(𝑘(.g‘(mulGrp‘𝑃))(var1‘𝑅))))) |
87 | 12, 15, 84, 86 | syl3anc 1368 |
. 2
⊢ (𝜑 → (dim‘𝐸) = (♯‘ran (𝑘 ∈ (0..^𝑁) ↦ (𝑘(.g‘(mulGrp‘𝑃))(var1‘𝑅))))) |
88 | 87, 81 | eqtrd 2764 |
1
⊢ (𝜑 → (dim‘𝐸) = 𝑁) |