Metamath Proof Explorer

Theorem fta1glem2

Description: Lemma for fta1g . (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 )
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 } ) )
fta1glem.6 
|- ( ph -> A. g e. B ( ( D ` g ) = N -> ( # ` ( `' ( O ` g ) " { W } ) ) <_ ( D ` g ) ) )
Assertion fta1glem2 
|- ( 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 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 fta1glem.6 
 |-  ( ph -> A. g e. B ( ( D ` g ) = N -> ( # ` ( `' ( O ` g ) " { W } ) ) <_ ( D ` g ) ) )
18 eqid 
 |-  ( R ^s K ) = ( R ^s K )
19 eqid 
 |-  ( Base ` ( R ^s K ) ) = ( Base ` ( R ^s K ) )
20 9 fvexi 
 |-  K e. _V
21 20 a1i 
 |-  ( ph -> K e. _V )
22 isidom 
 |-  ( R e. IDomn <-> ( R e. CRing /\ R e. Domn ) )
23 22 simplbi 
 |-  ( R e. IDomn -> R e. CRing )
24 7 23 syl 
 |-  ( ph -> R e. CRing )
25 4 1 18 9 evl1rhm 
 |-  ( R e. CRing -> O e. ( P RingHom ( R ^s K ) ) )
26 24 25 syl 
 |-  ( ph -> O e. ( P RingHom ( R ^s K ) ) )
27 2 19 rhmf 
 |-  ( O e. ( P RingHom ( R ^s K ) ) -> O : B --> ( Base ` ( R ^s K ) ) )
28 26 27 syl 
 |-  ( ph -> O : B --> ( Base ` ( R ^s K ) ) )
29 28 8 ffvelrnd 
 |-  ( ph -> ( O ` F ) e. ( Base ` ( R ^s K ) ) )
30 18 9 19 7 21 29 pwselbas 
 |-  ( ph -> ( O ` F ) : K --> K )
31 30 ffnd 
 |-  ( ph -> ( O ` F ) Fn K )
32 fniniseg 
 |-  ( ( O ` F ) Fn K -> ( T e. ( `' ( O ` F ) " { W } ) <-> ( T e. K /\ ( ( O ` F ) ` T ) = W ) ) )
33 31 32 syl 
 |-  ( ph -> ( T e. ( `' ( O ` F ) " { W } ) <-> ( T e. K /\ ( ( O ` F ) ` T ) = W ) ) )
34 16 33 mpbid 
 |-  ( ph -> ( T e. K /\ ( ( O ` F ) ` T ) = W ) )
35 34 simprd 
 |-  ( ph -> ( ( O ` F ) ` T ) = W )
36 22 simprbi 
 |-  ( R e. IDomn -> R e. Domn )
37 domnnzr 
 |-  ( R e. Domn -> R e. NzRing )
38 36 37 syl 
 |-  ( R e. IDomn -> R e. NzRing )
39 7 38 syl 
 |-  ( ph -> R e. NzRing )
40 34 simpld 
 |-  ( ph -> T e. K )
41 eqid 
 |-  ( ||r ` P ) = ( ||r ` P )
42 1 2 9 10 11 12 13 4 39 24 40 8 5 41 facth1 
 |-  ( ph -> ( G ( ||r ` P ) F <-> ( ( O ` F ) ` T ) = W ) )
43 35 42 mpbird 
 |-  ( ph -> G ( ||r ` P ) F )
44 nzrring 
 |-  ( R e. NzRing -> R e. Ring )
45 39 44 syl 
 |-  ( ph -> R e. Ring )
46 eqid 
 |-  ( Monic1p ` R ) = ( Monic1p ` R )
47 1 2 9 10 11 12 13 4 39 24 40 46 3 5 ply1remlem 
 |-  ( ph -> ( G e. ( Monic1p ` R ) /\ ( D ` G ) = 1 /\ ( `' ( O ` G ) " { W } ) = { T } ) )
48 47 simp1d 
 |-  ( ph -> G e. ( Monic1p ` R ) )
49 eqid 
 |-  ( Unic1p ` R ) = ( Unic1p ` R )
50 49 46 mon1puc1p 
 |-  ( ( R e. Ring /\ G e. ( Monic1p ` R ) ) -> G e. ( Unic1p ` R ) )
51 45 48 50 syl2anc 
 |-  ( ph -> G e. ( Unic1p ` R ) )
52 eqid 
 |-  ( .r ` P ) = ( .r ` P )
53 eqid 
 |-  ( quot1p ` R ) = ( quot1p ` R )
54 1 41 2 49 52 53 dvdsq1p 
 |-  ( ( R e. Ring /\ F e. B /\ G e. ( Unic1p ` R ) ) -> ( G ( ||r ` P ) F <-> F = ( ( F ( quot1p ` R ) G ) ( .r ` P ) G ) ) )
55 45 8 51 54 syl3anc 
 |-  ( ph -> ( G ( ||r ` P ) F <-> F = ( ( F ( quot1p ` R ) G ) ( .r ` P ) G ) ) )
56 43 55 mpbid 
 |-  ( ph -> F = ( ( F ( quot1p ` R ) G ) ( .r ` P ) G ) )
57 56 fveq2d 
 |-  ( ph -> ( O ` F ) = ( O ` ( ( F ( quot1p ` R ) G ) ( .r ` P ) G ) ) )
58 53 1 2 49 q1pcl 
 |-  ( ( R e. Ring /\ F e. B /\ G e. ( Unic1p ` R ) ) -> ( F ( quot1p ` R ) G ) e. B )
59 45 8 51 58 syl3anc 
 |-  ( ph -> ( F ( quot1p ` R ) G ) e. B )
60 1 2 46 mon1pcl 
 |-  ( G e. ( Monic1p ` R ) -> G e. B )
61 48 60 syl 
 |-  ( ph -> G e. B )
62 eqid 
 |-  ( .r ` ( R ^s K ) ) = ( .r ` ( R ^s K ) )
63 2 52 62 rhmmul 
 |-  ( ( O e. ( P RingHom ( R ^s K ) ) /\ ( F ( quot1p ` R ) G ) e. B /\ G e. B ) -> ( O ` ( ( F ( quot1p ` R ) G ) ( .r ` P ) G ) ) = ( ( O ` ( F ( quot1p ` R ) G ) ) ( .r ` ( R ^s K ) ) ( O ` G ) ) )
64 26 59 61 63 syl3anc 
 |-  ( ph -> ( O ` ( ( F ( quot1p ` R ) G ) ( .r ` P ) G ) ) = ( ( O ` ( F ( quot1p ` R ) G ) ) ( .r ` ( R ^s K ) ) ( O ` G ) ) )
65 28 59 ffvelrnd 
 |-  ( ph -> ( O ` ( F ( quot1p ` R ) G ) ) e. ( Base ` ( R ^s K ) ) )
66 28 61 ffvelrnd 
 |-  ( ph -> ( O ` G ) e. ( Base ` ( R ^s K ) ) )
67 eqid 
 |-  ( .r ` R ) = ( .r ` R )
68 18 19 7 21 65 66 67 62 pwsmulrval 
 |-  ( ph -> ( ( O ` ( F ( quot1p ` R ) G ) ) ( .r ` ( R ^s K ) ) ( O ` G ) ) = ( ( O ` ( F ( quot1p ` R ) G ) ) oF ( .r ` R ) ( O ` G ) ) )
69 57 64 68 3eqtrd 
 |-  ( ph -> ( O ` F ) = ( ( O ` ( F ( quot1p ` R ) G ) ) oF ( .r ` R ) ( O ` G ) ) )
70 69 fveq1d 
 |-  ( ph -> ( ( O ` F ) ` x ) = ( ( ( O ` ( F ( quot1p ` R ) G ) ) oF ( .r ` R ) ( O ` G ) ) ` x ) )
71 70 adantr 
 |-  ( ( ph /\ x e. K ) -> ( ( O ` F ) ` x ) = ( ( ( O ` ( F ( quot1p ` R ) G ) ) oF ( .r ` R ) ( O ` G ) ) ` x ) )
72 18 9 19 7 21 65 pwselbas 
 |-  ( ph -> ( O ` ( F ( quot1p ` R ) G ) ) : K --> K )
73 72 ffnd 
 |-  ( ph -> ( O ` ( F ( quot1p ` R ) G ) ) Fn K )
74 73 adantr 
 |-  ( ( ph /\ x e. K ) -> ( O ` ( F ( quot1p ` R ) G ) ) Fn K )
75 18 9 19 7 21 66 pwselbas 
 |-  ( ph -> ( O ` G ) : K --> K )
76 75 ffnd 
 |-  ( ph -> ( O ` G ) Fn K )
77 76 adantr 
 |-  ( ( ph /\ x e. K ) -> ( O ` G ) Fn K )
78 20 a1i 
 |-  ( ( ph /\ x e. K ) -> K e. _V )
79 simpr 
 |-  ( ( ph /\ x e. K ) -> x e. K )
80 fnfvof 
 |-  ( ( ( ( O ` ( F ( quot1p ` R ) G ) ) Fn K /\ ( O ` G ) Fn K ) /\ ( K e. _V /\ x e. K ) ) -> ( ( ( O ` ( F ( quot1p ` R ) G ) ) oF ( .r ` R ) ( O ` G ) ) ` x ) = ( ( ( O ` ( F ( quot1p ` R ) G ) ) ` x ) ( .r ` R ) ( ( O ` G ) ` x ) ) )
81 74 77 78 79 80 syl22anc 
 |-  ( ( ph /\ x e. K ) -> ( ( ( O ` ( F ( quot1p ` R ) G ) ) oF ( .r ` R ) ( O ` G ) ) ` x ) = ( ( ( O ` ( F ( quot1p ` R ) G ) ) ` x ) ( .r ` R ) ( ( O ` G ) ` x ) ) )
82 71 81 eqtrd 
 |-  ( ( ph /\ x e. K ) -> ( ( O ` F ) ` x ) = ( ( ( O ` ( F ( quot1p ` R ) G ) ) ` x ) ( .r ` R ) ( ( O ` G ) ` x ) ) )
83 82 eqeq1d 
 |-  ( ( ph /\ x e. K ) -> ( ( ( O ` F ) ` x ) = W <-> ( ( ( O ` ( F ( quot1p ` R ) G ) ) ` x ) ( .r ` R ) ( ( O ` G ) ` x ) ) = W ) )
84 7 36 syl 
 |-  ( ph -> R e. Domn )
85 84 adantr 
 |-  ( ( ph /\ x e. K ) -> R e. Domn )
86 72 ffvelrnda 
 |-  ( ( ph /\ x e. K ) -> ( ( O ` ( F ( quot1p ` R ) G ) ) ` x ) e. K )
87 75 ffvelrnda 
 |-  ( ( ph /\ x e. K ) -> ( ( O ` G ) ` x ) e. K )
88 9 67 5 domneq0 
 |-  ( ( R e. Domn /\ ( ( O ` ( F ( quot1p ` R ) G ) ) ` x ) e. K /\ ( ( O ` G ) ` x ) e. K ) -> ( ( ( ( O ` ( F ( quot1p ` R ) G ) ) ` x ) ( .r ` R ) ( ( O ` G ) ` x ) ) = W <-> ( ( ( O ` ( F ( quot1p ` R ) G ) ) ` x ) = W \/ ( ( O ` G ) ` x ) = W ) ) )
89 85 86 87 88 syl3anc 
 |-  ( ( ph /\ x e. K ) -> ( ( ( ( O ` ( F ( quot1p ` R ) G ) ) ` x ) ( .r ` R ) ( ( O ` G ) ` x ) ) = W <-> ( ( ( O ` ( F ( quot1p ` R ) G ) ) ` x ) = W \/ ( ( O ` G ) ` x ) = W ) ) )
90 83 89 bitrd 
 |-  ( ( ph /\ x e. K ) -> ( ( ( O ` F ) ` x ) = W <-> ( ( ( O ` ( F ( quot1p ` R ) G ) ) ` x ) = W \/ ( ( O ` G ) ` x ) = W ) ) )
91 90 pm5.32da 
 |-  ( ph -> ( ( x e. K /\ ( ( O ` F ) ` x ) = W ) <-> ( x e. K /\ ( ( ( O ` ( F ( quot1p ` R ) G ) ) ` x ) = W \/ ( ( O ` G ) ` x ) = W ) ) ) )
92 andi 
 |-  ( ( x e. K /\ ( ( ( O ` ( F ( quot1p ` R ) G ) ) ` x ) = W \/ ( ( O ` G ) ` x ) = W ) ) <-> ( ( x e. K /\ ( ( O ` ( F ( quot1p ` R ) G ) ) ` x ) = W ) \/ ( x e. K /\ ( ( O ` G ) ` x ) = W ) ) )
93 91 92 bitrdi 
 |-  ( ph -> ( ( x e. K /\ ( ( O ` F ) ` x ) = W ) <-> ( ( x e. K /\ ( ( O ` ( F ( quot1p ` R ) G ) ) ` x ) = W ) \/ ( x e. K /\ ( ( O ` G ) ` x ) = W ) ) ) )
94 fniniseg 
 |-  ( ( O ` F ) Fn K -> ( x e. ( `' ( O ` F ) " { W } ) <-> ( x e. K /\ ( ( O ` F ) ` x ) = W ) ) )
95 31 94 syl 
 |-  ( ph -> ( x e. ( `' ( O ` F ) " { W } ) <-> ( x e. K /\ ( ( O ` F ) ` x ) = W ) ) )
96 elun 
 |-  ( x e. ( ( `' ( O ` ( F ( quot1p ` R ) G ) ) " { W } ) u. { T } ) <-> ( x e. ( `' ( O ` ( F ( quot1p ` R ) G ) ) " { W } ) \/ x e. { T } ) )
97 fniniseg 
 |-  ( ( O ` ( F ( quot1p ` R ) G ) ) Fn K -> ( x e. ( `' ( O ` ( F ( quot1p ` R ) G ) ) " { W } ) <-> ( x e. K /\ ( ( O ` ( F ( quot1p ` R ) G ) ) ` x ) = W ) ) )
98 73 97 syl 
 |-  ( ph -> ( x e. ( `' ( O ` ( F ( quot1p ` R ) G ) ) " { W } ) <-> ( x e. K /\ ( ( O ` ( F ( quot1p ` R ) G ) ) ` x ) = W ) ) )
99 47 simp3d 
 |-  ( ph -> ( `' ( O ` G ) " { W } ) = { T } )
100 99 eleq2d 
 |-  ( ph -> ( x e. ( `' ( O ` G ) " { W } ) <-> x e. { T } ) )
101 fniniseg 
 |-  ( ( O ` G ) Fn K -> ( x e. ( `' ( O ` G ) " { W } ) <-> ( x e. K /\ ( ( O ` G ) ` x ) = W ) ) )
102 76 101 syl 
 |-  ( ph -> ( x e. ( `' ( O ` G ) " { W } ) <-> ( x e. K /\ ( ( O ` G ) ` x ) = W ) ) )
103 100 102 bitr3d 
 |-  ( ph -> ( x e. { T } <-> ( x e. K /\ ( ( O ` G ) ` x ) = W ) ) )
104 98 103 orbi12d 
 |-  ( ph -> ( ( x e. ( `' ( O ` ( F ( quot1p ` R ) G ) ) " { W } ) \/ x e. { T } ) <-> ( ( x e. K /\ ( ( O ` ( F ( quot1p ` R ) G ) ) ` x ) = W ) \/ ( x e. K /\ ( ( O ` G ) ` x ) = W ) ) ) )
105 96 104 syl5bb 
 |-  ( ph -> ( x e. ( ( `' ( O ` ( F ( quot1p ` R ) G ) ) " { W } ) u. { T } ) <-> ( ( x e. K /\ ( ( O ` ( F ( quot1p ` R ) G ) ) ` x ) = W ) \/ ( x e. K /\ ( ( O ` G ) ` x ) = W ) ) ) )
106 93 95 105 3bitr4d 
 |-  ( ph -> ( x e. ( `' ( O ` F ) " { W } ) <-> x e. ( ( `' ( O ` ( F ( quot1p ` R ) G ) ) " { W } ) u. { T } ) ) )
107 106 eqrdv 
 |-  ( ph -> ( `' ( O ` F ) " { W } ) = ( ( `' ( O ` ( F ( quot1p ` R ) G ) ) " { W } ) u. { T } ) )
108 107 fveq2d 
 |-  ( ph -> ( # ` ( `' ( O ` F ) " { W } ) ) = ( # ` ( ( `' ( O ` ( F ( quot1p ` R ) G ) ) " { W } ) u. { T } ) ) )
109 fvex 
 |-  ( O ` ( F ( quot1p ` R ) G ) ) e. _V
110 109 cnvex 
 |-  `' ( O ` ( F ( quot1p ` R ) G ) ) e. _V
111 110 imaex 
 |-  ( `' ( O ` ( F ( quot1p ` R ) G ) ) " { W } ) e. _V
112 111 a1i 
 |-  ( ph -> ( `' ( O ` ( F ( quot1p ` R ) G ) ) " { W } ) e. _V )
113 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 fta1glem1 
 |-  ( ph -> ( D ` ( F ( quot1p ` R ) G ) ) = N )
114 fveq2 
 |-  ( g = ( F ( quot1p ` R ) G ) -> ( D ` g ) = ( D ` ( F ( quot1p ` R ) G ) ) )
115 114 eqeq1d 
 |-  ( g = ( F ( quot1p ` R ) G ) -> ( ( D ` g ) = N <-> ( D ` ( F ( quot1p ` R ) G ) ) = N ) )
116 fveq2 
 |-  ( g = ( F ( quot1p ` R ) G ) -> ( O ` g ) = ( O ` ( F ( quot1p ` R ) G ) ) )
117 116 cnveqd 
 |-  ( g = ( F ( quot1p ` R ) G ) -> `' ( O ` g ) = `' ( O ` ( F ( quot1p ` R ) G ) ) )
118 117 imaeq1d 
 |-  ( g = ( F ( quot1p ` R ) G ) -> ( `' ( O ` g ) " { W } ) = ( `' ( O ` ( F ( quot1p ` R ) G ) ) " { W } ) )
119 118 fveq2d 
 |-  ( g = ( F ( quot1p ` R ) G ) -> ( # ` ( `' ( O ` g ) " { W } ) ) = ( # ` ( `' ( O ` ( F ( quot1p ` R ) G ) ) " { W } ) ) )
120 119 114 breq12d 
 |-  ( g = ( F ( quot1p ` R ) G ) -> ( ( # ` ( `' ( O ` g ) " { W } ) ) <_ ( D ` g ) <-> ( # ` ( `' ( O ` ( F ( quot1p ` R ) G ) ) " { W } ) ) <_ ( D ` ( F ( quot1p ` R ) G ) ) ) )
121 115 120 imbi12d 
 |-  ( g = ( F ( quot1p ` R ) G ) -> ( ( ( D ` g ) = N -> ( # ` ( `' ( O ` g ) " { W } ) ) <_ ( D ` g ) ) <-> ( ( D ` ( F ( quot1p ` R ) G ) ) = N -> ( # ` ( `' ( O ` ( F ( quot1p ` R ) G ) ) " { W } ) ) <_ ( D ` ( F ( quot1p ` R ) G ) ) ) ) )
122 121 17 59 rspcdva 
 |-  ( ph -> ( ( D ` ( F ( quot1p ` R ) G ) ) = N -> ( # ` ( `' ( O ` ( F ( quot1p ` R ) G ) ) " { W } ) ) <_ ( D ` ( F ( quot1p ` R ) G ) ) ) )
123 113 122 mpd 
 |-  ( ph -> ( # ` ( `' ( O ` ( F ( quot1p ` R ) G ) ) " { W } ) ) <_ ( D ` ( F ( quot1p ` R ) G ) ) )
124 123 113 breqtrd 
 |-  ( ph -> ( # ` ( `' ( O ` ( F ( quot1p ` R ) G ) ) " { W } ) ) <_ N )
125 hashbnd 
 |-  ( ( ( `' ( O ` ( F ( quot1p ` R ) G ) ) " { W } ) e. _V /\ N e. NN0 /\ ( # ` ( `' ( O ` ( F ( quot1p ` R ) G ) ) " { W } ) ) <_ N ) -> ( `' ( O ` ( F ( quot1p ` R ) G ) ) " { W } ) e. Fin )
126 112 14 124 125 syl3anc 
 |-  ( ph -> ( `' ( O ` ( F ( quot1p ` R ) G ) ) " { W } ) e. Fin )
127 snfi 
 |-  { T } e. Fin
128 unfi 
 |-  ( ( ( `' ( O ` ( F ( quot1p ` R ) G ) ) " { W } ) e. Fin /\ { T } e. Fin ) -> ( ( `' ( O ` ( F ( quot1p ` R ) G ) ) " { W } ) u. { T } ) e. Fin )
129 126 127 128 sylancl 
 |-  ( ph -> ( ( `' ( O ` ( F ( quot1p ` R ) G ) ) " { W } ) u. { T } ) e. Fin )
130 hashcl 
 |-  ( ( ( `' ( O ` ( F ( quot1p ` R ) G ) ) " { W } ) u. { T } ) e. Fin -> ( # ` ( ( `' ( O ` ( F ( quot1p ` R ) G ) ) " { W } ) u. { T } ) ) e. NN0 )
131 129 130 syl 
 |-  ( ph -> ( # ` ( ( `' ( O ` ( F ( quot1p ` R ) G ) ) " { W } ) u. { T } ) ) e. NN0 )
132 131 nn0red 
 |-  ( ph -> ( # ` ( ( `' ( O ` ( F ( quot1p ` R ) G ) ) " { W } ) u. { T } ) ) e. RR )
133 hashcl 
 |-  ( ( `' ( O ` ( F ( quot1p ` R ) G ) ) " { W } ) e. Fin -> ( # ` ( `' ( O ` ( F ( quot1p ` R ) G ) ) " { W } ) ) e. NN0 )
134 126 133 syl 
 |-  ( ph -> ( # ` ( `' ( O ` ( F ( quot1p ` R ) G ) ) " { W } ) ) e. NN0 )
135 134 nn0red 
 |-  ( ph -> ( # ` ( `' ( O ` ( F ( quot1p ` R ) G ) ) " { W } ) ) e. RR )
136 peano2re 
 |-  ( ( # ` ( `' ( O ` ( F ( quot1p ` R ) G ) ) " { W } ) ) e. RR -> ( ( # ` ( `' ( O ` ( F ( quot1p ` R ) G ) ) " { W } ) ) + 1 ) e. RR )
137 135 136 syl 
 |-  ( ph -> ( ( # ` ( `' ( O ` ( F ( quot1p ` R ) G ) ) " { W } ) ) + 1 ) e. RR )
138 peano2nn0 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN0 )
139 14 138 syl 
 |-  ( ph -> ( N + 1 ) e. NN0 )
140 15 139 eqeltrd 
 |-  ( ph -> ( D ` F ) e. NN0 )
141 140 nn0red 
 |-  ( ph -> ( D ` F ) e. RR )
142 hashun2 
 |-  ( ( ( `' ( O ` ( F ( quot1p ` R ) G ) ) " { W } ) e. Fin /\ { T } e. Fin ) -> ( # ` ( ( `' ( O ` ( F ( quot1p ` R ) G ) ) " { W } ) u. { T } ) ) <_ ( ( # ` ( `' ( O ` ( F ( quot1p ` R ) G ) ) " { W } ) ) + ( # ` { T } ) ) )
143 126 127 142 sylancl 
 |-  ( ph -> ( # ` ( ( `' ( O ` ( F ( quot1p ` R ) G ) ) " { W } ) u. { T } ) ) <_ ( ( # ` ( `' ( O ` ( F ( quot1p ` R ) G ) ) " { W } ) ) + ( # ` { T } ) ) )
144 hashsng 
 |-  ( T e. ( `' ( O ` F ) " { W } ) -> ( # ` { T } ) = 1 )
145 16 144 syl 
 |-  ( ph -> ( # ` { T } ) = 1 )
146 145 oveq2d 
 |-  ( ph -> ( ( # ` ( `' ( O ` ( F ( quot1p ` R ) G ) ) " { W } ) ) + ( # ` { T } ) ) = ( ( # ` ( `' ( O ` ( F ( quot1p ` R ) G ) ) " { W } ) ) + 1 ) )
147 143 146 breqtrd 
 |-  ( ph -> ( # ` ( ( `' ( O ` ( F ( quot1p ` R ) G ) ) " { W } ) u. { T } ) ) <_ ( ( # ` ( `' ( O ` ( F ( quot1p ` R ) G ) ) " { W } ) ) + 1 ) )
148 14 nn0red 
 |-  ( ph -> N e. RR )
149 1red 
 |-  ( ph -> 1 e. RR )
150 135 148 149 124 leadd1dd 
 |-  ( ph -> ( ( # ` ( `' ( O ` ( F ( quot1p ` R ) G ) ) " { W } ) ) + 1 ) <_ ( N + 1 ) )
151 150 15 breqtrrd 
 |-  ( ph -> ( ( # ` ( `' ( O ` ( F ( quot1p ` R ) G ) ) " { W } ) ) + 1 ) <_ ( D ` F ) )
152 132 137 141 147 151 letrd 
 |-  ( ph -> ( # ` ( ( `' ( O ` ( F ( quot1p ` R ) G ) ) " { W } ) u. { T } ) ) <_ ( D ` F ) )
153 108 152 eqbrtrd 
 |-  ( ph -> ( # ` ( `' ( O ` F ) " { W } ) ) <_ ( D ` F ) )