Proof of Theorem fta1glem1
Step | Hyp | Ref
| Expression |
1 | | 1cnd 9935 |
. 2
⊢ (𝜑 → 1 ∈
ℂ) |
2 | | fta1g.1 |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ IDomn) |
3 | | isidom 19125 |
. . . . . . . 8
⊢ (𝑅 ∈ IDomn ↔ (𝑅 ∈ CRing ∧ 𝑅 ∈ Domn)) |
4 | 3 | simprbi 479 |
. . . . . . 7
⊢ (𝑅 ∈ IDomn → 𝑅 ∈ Domn) |
5 | | domnnzr 19116 |
. . . . . . 7
⊢ (𝑅 ∈ Domn → 𝑅 ∈ NzRing) |
6 | 4, 5 | syl 17 |
. . . . . 6
⊢ (𝑅 ∈ IDomn → 𝑅 ∈ NzRing) |
7 | 2, 6 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ NzRing) |
8 | | nzrring 19082 |
. . . . 5
⊢ (𝑅 ∈ NzRing → 𝑅 ∈ Ring) |
9 | 7, 8 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑅 ∈ Ring) |
10 | | fta1g.2 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ 𝐵) |
11 | | fta1g.p |
. . . . . . . 8
⊢ 𝑃 = (Poly1‘𝑅) |
12 | | fta1g.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝑃) |
13 | | fta1glem.k |
. . . . . . . 8
⊢ 𝐾 = (Base‘𝑅) |
14 | | fta1glem.x |
. . . . . . . 8
⊢ 𝑋 = (var1‘𝑅) |
15 | | fta1glem.m |
. . . . . . . 8
⊢ − =
(-g‘𝑃) |
16 | | fta1glem.a |
. . . . . . . 8
⊢ 𝐴 = (algSc‘𝑃) |
17 | | fta1glem.g |
. . . . . . . 8
⊢ 𝐺 = (𝑋 − (𝐴‘𝑇)) |
18 | | fta1g.o |
. . . . . . . 8
⊢ 𝑂 = (eval1‘𝑅) |
19 | 3 | simplbi 475 |
. . . . . . . . 9
⊢ (𝑅 ∈ IDomn → 𝑅 ∈ CRing) |
20 | 2, 19 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ CRing) |
21 | | fta1glem.5 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑇 ∈ (◡(𝑂‘𝐹) “ {𝑊})) |
22 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢ (𝑅 ↑s 𝐾) = (𝑅 ↑s 𝐾) |
23 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(Base‘(𝑅
↑s 𝐾)) = (Base‘(𝑅 ↑s 𝐾)) |
24 | | fvex 6113 |
. . . . . . . . . . . . . . 15
⊢
(Base‘𝑅)
∈ V |
25 | 13, 24 | eqeltri 2684 |
. . . . . . . . . . . . . 14
⊢ 𝐾 ∈ V |
26 | 25 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐾 ∈ V) |
27 | 18, 11, 22, 13 | evl1rhm 19517 |
. . . . . . . . . . . . . . . 16
⊢ (𝑅 ∈ CRing → 𝑂 ∈ (𝑃 RingHom (𝑅 ↑s 𝐾))) |
28 | 20, 27 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑂 ∈ (𝑃 RingHom (𝑅 ↑s 𝐾))) |
29 | 12, 23 | rhmf 18549 |
. . . . . . . . . . . . . . 15
⊢ (𝑂 ∈ (𝑃 RingHom (𝑅 ↑s 𝐾)) → 𝑂:𝐵⟶(Base‘(𝑅 ↑s 𝐾))) |
30 | 28, 29 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑂:𝐵⟶(Base‘(𝑅 ↑s 𝐾))) |
31 | 30, 10 | ffvelrnd 6268 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑂‘𝐹) ∈ (Base‘(𝑅 ↑s 𝐾))) |
32 | 22, 13, 23, 2, 26, 31 | pwselbas 15972 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑂‘𝐹):𝐾⟶𝐾) |
33 | | ffn 5958 |
. . . . . . . . . . . 12
⊢ ((𝑂‘𝐹):𝐾⟶𝐾 → (𝑂‘𝐹) Fn 𝐾) |
34 | 32, 33 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑂‘𝐹) Fn 𝐾) |
35 | | fniniseg 6246 |
. . . . . . . . . . 11
⊢ ((𝑂‘𝐹) Fn 𝐾 → (𝑇 ∈ (◡(𝑂‘𝐹) “ {𝑊}) ↔ (𝑇 ∈ 𝐾 ∧ ((𝑂‘𝐹)‘𝑇) = 𝑊))) |
36 | 34, 35 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑇 ∈ (◡(𝑂‘𝐹) “ {𝑊}) ↔ (𝑇 ∈ 𝐾 ∧ ((𝑂‘𝐹)‘𝑇) = 𝑊))) |
37 | 21, 36 | mpbid 221 |
. . . . . . . . 9
⊢ (𝜑 → (𝑇 ∈ 𝐾 ∧ ((𝑂‘𝐹)‘𝑇) = 𝑊)) |
38 | 37 | simpld 474 |
. . . . . . . 8
⊢ (𝜑 → 𝑇 ∈ 𝐾) |
39 | | eqid 2610 |
. . . . . . . 8
⊢
(Monic1p‘𝑅) = (Monic1p‘𝑅) |
40 | | fta1g.d |
. . . . . . . 8
⊢ 𝐷 = ( deg1
‘𝑅) |
41 | | fta1g.w |
. . . . . . . 8
⊢ 𝑊 = (0g‘𝑅) |
42 | 11, 12, 13, 14, 15, 16, 17, 18, 7, 20, 38, 39, 40, 41 | ply1remlem 23726 |
. . . . . . 7
⊢ (𝜑 → (𝐺 ∈ (Monic1p‘𝑅) ∧ (𝐷‘𝐺) = 1 ∧ (◡(𝑂‘𝐺) “ {𝑊}) = {𝑇})) |
43 | 42 | simp1d 1066 |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ (Monic1p‘𝑅)) |
44 | | eqid 2610 |
. . . . . . 7
⊢
(Unic1p‘𝑅) = (Unic1p‘𝑅) |
45 | 44, 39 | mon1puc1p 23714 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐺 ∈
(Monic1p‘𝑅)) → 𝐺 ∈ (Unic1p‘𝑅)) |
46 | 9, 43, 45 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ (Unic1p‘𝑅)) |
47 | | eqid 2610 |
. . . . . 6
⊢
(quot1p‘𝑅) = (quot1p‘𝑅) |
48 | 47, 11, 12, 44 | q1pcl 23719 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ (Unic1p‘𝑅)) → (𝐹(quot1p‘𝑅)𝐺) ∈ 𝐵) |
49 | 9, 10, 46, 48 | syl3anc 1318 |
. . . 4
⊢ (𝜑 → (𝐹(quot1p‘𝑅)𝐺) ∈ 𝐵) |
50 | | fta1glem.4 |
. . . . . . . 8
⊢ (𝜑 → (𝐷‘𝐹) = (𝑁 + 1)) |
51 | | fta1glem.3 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
52 | | peano2nn0 11210 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ0) |
53 | 51, 52 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑁 + 1) ∈
ℕ0) |
54 | 50, 53 | eqeltrd 2688 |
. . . . . . 7
⊢ (𝜑 → (𝐷‘𝐹) ∈
ℕ0) |
55 | | fta1g.z |
. . . . . . . . 9
⊢ 0 =
(0g‘𝑃) |
56 | 40, 11, 55, 12 | deg1nn0clb 23654 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵) → (𝐹 ≠ 0 ↔ (𝐷‘𝐹) ∈
ℕ0)) |
57 | 9, 10, 56 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → (𝐹 ≠ 0 ↔ (𝐷‘𝐹) ∈
ℕ0)) |
58 | 54, 57 | mpbird 246 |
. . . . . 6
⊢ (𝜑 → 𝐹 ≠ 0 ) |
59 | 37 | simprd 478 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑂‘𝐹)‘𝑇) = 𝑊) |
60 | | eqid 2610 |
. . . . . . . . . 10
⊢
(∥r‘𝑃) = (∥r‘𝑃) |
61 | 11, 12, 13, 14, 15, 16, 17, 18, 7, 20, 38, 10, 41, 60 | facth1 23728 |
. . . . . . . . 9
⊢ (𝜑 → (𝐺(∥r‘𝑃)𝐹 ↔ ((𝑂‘𝐹)‘𝑇) = 𝑊)) |
62 | 59, 61 | mpbird 246 |
. . . . . . . 8
⊢ (𝜑 → 𝐺(∥r‘𝑃)𝐹) |
63 | | eqid 2610 |
. . . . . . . . . 10
⊢
(.r‘𝑃) = (.r‘𝑃) |
64 | 11, 60, 12, 44, 63, 47 | dvdsq1p 23724 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ (Unic1p‘𝑅)) → (𝐺(∥r‘𝑃)𝐹 ↔ 𝐹 = ((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺))) |
65 | 9, 10, 46, 64 | syl3anc 1318 |
. . . . . . . 8
⊢ (𝜑 → (𝐺(∥r‘𝑃)𝐹 ↔ 𝐹 = ((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺))) |
66 | 62, 65 | mpbid 221 |
. . . . . . 7
⊢ (𝜑 → 𝐹 = ((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺)) |
67 | 66 | eqcomd 2616 |
. . . . . 6
⊢ (𝜑 → ((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺) = 𝐹) |
68 | 11 | ply1crng 19389 |
. . . . . . . . 9
⊢ (𝑅 ∈ CRing → 𝑃 ∈ CRing) |
69 | 20, 68 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑃 ∈ CRing) |
70 | | crngring 18381 |
. . . . . . . 8
⊢ (𝑃 ∈ CRing → 𝑃 ∈ Ring) |
71 | 69, 70 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑃 ∈ Ring) |
72 | 11, 12, 39 | mon1pcl 23708 |
. . . . . . . 8
⊢ (𝐺 ∈
(Monic1p‘𝑅) → 𝐺 ∈ 𝐵) |
73 | 43, 72 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐺 ∈ 𝐵) |
74 | 12, 63, 55 | ringlz 18410 |
. . . . . . 7
⊢ ((𝑃 ∈ Ring ∧ 𝐺 ∈ 𝐵) → ( 0 (.r‘𝑃)𝐺) = 0 ) |
75 | 71, 73, 74 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → ( 0 (.r‘𝑃)𝐺) = 0 ) |
76 | 58, 67, 75 | 3netr4d 2859 |
. . . . 5
⊢ (𝜑 → ((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺) ≠ ( 0 (.r‘𝑃)𝐺)) |
77 | | oveq1 6556 |
. . . . . 6
⊢ ((𝐹(quot1p‘𝑅)𝐺) = 0 → ((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺) = ( 0 (.r‘𝑃)𝐺)) |
78 | 77 | necon3i 2814 |
. . . . 5
⊢ (((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺) ≠ ( 0 (.r‘𝑃)𝐺) → (𝐹(quot1p‘𝑅)𝐺) ≠ 0 ) |
79 | 76, 78 | syl 17 |
. . . 4
⊢ (𝜑 → (𝐹(quot1p‘𝑅)𝐺) ≠ 0 ) |
80 | 40, 11, 55, 12 | deg1nn0cl 23652 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ (𝐹(quot1p‘𝑅)𝐺) ∈ 𝐵 ∧ (𝐹(quot1p‘𝑅)𝐺) ≠ 0 ) → (𝐷‘(𝐹(quot1p‘𝑅)𝐺)) ∈
ℕ0) |
81 | 9, 49, 79, 80 | syl3anc 1318 |
. . 3
⊢ (𝜑 → (𝐷‘(𝐹(quot1p‘𝑅)𝐺)) ∈
ℕ0) |
82 | 81 | nn0cnd 11230 |
. 2
⊢ (𝜑 → (𝐷‘(𝐹(quot1p‘𝑅)𝐺)) ∈ ℂ) |
83 | 51 | nn0cnd 11230 |
. 2
⊢ (𝜑 → 𝑁 ∈ ℂ) |
84 | 12, 63 | crngcom 18385 |
. . . . . . 7
⊢ ((𝑃 ∈ CRing ∧ (𝐹(quot1p‘𝑅)𝐺) ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → ((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺) = (𝐺(.r‘𝑃)(𝐹(quot1p‘𝑅)𝐺))) |
85 | 69, 49, 73, 84 | syl3anc 1318 |
. . . . . 6
⊢ (𝜑 → ((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺) = (𝐺(.r‘𝑃)(𝐹(quot1p‘𝑅)𝐺))) |
86 | 66, 85 | eqtrd 2644 |
. . . . 5
⊢ (𝜑 → 𝐹 = (𝐺(.r‘𝑃)(𝐹(quot1p‘𝑅)𝐺))) |
87 | 86 | fveq2d 6107 |
. . . 4
⊢ (𝜑 → (𝐷‘𝐹) = (𝐷‘(𝐺(.r‘𝑃)(𝐹(quot1p‘𝑅)𝐺)))) |
88 | | eqid 2610 |
. . . . 5
⊢
(RLReg‘𝑅) =
(RLReg‘𝑅) |
89 | 42 | simp2d 1067 |
. . . . . . 7
⊢ (𝜑 → (𝐷‘𝐺) = 1) |
90 | | 1nn0 11185 |
. . . . . . 7
⊢ 1 ∈
ℕ0 |
91 | 89, 90 | syl6eqel 2696 |
. . . . . 6
⊢ (𝜑 → (𝐷‘𝐺) ∈
ℕ0) |
92 | 40, 11, 55, 12 | deg1nn0clb 23654 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐺 ∈ 𝐵) → (𝐺 ≠ 0 ↔ (𝐷‘𝐺) ∈
ℕ0)) |
93 | 9, 73, 92 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → (𝐺 ≠ 0 ↔ (𝐷‘𝐺) ∈
ℕ0)) |
94 | 91, 93 | mpbird 246 |
. . . . 5
⊢ (𝜑 → 𝐺 ≠ 0 ) |
95 | | eqid 2610 |
. . . . . . . 8
⊢
(Unit‘𝑅) =
(Unit‘𝑅) |
96 | 88, 95 | unitrrg 19114 |
. . . . . . 7
⊢ (𝑅 ∈ Ring →
(Unit‘𝑅) ⊆
(RLReg‘𝑅)) |
97 | 9, 96 | syl 17 |
. . . . . 6
⊢ (𝜑 → (Unit‘𝑅) ⊆ (RLReg‘𝑅)) |
98 | 40, 95, 44 | uc1pldg 23712 |
. . . . . . 7
⊢ (𝐺 ∈
(Unic1p‘𝑅)
→ ((coe1‘𝐺)‘(𝐷‘𝐺)) ∈ (Unit‘𝑅)) |
99 | 46, 98 | syl 17 |
. . . . . 6
⊢ (𝜑 →
((coe1‘𝐺)‘(𝐷‘𝐺)) ∈ (Unit‘𝑅)) |
100 | 97, 99 | sseldd 3569 |
. . . . 5
⊢ (𝜑 →
((coe1‘𝐺)‘(𝐷‘𝐺)) ∈ (RLReg‘𝑅)) |
101 | 40, 11, 88, 12, 63, 55, 9, 73, 94, 100, 49, 79 | deg1mul2 23678 |
. . . 4
⊢ (𝜑 → (𝐷‘(𝐺(.r‘𝑃)(𝐹(quot1p‘𝑅)𝐺))) = ((𝐷‘𝐺) + (𝐷‘(𝐹(quot1p‘𝑅)𝐺)))) |
102 | 87, 50, 101 | 3eqtr3d 2652 |
. . 3
⊢ (𝜑 → (𝑁 + 1) = ((𝐷‘𝐺) + (𝐷‘(𝐹(quot1p‘𝑅)𝐺)))) |
103 | | ax-1cn 9873 |
. . . 4
⊢ 1 ∈
ℂ |
104 | | addcom 10101 |
. . . 4
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → (𝑁 + 1) =
(1 + 𝑁)) |
105 | 83, 103, 104 | sylancl 693 |
. . 3
⊢ (𝜑 → (𝑁 + 1) = (1 + 𝑁)) |
106 | 89 | oveq1d 6564 |
. . 3
⊢ (𝜑 → ((𝐷‘𝐺) + (𝐷‘(𝐹(quot1p‘𝑅)𝐺))) = (1 + (𝐷‘(𝐹(quot1p‘𝑅)𝐺)))) |
107 | 102, 105,
106 | 3eqtr3rd 2653 |
. 2
⊢ (𝜑 → (1 + (𝐷‘(𝐹(quot1p‘𝑅)𝐺))) = (1 + 𝑁)) |
108 | 1, 82, 83, 107 | addcanad 10120 |
1
⊢ (𝜑 → (𝐷‘(𝐹(quot1p‘𝑅)𝐺)) = 𝑁) |