Metamath Proof Explorer

Theorem fta1glem1

Description: Lemma for fta1g . (Contributed by Mario Carneiro, 7-Jun-2016)

Ref Expression
Hypotheses 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 fta1glem1 ( 𝜑 → ( 𝐷 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) = 𝑁 )

Proof

Step Hyp Ref Expression
1 fta1g.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 fta1g.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
3 fta1g.d ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
4 fta1g.o ⊢ 𝑂 = ( eval1 ‘ 𝑅 )
5 fta1g.w ⊢ 𝑊 = ( 0g ‘ 𝑅 )
6 fta1g.z ⊢ 0 = ( 0g ‘ 𝑃 )
7 fta1g.1 ⊢ ( 𝜑 → 𝑅 ∈ IDomn )
8 fta1g.2 ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
9 fta1glem.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
10 fta1glem.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
11 fta1glem.m ⊢ − = ( -g ‘ 𝑃 )
12 fta1glem.a ⊢ 𝐴 = ( algSc ‘ 𝑃 )
13 fta1glem.g ⊢ 𝐺 = ( 𝑋 − ( 𝐴 ‘ 𝑇 ) )
14 fta1glem.3 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
15 fta1glem.4 ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) = ( 𝑁 + 1 ) )
16 fta1glem.5 ⊢ ( 𝜑 → 𝑇 ∈ ( ◡ ( 𝑂 ‘ 𝐹 ) “ { 𝑊 } ) )
17 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
18 isidom ⊢ ( 𝑅 ∈ IDomn ↔ ( 𝑅 ∈ CRing ∧ 𝑅 ∈ Domn ) )
19 domnnzr ⊢ ( 𝑅 ∈ Domn → 𝑅 ∈ NzRing )
20 18 19 simplbiim ⊢ ( 𝑅 ∈ IDomn → 𝑅 ∈ NzRing )
21 7 20 syl ⊢ ( 𝜑 → 𝑅 ∈ NzRing )
22 nzrring ⊢ ( 𝑅 ∈ NzRing → 𝑅 ∈ Ring )
23 21 22 syl ⊢ ( 𝜑 → 𝑅 ∈ Ring )
24 18 simplbi ⊢ ( 𝑅 ∈ IDomn → 𝑅 ∈ CRing )
25 7 24 syl ⊢ ( 𝜑 → 𝑅 ∈ CRing )
26 eqid ⊢ ( 𝑅 ↑s 𝐾 ) = ( 𝑅 ↑s 𝐾 )
27 eqid ⊢ ( Base ‘ ( 𝑅 ↑s 𝐾 ) ) = ( Base ‘ ( 𝑅 ↑s 𝐾 ) )
28 9 fvexi ⊢ 𝐾 ∈ V
29 28 a1i ⊢ ( 𝜑 → 𝐾 ∈ V )
30 4 1 26 9 evl1rhm ⊢ ( 𝑅 ∈ CRing → 𝑂 ∈ ( 𝑃 RingHom ( 𝑅 ↑s 𝐾 ) ) )
31 25 30 syl ⊢ ( 𝜑 → 𝑂 ∈ ( 𝑃 RingHom ( 𝑅 ↑s 𝐾 ) ) )
32 2 27 rhmf ⊢ ( 𝑂 ∈ ( 𝑃 RingHom ( 𝑅 ↑s 𝐾 ) ) → 𝑂 : 𝐵 ⟶ ( Base ‘ ( 𝑅 ↑s 𝐾 ) ) )
33 31 32 syl ⊢ ( 𝜑 → 𝑂 : 𝐵 ⟶ ( Base ‘ ( 𝑅 ↑s 𝐾 ) ) )
34 33 8 ffvelrnd ⊢ ( 𝜑 → ( 𝑂 ‘ 𝐹 ) ∈ ( Base ‘ ( 𝑅 ↑s 𝐾 ) ) )
35 26 9 27 7 29 34 pwselbas ⊢ ( 𝜑 → ( 𝑂 ‘ 𝐹 ) : 𝐾 ⟶ 𝐾 )
36 35 ffnd ⊢ ( 𝜑 → ( 𝑂 ‘ 𝐹 ) Fn 𝐾 )
37 fniniseg ⊢ ( ( 𝑂 ‘ 𝐹 ) Fn 𝐾 → ( 𝑇 ∈ ( ◡ ( 𝑂 ‘ 𝐹 ) “ { 𝑊 } ) ↔ ( 𝑇 ∈ 𝐾 ∧ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑇 ) = 𝑊 ) ) )
38 36 37 syl ⊢ ( 𝜑 → ( 𝑇 ∈ ( ◡ ( 𝑂 ‘ 𝐹 ) “ { 𝑊 } ) ↔ ( 𝑇 ∈ 𝐾 ∧ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑇 ) = 𝑊 ) ) )
39 16 38 mpbid ⊢ ( 𝜑 → ( 𝑇 ∈ 𝐾 ∧ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑇 ) = 𝑊 ) )
40 39 simpld ⊢ ( 𝜑 → 𝑇 ∈ 𝐾 )
41 eqid ⊢ ( Monic1p ‘ 𝑅 ) = ( Monic1p ‘ 𝑅 )
42 1 2 9 10 11 12 13 4 21 25 40 41 3 5 ply1remlem ⊢ ( 𝜑 → ( 𝐺 ∈ ( Monic1p ‘ 𝑅 ) ∧ ( 𝐷 ‘ 𝐺 ) = 1 ∧ ( ◡ ( 𝑂 ‘ 𝐺 ) “ { 𝑊 } ) = { 𝑇 } ) )
43 42 simp1d ⊢ ( 𝜑 → 𝐺 ∈ ( Monic1p ‘ 𝑅 ) )
44 eqid ⊢ ( Unic1p ‘ 𝑅 ) = ( Unic1p ‘ 𝑅 )
45 44 41 mon1puc1p ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ ( Monic1p ‘ 𝑅 ) ) → 𝐺 ∈ ( Unic1p ‘ 𝑅 ) )
46 23 43 45 syl2anc ⊢ ( 𝜑 → 𝐺 ∈ ( Unic1p ‘ 𝑅 ) )
47 eqid ⊢ ( quot1p ‘ 𝑅 ) = ( quot1p ‘ 𝑅 )
48 47 1 2 44 q1pcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ( Unic1p ‘ 𝑅 ) ) → ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ∈ 𝐵 )
49 23 8 46 48 syl3anc ⊢ ( 𝜑 → ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ∈ 𝐵 )
50 peano2nn0 ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ0 )
51 14 50 syl ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℕ0 )
52 15 51 eqeltrd ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) ∈ ℕ0 )
53 3 1 6 2 deg1nn0clb ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ) → ( 𝐹 ≠ 0 ↔ ( 𝐷 ‘ 𝐹 ) ∈ ℕ0 ) )
54 23 8 53 syl2anc ⊢ ( 𝜑 → ( 𝐹 ≠ 0 ↔ ( 𝐷 ‘ 𝐹 ) ∈ ℕ0 ) )
55 52 54 mpbird ⊢ ( 𝜑 → 𝐹 ≠ 0 )
56 39 simprd ⊢ ( 𝜑 → ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑇 ) = 𝑊 )
57 eqid ⊢ ( ∥r ‘ 𝑃 ) = ( ∥r ‘ 𝑃 )
58 1 2 9 10 11 12 13 4 21 25 40 8 5 57 facth1 ⊢ ( 𝜑 → ( 𝐺 ( ∥r ‘ 𝑃 ) 𝐹 ↔ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑇 ) = 𝑊 ) )
59 56 58 mpbird ⊢ ( 𝜑 → 𝐺 ( ∥r ‘ 𝑃 ) 𝐹 )
60 eqid ⊢ ( .r ‘ 𝑃 ) = ( .r ‘ 𝑃 )
61 1 57 2 44 60 47 dvdsq1p ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ( Unic1p ‘ 𝑅 ) ) → ( 𝐺 ( ∥r ‘ 𝑃 ) 𝐹 ↔ 𝐹 = ( ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ( .r ‘ 𝑃 ) 𝐺 ) ) )
62 23 8 46 61 syl3anc ⊢ ( 𝜑 → ( 𝐺 ( ∥r ‘ 𝑃 ) 𝐹 ↔ 𝐹 = ( ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ( .r ‘ 𝑃 ) 𝐺 ) ) )
63 59 62 mpbid ⊢ ( 𝜑 → 𝐹 = ( ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ( .r ‘ 𝑃 ) 𝐺 ) )
64 63 eqcomd ⊢ ( 𝜑 → ( ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ( .r ‘ 𝑃 ) 𝐺 ) = 𝐹 )
65 1 ply1crng ⊢ ( 𝑅 ∈ CRing → 𝑃 ∈ CRing )
66 25 65 syl ⊢ ( 𝜑 → 𝑃 ∈ CRing )
67 crngring ⊢ ( 𝑃 ∈ CRing → 𝑃 ∈ Ring )
68 66 67 syl ⊢ ( 𝜑 → 𝑃 ∈ Ring )
69 1 2 41 mon1pcl ⊢ ( 𝐺 ∈ ( Monic1p ‘ 𝑅 ) → 𝐺 ∈ 𝐵 )
70 43 69 syl ⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
71 2 60 6 ringlz ⊢ ( ( 𝑃 ∈ Ring ∧ 𝐺 ∈ 𝐵 ) → ( 0 ( .r ‘ 𝑃 ) 𝐺 ) = 0 )
72 68 70 71 syl2anc ⊢ ( 𝜑 → ( 0 ( .r ‘ 𝑃 ) 𝐺 ) = 0 )
73 55 64 72 3netr4d ⊢ ( 𝜑 → ( ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ( .r ‘ 𝑃 ) 𝐺 ) ≠ ( 0 ( .r ‘ 𝑃 ) 𝐺 ) )
74 oveq1 ⊢ ( ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) = 0 → ( ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ( .r ‘ 𝑃 ) 𝐺 ) = ( 0 ( .r ‘ 𝑃 ) 𝐺 ) )
75 74 necon3i ⊢ ( ( ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ( .r ‘ 𝑃 ) 𝐺 ) ≠ ( 0 ( .r ‘ 𝑃 ) 𝐺 ) → ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ≠ 0 )
76 73 75 syl ⊢ ( 𝜑 → ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ≠ 0 )
77 3 1 6 2 deg1nn0cl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ∈ 𝐵 ∧ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ≠ 0 ) → ( 𝐷 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) ∈ ℕ0 )
78 23 49 76 77 syl3anc ⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) ∈ ℕ0 )
79 78 nn0cnd ⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) ∈ ℂ )
80 14 nn0cnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
81 2 60 crngcom ⊢ ( ( 𝑃 ∈ CRing ∧ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ( .r ‘ 𝑃 ) 𝐺 ) = ( 𝐺 ( .r ‘ 𝑃 ) ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) )
82 66 49 70 81 syl3anc ⊢ ( 𝜑 → ( ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ( .r ‘ 𝑃 ) 𝐺 ) = ( 𝐺 ( .r ‘ 𝑃 ) ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) )
83 63 82 eqtrd ⊢ ( 𝜑 → 𝐹 = ( 𝐺 ( .r ‘ 𝑃 ) ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) )
84 83 fveq2d ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) = ( 𝐷 ‘ ( 𝐺 ( .r ‘ 𝑃 ) ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) ) )
85 eqid ⊢ ( RLReg ‘ 𝑅 ) = ( RLReg ‘ 𝑅 )
86 42 simp2d ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐺 ) = 1 )
87 1nn0 ⊢ 1 ∈ ℕ0
88 86 87 eqeltrdi ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐺 ) ∈ ℕ0 )
89 3 1 6 2 deg1nn0clb ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ 𝐵 ) → ( 𝐺 ≠ 0 ↔ ( 𝐷 ‘ 𝐺 ) ∈ ℕ0 ) )
90 23 70 89 syl2anc ⊢ ( 𝜑 → ( 𝐺 ≠ 0 ↔ ( 𝐷 ‘ 𝐺 ) ∈ ℕ0 ) )
91 88 90 mpbird ⊢ ( 𝜑 → 𝐺 ≠ 0 )
92 eqid ⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
93 85 92 unitrrg ⊢ ( 𝑅 ∈ Ring → ( Unit ‘ 𝑅 ) ⊆ ( RLReg ‘ 𝑅 ) )
94 23 93 syl ⊢ ( 𝜑 → ( Unit ‘ 𝑅 ) ⊆ ( RLReg ‘ 𝑅 ) )
95 3 92 44 uc1pldg ⊢ ( 𝐺 ∈ ( Unic1p ‘ 𝑅 ) → ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) ∈ ( Unit ‘ 𝑅 ) )
96 46 95 syl ⊢ ( 𝜑 → ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) ∈ ( Unit ‘ 𝑅 ) )
97 94 96 sseldd ⊢ ( 𝜑 → ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) ∈ ( RLReg ‘ 𝑅 ) )
98 3 1 85 2 60 6 23 70 91 97 49 76 deg1mul2 ⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐺 ( .r ‘ 𝑃 ) ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) ) = ( ( 𝐷 ‘ 𝐺 ) + ( 𝐷 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) ) )
99 84 15 98 3eqtr3d ⊢ ( 𝜑 → ( 𝑁 + 1 ) = ( ( 𝐷 ‘ 𝐺 ) + ( 𝐷 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) ) )
100 ax-1cn ⊢ 1 ∈ ℂ
101 addcom ⊢ ( ( 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 𝑁 + 1 ) = ( 1 + 𝑁 ) )
102 80 100 101 sylancl ⊢ ( 𝜑 → ( 𝑁 + 1 ) = ( 1 + 𝑁 ) )
103 86 oveq1d ⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝐺 ) + ( 𝐷 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) ) = ( 1 + ( 𝐷 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) ) )
104 99 102 103 3eqtr3rd ⊢ ( 𝜑 → ( 1 + ( 𝐷 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) ) = ( 1 + 𝑁 ) )
105 17 79 80 104 addcanad ⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐹 ( quot1p ‘ 𝑅 ) 𝐺 ) ) = 𝑁 )