Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  fta1glem1 Structured version   Visualization version   GIF version

Theorem fta1glem1 24810
 Description: Lemma for fta1g 24812. (Contributed by Mario Carneiro, 7-Jun-2016.)
Hypotheses
Ref Expression
fta1g.p 𝑃 = (Poly1𝑅)
fta1g.b 𝐵 = (Base‘𝑃)
fta1g.d 𝐷 = ( deg1𝑅)
fta1g.o 𝑂 = (eval1𝑅)
fta1g.w 𝑊 = (0g𝑅)
fta1g.z 0 = (0g𝑃)
fta1g.1 (𝜑𝑅 ∈ IDomn)
fta1g.2 (𝜑𝐹𝐵)
fta1glem.k 𝐾 = (Base‘𝑅)
fta1glem.x 𝑋 = (var1𝑅)
fta1glem.m = (-g𝑃)
fta1glem.a 𝐴 = (algSc‘𝑃)
fta1glem.g 𝐺 = (𝑋 (𝐴𝑇))
fta1glem.3 (𝜑𝑁 ∈ ℕ0)
fta1glem.4 (𝜑 → (𝐷𝐹) = (𝑁 + 1))
fta1glem.5 (𝜑𝑇 ∈ ((𝑂𝐹) “ {𝑊}))
Assertion
Ref Expression
fta1glem1 (𝜑 → (𝐷‘(𝐹(quot1p𝑅)𝐺)) = 𝑁)

