Metamath Proof Explorer

Theorem fta1g

Description: The one-sided fundamental theorem of algebra. A polynomial of degree n has at most n roots. Unlike the real fundamental theorem fta , which is only true in CC and other algebraically closed fields, this is true in any integral domain. (Contributed by Mario Carneiro, 12-Jun-2015)

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 )
fta1g.3 
|- ( ph -> F =/= .0. )
Assertion fta1g 
|- ( ph -> ( # ` ( `' ( O ` F ) " { W } ) ) <_ ( D ` F ) )

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 fta1g.3 
 |-  ( ph -> F =/= .0. )
10 eqid 
 |-  ( D ` F ) = ( D ` F )
11 fveqeq2 
 |-  ( f = F -> ( ( D ` f ) = ( D ` F ) <-> ( D ` F ) = ( D ` F ) ) )
12 fveq2 
 |-  ( f = F -> ( O ` f ) = ( O ` F ) )
13 12 cnveqd 
 |-  ( f = F -> `' ( O ` f ) = `' ( O ` F ) )
14 13 imaeq1d 
 |-  ( f = F -> ( `' ( O ` f ) " { W } ) = ( `' ( O ` F ) " { W } ) )
15 14 fveq2d 
 |-  ( f = F -> ( # ` ( `' ( O ` f ) " { W } ) ) = ( # ` ( `' ( O ` F ) " { W } ) ) )
16 fveq2 
 |-  ( f = F -> ( D ` f ) = ( D ` F ) )
17 15 16 breq12d 
 |-  ( f = F -> ( ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) <-> ( # ` ( `' ( O ` F ) " { W } ) ) <_ ( D ` F ) ) )
18 11 17 imbi12d 
 |-  ( f = F -> ( ( ( D ` f ) = ( D ` F ) -> ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) <-> ( ( D ` F ) = ( D ` F ) -> ( # ` ( `' ( O ` F ) " { W } ) ) <_ ( D ` F ) ) ) )
19 isidom 
 |-  ( R e. IDomn <-> ( R e. CRing /\ R e. Domn ) )
20 19 simplbi 
 |-  ( R e. IDomn -> R e. CRing )
21 crngring 
 |-  ( R e. CRing -> R e. Ring )
22 7 20 21 3syl 
 |-  ( ph -> R e. Ring )
23 3 1 6 2 deg1nn0cl 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= .0. ) -> ( D ` F ) e. NN0 )
24 22 8 9 23 syl3anc 
 |-  ( ph -> ( D ` F ) e. NN0 )
25 eqeq2 
 |-  ( x = 0 -> ( ( D ` f ) = x <-> ( D ` f ) = 0 ) )
26 25 imbi1d 
 |-  ( x = 0 -> ( ( ( D ` f ) = x -> ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) <-> ( ( D ` f ) = 0 -> ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) ) )
27 26 ralbidv 
 |-  ( x = 0 -> ( A. f e. B ( ( D ` f ) = x -> ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) <-> A. f e. B ( ( D ` f ) = 0 -> ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) ) )
28 27 imbi2d 
 |-  ( x = 0 -> ( ( R e. IDomn -> A. f e. B ( ( D ` f ) = x -> ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) ) <-> ( R e. IDomn -> A. f e. B ( ( D ` f ) = 0 -> ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) ) ) )
29 eqeq2 
 |-  ( x = d -> ( ( D ` f ) = x <-> ( D ` f ) = d ) )
30 29 imbi1d 
 |-  ( x = d -> ( ( ( D ` f ) = x -> ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) <-> ( ( D ` f ) = d -> ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) ) )
31 30 ralbidv 
 |-  ( x = d -> ( A. f e. B ( ( D ` f ) = x -> ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) <-> A. f e. B ( ( D ` f ) = d -> ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) ) )
32 31 imbi2d 
 |-  ( x = d -> ( ( R e. IDomn -> A. f e. B ( ( D ` f ) = x -> ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) ) <-> ( R e. IDomn -> A. f e. B ( ( D ` f ) = d -> ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) ) ) )
33 eqeq2 
 |-  ( x = ( d + 1 ) -> ( ( D ` f ) = x <-> ( D ` f ) = ( d + 1 ) ) )
34 33 imbi1d 
 |-  ( x = ( d + 1 ) -> ( ( ( D ` f ) = x -> ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) <-> ( ( D ` f ) = ( d + 1 ) -> ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) ) )
35 34 ralbidv 
 |-  ( x = ( d + 1 ) -> ( A. f e. B ( ( D ` f ) = x -> ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) <-> A. f e. B ( ( D ` f ) = ( d + 1 ) -> ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) ) )
36 35 imbi2d 
 |-  ( x = ( d + 1 ) -> ( ( R e. IDomn -> A. f e. B ( ( D ` f ) = x -> ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) ) <-> ( R e. IDomn -> A. f e. B ( ( D ` f ) = ( d + 1 ) -> ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) ) ) )
37 eqeq2 
 |-  ( x = ( D ` F ) -> ( ( D ` f ) = x <-> ( D ` f ) = ( D ` F ) ) )
38 37 imbi1d 
 |-  ( x = ( D ` F ) -> ( ( ( D ` f ) = x -> ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) <-> ( ( D ` f ) = ( D ` F ) -> ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) ) )
39 38 ralbidv 
 |-  ( x = ( D ` F ) -> ( A. f e. B ( ( D ` f ) = x -> ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) <-> A. f e. B ( ( D ` f ) = ( D ` F ) -> ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) ) )
40 39 imbi2d 
 |-  ( x = ( D ` F ) -> ( ( R e. IDomn -> A. f e. B ( ( D ` f ) = x -> ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) ) <-> ( R e. IDomn -> A. f e. B ( ( D ` f ) = ( D ` F ) -> ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) ) ) )
