Metamath Proof Explorer


Theorem fta1glem1

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

Ref Expression
Hypotheses fta1g.p P = Poly 1 R
fta1g.b B = Base P
fta1g.d D = deg 1 R
fta1g.o O = eval 1 R
fta1g.w W = 0 R
fta1g.z 0 ˙ = 0 P
fta1g.1 φ R IDomn
fta1g.2 φ F B
fta1glem.k K = Base R
fta1glem.x X = var 1 R
fta1glem.m - ˙ = - P
fta1glem.a A = algSc P
fta1glem.g G = X - ˙ A T
fta1glem.3 φ N 0
fta1glem.4 φ D F = N + 1
fta1glem.5 φ T O F -1 W
Assertion fta1glem1 φ D F quot 1p R G = N

Proof

Step Hyp Ref Expression
1 fta1g.p P = Poly 1 R
2 fta1g.b B = Base P
3 fta1g.d D = deg 1 R
4 fta1g.o O = eval 1 R
5 fta1g.w W = 0 R
6 fta1g.z 0 ˙ = 0 P
7 fta1g.1 φ R IDomn
8 fta1g.2 φ F B
9 fta1glem.k K = Base R
10 fta1glem.x X = var 1 R
11 fta1glem.m - ˙ = - P
12 fta1glem.a A = algSc P
13 fta1glem.g G = X - ˙ A T
14 fta1glem.3 φ N 0
15 fta1glem.4 φ D F = N + 1
16 fta1glem.5 φ T O F -1 W
17 1cnd φ 1
18 isidom R IDomn R CRing R Domn
19 domnnzr R Domn R NzRing
20 18 19 simplbiim R IDomn R NzRing
21 7 20 syl φ R NzRing
22 nzrring R NzRing R Ring
23 21 22 syl φ R Ring
24 18 simplbi R IDomn R CRing
25 7 24 syl φ R CRing
26 eqid R 𝑠 K = R 𝑠 K
27 eqid Base R 𝑠 K = Base R 𝑠 K
28 9 fvexi K V
29 28 a1i φ K V
30 4 1 26 9 evl1rhm R CRing O P RingHom R 𝑠 K
31 25 30 syl φ O P RingHom R 𝑠 K
32 2 27 rhmf O P RingHom R 𝑠 K O : B Base R 𝑠 K
33 31 32 syl φ O : B Base R 𝑠 K
34 33 8 ffvelrnd φ O F Base R 𝑠 K
35 26 9 27 7 29 34 pwselbas φ O F : K K
36 35 ffnd φ O F Fn K
37 fniniseg O F Fn K T O F -1 W T K O F T = W
38 36 37 syl φ T O F -1 W T K O F T = W
39 16 38 mpbid φ T K O F T = W
40 39 simpld φ T K
41 eqid Monic 1p R = Monic 1p R
42 1 2 9 10 11 12 13 4 21 25 40 41 3 5 ply1remlem φ G Monic 1p R D G = 1 O G -1 W = T
43 42 simp1d φ G Monic 1p R
44 eqid Unic 1p R = Unic 1p R
45 44 41 mon1puc1p R Ring G Monic 1p R G Unic 1p R
46 23 43 45 syl2anc φ G Unic 1p R
47 eqid quot 1p R = quot 1p R
48 47 1 2 44 q1pcl R Ring F B G Unic 1p R F quot 1p R G B
49 23 8 46 48 syl3anc φ F quot 1p R G B
50 peano2nn0 N 0 N + 1 0
51 14 50 syl φ N + 1 0
52 15 51 eqeltrd φ D F 0
53 3 1 6 2 deg1nn0clb R Ring F B F 0 ˙ D F 0
54 23 8 53 syl2anc φ F 0 ˙ D F 0
55 52 54 mpbird φ F 0 ˙
56 39 simprd φ O F T = W
57 eqid r P = r P
58 1 2 9 10 11 12 13 4 21 25 40 8 5 57 facth1 φ G r P F O F T = W
59 56 58 mpbird φ G r P F
60 eqid P = P
61 1 57 2 44 60 47 dvdsq1p R Ring F B G Unic 1p R G r P F F = F quot 1p R G P G
62 23 8 46 61 syl3anc φ G r P F F = F quot 1p R G P G
63 59 62 mpbid φ F = F quot 1p R G P G
64 63 eqcomd φ F quot 1p R G P G = F
65 1 ply1crng R CRing P CRing
66 25 65 syl φ P CRing
67 crngring P CRing P Ring
68 66 67 syl φ P Ring
69 1 2 41 mon1pcl G Monic 1p R G B
70 43 69 syl φ G B
71 2 60 6 ringlz P Ring G B 0 ˙ P G = 0 ˙
72 68 70 71 syl2anc φ 0 ˙ P G = 0 ˙
73 55 64 72 3netr4d φ F quot 1p R G P G 0 ˙ P G
74 oveq1 F quot 1p R G = 0 ˙ F quot 1p R G P G = 0 ˙ P G
75 74 necon3i F quot 1p R G P G 0 ˙ P G F quot 1p R G 0 ˙
76 73 75 syl φ F quot 1p R G 0 ˙
77 3 1 6 2 deg1nn0cl R Ring F quot 1p R G B F quot 1p R G 0 ˙ D F quot 1p R G 0
78 23 49 76 77 syl3anc φ D F quot 1p R G 0
79 78 nn0cnd φ D F quot 1p R G
80 14 nn0cnd φ N
81 2 60 crngcom P CRing F quot 1p R G B G B F quot 1p R G P G = G P F quot 1p R G
82 66 49 70 81 syl3anc φ F quot 1p R G P G = G P F quot 1p R G
83 63 82 eqtrd φ F = G P F quot 1p R G
84 83 fveq2d φ D F = D G P F quot 1p R G
85 eqid RLReg R = RLReg R
86 42 simp2d φ D G = 1
87 1nn0 1 0
88 86 87 syl6eqel φ D G 0
89 3 1 6 2 deg1nn0clb R Ring G B G 0 ˙ D G 0
90 23 70 89 syl2anc φ G 0 ˙ D G 0
91 88 90 mpbird φ G 0 ˙
92 eqid Unit R = Unit R
93 85 92 unitrrg R Ring Unit R RLReg R
94 23 93 syl φ Unit R RLReg R
95 3 92 44 uc1pldg G Unic 1p R coe 1 G D G Unit R
96 46 95 syl φ coe 1 G D G Unit R
97 94 96 sseldd φ coe 1 G D G RLReg R
98 3 1 85 2 60 6 23 70 91 97 49 76 deg1mul2 φ D G P F quot 1p R G = D G + D F quot 1p R G
99 84 15 98 3eqtr3d φ N + 1 = D G + D F quot 1p R G
100 ax-1cn 1
101 addcom N 1 N + 1 = 1 + N
102 80 100 101 sylancl φ N + 1 = 1 + N
103 86 oveq1d φ D G + D F quot 1p R G = 1 + D F quot 1p R G
104 99 102 103 3eqtr3rd φ 1 + D F quot 1p R G = 1 + N
105 17 79 80 104 addcanad φ D F quot 1p R G = N