Proof of Theorem fta1glem1
Step | Hyp | Ref
| Expression |
1 | | 1cnd 10323 |
. 2
⊢ (𝜑 → 1 ∈
ℂ) |
2 | | fta1g.1 |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ IDomn) |
3 | | isidom 19627 |
. . . . . . . 8
⊢ (𝑅 ∈ IDomn ↔ (𝑅 ∈ CRing ∧ 𝑅 ∈ Domn)) |
4 | 3 | simprbi 491 |
. . . . . . 7
⊢ (𝑅 ∈ IDomn → 𝑅 ∈ Domn) |
5 | | domnnzr 19618 |
. . . . . . 7
⊢ (𝑅 ∈ Domn → 𝑅 ∈ NzRing) |
6 | 4, 5 | syl 17 |
. . . . . 6
⊢ (𝑅 ∈ IDomn → 𝑅 ∈ NzRing) |
7 | 2, 6 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ NzRing) |
8 | | nzrring 19584 |
. . . . 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 492 |
. . . . . . . . 9
⊢ (𝑅 ∈ IDomn → 𝑅 ∈ CRing) |
20 | 2, 19 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ CRing) |
21 | | fta1glem.5 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑇 ∈ (◡(𝑂‘𝐹) “ {𝑊})) |
22 | | eqid 2799 |
. . . . . . . . . . . . 13
⊢ (𝑅 ↑s 𝐾) = (𝑅 ↑s 𝐾) |
23 | | eqid 2799 |
. . . . . . . . . . . . 13
⊢
(Base‘(𝑅
↑s 𝐾)) = (Base‘(𝑅 ↑s 𝐾)) |
24 | 13 | fvexi 6425 |
. . . . . . . . . . . . . 14
⊢ 𝐾 ∈ V |
25 | 24 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐾 ∈ V) |
26 | 18, 11, 22, 13 | evl1rhm 20018 |
. . . . . . . . . . . . . . . 16
⊢ (𝑅 ∈ CRing → 𝑂 ∈ (𝑃 RingHom (𝑅 ↑s 𝐾))) |
27 | 20, 26 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑂 ∈ (𝑃 RingHom (𝑅 ↑s 𝐾))) |
28 | 12, 23 | rhmf 19044 |
. . . . . . . . . . . . . . 15
⊢ (𝑂 ∈ (𝑃 RingHom (𝑅 ↑s 𝐾)) → 𝑂:𝐵⟶(Base‘(𝑅 ↑s 𝐾))) |
29 | 27, 28 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑂:𝐵⟶(Base‘(𝑅 ↑s 𝐾))) |
30 | 29, 10 | ffvelrnd 6586 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑂‘𝐹) ∈ (Base‘(𝑅 ↑s 𝐾))) |
31 | 22, 13, 23, 2, 25, 30 | pwselbas 16464 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑂‘𝐹):𝐾⟶𝐾) |
32 | 31 | ffnd 6257 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑂‘𝐹) Fn 𝐾) |
33 | | fniniseg 6564 |
. . . . . . . . . . 11
⊢ ((𝑂‘𝐹) Fn 𝐾 → (𝑇 ∈ (◡(𝑂‘𝐹) “ {𝑊}) ↔ (𝑇 ∈ 𝐾 ∧ ((𝑂‘𝐹)‘𝑇) = 𝑊))) |
34 | 32, 33 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑇 ∈ (◡(𝑂‘𝐹) “ {𝑊}) ↔ (𝑇 ∈ 𝐾 ∧ ((𝑂‘𝐹)‘𝑇) = 𝑊))) |
35 | 21, 34 | mpbid 224 |
. . . . . . . . 9
⊢ (𝜑 → (𝑇 ∈ 𝐾 ∧ ((𝑂‘𝐹)‘𝑇) = 𝑊)) |
36 | 35 | simpld 489 |
. . . . . . . 8
⊢ (𝜑 → 𝑇 ∈ 𝐾) |
37 | | eqid 2799 |
. . . . . . . 8
⊢
(Monic1p‘𝑅) = (Monic1p‘𝑅) |
38 | | fta1g.d |
. . . . . . . 8
⊢ 𝐷 = ( deg1
‘𝑅) |
39 | | fta1g.w |
. . . . . . . 8
⊢ 𝑊 = (0g‘𝑅) |
40 | 11, 12, 13, 14, 15, 16, 17, 18, 7, 20, 36, 37, 38, 39 | ply1remlem 24263 |
. . . . . . 7
⊢ (𝜑 → (𝐺 ∈ (Monic1p‘𝑅) ∧ (𝐷‘𝐺) = 1 ∧ (◡(𝑂‘𝐺) “ {𝑊}) = {𝑇})) |
41 | 40 | simp1d 1173 |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ (Monic1p‘𝑅)) |
42 | | eqid 2799 |
. . . . . . 7
⊢
(Unic1p‘𝑅) = (Unic1p‘𝑅) |
43 | 42, 37 | mon1puc1p 24251 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐺 ∈
(Monic1p‘𝑅)) → 𝐺 ∈ (Unic1p‘𝑅)) |
44 | 9, 41, 43 | syl2anc 580 |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ (Unic1p‘𝑅)) |
45 | | eqid 2799 |
. . . . . 6
⊢
(quot1p‘𝑅) = (quot1p‘𝑅) |
46 | 45, 11, 12, 42 | q1pcl 24256 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ (Unic1p‘𝑅)) → (𝐹(quot1p‘𝑅)𝐺) ∈ 𝐵) |
47 | 9, 10, 44, 46 | syl3anc 1491 |
. . . 4
⊢ (𝜑 → (𝐹(quot1p‘𝑅)𝐺) ∈ 𝐵) |
48 | | fta1glem.4 |
. . . . . . . 8
⊢ (𝜑 → (𝐷‘𝐹) = (𝑁 + 1)) |
49 | | fta1glem.3 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
50 | | peano2nn0 11622 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ0) |
51 | 49, 50 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑁 + 1) ∈
ℕ0) |
52 | 48, 51 | eqeltrd 2878 |
. . . . . . 7
⊢ (𝜑 → (𝐷‘𝐹) ∈
ℕ0) |
53 | | fta1g.z |
. . . . . . . . 9
⊢ 0 =
(0g‘𝑃) |
54 | 38, 11, 53, 12 | deg1nn0clb 24191 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵) → (𝐹 ≠ 0 ↔ (𝐷‘𝐹) ∈
ℕ0)) |
55 | 9, 10, 54 | syl2anc 580 |
. . . . . . 7
⊢ (𝜑 → (𝐹 ≠ 0 ↔ (𝐷‘𝐹) ∈
ℕ0)) |
56 | 52, 55 | mpbird 249 |
. . . . . 6
⊢ (𝜑 → 𝐹 ≠ 0 ) |
57 | 35 | simprd 490 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑂‘𝐹)‘𝑇) = 𝑊) |
58 | | eqid 2799 |
. . . . . . . . . 10
⊢
(∥r‘𝑃) = (∥r‘𝑃) |
59 | 11, 12, 13, 14, 15, 16, 17, 18, 7, 20, 36, 10, 39, 58 | facth1 24265 |
. . . . . . . . 9
⊢ (𝜑 → (𝐺(∥r‘𝑃)𝐹 ↔ ((𝑂‘𝐹)‘𝑇) = 𝑊)) |
60 | 57, 59 | mpbird 249 |
. . . . . . . 8
⊢ (𝜑 → 𝐺(∥r‘𝑃)𝐹) |
61 | | eqid 2799 |
. . . . . . . . . 10
⊢
(.r‘𝑃) = (.r‘𝑃) |
62 | 11, 58, 12, 42, 61, 45 | dvdsq1p 24261 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ (Unic1p‘𝑅)) → (𝐺(∥r‘𝑃)𝐹 ↔ 𝐹 = ((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺))) |
63 | 9, 10, 44, 62 | syl3anc 1491 |
. . . . . . . 8
⊢ (𝜑 → (𝐺(∥r‘𝑃)𝐹 ↔ 𝐹 = ((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺))) |
64 | 60, 63 | mpbid 224 |
. . . . . . 7
⊢ (𝜑 → 𝐹 = ((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺)) |
65 | 64 | eqcomd 2805 |
. . . . . 6
⊢ (𝜑 → ((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺) = 𝐹) |
66 | 11 | ply1crng 19890 |
. . . . . . . . 9
⊢ (𝑅 ∈ CRing → 𝑃 ∈ CRing) |
67 | 20, 66 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑃 ∈ CRing) |
68 | | crngring 18874 |
. . . . . . . 8
⊢ (𝑃 ∈ CRing → 𝑃 ∈ Ring) |
69 | 67, 68 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑃 ∈ Ring) |
70 | 11, 12, 37 | mon1pcl 24245 |
. . . . . . . 8
⊢ (𝐺 ∈
(Monic1p‘𝑅) → 𝐺 ∈ 𝐵) |
71 | 41, 70 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐺 ∈ 𝐵) |
72 | 12, 61, 53 | ringlz 18903 |
. . . . . . 7
⊢ ((𝑃 ∈ Ring ∧ 𝐺 ∈ 𝐵) → ( 0 (.r‘𝑃)𝐺) = 0 ) |
73 | 69, 71, 72 | syl2anc 580 |
. . . . . 6
⊢ (𝜑 → ( 0 (.r‘𝑃)𝐺) = 0 ) |
74 | 56, 65, 73 | 3netr4d 3048 |
. . . . 5
⊢ (𝜑 → ((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺) ≠ ( 0 (.r‘𝑃)𝐺)) |
75 | | oveq1 6885 |
. . . . . 6
⊢ ((𝐹(quot1p‘𝑅)𝐺) = 0 → ((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺) = ( 0 (.r‘𝑃)𝐺)) |
76 | 75 | necon3i 3003 |
. . . . 5
⊢ (((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺) ≠ ( 0 (.r‘𝑃)𝐺) → (𝐹(quot1p‘𝑅)𝐺) ≠ 0 ) |
77 | 74, 76 | syl 17 |
. . . 4
⊢ (𝜑 → (𝐹(quot1p‘𝑅)𝐺) ≠ 0 ) |
78 | 38, 11, 53, 12 | deg1nn0cl 24189 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ (𝐹(quot1p‘𝑅)𝐺) ∈ 𝐵 ∧ (𝐹(quot1p‘𝑅)𝐺) ≠ 0 ) → (𝐷‘(𝐹(quot1p‘𝑅)𝐺)) ∈
ℕ0) |
79 | 9, 47, 77, 78 | syl3anc 1491 |
. . 3
⊢ (𝜑 → (𝐷‘(𝐹(quot1p‘𝑅)𝐺)) ∈
ℕ0) |
80 | 79 | nn0cnd 11642 |
. 2
⊢ (𝜑 → (𝐷‘(𝐹(quot1p‘𝑅)𝐺)) ∈ ℂ) |
81 | 49 | nn0cnd 11642 |
. 2
⊢ (𝜑 → 𝑁 ∈ ℂ) |
82 | 12, 61 | crngcom 18878 |
. . . . . . 7
⊢ ((𝑃 ∈ CRing ∧ (𝐹(quot1p‘𝑅)𝐺) ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → ((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺) = (𝐺(.r‘𝑃)(𝐹(quot1p‘𝑅)𝐺))) |
83 | 67, 47, 71, 82 | syl3anc 1491 |
. . . . . 6
⊢ (𝜑 → ((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺) = (𝐺(.r‘𝑃)(𝐹(quot1p‘𝑅)𝐺))) |
84 | 64, 83 | eqtrd 2833 |
. . . . 5
⊢ (𝜑 → 𝐹 = (𝐺(.r‘𝑃)(𝐹(quot1p‘𝑅)𝐺))) |
85 | 84 | fveq2d 6415 |
. . . 4
⊢ (𝜑 → (𝐷‘𝐹) = (𝐷‘(𝐺(.r‘𝑃)(𝐹(quot1p‘𝑅)𝐺)))) |
86 | | eqid 2799 |
. . . . 5
⊢
(RLReg‘𝑅) =
(RLReg‘𝑅) |
87 | 40 | simp2d 1174 |
. . . . . . 7
⊢ (𝜑 → (𝐷‘𝐺) = 1) |
88 | | 1nn0 11598 |
. . . . . . 7
⊢ 1 ∈
ℕ0 |
89 | 87, 88 | syl6eqel 2886 |
. . . . . 6
⊢ (𝜑 → (𝐷‘𝐺) ∈
ℕ0) |
90 | 38, 11, 53, 12 | deg1nn0clb 24191 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐺 ∈ 𝐵) → (𝐺 ≠ 0 ↔ (𝐷‘𝐺) ∈
ℕ0)) |
91 | 9, 71, 90 | syl2anc 580 |
. . . . . 6
⊢ (𝜑 → (𝐺 ≠ 0 ↔ (𝐷‘𝐺) ∈
ℕ0)) |
92 | 89, 91 | mpbird 249 |
. . . . 5
⊢ (𝜑 → 𝐺 ≠ 0 ) |
93 | | eqid 2799 |
. . . . . . . 8
⊢
(Unit‘𝑅) =
(Unit‘𝑅) |
94 | 86, 93 | unitrrg 19616 |
. . . . . . 7
⊢ (𝑅 ∈ Ring →
(Unit‘𝑅) ⊆
(RLReg‘𝑅)) |
95 | 9, 94 | syl 17 |
. . . . . 6
⊢ (𝜑 → (Unit‘𝑅) ⊆ (RLReg‘𝑅)) |
96 | 38, 93, 42 | uc1pldg 24249 |
. . . . . . 7
⊢ (𝐺 ∈
(Unic1p‘𝑅)
→ ((coe1‘𝐺)‘(𝐷‘𝐺)) ∈ (Unit‘𝑅)) |
97 | 44, 96 | syl 17 |
. . . . . 6
⊢ (𝜑 →
((coe1‘𝐺)‘(𝐷‘𝐺)) ∈ (Unit‘𝑅)) |
98 | 95, 97 | sseldd 3799 |
. . . . 5
⊢ (𝜑 →
((coe1‘𝐺)‘(𝐷‘𝐺)) ∈ (RLReg‘𝑅)) |
99 | 38, 11, 86, 12, 61, 53, 9, 71, 92, 98, 47, 77 | deg1mul2 24215 |
. . . 4
⊢ (𝜑 → (𝐷‘(𝐺(.r‘𝑃)(𝐹(quot1p‘𝑅)𝐺))) = ((𝐷‘𝐺) + (𝐷‘(𝐹(quot1p‘𝑅)𝐺)))) |
100 | 85, 48, 99 | 3eqtr3d 2841 |
. . 3
⊢ (𝜑 → (𝑁 + 1) = ((𝐷‘𝐺) + (𝐷‘(𝐹(quot1p‘𝑅)𝐺)))) |
101 | | ax-1cn 10282 |
. . . 4
⊢ 1 ∈
ℂ |
102 | | addcom 10512 |
. . . 4
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → (𝑁 + 1) =
(1 + 𝑁)) |
103 | 81, 101, 102 | sylancl 581 |
. . 3
⊢ (𝜑 → (𝑁 + 1) = (1 + 𝑁)) |
104 | 87 | oveq1d 6893 |
. . 3
⊢ (𝜑 → ((𝐷‘𝐺) + (𝐷‘(𝐹(quot1p‘𝑅)𝐺))) = (1 + (𝐷‘(𝐹(quot1p‘𝑅)𝐺)))) |
105 | 100, 103,
104 | 3eqtr3rd 2842 |
. 2
⊢ (𝜑 → (1 + (𝐷‘(𝐹(quot1p‘𝑅)𝐺))) = (1 + 𝑁)) |
106 | 1, 80, 81, 105 | addcanad 10531 |
1
⊢ (𝜑 → (𝐷‘(𝐹(quot1p‘𝑅)𝐺)) = 𝑁) |