41 simprr 
 |-  ( ( R e. IDomn /\ ( f e. B /\ ( D ` f ) = 0 ) ) -> ( D ` f ) = 0 )
42 0nn0 
 |-  0 e. NN0
43 41 42 eqeltrdi 
 |-  ( ( R e. IDomn /\ ( f e. B /\ ( D ` f ) = 0 ) ) -> ( D ` f ) e. NN0 )
44 20 21 syl 
 |-  ( R e. IDomn -> R e. Ring )
45 simpl 
 |-  ( ( f e. B /\ ( D ` f ) = 0 ) -> f e. B )
46 3 1 6 2 deg1nn0clb 
 |-  ( ( R e. Ring /\ f e. B ) -> ( f =/= .0. <-> ( D ` f ) e. NN0 ) )
47 44 45 46 syl2an 
 |-  ( ( R e. IDomn /\ ( f e. B /\ ( D ` f ) = 0 ) ) -> ( f =/= .0. <-> ( D ` f ) e. NN0 ) )
48 43 47 mpbird 
 |-  ( ( R e. IDomn /\ ( f e. B /\ ( D ` f ) = 0 ) ) -> f =/= .0. )
49 simplrr 
 |-  ( ( ( R e. IDomn /\ ( f e. B /\ ( D ` f ) = 0 ) ) /\ x e. ( `' ( O ` f ) " { W } ) ) -> ( D ` f ) = 0 )
50 0le0 
 |-  0 <_ 0
51 49 50 eqbrtrdi 
 |-  ( ( ( R e. IDomn /\ ( f e. B /\ ( D ` f ) = 0 ) ) /\ x e. ( `' ( O ` f ) " { W } ) ) -> ( D ` f ) <_ 0 )
52 44 ad2antrr 
 |-  ( ( ( R e. IDomn /\ ( f e. B /\ ( D ` f ) = 0 ) ) /\ x e. ( `' ( O ` f ) " { W } ) ) -> R e. Ring )
53 simplrl 
 |-  ( ( ( R e. IDomn /\ ( f e. B /\ ( D ` f ) = 0 ) ) /\ x e. ( `' ( O ` f ) " { W } ) ) -> f e. B )
54 eqid 
 |-  ( algSc ` P ) = ( algSc ` P )
55 3 1 2 54 deg1le0 
 |-  ( ( R e. Ring /\ f e. B ) -> ( ( D ` f ) <_ 0 <-> f = ( ( algSc ` P ) ` ( ( coe1 ` f ) ` 0 ) ) ) )
56 52 53 55 syl2anc 
 |-  ( ( ( R e. IDomn /\ ( f e. B /\ ( D ` f ) = 0 ) ) /\ x e. ( `' ( O ` f ) " { W } ) ) -> ( ( D ` f ) <_ 0 <-> f = ( ( algSc ` P ) ` ( ( coe1 ` f ) ` 0 ) ) ) )
57 51 56 mpbid 
 |-  ( ( ( R e. IDomn /\ ( f e. B /\ ( D ` f ) = 0 ) ) /\ x e. ( `' ( O ` f ) " { W } ) ) -> f = ( ( algSc ` P ) ` ( ( coe1 ` f ) ` 0 ) ) )
58 57 fveq2d 
 |-  ( ( ( R e. IDomn /\ ( f e. B /\ ( D ` f ) = 0 ) ) /\ x e. ( `' ( O ` f ) " { W } ) ) -> ( O ` f ) = ( O ` ( ( algSc ` P ) ` ( ( coe1 ` f ) ` 0 ) ) ) )
59 20 adantr 
 |-  ( ( R e. IDomn /\ ( f e. B /\ ( D ` f ) = 0 ) ) -> R e. CRing )
60 59 adantr 
 |-  ( ( ( R e. IDomn /\ ( f e. B /\ ( D ` f ) = 0 ) ) /\ x e. ( `' ( O ` f ) " { W } ) ) -> R e. CRing )
61 eqid 
 |-  ( coe1 ` f ) = ( coe1 ` f )
62 eqid 
 |-  ( Base ` R ) = ( Base ` R )
63 61 2 1 62 coe1f 
 |-  ( f e. B -> ( coe1 ` f ) : NN0 --> ( Base ` R ) )
64 53 63 syl 
 |-  ( ( ( R e. IDomn /\ ( f e. B /\ ( D ` f ) = 0 ) ) /\ x e. ( `' ( O ` f ) " { W } ) ) -> ( coe1 ` f ) : NN0 --> ( Base ` R ) )
65 ffvelcdm 
 |-  ( ( ( coe1 ` f ) : NN0 --> ( Base ` R ) /\ 0 e. NN0 ) -> ( ( coe1 ` f ) ` 0 ) e. ( Base ` R ) )
66 64 42 65 sylancl 
 |-  ( ( ( R e. IDomn /\ ( f e. B /\ ( D ` f ) = 0 ) ) /\ x e. ( `' ( O ` f ) " { W } ) ) -> ( ( coe1 ` f ) ` 0 ) e. ( Base ` R ) )
67 4 1 62 54 evl1sca 
 |-  ( ( R e. CRing /\ ( ( coe1 ` f ) ` 0 ) e. ( Base ` R ) ) -> ( O ` ( ( algSc ` P ) ` ( ( coe1 ` f ) ` 0 ) ) ) = ( ( Base ` R ) X. { ( ( coe1 ` f ) ` 0 ) } ) )
68 60 66 67 syl2anc 
 |-  ( ( ( R e. IDomn /\ ( f e. B /\ ( D ` f ) = 0 ) ) /\ x e. ( `' ( O ` f ) " { W } ) ) -> ( O ` ( ( algSc ` P ) ` ( ( coe1 ` f ) ` 0 ) ) ) = ( ( Base ` R ) X. { ( ( coe1 ` f ) ` 0 ) } ) )
69 58 68 eqtrd 
 |-  ( ( ( R e. IDomn /\ ( f e. B /\ ( D ` f ) = 0 ) ) /\ x e. ( `' ( O ` f ) " { W } ) ) -> ( O ` f ) = ( ( Base ` R ) X. { ( ( coe1 ` f ) ` 0 ) } ) )
70 69 fveq1d 
 |-  ( ( ( R e. IDomn /\ ( f e. B /\ ( D ` f ) = 0 ) ) /\ x e. ( `' ( O ` f ) " { W } ) ) -> ( ( O ` f ) ` x ) = ( ( ( Base ` R ) X. { ( ( coe1 ` f ) ` 0 ) } ) ` x ) )
71 eqid 
 |-  ( R ^s ( Base ` R ) ) = ( R ^s ( Base ` R ) )
72 eqid 
 |-  ( Base ` ( R ^s ( Base ` R ) ) ) = ( Base ` ( R ^s ( Base ` R ) ) )
73 simpl 
 |-  ( ( R e. IDomn /\ ( f e. B /\ ( D ` f ) = 0 ) ) -> R e. IDomn )
74 fvexd 
 |-  ( ( R e. IDomn /\ ( f e. B /\ ( D ` f ) = 0 ) ) -> ( Base ` R ) e. _V )
75 4 1 71 62 evl1rhm 
 |-  ( R e. CRing -> O e. ( P RingHom ( R ^s ( Base ` R ) ) ) )
76 2 72 rhmf 
 |-  ( O e. ( P RingHom ( R ^s ( Base ` R ) ) ) -> O : B --> ( Base ` ( R ^s ( Base ` R ) ) ) )
77 59 75 76 3syl 
 |-  ( ( R e. IDomn /\ ( f e. B /\ ( D ` f ) = 0 ) ) -> O : B --> ( Base ` ( R ^s ( Base ` R ) ) ) )
78 simprl 
 |-  ( ( R e. IDomn /\ ( f e. B /\ ( D ` f ) = 0 ) ) -> f e. B )
79 77 78 ffvelcdmd 
 |-  ( ( R e. IDomn /\ ( f e. B /\ ( D ` f ) = 0 ) ) -> ( O ` f ) e. ( Base ` ( R ^s ( Base ` R ) ) ) )
80 71 62 72 73 74 79 pwselbas 
 |-  ( ( R e. IDomn /\ ( f e. B /\ ( D ` f ) = 0 ) ) -> ( O ` f ) : ( Base ` R ) --> ( Base ` R ) )
81 ffn 
 |-  ( ( O ` f ) : ( Base ` R ) --> ( Base ` R ) -> ( O ` f ) Fn ( Base ` R ) )
82 fniniseg 
 |-  ( ( O ` f ) Fn ( Base ` R ) -> ( x e. ( `' ( O ` f ) " { W } ) <-> ( x e. ( Base ` R ) /\ ( ( O ` f ) ` x ) = W ) ) )
83 80 81 82 3syl 
 |-  ( ( R e. IDomn /\ ( f e. B /\ ( D ` f ) = 0 ) ) -> ( x e. ( `' ( O ` f ) " { W } ) <-> ( x e. ( Base ` R ) /\ ( ( O ` f ) ` x ) = W ) ) )
84 83 simplbda 
 |-  ( ( ( R e. IDomn /\ ( f e. B /\ ( D ` f ) = 0 ) ) /\ x e. ( `' ( O ` f ) " { W } ) ) -> ( ( O ` f ) ` x ) = W )
85 83 simprbda 
 |-  ( ( ( R e. IDomn /\ ( f e. B /\ ( D ` f ) = 0 ) ) /\ x e. ( `' ( O ` f ) " { W } ) ) -> x e. ( Base ` R ) )
86 fvex 
 |-  ( ( coe1 ` f ) ` 0 ) e. _V
87 86 fvconst2 
 |-  ( x e. ( Base ` R ) -> ( ( ( Base ` R ) X. { ( ( coe1 ` f ) ` 0 ) } ) ` x ) = ( ( coe1 ` f ) ` 0 ) )
88 85 87 syl 
 |-  ( ( ( R e. IDomn /\ ( f e. B /\ ( D ` f ) = 0 ) ) /\ x e. ( `' ( O ` f ) " { W } ) ) -> ( ( ( Base ` R ) X. { ( ( coe1 ` f ) ` 0 ) } ) ` x ) = ( ( coe1 ` f ) ` 0 ) )
89 70 84 88 3eqtr3rd 
 |-  ( ( ( R e. IDomn /\ ( f e. B /\ ( D ` f ) = 0 ) ) /\ x e. ( `' ( O ` f ) " { W } ) ) -> ( ( coe1 ` f ) ` 0 ) = W )
90 89 fveq2d 
 |-  ( ( ( R e. IDomn /\ ( f e. B /\ ( D ` f ) = 0 ) ) /\ x e. ( `' ( O ` f ) " { W } ) ) -> ( ( algSc ` P ) ` ( ( coe1 ` f ) ` 0 ) ) = ( ( algSc ` P ) ` W ) )
91 1 54 5 6 ply1scl0 
 |-  ( R e. Ring -> ( ( algSc ` P ) ` W ) = .0. )
92 52 91 syl 
 |-  ( ( ( R e. IDomn /\ ( f e. B /\ ( D ` f ) = 0 ) ) /\ x e. ( `' ( O ` f ) " { W } ) ) -> ( ( algSc ` P ) ` W ) = .0. )
93 57 90 92 3eqtrd 
 |-  ( ( ( R e. IDomn /\ ( f e. B /\ ( D ` f ) = 0 ) ) /\ x e. ( `' ( O ` f ) " { W } ) ) -> f = .0. )
94 93 ex 
 |-  ( ( R e. IDomn /\ ( f e. B /\ ( D ` f ) = 0 ) ) -> ( x e. ( `' ( O ` f ) " { W } ) -> f = .0. ) )
95 94 necon3ad 
 |-  ( ( R e. IDomn /\ ( f e. B /\ ( D ` f ) = 0 ) ) -> ( f =/= .0. -> -. x e. ( `' ( O ` f ) " { W } ) ) )
96 48 95 mpd 
 |-  ( ( R e. IDomn /\ ( f e. B /\ ( D ` f ) = 0 ) ) -> -. x e. ( `' ( O ` f ) " { W } ) )
97 96 eq0rdv 
 |-  ( ( R e. IDomn /\ ( f e. B /\ ( D ` f ) = 0 ) ) -> ( `' ( O ` f ) " { W } ) = (/) )
98 97 fveq2d 
 |-  ( ( R e. IDomn /\ ( f e. B /\ ( D ` f ) = 0 ) ) -> ( # ` ( `' ( O ` f ) " { W } ) ) = ( # ` (/) ) )
99 hash0 
 |-  ( # ` (/) ) = 0
100 98 99 eqtrdi 
 |-  ( ( R e. IDomn /\ ( f e. B /\ ( D ` f ) = 0 ) ) -> ( # ` ( `' ( O ` f ) " { W } ) ) = 0 )
101 50 41 breqtrrid 
 |-  ( ( R e. IDomn /\ ( f e. B /\ ( D ` f ) = 0 ) ) -> 0 <_ ( D ` f ) )
102 100 101 eqbrtrd 
 |-  ( ( R e. IDomn /\ ( f e. B /\ ( D ` f ) = 0 ) ) -> ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) )
103 102 expr 
 |-  ( ( R e. IDomn /\ f e. B ) -> ( ( D ` f ) = 0 -> ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) )
104 103 ralrimiva 
 |-  ( R e. IDomn -> A. f e. B ( ( D ` f ) = 0 -> ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) )
105 fveqeq2 
 |-  ( f = g -> ( ( D ` f ) = d <-> ( D ` g ) = d ) )
106 fveq2 
 |-  ( f = g -> ( O ` f ) = ( O ` g ) )
107 106 cnveqd 
 |-  ( f = g -> `' ( O ` f ) = `' ( O ` g ) )
108 107 imaeq1d 
 |-  ( f = g -> ( `' ( O ` f ) " { W } ) = ( `' ( O ` g ) " { W } ) )
109 108 fveq2d 
 |-  ( f = g -> ( # ` ( `' ( O ` f ) " { W } ) ) = ( # ` ( `' ( O ` g ) " { W } ) ) )
110 fveq2 
 |-  ( f = g -> ( D ` f ) = ( D ` g ) )
111 109 110 breq12d 
 |-  ( f = g -> ( ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) <-> ( # ` ( `' ( O ` g ) " { W } ) ) <_ ( D ` g ) ) )
112 105 111 imbi12d 
 |-  ( f = g -> ( ( ( D ` f ) = d -> ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) <-> ( ( D ` g ) = d -> ( # ` ( `' ( O ` g ) " { W } ) ) <_ ( D ` g ) ) ) )
113 112 cbvralvw 
 |-  ( A. f e. B ( ( D ` f ) = d -> ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) <-> A. g e. B ( ( D ` g ) = d -> ( # ` ( `' ( O ` g ) " { W } ) ) <_ ( D ` g ) ) )
114 simprr 
 |-  ( ( ( R e. IDomn /\ d e. NN0 ) /\ ( f e. B /\ ( D ` f ) = ( d + 1 ) ) ) -> ( D ` f ) = ( d + 1 ) )
115 peano2nn0 
 |-  ( d e. NN0 -> ( d + 1 ) e. NN0 )
116 115 ad2antlr 
 |-  ( ( ( R e. IDomn /\ d e. NN0 ) /\ ( f e. B /\ ( D ` f ) = ( d + 1 ) ) ) -> ( d + 1 ) e. NN0 )
117 114 116 eqeltrd 
 |-  ( ( ( R e. IDomn /\ d e. NN0 ) /\ ( f e. B /\ ( D ` f ) = ( d + 1 ) ) ) -> ( D ` f ) e. NN0 )
118 117 nn0ge0d 
 |-  ( ( ( R e. IDomn /\ d e. NN0 ) /\ ( f e. B /\ ( D ` f ) = ( d + 1 ) ) ) -> 0 <_ ( D ` f ) )
119 fveq2 
 |-  ( ( `' ( O ` f ) " { W } ) = (/) -> ( # ` ( `' ( O ` f ) " { W } ) ) = ( # ` (/) ) )
120 119 99 eqtrdi 
 |-  ( ( `' ( O ` f ) " { W } ) = (/) -> ( # ` ( `' ( O ` f ) " { W } ) ) = 0 )
121 120 breq1d 
 |-  ( ( `' ( O ` f ) " { W } ) = (/) -> ( ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) <-> 0 <_ ( D ` f ) ) )
122 118 121 syl5ibrcom 
 |-  ( ( ( R e. IDomn /\ d e. NN0 ) /\ ( f e. B /\ ( D ` f ) = ( d + 1 ) ) ) -> ( ( `' ( O ` f ) " { W } ) = (/) -> ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) )
123 122 a1dd 
 |-  ( ( ( R e. IDomn /\ d e. NN0 ) /\ ( f e. B /\ ( D ` f ) = ( d + 1 ) ) ) -> ( ( `' ( O ` f ) " { W } ) = (/) -> ( A. g e. B ( ( D ` g ) = d -> ( # ` ( `' ( O ` g ) " { W } ) ) <_ ( D ` g ) ) -> ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) ) )
124 n0 
 |-  ( ( `' ( O ` f ) " { W } ) =/= (/) <-> E. x x e. ( `' ( O ` f ) " { W } ) )
125 simplll 
 |-  ( ( ( ( R e. IDomn /\ d e. NN0 ) /\ ( f e. B /\ ( D ` f ) = ( d + 1 ) ) ) /\ ( x e. ( `' ( O ` f ) " { W } ) /\ A. g e. B ( ( D ` g ) = d -> ( # ` ( `' ( O ` g ) " { W } ) ) <_ ( D ` g ) ) ) ) -> R e. IDomn )
126 simplrl 
 |-  ( ( ( ( R e. IDomn /\ d e. NN0 ) /\ ( f e. B /\ ( D ` f ) = ( d + 1 ) ) ) /\ ( x e. ( `' ( O ` f ) " { W } ) /\ A. g e. B ( ( D ` g ) = d -> ( # ` ( `' ( O ` g ) " { W } ) ) <_ ( D ` g ) ) ) ) -> f e. B )
127 eqid 
 |-  ( var1 ` R ) = ( var1 ` R )
128 eqid 
 |-  ( -g ` P ) = ( -g ` P )
129 eqid 
 |-  ( ( var1 ` R ) ( -g ` P ) ( ( algSc ` P ) ` x ) ) = ( ( var1 ` R ) ( -g ` P ) ( ( algSc ` P ) ` x ) )
130 simpllr 
 |-  ( ( ( ( R e. IDomn /\ d e. NN0 ) /\ ( f e. B /\ ( D ` f ) = ( d + 1 ) ) ) /\ ( x e. ( `' ( O ` f ) " { W } ) /\ A. g e. B ( ( D ` g ) = d -> ( # ` ( `' ( O ` g ) " { W } ) ) <_ ( D ` g ) ) ) ) -> d e. NN0 )
131 simplrr 
 |-  ( ( ( ( R e. IDomn /\ d e. NN0 ) /\ ( f e. B /\ ( D ` f ) = ( d + 1 ) ) ) /\ ( x e. ( `' ( O ` f ) " { W } ) /\ A. g e. B ( ( D ` g ) = d -> ( # ` ( `' ( O ` g ) " { W } ) ) <_ ( D ` g ) ) ) ) -> ( D ` f ) = ( d + 1 ) )
132 simprl 
 |-  ( ( ( ( R e. IDomn /\ d e. NN0 ) /\ ( f e. B /\ ( D ` f ) = ( d + 1 ) ) ) /\ ( x e. ( `' ( O ` f ) " { W } ) /\ A. g e. B ( ( D ` g ) = d -> ( # ` ( `' ( O ` g ) " { W } ) ) <_ ( D ` g ) ) ) ) -> x e. ( `' ( O ` f ) " { W } ) )
133 simprr 
 |-  ( ( ( ( R e. IDomn /\ d e. NN0 ) /\ ( f e. B /\ ( D ` f ) = ( d + 1 ) ) ) /\ ( x e. ( `' ( O ` f ) " { W } ) /\ A. g e. B ( ( D ` g ) = d -> ( # ` ( `' ( O ` g ) " { W } ) ) <_ ( D ` g ) ) ) ) -> A. g e. B ( ( D ` g ) = d -> ( # ` ( `' ( O ` g ) " { W } ) ) <_ ( D ` g ) ) )
134 1 2 3 4 5 6 125 126 62 127 128 54 129 130 131 132 133 fta1glem2 
 |-  ( ( ( ( R e. IDomn /\ d e. NN0 ) /\ ( f e. B /\ ( D ` f ) = ( d + 1 ) ) ) /\ ( x e. ( `' ( O ` f ) " { W } ) /\ A. g e. B ( ( D ` g ) = d -> ( # ` ( `' ( O ` g ) " { W } ) ) <_ ( D ` g ) ) ) ) -> ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) )
135 134 exp32 
 |-  ( ( ( R e. IDomn /\ d e. NN0 ) /\ ( f e. B /\ ( D ` f ) = ( d + 1 ) ) ) -> ( x e. ( `' ( O ` f ) " { W } ) -> ( A. g e. B ( ( D ` g ) = d -> ( # ` ( `' ( O ` g ) " { W } ) ) <_ ( D ` g ) ) -> ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) ) )
136 135 exlimdv 
 |-  ( ( ( R e. IDomn /\ d e. NN0 ) /\ ( f e. B /\ ( D ` f ) = ( d + 1 ) ) ) -> ( E. x x e. ( `' ( O ` f ) " { W } ) -> ( A. g e. B ( ( D ` g ) = d -> ( # ` ( `' ( O ` g ) " { W } ) ) <_ ( D ` g ) ) -> ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) ) )
137 124 136 biimtrid 
 |-  ( ( ( R e. IDomn /\ d e. NN0 ) /\ ( f e. B /\ ( D ` f ) = ( d + 1 ) ) ) -> ( ( `' ( O ` f ) " { W } ) =/= (/) -> ( A. g e. B ( ( D ` g ) = d -> ( # ` ( `' ( O ` g ) " { W } ) ) <_ ( D ` g ) ) -> ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) ) )
138 123 137 pm2.61dne 
 |-  ( ( ( R e. IDomn /\ d e. NN0 ) /\ ( f e. B /\ ( D ` f ) = ( d + 1 ) ) ) -> ( A. g e. B ( ( D ` g ) = d -> ( # ` ( `' ( O ` g ) " { W } ) ) <_ ( D ` g ) ) -> ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) )
139 138 expr 
 |-  ( ( ( R e. IDomn /\ d e. NN0 ) /\ f e. B ) -> ( ( D ` f ) = ( d + 1 ) -> ( A. g e. B ( ( D ` g ) = d -> ( # ` ( `' ( O ` g ) " { W } ) ) <_ ( D ` g ) ) -> ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) ) )
140 139 com23 
 |-  ( ( ( R e. IDomn /\ d e. NN0 ) /\ f e. B ) -> ( A. g e. B ( ( D ` g ) = d -> ( # ` ( `' ( O ` g ) " { W } ) ) <_ ( D ` g ) ) -> ( ( D ` f ) = ( d + 1 ) -> ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) ) )
141 140 ralrimdva 
 |-  ( ( R e. IDomn /\ d e. NN0 ) -> ( A. g e. B ( ( D ` g ) = d -> ( # ` ( `' ( O ` g ) " { W } ) ) <_ ( D ` g ) ) -> A. f e. B ( ( D ` f ) = ( d + 1 ) -> ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) ) )
142 113 141 biimtrid 
 |-  ( ( R e. IDomn /\ d e. NN0 ) -> ( A. f e. B ( ( D ` f ) = d -> ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) -> A. f e. B ( ( D ` f ) = ( d + 1 ) -> ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) ) )
143 142 expcom 
 |-  ( d e. NN0 -> ( R e. IDomn -> ( A. f e. B ( ( D ` f ) = d -> ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) -> A. f e. B ( ( D ` f ) = ( d + 1 ) -> ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) ) ) )
144 143 a2d 
 |-  ( d e. NN0 -> ( ( R e. IDomn -> A. f e. B ( ( D ` f ) = d -> ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) ) -> ( R e. IDomn -> A. f e. B ( ( D ` f ) = ( d + 1 ) -> ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) ) ) )
145 28 32 36 40 104 144 nn0ind 
 |-  ( ( D ` F ) e. NN0 -> ( R e. IDomn -> A. f e. B ( ( D ` f ) = ( D ` F ) -> ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) ) )
146 24 7 145 sylc 
 |-  ( ph -> A. f e. B ( ( D ` f ) = ( D ` F ) -> ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) )
147 18 146 8 rspcdva 
 |-  ( ph -> ( ( D ` F ) = ( D ` F ) -> ( # ` ( `' ( O ` F ) " { W } ) ) <_ ( D ` F ) ) )
148 10 147 mpi 
 |-  ( ph -> ( # ` ( `' ( O ` F ) " { W } ) ) <_ ( D ` F ) )