Proof of Theorem fta1glem1
StepHypRef Expression
1 1cnd 10643 . 2 (𝜑 → 1 ∈ ℂ)
2 fta1g.1 . . . . . 6 (𝜑𝑅 ∈ IDomn)
3 isidom 20091 . . . . . . 7 (𝑅 ∈ IDomn ↔ (𝑅 ∈ CRing ∧ 𝑅 ∈ Domn))
4 domnnzr 20082 . . . . . . 7 (𝑅 ∈ Domn → 𝑅 ∈ NzRing)
53, 4simplbiim 508 . . . . . 6 (𝑅 ∈ IDomn → 𝑅 ∈ NzRing)
62, 5syl 17 . . . . 5 (𝜑𝑅 ∈ NzRing)
7 nzrring 20048 . . . . 5 (𝑅 ∈ NzRing → 𝑅 ∈ Ring)
86, 7syl 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𝑅)
183simplbi 501 . . . . . . . . 9 (𝑅 ∈ IDomn → 𝑅 ∈ CRing)
192, 18syl 17 . . . . . . . 8 (𝜑𝑅 ∈ CRing)
20 fta1glem.5 . . . . . . . . . 10 (𝜑𝑇 ∈ ((𝑂𝐹) “ {𝑊}))
21 eqid 2798 . . . . . . . . . . . . 13 (𝑅s 𝐾) = (𝑅s 𝐾)
22 eqid 2798 . . . . . . . . . . . . 13 (Base‘(𝑅s 𝐾)) = (Base‘(𝑅s 𝐾))
2312fvexi 6669 . . . . . . . . . . . . . 14 𝐾 ∈ V
2423a1i 11 . . . . . . . . . . . . 13 (𝜑𝐾 ∈ V)
2517, 10, 21, 12evl1rhm 20997 . . . . . . . . . . . . . . . 16 (𝑅 ∈ CRing → 𝑂 ∈ (𝑃 RingHom (𝑅s 𝐾)))
2619, 25syl 17 . . . . . . . . . . . . . . 15 (𝜑𝑂 ∈ (𝑃 RingHom (𝑅s 𝐾)))
2711, 22rhmf 19495 . . . . . . . . . . . . . . 15 (𝑂 ∈ (𝑃 RingHom (𝑅s 𝐾)) → 𝑂:𝐵⟶(Base‘(𝑅s 𝐾)))
2826, 27syl 17 . . . . . . . . . . . . . 14 (𝜑𝑂:𝐵⟶(Base‘(𝑅s 𝐾)))
2928, 9ffvelrnd 6839 . . . . . . . . . . . . 13 (𝜑 → (𝑂𝐹) ∈ (Base‘(𝑅s 𝐾)))
3021, 12, 22, 2, 24, 29pwselbas 16774 . . . . . . . . . . . 12 (𝜑 → (𝑂𝐹):𝐾𝐾)
3130ffnd 6496 . . . . . . . . . . 11 (𝜑 → (𝑂𝐹) Fn 𝐾)
32 fniniseg 6817 . . . . . . . . . . 11 ((𝑂𝐹) Fn 𝐾 → (𝑇 ∈ ((𝑂𝐹) “ {𝑊}) ↔ (𝑇𝐾 ∧ ((𝑂𝐹)‘𝑇) = 𝑊)))
3331, 32syl 17 . . . . . . . . . 10 (𝜑 → (𝑇 ∈ ((𝑂𝐹) “ {𝑊}) ↔ (𝑇𝐾 ∧ ((𝑂𝐹)‘𝑇) = 𝑊)))
3420, 33mpbid 235 . . . . . . . . 9 (𝜑 → (𝑇𝐾 ∧ ((𝑂𝐹)‘𝑇) = 𝑊))
3534simpld 498 . . . . . . . 8 (𝜑𝑇𝐾)
36 eqid 2798 . . . . . . . 8 (Monic1p𝑅) = (Monic1p𝑅)
37 fta1g.d . . . . . . . 8 𝐷 = ( deg1𝑅)
38 fta1g.w . . . . . . . 8 𝑊 = (0g𝑅)
3910, 11, 12, 13, 14, 15, 16, 17, 6, 19, 35, 36, 37, 38ply1remlem 24807 . . . . . . 7 (𝜑 → (𝐺 ∈ (Monic1p𝑅) ∧ (𝐷𝐺) = 1 ∧ ((𝑂𝐺) “ {𝑊}) = {𝑇}))
4039simp1d 1139 . . . . . 6 (𝜑𝐺 ∈ (Monic1p𝑅))
41 eqid 2798 . . . . . . 7 (Unic1p𝑅) = (Unic1p𝑅)
4241, 36mon1puc1p 24795 . . . . . 6 ((𝑅 ∈ Ring ∧ 𝐺 ∈ (Monic1p𝑅)) → 𝐺 ∈ (Unic1p𝑅))
438, 40, 42syl2anc 587 . . . . 5 (𝜑𝐺 ∈ (Unic1p𝑅))
44 eqid 2798 . . . . . 6 (quot1p𝑅) = (quot1p𝑅)
4544, 10, 11, 41q1pcl 24800 . . . . 5 ((𝑅 ∈ Ring ∧ 𝐹𝐵𝐺 ∈ (Unic1p𝑅)) → (𝐹(quot1p𝑅)𝐺) ∈ 𝐵)
468, 9, 43, 45syl3anc 1368 . . . 4 (𝜑 → (𝐹(quot1p𝑅)𝐺) ∈ 𝐵)
47 fta1glem.4 . . . . . . . 8 (𝜑 → (𝐷𝐹) = (𝑁 + 1))
48 fta1glem.3 . . . . . . . . 9 (𝜑𝑁 ∈ ℕ0)
49 peano2nn0 11943 . . . . . . . . 9 (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℕ0)
5048, 49syl 17 . . . . . . . 8 (𝜑 → (𝑁 + 1) ∈ ℕ0)
5147, 50eqeltrd 2890 . . . . . . 7 (𝜑 → (𝐷𝐹) ∈ ℕ0)
52 fta1g.z . . . . . . . . 9 0 = (0g𝑃)
5337, 10, 52, 11deg1nn0clb 24735 . . . . . . . 8 ((𝑅 ∈ Ring ∧ 𝐹𝐵) → (𝐹0 ↔ (𝐷𝐹) ∈ ℕ0))
548, 9, 53syl2anc 587 . . . . . . 7 (𝜑 → (𝐹0 ↔ (𝐷𝐹) ∈ ℕ0))
5551, 54mpbird 260 . . . . . 6 (𝜑𝐹0 )
5634simprd 499 . . . . . . . . 9 (𝜑 → ((𝑂𝐹)‘𝑇) = 𝑊)
57 eqid 2798 . . . . . . . . . 10 (∥r𝑃) = (∥r𝑃)
5810, 11, 12, 13, 14, 15, 16, 17, 6, 19, 35, 9, 38, 57facth1 24809 . . . . . . . . 9 (𝜑 → (𝐺(∥r𝑃)𝐹 ↔ ((𝑂𝐹)‘𝑇) = 𝑊))
5956, 58mpbird 260 . . . . . . . 8 (𝜑𝐺(∥r𝑃)𝐹)
60 eqid 2798 . . . . . . . . . 10 (.r𝑃) = (.r𝑃)
6110, 57, 11, 41, 60, 44dvdsq1p 24805 . . . . . . . . 9 ((𝑅 ∈ Ring ∧ 𝐹𝐵𝐺 ∈ (Unic1p𝑅)) → (𝐺(∥r𝑃)𝐹𝐹 = ((𝐹(quot1p𝑅)𝐺)(.r𝑃)𝐺)))
628, 9, 43, 61syl3anc 1368 . . . . . . . 8 (𝜑 → (𝐺(∥r𝑃)𝐹𝐹 = ((𝐹(quot1p𝑅)𝐺)(.r𝑃)𝐺)))
6359, 62mpbid 235 . . . . . . 7 (𝜑𝐹 = ((𝐹(quot1p𝑅)𝐺)(.r𝑃)𝐺))
6463eqcomd 2804 . . . . . 6 (𝜑 → ((𝐹(quot1p𝑅)𝐺)(.r𝑃)𝐺) = 𝐹)
6510ply1crng 20868 . . . . . . . . 9 (𝑅 ∈ CRing → 𝑃 ∈ CRing)
6619, 65syl 17 . . . . . . . 8 (𝜑𝑃 ∈ CRing)
67 crngring 19323 . . . . . . . 8 (𝑃 ∈ CRing → 𝑃 ∈ Ring)
6866, 67syl 17 . . . . . . 7 (𝜑𝑃 ∈ Ring)
6910, 11, 36mon1pcl 24789 . . . . . . . 8 (𝐺 ∈ (Monic1p𝑅) → 𝐺𝐵)
7040, 69syl 17 . . . . . . 7 (𝜑𝐺𝐵)
7111, 60, 52ringlz 19354 . . . . . . 7 ((𝑃 ∈ Ring ∧ 𝐺𝐵) → ( 0 (.r𝑃)𝐺) = 0 )
7268, 70, 71syl2anc 587 . . . . . 6 (𝜑 → ( 0 (.r𝑃)𝐺) = 0 )
7355, 64, 723netr4d 3064 . . . . 5 (𝜑 → ((𝐹(quot1p𝑅)𝐺)(.r𝑃)𝐺) ≠ ( 0 (.r𝑃)𝐺))
74 oveq1 7152 . . . . . 6 ((𝐹(quot1p𝑅)𝐺) = 0 → ((𝐹(quot1p𝑅)𝐺)(.r𝑃)𝐺) = ( 0 (.r𝑃)𝐺))
7574necon3i 3019 . . . . 5 (((𝐹(quot1p𝑅)𝐺)(.r𝑃)𝐺) ≠ ( 0 (.r𝑃)𝐺) → (𝐹(quot1p𝑅)𝐺) ≠ 0 )
7673, 75syl 17 . . . 4 (𝜑 → (𝐹(quot1p𝑅)𝐺) ≠ 0 )
7737, 10, 52, 11deg1nn0cl 24733 . . . 4 ((𝑅 ∈ Ring ∧ (𝐹(quot1p𝑅)𝐺) ∈ 𝐵 ∧ (𝐹(quot1p𝑅)𝐺) ≠ 0 ) → (𝐷‘(𝐹(quot1p𝑅)𝐺)) ∈ ℕ0)
788, 46, 76, 77syl3anc 1368 . . 3 (𝜑 → (𝐷‘(𝐹(quot1p𝑅)𝐺)) ∈ ℕ0)
7978nn0cnd 11965 . 2 (𝜑 → (𝐷‘(𝐹(quot1p𝑅)𝐺)) ∈ ℂ)
8048nn0cnd 11965 . 2 (𝜑𝑁 ∈ ℂ)
8111, 60crngcom 19329 . . . . . . 7 ((𝑃 ∈ CRing ∧ (𝐹(quot1p𝑅)𝐺) ∈ 𝐵𝐺𝐵) → ((𝐹(quot1p𝑅)𝐺)(.r𝑃)𝐺) = (𝐺(.r𝑃)(𝐹(quot1p𝑅)𝐺)))
8266, 46, 70, 81syl3anc 1368 . . . . . 6 (𝜑 → ((𝐹(quot1p𝑅)𝐺)(.r𝑃)𝐺) = (𝐺(.r𝑃)(𝐹(quot1p𝑅)𝐺)))
8363, 82eqtrd 2833 . . . . 5 (𝜑𝐹 = (𝐺(.r𝑃)(𝐹(quot1p𝑅)𝐺)))
8483fveq2d 6659 . . . 4 (𝜑 → (𝐷𝐹) = (𝐷‘(𝐺(.r𝑃)(𝐹(quot1p𝑅)𝐺))))
85 eqid 2798 . . . . 5 (RLReg‘𝑅) = (RLReg‘𝑅)
8639simp2d 1140 . . . . . . 7 (𝜑 → (𝐷𝐺) = 1)
87 1nn0 11919 . . . . . . 7 1 ∈ ℕ0
8886, 87eqeltrdi 2898 . . . . . 6 (𝜑 → (𝐷𝐺) ∈ ℕ0)
8937, 10, 52, 11deg1nn0clb 24735 . . . . . . 7 ((𝑅 ∈ Ring ∧ 𝐺𝐵) → (𝐺0 ↔ (𝐷𝐺) ∈ ℕ0))
908, 70, 89syl2anc 587 . . . . . 6 (𝜑 → (𝐺0 ↔ (𝐷𝐺) ∈ ℕ0))
9188, 90mpbird 260 . . . . 5 (𝜑𝐺0 )
92 eqid 2798 . . . . . . . 8 (Unit‘𝑅) = (Unit‘𝑅)
9385, 92unitrrg 20080 . . . . . . 7 (𝑅 ∈ Ring → (Unit‘𝑅) ⊆ (RLReg‘𝑅))
948, 93syl 17 . . . . . 6 (𝜑 → (Unit‘𝑅) ⊆ (RLReg‘𝑅))
9537, 92, 41uc1pldg 24793 . . . . . . 7 (𝐺 ∈ (Unic1p𝑅) → ((coe1𝐺)‘(𝐷𝐺)) ∈ (Unit‘𝑅))
9643, 95syl 17 . . . . . 6 (𝜑 → ((coe1𝐺)‘(𝐷𝐺)) ∈ (Unit‘𝑅))
9794, 96sseldd 3918 . . . . 5 (𝜑 → ((coe1𝐺)‘(𝐷𝐺)) ∈ (RLReg‘𝑅))
9837, 10, 85, 11, 60, 52, 8, 70, 91, 97, 46, 76deg1mul2 24759 . . . 4 (𝜑 → (𝐷‘(𝐺(.r𝑃)(𝐹(quot1p𝑅)𝐺))) = ((𝐷𝐺) + (𝐷‘(𝐹(quot1p𝑅)𝐺))))
9984, 47, 983eqtr3d 2841 . . 3 (𝜑 → (𝑁 + 1) = ((𝐷𝐺) + (𝐷‘(𝐹(quot1p𝑅)𝐺))))
100 ax-1cn 10602 . . . 4 1 ∈ ℂ
101 addcom 10833 . . . 4 ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → (𝑁 + 1) = (1 + 𝑁))
10280, 100, 101sylancl 589 . . 3 (𝜑 → (𝑁 + 1) = (1 + 𝑁))
10386oveq1d 7160 . . 3 (𝜑 → ((𝐷𝐺) + (𝐷‘(𝐹(quot1p𝑅)𝐺))) = (1 + (𝐷‘(𝐹(quot1p𝑅)𝐺))))
10499, 102, 1033eqtr3rd 2842 . 2 (𝜑 → (1 + (𝐷‘(𝐹(quot1p𝑅)𝐺))) = (1 + 𝑁))