Proof of Theorem idomrootle
| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . 3
⊢
(Poly1‘𝑅) = (Poly1‘𝑅) |
| 2 | | eqid 2737 |
. . 3
⊢
(Base‘(Poly1‘𝑅)) =
(Base‘(Poly1‘𝑅)) |
| 3 | | eqid 2737 |
. . 3
⊢
(deg1‘𝑅) = (deg1‘𝑅) |
| 4 | | eqid 2737 |
. . 3
⊢
(eval1‘𝑅) = (eval1‘𝑅) |
| 5 | | eqid 2737 |
. . 3
⊢
(0g‘𝑅) = (0g‘𝑅) |
| 6 | | eqid 2737 |
. . 3
⊢
(0g‘(Poly1‘𝑅)) =
(0g‘(Poly1‘𝑅)) |
| 7 | | simp1 1137 |
. . 3
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) → 𝑅 ∈ IDomn) |
| 8 | | isidom 20725 |
. . . . . . . . 9
⊢ (𝑅 ∈ IDomn ↔ (𝑅 ∈ CRing ∧ 𝑅 ∈ Domn)) |
| 9 | 8 | simplbi 497 |
. . . . . . . 8
⊢ (𝑅 ∈ IDomn → 𝑅 ∈ CRing) |
| 10 | 7, 9 | syl 17 |
. . . . . . 7
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) → 𝑅 ∈ CRing) |
| 11 | | crngring 20242 |
. . . . . . 7
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
| 12 | 10, 11 | syl 17 |
. . . . . 6
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) → 𝑅 ∈ Ring) |
| 13 | 1 | ply1ring 22249 |
. . . . . 6
⊢ (𝑅 ∈ Ring →
(Poly1‘𝑅)
∈ Ring) |
| 14 | 12, 13 | syl 17 |
. . . . 5
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) →
(Poly1‘𝑅)
∈ Ring) |
| 15 | | ringgrp 20235 |
. . . . 5
⊢
((Poly1‘𝑅) ∈ Ring →
(Poly1‘𝑅)
∈ Grp) |
| 16 | 14, 15 | syl 17 |
. . . 4
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) →
(Poly1‘𝑅)
∈ Grp) |
| 17 | | eqid 2737 |
. . . . . . . 8
⊢
(mulGrp‘(Poly1‘𝑅)) =
(mulGrp‘(Poly1‘𝑅)) |
| 18 | 17 | ringmgp 20236 |
. . . . . . 7
⊢
((Poly1‘𝑅) ∈ Ring →
(mulGrp‘(Poly1‘𝑅)) ∈ Mnd) |
| 19 | 14, 18 | syl 17 |
. . . . . 6
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) →
(mulGrp‘(Poly1‘𝑅)) ∈ Mnd) |
| 20 | | mndmgm 18754 |
. . . . . 6
⊢
((mulGrp‘(Poly1‘𝑅)) ∈ Mnd →
(mulGrp‘(Poly1‘𝑅)) ∈ Mgm) |
| 21 | 19, 20 | syl 17 |
. . . . 5
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) →
(mulGrp‘(Poly1‘𝑅)) ∈ Mgm) |
| 22 | | simp3 1139 |
. . . . 5
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ ℕ) |
| 23 | | eqid 2737 |
. . . . . . 7
⊢
(var1‘𝑅) = (var1‘𝑅) |
| 24 | 23, 1, 2 | vr1cl 22219 |
. . . . . 6
⊢ (𝑅 ∈ Ring →
(var1‘𝑅)
∈ (Base‘(Poly1‘𝑅))) |
| 25 | 12, 24 | syl 17 |
. . . . 5
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) →
(var1‘𝑅)
∈ (Base‘(Poly1‘𝑅))) |
| 26 | 17, 2 | mgpbas 20142 |
. . . . . 6
⊢
(Base‘(Poly1‘𝑅)) =
(Base‘(mulGrp‘(Poly1‘𝑅))) |
| 27 | | eqid 2737 |
. . . . . 6
⊢
(.g‘(mulGrp‘(Poly1‘𝑅))) =
(.g‘(mulGrp‘(Poly1‘𝑅))) |
| 28 | 26, 27 | mulgnncl 19107 |
. . . . 5
⊢
(((mulGrp‘(Poly1‘𝑅)) ∈ Mgm ∧ 𝑁 ∈ ℕ ∧
(var1‘𝑅)
∈ (Base‘(Poly1‘𝑅))) → (𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅)) ∈ (Base‘(Poly1‘𝑅))) |
| 29 | 21, 22, 25, 28 | syl3anc 1373 |
. . . 4
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) → (𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅)) ∈ (Base‘(Poly1‘𝑅))) |
| 30 | | eqid 2737 |
. . . . . . 7
⊢
(algSc‘(Poly1‘𝑅)) =
(algSc‘(Poly1‘𝑅)) |
| 31 | | idomrootle.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑅) |
| 32 | 1, 30, 31, 2 | ply1sclf 22288 |
. . . . . 6
⊢ (𝑅 ∈ Ring →
(algSc‘(Poly1‘𝑅)):𝐵⟶(Base‘(Poly1‘𝑅))) |
| 33 | 12, 32 | syl 17 |
. . . . 5
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) →
(algSc‘(Poly1‘𝑅)):𝐵⟶(Base‘(Poly1‘𝑅))) |
| 34 | | simp2 1138 |
. . . . 5
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) → 𝑋 ∈ 𝐵) |
| 35 | 33, 34 | ffvelcdmd 7105 |
. . . 4
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) →
((algSc‘(Poly1‘𝑅))‘𝑋) ∈
(Base‘(Poly1‘𝑅))) |
| 36 | | eqid 2737 |
. . . . 5
⊢
(-g‘(Poly1‘𝑅)) =
(-g‘(Poly1‘𝑅)) |
| 37 | 2, 36 | grpsubcl 19038 |
. . . 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 1373 |
. . 3
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) → ((𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅))(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑋))
∈ (Base‘(Poly1‘𝑅))) |
| 39 | 3, 1, 2 | deg1xrcl 26121 |
. . . . . . . . . 10
⊢
(((algSc‘(Poly1‘𝑅))‘𝑋) ∈
(Base‘(Poly1‘𝑅)) → ((deg1‘𝑅)‘((algSc‘(Poly1‘𝑅))‘𝑋)) ∈ ℝ*) |
| 40 | 35, 39 | syl 17 |
. . . . . . . . 9
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) →
((deg1‘𝑅)‘((algSc‘(Poly1‘𝑅))‘𝑋)) ∈ ℝ*) |
| 41 | | 0xr 11308 |
. . . . . . . . . 10
⊢ 0 ∈
ℝ* |
| 42 | 41 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) → 0 ∈
ℝ*) |
| 43 | | nnre 12273 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
| 44 | 43 | rexrd 11311 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ*) |
| 45 | 44 | 3ad2ant3 1136 |
. . . . . . . . 9
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℝ*) |
| 46 | 3, 1, 31, 30 | deg1sclle 26151 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → ((deg1‘𝑅)‘((algSc‘(Poly1‘𝑅))‘𝑋)) ≤ 0) |
| 47 | 12, 34, 46 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) →
((deg1‘𝑅)‘((algSc‘(Poly1‘𝑅))‘𝑋)) ≤ 0) |
| 48 | | nngt0 12297 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → 0 <
𝑁) |
| 49 | 48 | 3ad2ant3 1136 |
. . . . . . . . 9
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) → 0 < 𝑁) |
| 50 | 40, 42, 45, 47, 49 | xrlelttrd 13202 |
. . . . . . . 8
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) →
((deg1‘𝑅)‘((algSc‘(Poly1‘𝑅))‘𝑋)) < 𝑁) |
| 51 | 8 | simprbi 496 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ IDomn → 𝑅 ∈ Domn) |
| 52 | | domnnzr 20706 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ Domn → 𝑅 ∈ NzRing) |
| 53 | 51, 52 | syl 17 |
. . . . . . . . . 10
⊢ (𝑅 ∈ IDomn → 𝑅 ∈ NzRing) |
| 54 | 7, 53 | syl 17 |
. . . . . . . . 9
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) → 𝑅 ∈ NzRing) |
| 55 | | nnnn0 12533 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
| 56 | 55 | 3ad2ant3 1136 |
. . . . . . . . 9
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℕ0) |
| 57 | 3, 1, 23, 17, 27 | deg1pw 26160 |
. . . . . . . . 9
⊢ ((𝑅 ∈ NzRing ∧ 𝑁 ∈ ℕ0)
→ ((deg1‘𝑅)‘(𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅))) = 𝑁) |
| 58 | 54, 56, 57 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) →
((deg1‘𝑅)‘(𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅))) = 𝑁) |
| 59 | 50, 58 | breqtrrd 5171 |
. . . . . . 7
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) →
((deg1‘𝑅)‘((algSc‘(Poly1‘𝑅))‘𝑋)) < ((deg1‘𝑅)‘(𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅)))) |
| 60 | 1, 3, 12, 2, 36, 29, 35, 59 | deg1sub 26147 |
. . . . . 6
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) →
((deg1‘𝑅)‘((𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅))(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑋))) = ((deg1‘𝑅)‘(𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅)))) |
| 61 | 60, 58 | eqtrd 2777 |
. . . . 5
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) →
((deg1‘𝑅)‘((𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅))(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑋))) = 𝑁) |
| 62 | 61, 56 | eqeltrd 2841 |
. . . 4
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) →
((deg1‘𝑅)‘((𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅))(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑋))) ∈ ℕ0) |
| 63 | 3, 1, 6, 2 | deg1nn0clb 26129 |
. . . . 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 584 |
. . . 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 257 |
. . 3
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) → ((𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅))(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑋))
≠ (0g‘(Poly1‘𝑅))) |
| 66 | 1, 2, 3, 4, 5, 6, 7, 38, 65 | fta1g 26209 |
. 2
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) →
(♯‘(◡((eval1‘𝑅)‘((𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅))(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑋))) “ {(0g‘𝑅)})) ≤ ((deg1‘𝑅)‘((𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅))(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑋)))) |
| 67 | | eqid 2737 |
. . . . . . 7
⊢ (𝑅 ↑s 𝐵) = (𝑅 ↑s 𝐵) |
| 68 | | eqid 2737 |
. . . . . . 7
⊢
(Base‘(𝑅
↑s 𝐵)) = (Base‘(𝑅 ↑s 𝐵)) |
| 69 | 31 | fvexi 6920 |
. . . . . . . 8
⊢ 𝐵 ∈ V |
| 70 | 69 | a1i 11 |
. . . . . . 7
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) → 𝐵 ∈ V) |
| 71 | 4, 1, 67, 31 | evl1rhm 22336 |
. . . . . . . . . 10
⊢ (𝑅 ∈ CRing →
(eval1‘𝑅)
∈ ((Poly1‘𝑅) RingHom (𝑅 ↑s 𝐵))) |
| 72 | 10, 71 | syl 17 |
. . . . . . . . 9
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) →
(eval1‘𝑅)
∈ ((Poly1‘𝑅) RingHom (𝑅 ↑s 𝐵))) |
| 73 | 2, 68 | rhmf 20485 |
. . . . . . . . 9
⊢
((eval1‘𝑅) ∈ ((Poly1‘𝑅) RingHom (𝑅 ↑s 𝐵)) → (eval1‘𝑅):(Base‘(Poly1‘𝑅))⟶(Base‘(𝑅 ↑s 𝐵))) |
| 74 | 72, 73 | syl 17 |
. . . . . . . 8
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) →
(eval1‘𝑅):(Base‘(Poly1‘𝑅))⟶(Base‘(𝑅 ↑s 𝐵))) |
| 75 | 74, 38 | ffvelcdmd 7105 |
. . . . . . 7
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) →
((eval1‘𝑅)‘((𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅))(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑋))) ∈ (Base‘(𝑅 ↑s 𝐵))) |
| 76 | 67, 31, 68, 7, 70, 75 | pwselbas 17534 |
. . . . . 6
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) →
((eval1‘𝑅)‘((𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅))(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑋))):𝐵⟶𝐵) |
| 77 | 76 | ffnd 6737 |
. . . . 5
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) →
((eval1‘𝑅)‘((𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅))(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑋))) Fn 𝐵) |
| 78 | | fniniseg2 7082 |
. . . . 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‘𝑅)}) |
| 79 | 77, 78 | syl 17 |
. . . 4
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) → (◡((eval1‘𝑅)‘((𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅))(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑋))) “ {(0g‘𝑅)}) = {𝑦
∈ 𝐵 ∣
(((eval1‘𝑅)‘((𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅))(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑋)))‘𝑦)
= (0g‘𝑅)}) |
| 80 | 10 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → 𝑅 ∈ CRing) |
| 81 | | simpr 484 |
. . . . . . . . 9
⊢ (((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ 𝐵) |
| 82 | 4, 23, 31, 1, 2, 80, 81 | evl1vard 22341 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → ((var1‘𝑅) ∈
(Base‘(Poly1‘𝑅)) ∧ (((eval1‘𝑅)‘(var1‘𝑅))‘𝑦) = 𝑦)) |
| 83 | | idomrootle.e |
. . . . . . . . . 10
⊢ ↑ =
(.g‘(mulGrp‘𝑅)) |
| 84 | | simpl3 1194 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → 𝑁 ∈ ℕ) |
| 85 | 84, 55 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → 𝑁 ∈
ℕ0) |
| 86 | 4, 1, 31, 2, 80, 81, 82, 27, 83, 85 | evl1expd 22349 |
. . . . . . . . 9
⊢ (((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → ((𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅)) ∈ (Base‘(Poly1‘𝑅)) ∧ (((eval1‘𝑅)‘(𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅)))‘𝑦)
= (𝑁 ↑ 𝑦))) |
| 87 | | simpl2 1193 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → 𝑋 ∈ 𝐵) |
| 88 | 4, 1, 31, 30, 2, 80, 87, 81 | evl1scad 22339 |
. . . . . . . . 9
⊢ (((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) →
(((algSc‘(Poly1‘𝑅))‘𝑋) ∈
(Base‘(Poly1‘𝑅)) ∧ (((eval1‘𝑅)‘((algSc‘(Poly1‘𝑅))‘𝑋))‘𝑦) = 𝑋)) |
| 89 | | eqid 2737 |
. . . . . . . . 9
⊢
(-g‘𝑅) = (-g‘𝑅) |
| 90 | 4, 1, 31, 2, 80, 81, 86, 88, 36, 89 | evl1subd 22346 |
. . . . . . . 8
⊢ (((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → (((𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅))(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑋))
∈ (Base‘(Poly1‘𝑅))
∧ (((eval1‘𝑅)‘((𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅))(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑋)))‘𝑦)
= ((𝑁 ↑ 𝑦)(-g‘𝑅)𝑋))) |
| 91 | 90 | simprd 495 |
. . . . . . 7
⊢ (((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → (((eval1‘𝑅)‘((𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅))(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑋)))‘𝑦)
= ((𝑁 ↑ 𝑦)(-g‘𝑅)𝑋)) |
| 92 | 91 | eqeq1d 2739 |
. . . . . 6
⊢ (((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → ((((eval1‘𝑅)‘((𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅))(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑋)))‘𝑦)
= (0g‘𝑅) ↔ ((𝑁 ↑ 𝑦)(-g‘𝑅)𝑋) =
(0g‘𝑅))) |
| 93 | | ringgrp 20235 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) |
| 94 | 12, 93 | syl 17 |
. . . . . . . 8
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) → 𝑅 ∈ Grp) |
| 95 | 94 | adantr 480 |
. . . . . . 7
⊢ (((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → 𝑅 ∈ Grp) |
| 96 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(mulGrp‘𝑅) =
(mulGrp‘𝑅) |
| 97 | 96 | ringmgp 20236 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ Ring →
(mulGrp‘𝑅) ∈
Mnd) |
| 98 | 12, 97 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) → (mulGrp‘𝑅) ∈ Mnd) |
| 99 | 98 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → (mulGrp‘𝑅) ∈ Mnd) |
| 100 | | mndmgm 18754 |
. . . . . . . . 9
⊢
((mulGrp‘𝑅)
∈ Mnd → (mulGrp‘𝑅) ∈ Mgm) |
| 101 | 99, 100 | syl 17 |
. . . . . . . 8
⊢ (((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → (mulGrp‘𝑅) ∈ Mgm) |
| 102 | 96, 31 | mgpbas 20142 |
. . . . . . . . 9
⊢ 𝐵 =
(Base‘(mulGrp‘𝑅)) |
| 103 | 102, 83 | mulgnncl 19107 |
. . . . . . . 8
⊢
(((mulGrp‘𝑅)
∈ Mgm ∧ 𝑁 ∈
ℕ ∧ 𝑦 ∈
𝐵) → (𝑁 ↑ 𝑦) ∈ 𝐵) |
| 104 | 101, 84, 81, 103 | syl3anc 1373 |
. . . . . . 7
⊢ (((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → (𝑁 ↑ 𝑦) ∈ 𝐵) |
| 105 | 31, 5, 89 | grpsubeq0 19044 |
. . . . . . 7
⊢ ((𝑅 ∈ Grp ∧ (𝑁 ↑ 𝑦) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → (((𝑁 ↑ 𝑦)(-g‘𝑅)𝑋) = (0g‘𝑅) ↔ (𝑁 ↑ 𝑦) = 𝑋)) |
| 106 | 95, 104, 87, 105 | syl3anc 1373 |
. . . . . 6
⊢ (((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → (((𝑁 ↑ 𝑦)(-g‘𝑅)𝑋) = (0g‘𝑅) ↔ (𝑁 ↑ 𝑦) = 𝑋)) |
| 107 | 92, 106 | bitrd 279 |
. . . . 5
⊢ (((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → ((((eval1‘𝑅)‘((𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅))(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑋)))‘𝑦)
= (0g‘𝑅) ↔ (𝑁 ↑ 𝑦) = 𝑋)) |
| 108 | 107 | rabbidva 3443 |
. . . 4
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) → {𝑦 ∈ 𝐵 ∣ (((eval1‘𝑅)‘((𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅))(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑋)))‘𝑦)
= (0g‘𝑅)} = {𝑦 ∈ 𝐵 ∣ (𝑁
↑ 𝑦) = 𝑋}) |
| 109 | 79, 108 | eqtrd 2777 |
. . 3
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) → (◡((eval1‘𝑅)‘((𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅))(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑋))) “ {(0g‘𝑅)}) = {𝑦
∈ 𝐵 ∣ (𝑁 ↑ 𝑦) = 𝑋}) |
| 110 | 109 | fveq2d 6910 |
. 2
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) →
(♯‘(◡((eval1‘𝑅)‘((𝑁(.g‘(mulGrp‘(Poly1‘𝑅)))(var1‘𝑅))(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑋))) “ {(0g‘𝑅)})) = (♯‘{𝑦 ∈ 𝐵
∣ (𝑁 ↑ 𝑦) = 𝑋})) |
| 111 | 66, 110, 61 | 3brtr3d 5174 |
1
⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) →
(♯‘{𝑦 ∈
𝐵 ∣ (𝑁 ↑ 𝑦) = 𝑋}) ≤ 𝑁) |