Proof of Theorem fta1glem1
Step | Hyp | Ref
| Expression |
1 | | 1cnd 10828 |
. 2
⊢ (𝜑 → 1 ∈
ℂ) |
2 | | fta1g.1 |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ IDomn) |
3 | | isidom 20342 |
. . . . . . 7
⊢ (𝑅 ∈ IDomn ↔ (𝑅 ∈ CRing ∧ 𝑅 ∈ Domn)) |
4 | | domnnzr 20333 |
. . . . . . 7
⊢ (𝑅 ∈ Domn → 𝑅 ∈ NzRing) |
5 | 3, 4 | simplbiim 508 |
. . . . . 6
⊢ (𝑅 ∈ IDomn → 𝑅 ∈ NzRing) |
6 | 2, 5 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ NzRing) |
7 | | nzrring 20299 |
. . . . 5
⊢ (𝑅 ∈ NzRing → 𝑅 ∈ Ring) |
8 | 6, 7 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑅 ∈ Ring) |
9 | | fta1g.2 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ 𝐵) |
10 | | fta1g.p |
. . . . . . . 8
⊢ 𝑃 = (Poly1‘𝑅) |
11 | | fta1g.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝑃) |
12 | | fta1glem.k |
. . . . . . . 8
⊢ 𝐾 = (Base‘𝑅) |
13 | | fta1glem.x |
. . . . . . . 8
⊢ 𝑋 = (var1‘𝑅) |
14 | | fta1glem.m |
. . . . . . . 8
⊢ − =
(-g‘𝑃) |
15 | | fta1glem.a |
. . . . . . . 8
⊢ 𝐴 = (algSc‘𝑃) |
16 | | fta1glem.g |
. . . . . . . 8
⊢ 𝐺 = (𝑋 − (𝐴‘𝑇)) |
17 | | fta1g.o |
. . . . . . . 8
⊢ 𝑂 = (eval1‘𝑅) |
18 | 3 | simplbi 501 |
. . . . . . . . 9
⊢ (𝑅 ∈ IDomn → 𝑅 ∈ CRing) |
19 | 2, 18 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ CRing) |
20 | | fta1glem.5 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑇 ∈ (◡(𝑂‘𝐹) “ {𝑊})) |
21 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢ (𝑅 ↑s 𝐾) = (𝑅 ↑s 𝐾) |
22 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(Base‘(𝑅
↑s 𝐾)) = (Base‘(𝑅 ↑s 𝐾)) |
23 | 12 | fvexi 6731 |
. . . . . . . . . . . . . 14
⊢ 𝐾 ∈ V |
24 | 23 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐾 ∈ V) |
25 | 17, 10, 21, 12 | evl1rhm 21248 |
. . . . . . . . . . . . . . . 16
⊢ (𝑅 ∈ CRing → 𝑂 ∈ (𝑃 RingHom (𝑅 ↑s 𝐾))) |
26 | 19, 25 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑂 ∈ (𝑃 RingHom (𝑅 ↑s 𝐾))) |
27 | 11, 22 | rhmf 19746 |
. . . . . . . . . . . . . . 15
⊢ (𝑂 ∈ (𝑃 RingHom (𝑅 ↑s 𝐾)) → 𝑂:𝐵⟶(Base‘(𝑅 ↑s 𝐾))) |
28 | 26, 27 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑂:𝐵⟶(Base‘(𝑅 ↑s 𝐾))) |
29 | 28, 9 | ffvelrnd 6905 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑂‘𝐹) ∈ (Base‘(𝑅 ↑s 𝐾))) |
30 | 21, 12, 22, 2, 24, 29 | pwselbas 16994 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑂‘𝐹):𝐾⟶𝐾) |
31 | 30 | ffnd 6546 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑂‘𝐹) Fn 𝐾) |
32 | | fniniseg 6880 |
. . . . . . . . . . 11
⊢ ((𝑂‘𝐹) Fn 𝐾 → (𝑇 ∈ (◡(𝑂‘𝐹) “ {𝑊}) ↔ (𝑇 ∈ 𝐾 ∧ ((𝑂‘𝐹)‘𝑇) = 𝑊))) |
33 | 31, 32 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑇 ∈ (◡(𝑂‘𝐹) “ {𝑊}) ↔ (𝑇 ∈ 𝐾 ∧ ((𝑂‘𝐹)‘𝑇) = 𝑊))) |
34 | 20, 33 | mpbid 235 |
. . . . . . . . 9
⊢ (𝜑 → (𝑇 ∈ 𝐾 ∧ ((𝑂‘𝐹)‘𝑇) = 𝑊)) |
35 | 34 | simpld 498 |
. . . . . . . 8
⊢ (𝜑 → 𝑇 ∈ 𝐾) |
36 | | eqid 2737 |
. . . . . . . 8
⊢
(Monic1p‘𝑅) = (Monic1p‘𝑅) |
37 | | fta1g.d |
. . . . . . . 8
⊢ 𝐷 = ( deg1
‘𝑅) |
38 | | fta1g.w |
. . . . . . . 8
⊢ 𝑊 = (0g‘𝑅) |
39 | 10, 11, 12, 13, 14, 15, 16, 17, 6, 19, 35, 36, 37, 38 | ply1remlem 25060 |
. . . . . . 7
⊢ (𝜑 → (𝐺 ∈ (Monic1p‘𝑅) ∧ (𝐷‘𝐺) = 1 ∧ (◡(𝑂‘𝐺) “ {𝑊}) = {𝑇})) |
40 | 39 | simp1d 1144 |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ (Monic1p‘𝑅)) |
41 | | eqid 2737 |
. . . . . . 7
⊢
(Unic1p‘𝑅) = (Unic1p‘𝑅) |
42 | 41, 36 | mon1puc1p 25048 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐺 ∈
(Monic1p‘𝑅)) → 𝐺 ∈ (Unic1p‘𝑅)) |
43 | 8, 40, 42 | syl2anc 587 |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ (Unic1p‘𝑅)) |
44 | | eqid 2737 |
. . . . . 6
⊢
(quot1p‘𝑅) = (quot1p‘𝑅) |
45 | 44, 10, 11, 41 | q1pcl 25053 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ (Unic1p‘𝑅)) → (𝐹(quot1p‘𝑅)𝐺) ∈ 𝐵) |
46 | 8, 9, 43, 45 | syl3anc 1373 |
. . . 4
⊢ (𝜑 → (𝐹(quot1p‘𝑅)𝐺) ∈ 𝐵) |
47 | | fta1glem.4 |
. . . . . . . 8
⊢ (𝜑 → (𝐷‘𝐹) = (𝑁 + 1)) |
48 | | fta1glem.3 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
49 | | peano2nn0 12130 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ0) |
50 | 48, 49 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑁 + 1) ∈
ℕ0) |
51 | 47, 50 | eqeltrd 2838 |
. . . . . . 7
⊢ (𝜑 → (𝐷‘𝐹) ∈
ℕ0) |
52 | | fta1g.z |
. . . . . . . . 9
⊢ 0 =
(0g‘𝑃) |
53 | 37, 10, 52, 11 | deg1nn0clb 24988 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵) → (𝐹 ≠ 0 ↔ (𝐷‘𝐹) ∈
ℕ0)) |
54 | 8, 9, 53 | syl2anc 587 |
. . . . . . 7
⊢ (𝜑 → (𝐹 ≠ 0 ↔ (𝐷‘𝐹) ∈
ℕ0)) |
55 | 51, 54 | mpbird 260 |
. . . . . 6
⊢ (𝜑 → 𝐹 ≠ 0 ) |
56 | 34 | simprd 499 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑂‘𝐹)‘𝑇) = 𝑊) |
57 | | eqid 2737 |
. . . . . . . . . 10
⊢
(∥r‘𝑃) = (∥r‘𝑃) |
58 | 10, 11, 12, 13, 14, 15, 16, 17, 6, 19, 35, 9, 38, 57 | facth1 25062 |
. . . . . . . . 9
⊢ (𝜑 → (𝐺(∥r‘𝑃)𝐹 ↔ ((𝑂‘𝐹)‘𝑇) = 𝑊)) |
59 | 56, 58 | mpbird 260 |
. . . . . . . 8
⊢ (𝜑 → 𝐺(∥r‘𝑃)𝐹) |
60 | | eqid 2737 |
. . . . . . . . . 10
⊢
(.r‘𝑃) = (.r‘𝑃) |
61 | 10, 57, 11, 41, 60, 44 | dvdsq1p 25058 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ (Unic1p‘𝑅)) → (𝐺(∥r‘𝑃)𝐹 ↔ 𝐹 = ((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺))) |
62 | 8, 9, 43, 61 | syl3anc 1373 |
. . . . . . . 8
⊢ (𝜑 → (𝐺(∥r‘𝑃)𝐹 ↔ 𝐹 = ((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺))) |
63 | 59, 62 | mpbid 235 |
. . . . . . 7
⊢ (𝜑 → 𝐹 = ((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺)) |
64 | 63 | eqcomd 2743 |
. . . . . 6
⊢ (𝜑 → ((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺) = 𝐹) |
65 | 10 | ply1crng 21119 |
. . . . . . . . 9
⊢ (𝑅 ∈ CRing → 𝑃 ∈ CRing) |
66 | 19, 65 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑃 ∈ CRing) |
67 | | crngring 19574 |
. . . . . . . 8
⊢ (𝑃 ∈ CRing → 𝑃 ∈ Ring) |
68 | 66, 67 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑃 ∈ Ring) |
69 | 10, 11, 36 | mon1pcl 25042 |
. . . . . . . 8
⊢ (𝐺 ∈
(Monic1p‘𝑅) → 𝐺 ∈ 𝐵) |
70 | 40, 69 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐺 ∈ 𝐵) |
71 | 11, 60, 52 | ringlz 19605 |
. . . . . . 7
⊢ ((𝑃 ∈ Ring ∧ 𝐺 ∈ 𝐵) → ( 0 (.r‘𝑃)𝐺) = 0 ) |
72 | 68, 70, 71 | syl2anc 587 |
. . . . . 6
⊢ (𝜑 → ( 0 (.r‘𝑃)𝐺) = 0 ) |
73 | 55, 64, 72 | 3netr4d 3018 |
. . . . 5
⊢ (𝜑 → ((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺) ≠ ( 0 (.r‘𝑃)𝐺)) |
74 | | oveq1 7220 |
. . . . . 6
⊢ ((𝐹(quot1p‘𝑅)𝐺) = 0 → ((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺) = ( 0 (.r‘𝑃)𝐺)) |
75 | 74 | necon3i 2973 |
. . . . 5
⊢ (((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺) ≠ ( 0 (.r‘𝑃)𝐺) → (𝐹(quot1p‘𝑅)𝐺) ≠ 0 ) |
76 | 73, 75 | syl 17 |
. . . 4
⊢ (𝜑 → (𝐹(quot1p‘𝑅)𝐺) ≠ 0 ) |
77 | 37, 10, 52, 11 | deg1nn0cl 24986 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ (𝐹(quot1p‘𝑅)𝐺) ∈ 𝐵 ∧ (𝐹(quot1p‘𝑅)𝐺) ≠ 0 ) → (𝐷‘(𝐹(quot1p‘𝑅)𝐺)) ∈
ℕ0) |
78 | 8, 46, 76, 77 | syl3anc 1373 |
. . 3
⊢ (𝜑 → (𝐷‘(𝐹(quot1p‘𝑅)𝐺)) ∈
ℕ0) |
79 | 78 | nn0cnd 12152 |
. 2
⊢ (𝜑 → (𝐷‘(𝐹(quot1p‘𝑅)𝐺)) ∈ ℂ) |
80 | 48 | nn0cnd 12152 |
. 2
⊢ (𝜑 → 𝑁 ∈ ℂ) |
81 | 11, 60 | crngcom 19580 |
. . . . . . 7
⊢ ((𝑃 ∈ CRing ∧ (𝐹(quot1p‘𝑅)𝐺) ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → ((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺) = (𝐺(.r‘𝑃)(𝐹(quot1p‘𝑅)𝐺))) |
82 | 66, 46, 70, 81 | syl3anc 1373 |
. . . . . 6
⊢ (𝜑 → ((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺) = (𝐺(.r‘𝑃)(𝐹(quot1p‘𝑅)𝐺))) |
83 | 63, 82 | eqtrd 2777 |
. . . . 5
⊢ (𝜑 → 𝐹 = (𝐺(.r‘𝑃)(𝐹(quot1p‘𝑅)𝐺))) |
84 | 83 | fveq2d 6721 |
. . . 4
⊢ (𝜑 → (𝐷‘𝐹) = (𝐷‘(𝐺(.r‘𝑃)(𝐹(quot1p‘𝑅)𝐺)))) |
85 | | eqid 2737 |
. . . . 5
⊢
(RLReg‘𝑅) =
(RLReg‘𝑅) |
86 | 39 | simp2d 1145 |
. . . . . . 7
⊢ (𝜑 → (𝐷‘𝐺) = 1) |
87 | | 1nn0 12106 |
. . . . . . 7
⊢ 1 ∈
ℕ0 |
88 | 86, 87 | eqeltrdi 2846 |
. . . . . 6
⊢ (𝜑 → (𝐷‘𝐺) ∈
ℕ0) |
89 | 37, 10, 52, 11 | deg1nn0clb 24988 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐺 ∈ 𝐵) → (𝐺 ≠ 0 ↔ (𝐷‘𝐺) ∈
ℕ0)) |
90 | 8, 70, 89 | syl2anc 587 |
. . . . . 6
⊢ (𝜑 → (𝐺 ≠ 0 ↔ (𝐷‘𝐺) ∈
ℕ0)) |
91 | 88, 90 | mpbird 260 |
. . . . 5
⊢ (𝜑 → 𝐺 ≠ 0 ) |
92 | | eqid 2737 |
. . . . . . . 8
⊢
(Unit‘𝑅) =
(Unit‘𝑅) |
93 | 85, 92 | unitrrg 20331 |
. . . . . . 7
⊢ (𝑅 ∈ Ring →
(Unit‘𝑅) ⊆
(RLReg‘𝑅)) |
94 | 8, 93 | syl 17 |
. . . . . 6
⊢ (𝜑 → (Unit‘𝑅) ⊆ (RLReg‘𝑅)) |
95 | 37, 92, 41 | uc1pldg 25046 |
. . . . . . 7
⊢ (𝐺 ∈
(Unic1p‘𝑅)
→ ((coe1‘𝐺)‘(𝐷‘𝐺)) ∈ (Unit‘𝑅)) |
96 | 43, 95 | syl 17 |
. . . . . 6
⊢ (𝜑 →
((coe1‘𝐺)‘(𝐷‘𝐺)) ∈ (Unit‘𝑅)) |
97 | 94, 96 | sseldd 3902 |
. . . . 5
⊢ (𝜑 →
((coe1‘𝐺)‘(𝐷‘𝐺)) ∈ (RLReg‘𝑅)) |
98 | 37, 10, 85, 11, 60, 52, 8, 70, 91, 97, 46, 76 | deg1mul2 25012 |
. . . 4
⊢ (𝜑 → (𝐷‘(𝐺(.r‘𝑃)(𝐹(quot1p‘𝑅)𝐺))) = ((𝐷‘𝐺) + (𝐷‘(𝐹(quot1p‘𝑅)𝐺)))) |
99 | 84, 47, 98 | 3eqtr3d 2785 |
. . 3
⊢ (𝜑 → (𝑁 + 1) = ((𝐷‘𝐺) + (𝐷‘(𝐹(quot1p‘𝑅)𝐺)))) |
100 | | ax-1cn 10787 |
. . . 4
⊢ 1 ∈
ℂ |
101 | | addcom 11018 |
. . . 4
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → (𝑁 + 1) =
(1 + 𝑁)) |
102 | 80, 100, 101 | sylancl 589 |
. . 3
⊢ (𝜑 → (𝑁 + 1) = (1 + 𝑁)) |
103 | 86 | oveq1d 7228 |
. . 3
⊢ (𝜑 → ((𝐷‘𝐺) + (𝐷‘(𝐹(quot1p‘𝑅)𝐺))) = (1 + (𝐷‘(𝐹(quot1p‘𝑅)𝐺)))) |
104 | 99, 102, 103 | 3eqtr3rd 2786 |
. 2
⊢ (𝜑 → (1 + (𝐷‘(𝐹(quot1p‘𝑅)𝐺))) = (1 + 𝑁)) |
105 | 1, 79, 80, 104 | addcanad 11037 |
1
⊢ (𝜑 → (𝐷‘(𝐹(quot1p‘𝑅)𝐺)) = 𝑁) |