This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fta1glem1

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

Ref Expression
Hypotheses fta1g.p 
|- P = ( Poly1 ` R )
fta1g.b 
|- B = ( Base ` P )
fta1g.d 
|- D = ( deg1 ` R )
fta1g.o 
|- O = ( eval1 ` R )
fta1g.w 
|- W = ( 0g ` R )
fta1g.z 
|- .0. = ( 0g ` P )
fta1g.1 
|- ( ph -> R e. IDomn )
fta1g.2 
|- ( ph -> F e. B )
fta1glem.k 
|- K = ( Base ` R )
fta1glem.x 
|- X = ( var1 ` R )
fta1glem.m 
|- .- = ( -g ` P )
fta1glem.a 
|- A = ( algSc ` P )
fta1glem.g 
|- G = ( X .- ( A ` T ) )
fta1glem.3 
|- ( ph -> N e. NN0 )
fta1glem.4 
|- ( ph -> ( D ` F ) = ( N + 1 ) )
fta1glem.5 
|- ( ph -> T e. ( `' ( O ` F ) " { W } ) )
Assertion fta1glem1 
|- ( ph -> ( D ` ( F ( quot1p ` R ) G ) ) = N )

Proof

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