Proof of Theorem idomrootle
Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. . 3
⊢
(Poly1‘𝑅) = (Poly1‘𝑅) |
2 | | eqid 2610 |
. . 3
⊢
(Base‘(Poly1‘𝑅)) =
(Base‘(Poly1‘𝑅)) |
3 | | eqid 2610 |
. . 3
⊢ (
deg1 ‘𝑅) =
( deg1 ‘𝑅) |
4 | | eqid 2610 |
. . 3
⊢
(eval1‘𝑅) = (eval1‘𝑅) |
5 | | eqid 2610 |
. . 3
⊢
(0g‘𝑅) = (0g‘𝑅) |
6 | | eqid 2610 |
. . 3
⊢
(0g‘(Poly1‘𝑅)) =
(0g‘(Poly1‘𝑅)) |
7 | | simp1 1054 |
. . 3
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) → 𝑅 ∈ IDomn) |
8 | | isidom 19125 |
. . . . . . . . 9
⊢ (𝑅 ∈ IDomn ↔ (𝑅 ∈ CRing ∧ 𝑅 ∈ Domn)) |
9 | 8 | simplbi 475 |
. . . . . . . 8
⊢ (𝑅 ∈ IDomn → 𝑅 ∈ CRing) |
10 | 7, 9 | syl 17 |
. . . . . . 7
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) → 𝑅 ∈ CRing) |
11 | | crngring 18381 |
. . . . . . 7
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
12 | 10, 11 | syl 17 |
. . . . . 6
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) → 𝑅 ∈ Ring) |
13 | 1 | ply1ring 19439 |
. . . . . 6
⊢ (𝑅 ∈ Ring →
(Poly1‘𝑅)
∈ Ring) |
14 | 12, 13 | syl 17 |
. . . . 5
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) →
(Poly1‘𝑅)
∈ Ring) |
15 | | ringgrp 18375 |
. . . . 5
⊢
((Poly1‘𝑅) ∈ Ring →
(Poly1‘𝑅)
∈ Grp) |
16 | 14, 15 | syl 17 |
. . . 4
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) →
(Poly1‘𝑅)
∈ Grp) |
17 | | eqid 2610 |
. . . . . . . 8
⊢
(mulGrp‘(Poly1‘𝑅)) =
(mulGrp‘(Poly1‘𝑅)) |
18 | 17 | ringmgp 18376 |
. . . . . . 7
⊢
((Poly1‘𝑅) ∈ Ring →
(mulGrp‘(Poly1‘𝑅)) ∈ Mnd) |
19 | 14, 18 | syl 17 |
. . . . . 6
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) →
(mulGrp‘(Poly1‘𝑅)) ∈ Mnd) |
20 | | mndmgm 17123 |
. . . . . 6
⊢
((mulGrp‘(Poly1‘𝑅)) ∈ Mnd →
(mulGrp‘(Poly1‘𝑅)) ∈ Mgm) |
21 | 19, 20 | syl 17 |
. . . . 5
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) →
(mulGrp‘(Poly1‘𝑅)) ∈ Mgm) |
22 | | simp3 1056 |
. . . . 5
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ ℕ) |
23 | | eqid 2610 |
. . . . . . 7
⊢
(var1‘𝑅) = (var1‘𝑅) |
24 | 23, 1, 2 | vr1cl 19408 |
. . . . . 6
⊢ (𝑅 ∈ Ring →
(var1‘𝑅)
∈ (Base‘(Poly1‘𝑅))) |
25 | 12, 24 | syl 17 |
. . . . 5
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) →
(var1‘𝑅)
∈ (Base‘(Poly1‘𝑅))) |
26 | 17, 2 | mgpbas 18318 |
. . . . . 6
⊢
(Base‘(Poly1‘𝑅)) =
(Base‘(mulGrp‘(Poly1‘𝑅))) |
27 | | eqid 2610 |
. . . . . 6
⊢
(.g‘(mulGrp‘(Poly1‘𝑅))) =
(.g‘(mulGrp‘(Poly1‘𝑅))) |
28 | 26, 27 | mulgnncl 17379 |
. . . . 5
⊢
(((mulGrp‘(Poly1‘𝑅)) ∈ Mgm ∧ 𝑁 ∈ ℕ ∧
(var1‘𝑅)
∈ (Base‘(Poly1‘𝑅))) → (𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅)) ∈ (Base‘(Poly1‘𝑅))) |
29 | 21, 22, 25, 28 | syl3anc 1318 |
. . . 4
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) → (𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅)) ∈ (Base‘(Poly1‘𝑅))) |
30 | | eqid 2610 |
. . . . . . 7
⊢
(algSc‘(Poly1‘𝑅)) =
(algSc‘(Poly1‘𝑅)) |
31 | | idomrootle.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑅) |
32 | 1, 30, 31, 2 | ply1sclf 19476 |
. . . . . 6
⊢ (𝑅 ∈ Ring →
(algSc‘(Poly1‘𝑅)):𝐵⟶(Base‘(Poly1‘𝑅))) |
33 | 12, 32 | syl 17 |
. . . . 5
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) →
(algSc‘(Poly1‘𝑅)):𝐵⟶(Base‘(Poly1‘𝑅))) |
34 | | simp2 1055 |
. . . . 5
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) → 𝑋 ∈ 𝐵) |
35 | 33, 34 | ffvelrnd 6268 |
. . . 4
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) →
((algSc‘(Poly1‘𝑅))‘𝑋) ∈
(Base‘(Poly1‘𝑅))) |
36 | | eqid 2610 |
. . . . 5
⊢
(-g‘(Poly1‘𝑅)) =
(-g‘(Poly1‘𝑅)) |
37 | 2, 36 | grpsubcl 17318 |
. . . 4
⊢
(((Poly1‘𝑅) ∈ Grp ∧ (𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅)) ∈ (Base‘(Poly1‘𝑅)) ∧ ((algSc‘(Poly1‘𝑅))‘𝑋)
∈ (Base‘(Poly1‘𝑅)))
→ ((𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅))(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑋))
∈ (Base‘(Poly1‘𝑅))) |
38 | 16, 29, 35, 37 | syl3anc 1318 |
. . 3
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) → ((𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅))(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑋))
∈ (Base‘(Poly1‘𝑅))) |
39 | 3, 1, 2 | deg1xrcl 23646 |
. . . . . . . . . 10
⊢
(((algSc‘(Poly1‘𝑅))‘𝑋) ∈
(Base‘(Poly1‘𝑅)) → (( deg1 ‘𝑅)‘((algSc‘(Poly1‘𝑅))‘𝑋)) ∈ ℝ*) |
40 | 35, 39 | syl 17 |
. . . . . . . . 9
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) → (( deg1
‘𝑅)‘((algSc‘(Poly1‘𝑅))‘𝑋)) ∈ ℝ*) |
41 | | 0xr 9965 |
. . . . . . . . . 10
⊢ 0 ∈
ℝ* |
42 | 41 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) → 0 ∈
ℝ*) |
43 | | nnre 10904 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
44 | 43 | rexrd 9968 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ*) |
45 | 44 | 3ad2ant3 1077 |
. . . . . . . . 9
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℝ*) |
46 | 3, 1, 31, 30 | deg1sclle 23676 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → (( deg1 ‘𝑅)‘((algSc‘(Poly1‘𝑅))‘𝑋)) ≤ 0) |
47 | 12, 34, 46 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) → (( deg1
‘𝑅)‘((algSc‘(Poly1‘𝑅))‘𝑋)) ≤ 0) |
48 | | nngt0 10926 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → 0 <
𝑁) |
49 | 48 | 3ad2ant3 1077 |
. . . . . . . . 9
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) → 0 < 𝑁) |
50 | 40, 42, 45, 47, 49 | xrlelttrd 11867 |
. . . . . . . 8
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) → (( deg1
‘𝑅)‘((algSc‘(Poly1‘𝑅))‘𝑋)) < 𝑁) |
51 | 8 | simprbi 479 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ IDomn → 𝑅 ∈ Domn) |
52 | | domnnzr 19116 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ Domn → 𝑅 ∈ NzRing) |
53 | 51, 52 | syl 17 |
. . . . . . . . . 10
⊢ (𝑅 ∈ IDomn → 𝑅 ∈ NzRing) |
54 | 7, 53 | syl 17 |
. . . . . . . . 9
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) → 𝑅 ∈ NzRing) |
55 | | nnnn0 11176 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
56 | 55 | 3ad2ant3 1077 |
. . . . . . . . 9
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℕ0) |
57 | 3, 1, 23, 17, 27 | deg1pw 23684 |
. . . . . . . . 9
⊢ ((𝑅 ∈ NzRing ∧ 𝑁 ∈ ℕ0)
→ (( deg1 ‘𝑅)‘(𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅))) = 𝑁) |
58 | 54, 56, 57 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) → (( deg1
‘𝑅)‘(𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅))) = 𝑁) |
59 | 50, 58 | breqtrrd 4611 |
. . . . . . 7
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) → (( deg1
‘𝑅)‘((algSc‘(Poly1‘𝑅))‘𝑋)) < (( deg1 ‘𝑅)‘(𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅)))) |
60 | 1, 3, 12, 2, 36, 29, 35, 59 | deg1sub 23672 |
. . . . . 6
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) → (( deg1
‘𝑅)‘((𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅))(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑋))) = (( deg1 ‘𝑅)‘(𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅)))) |
61 | 60, 58 | eqtrd 2644 |
. . . . 5
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) → (( deg1
‘𝑅)‘((𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅))(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑋))) = 𝑁) |
62 | 61, 56 | eqeltrd 2688 |
. . . 4
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) → (( deg1
‘𝑅)‘((𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅))(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑋))) ∈ ℕ0) |
63 | 3, 1, 6, 2 | deg1nn0clb 23654 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ ((𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅))(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑋))
∈ (Base‘(Poly1‘𝑅)))
→ (((𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅))(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑋))
≠ (0g‘(Poly1‘𝑅)) ↔ (( deg1 ‘𝑅)‘((𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅))(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑋))) ∈ ℕ0)) |
64 | 12, 38, 63 | syl2anc 691 |
. . . 4
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) → (((𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅))(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑋))
≠ (0g‘(Poly1‘𝑅)) ↔ (( deg1 ‘𝑅)‘((𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅))(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑋))) ∈ ℕ0)) |
65 | 62, 64 | mpbird 246 |
. . 3
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) → ((𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅))(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑋))
≠ (0g‘(Poly1‘𝑅))) |
66 | 1, 2, 3, 4, 5, 6, 7, 38, 65 | fta1g 23731 |
. 2
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) → (#‘(◡((eval1‘𝑅)‘((𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅))(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑋))) “ {(0g‘𝑅)})) ≤ (( deg1 ‘𝑅)‘((𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅))(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑋)))) |
67 | | eqid 2610 |
. . . . . . 7
⊢ (𝑅 ↑s 𝐵) = (𝑅 ↑s 𝐵) |
68 | | eqid 2610 |
. . . . . . 7
⊢
(Base‘(𝑅
↑s 𝐵)) = (Base‘(𝑅 ↑s 𝐵)) |
69 | | fvex 6113 |
. . . . . . . . 9
⊢
(Base‘𝑅)
∈ V |
70 | 31, 69 | eqeltri 2684 |
. . . . . . . 8
⊢ 𝐵 ∈ V |
71 | 70 | a1i 11 |
. . . . . . 7
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) → 𝐵 ∈ V) |
72 | 4, 1, 67, 31 | evl1rhm 19517 |
. . . . . . . . . 10
⊢ (𝑅 ∈ CRing →
(eval1‘𝑅)
∈ ((Poly1‘𝑅) RingHom (𝑅 ↑s 𝐵))) |
73 | 10, 72 | syl 17 |
. . . . . . . . 9
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) →
(eval1‘𝑅)
∈ ((Poly1‘𝑅) RingHom (𝑅 ↑s 𝐵))) |
74 | 2, 68 | rhmf 18549 |
. . . . . . . . 9
⊢
((eval1‘𝑅) ∈ ((Poly1‘𝑅) RingHom (𝑅 ↑s 𝐵)) → (eval1‘𝑅):(Base‘(Poly1‘𝑅))⟶(Base‘(𝑅 ↑s 𝐵))) |
75 | 73, 74 | syl 17 |
. . . . . . . 8
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) →
(eval1‘𝑅):(Base‘(Poly1‘𝑅))⟶(Base‘(𝑅 ↑s 𝐵))) |
76 | 75, 38 | ffvelrnd 6268 |
. . . . . . 7
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) →
((eval1‘𝑅)‘((𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅))(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑋))) ∈ (Base‘(𝑅 ↑s 𝐵))) |
77 | 67, 31, 68, 7, 71, 76 | pwselbas 15972 |
. . . . . 6
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) →
((eval1‘𝑅)‘((𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅))(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑋))):𝐵⟶𝐵) |
78 | | ffn 5958 |
. . . . . 6
⊢
(((eval1‘𝑅)‘((𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅))(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑋))):𝐵⟶𝐵
→ ((eval1‘𝑅)‘((𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅))(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑋))) Fn 𝐵) |
79 | 77, 78 | syl 17 |
. . . . 5
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) →
((eval1‘𝑅)‘((𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅))(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑋))) Fn 𝐵) |
80 | | fniniseg2 6248 |
. . . . 5
⊢
(((eval1‘𝑅)‘((𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅))(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑋))) Fn 𝐵
→ (◡((eval1‘𝑅)‘((𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅))(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑋))) “ {(0g‘𝑅)}) = {𝑦
∈ 𝐵 ∣
(((eval1‘𝑅)‘((𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅))(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑋)))‘𝑦)
= (0g‘𝑅)}) |
81 | 79, 80 | syl 17 |
. . . 4
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) → (◡((eval1‘𝑅)‘((𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅))(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑋))) “ {(0g‘𝑅)}) = {𝑦
∈ 𝐵 ∣
(((eval1‘𝑅)‘((𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅))(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑋)))‘𝑦)
= (0g‘𝑅)}) |
82 | 10 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → 𝑅 ∈ CRing) |
83 | | simpr 476 |
. . . . . . . . 9
⊢ (((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ 𝐵) |
84 | 4, 23, 31, 1, 2, 82, 83 | evl1vard 19522 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → ((var1‘𝑅) ∈
(Base‘(Poly1‘𝑅)) ∧ (((eval1‘𝑅)‘(var1‘𝑅))‘𝑦) = 𝑦)) |
85 | | idomrootle.e |
. . . . . . . . . 10
⊢ ↑ =
(.g‘(mulGrp‘𝑅)) |
86 | | simpl3 1059 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → 𝑁 ∈ ℕ) |
87 | 86, 55 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → 𝑁 ∈
ℕ0) |
88 | 4, 1, 31, 2, 82, 83, 84, 27, 85, 87 | evl1expd 19530 |
. . . . . . . . 9
⊢ (((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → ((𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅)) ∈ (Base‘(Poly1‘𝑅)) ∧ (((eval1‘𝑅)‘(𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅)))‘𝑦)
= (𝑁 ↑ 𝑦))) |
89 | | simpl2 1058 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → 𝑋 ∈ 𝐵) |
90 | 4, 1, 31, 30, 2, 82, 89, 83 | evl1scad 19520 |
. . . . . . . . 9
⊢ (((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) →
(((algSc‘(Poly1‘𝑅))‘𝑋) ∈
(Base‘(Poly1‘𝑅)) ∧ (((eval1‘𝑅)‘((algSc‘(Poly1‘𝑅))‘𝑋))‘𝑦) = 𝑋)) |
91 | | eqid 2610 |
. . . . . . . . 9
⊢
(-g‘𝑅) = (-g‘𝑅) |
92 | 4, 1, 31, 2, 82, 83, 88, 90, 36, 91 | evl1subd 19527 |
. . . . . . . 8
⊢ (((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → (((𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅))(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑋))
∈ (Base‘(Poly1‘𝑅))
∧ (((eval1‘𝑅)‘((𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅))(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑋)))‘𝑦)
= ((𝑁 ↑ 𝑦)(-g‘𝑅)𝑋))) |
93 | 92 | simprd 478 |
. . . . . . 7
⊢ (((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → (((eval1‘𝑅)‘((𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅))(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑋)))‘𝑦)
= ((𝑁 ↑ 𝑦)(-g‘𝑅)𝑋)) |
94 | 93 | eqeq1d 2612 |
. . . . . 6
⊢ (((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → ((((eval1‘𝑅)‘((𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅))(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑋)))‘𝑦)
= (0g‘𝑅) ↔ ((𝑁 ↑ 𝑦)(-g‘𝑅)𝑋) =
(0g‘𝑅))) |
95 | | ringgrp 18375 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) |
96 | 12, 95 | syl 17 |
. . . . . . . 8
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) → 𝑅 ∈ Grp) |
97 | 96 | adantr 480 |
. . . . . . 7
⊢ (((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → 𝑅 ∈ Grp) |
98 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(mulGrp‘𝑅) =
(mulGrp‘𝑅) |
99 | 98 | ringmgp 18376 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ Ring →
(mulGrp‘𝑅) ∈
Mnd) |
100 | 12, 99 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) → (mulGrp‘𝑅) ∈ Mnd) |
101 | 100 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → (mulGrp‘𝑅) ∈ Mnd) |
102 | | mndmgm 17123 |
. . . . . . . . 9
⊢
((mulGrp‘𝑅)
∈ Mnd → (mulGrp‘𝑅) ∈ Mgm) |
103 | 101, 102 | syl 17 |
. . . . . . . 8
⊢ (((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → (mulGrp‘𝑅) ∈ Mgm) |
104 | 98, 31 | mgpbas 18318 |
. . . . . . . . 9
⊢ 𝐵 =
(Base‘(mulGrp‘𝑅)) |
105 | 104, 85 | mulgnncl 17379 |
. . . . . . . 8
⊢
(((mulGrp‘𝑅)
∈ Mgm ∧ 𝑁 ∈
ℕ ∧ 𝑦 ∈
𝐵) → (𝑁 ↑ 𝑦) ∈ 𝐵) |
106 | 103, 86, 83, 105 | syl3anc 1318 |
. . . . . . 7
⊢ (((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → (𝑁 ↑ 𝑦) ∈ 𝐵) |
107 | 31, 5, 91 | grpsubeq0 17324 |
. . . . . . 7
⊢ ((𝑅 ∈ Grp ∧ (𝑁 ↑ 𝑦) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → (((𝑁 ↑ 𝑦)(-g‘𝑅)𝑋) = (0g‘𝑅) ↔ (𝑁 ↑ 𝑦) = 𝑋)) |
108 | 97, 106, 89, 107 | syl3anc 1318 |
. . . . . 6
⊢ (((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → (((𝑁 ↑ 𝑦)(-g‘𝑅)𝑋) = (0g‘𝑅) ↔ (𝑁 ↑ 𝑦) = 𝑋)) |
109 | 94, 108 | bitrd 267 |
. . . . 5
⊢ (((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → ((((eval1‘𝑅)‘((𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅))(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑋)))‘𝑦)
= (0g‘𝑅) ↔ (𝑁 ↑ 𝑦) = 𝑋)) |
110 | 109 | rabbidva 3163 |
. . . 4
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) → {𝑦 ∈ 𝐵 ∣ (((eval1‘𝑅)‘((𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅))(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑋)))‘𝑦)
= (0g‘𝑅)} = {𝑦 ∈ 𝐵 ∣ (𝑁
↑ 𝑦) = 𝑋}) |
111 | 81, 110 | eqtrd 2644 |
. . 3
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) → (◡((eval1‘𝑅)‘((𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅))(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑋))) “ {(0g‘𝑅)}) = {𝑦
∈ 𝐵 ∣ (𝑁 ↑ 𝑦) = 𝑋}) |
112 | 111 | fveq2d 6107 |
. 2
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) → (#‘(◡((eval1‘𝑅)‘((𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅))(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑋))) “ {(0g‘𝑅)})) = (#‘{𝑦 ∈ 𝐵
∣ (𝑁 ↑ 𝑦) = 𝑋})) |
113 | 66, 112, 61 | 3brtr3d 4614 |
1
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) → (#‘{𝑦 ∈ 𝐵 ∣ (𝑁 ↑ 𝑦) = 𝑋}) ≤ 𝑁) |