Metamath Proof Explorer

Theorem r1peuqusdeg1

Description: Uniqueness of polynomial remainder in terms of a quotient structure in the sense of the right hand side of r1pid2 . (Contributed by SN, 21-Jun-2025)

Ref Expression
Hypotheses r1peuqus.p 
|- P = ( Poly1 ` R )
r1peuqus.i 
|- I = ( ( RSpan ` P ) ` { F } )
r1peuqus.t 
|- T = ( P /s ( P ~QG I ) )
r1peuqus.q 
|- Q = ( Base ` T )
r1peuqus.n 
|- N = ( Unic1p ` R )
r1peuqus.d 
|- D = ( deg1 ` R )
r1peuqus.r 
|- ( ph -> R e. Domn )
r1peuqus.f 
|- ( ph -> F e. N )
r1peuqus.z 
|- ( ph -> Z e. Q )
Assertion r1peuqusdeg1 
|- ( ph -> E! q e. Z ( D ` q ) < ( D ` F ) )

Proof

Step Hyp Ref Expression
1 r1peuqus.p 
 |-  P = ( Poly1 ` R )
2 r1peuqus.i 
 |-  I = ( ( RSpan ` P ) ` { F } )
3 r1peuqus.t 
 |-  T = ( P /s ( P ~QG I ) )
4 r1peuqus.q 
 |-  Q = ( Base ` T )
5 r1peuqus.n 
 |-  N = ( Unic1p ` R )
6 r1peuqus.d 
 |-  D = ( deg1 ` R )
7 r1peuqus.r 
 |-  ( ph -> R e. Domn )
8 r1peuqus.f 
 |-  ( ph -> F e. N )
9 r1peuqus.z 
 |-  ( ph -> Z e. Q )
10 eqid 
 |-  ( Base ` P ) = ( Base ` P )
11 eqid 
 |-  ( +g ` P ) = ( +g ` P )
12 eqid 
 |-  ( .r ` P ) = ( .r ` P )
13 eqid 
 |-  ( P ~QG I ) = ( P ~QG I )
14 1 ply1domn 
 |-  ( R e. Domn -> P e. Domn )
15 7 14 syl 
 |-  ( ph -> P e. Domn )
16 domnring 
 |-  ( P e. Domn -> P e. Ring )
17 15 16 syl 
 |-  ( ph -> P e. Ring )
18 1 10 5 uc1pcl 
 |-  ( F e. N -> F e. ( Base ` P ) )
19 8 18 syl 
 |-  ( ph -> F e. ( Base ` P ) )
20 9 4 eleqtrdi 
 |-  ( ph -> Z e. ( Base ` T ) )
21 10 11 12 13 3 2 17 19 20 ellcsrspsn 
 |-  ( ph -> E. p e. ( Base ` P ) ( Z = [ p ] ( P ~QG I ) /\ Z = { z | E. y e. ( Base ` P ) z = ( p ( +g ` P ) ( y ( .r ` P ) F ) ) } ) )
22 domnring 
 |-  ( R e. Domn -> R e. Ring )
23 7 22 syl 
 |-  ( ph -> R e. Ring )
24 23 adantr 
 |-  ( ( ph /\ p e. ( Base ` P ) ) -> R e. Ring )
25 simpr 
 |-  ( ( ph /\ p e. ( Base ` P ) ) -> p e. ( Base ` P ) )
26 8 adantr 
 |-  ( ( ph /\ p e. ( Base ` P ) ) -> F e. N )
27 1 6 10 11 12 5 24 25 26 ply1divalg3 
 |-  ( ( ph /\ p e. ( Base ` P ) ) -> E! s e. ( Base ` P ) ( D ` ( p ( +g ` P ) ( s ( .r ` P ) F ) ) ) < ( D ` F ) )
28 27 adantr 
 |-  ( ( ( ph /\ p e. ( Base ` P ) ) /\ ( Z = [ p ] ( P ~QG I ) /\ Z = { z | E. y e. ( Base ` P ) z = ( p ( +g ` P ) ( y ( .r ` P ) F ) ) } ) ) -> E! s e. ( Base ` P ) ( D ` ( p ( +g ` P ) ( s ( .r ` P ) F ) ) ) < ( D ` F ) )
29 ovexd 
 |-  ( ( ( ( ph /\ p e. ( Base ` P ) ) /\ ( Z = [ p ] ( P ~QG I ) /\ Z = { z | E. y e. ( Base ` P ) z = ( p ( +g ` P ) ( y ( .r ` P ) F ) ) } ) ) /\ s e. ( Base ` P ) ) -> ( p ( +g ` P ) ( s ( .r ` P ) F ) ) e. _V )
30 simpr 
 |-  ( ( ( ( ph /\ p e. ( Base ` P ) ) /\ ( Z = [ p ] ( P ~QG I ) /\ Z = { z | E. y e. ( Base ` P ) z = ( p ( +g ` P ) ( y ( .r ` P ) F ) ) } ) ) /\ s e. ( Base ` P ) ) -> s e. ( Base ` P ) )
31 eqidd 
 |-  ( ( ( ( ph /\ p e. ( Base ` P ) ) /\ ( Z = [ p ] ( P ~QG I ) /\ Z = { z | E. y e. ( Base ` P ) z = ( p ( +g ` P ) ( y ( .r ` P ) F ) ) } ) ) /\ s e. ( Base ` P ) ) -> ( p ( +g ` P ) ( s ( .r ` P ) F ) ) = ( p ( +g ` P ) ( s ( .r ` P ) F ) ) )
32 oveq1 
 |-  ( y = s -> ( y ( .r ` P ) F ) = ( s ( .r ` P ) F ) )
33 32 oveq2d 
 |-  ( y = s -> ( p ( +g ` P ) ( y ( .r ` P ) F ) ) = ( p ( +g ` P ) ( s ( .r ` P ) F ) ) )
34 33 eqeq2d 
 |-  ( y = s -> ( ( p ( +g ` P ) ( s ( .r ` P ) F ) ) = ( p ( +g ` P ) ( y ( .r ` P ) F ) ) <-> ( p ( +g ` P ) ( s ( .r ` P ) F ) ) = ( p ( +g ` P ) ( s ( .r ` P ) F ) ) ) )
35 34 rspcev 
 |-  ( ( s e. ( Base ` P ) /\ ( p ( +g ` P ) ( s ( .r ` P ) F ) ) = ( p ( +g ` P ) ( s ( .r ` P ) F ) ) ) -> E. y e. ( Base ` P ) ( p ( +g ` P ) ( s ( .r ` P ) F ) ) = ( p ( +g ` P ) ( y ( .r ` P ) F ) ) )
36 30 31 35 syl2anc 
 |-  ( ( ( ( ph /\ p e. ( Base ` P ) ) /\ ( Z = [ p ] ( P ~QG I ) /\ Z = { z | E. y e. ( Base ` P ) z = ( p ( +g ` P ) ( y ( .r ` P ) F ) ) } ) ) /\ s e. ( Base ` P ) ) -> E. y e. ( Base ` P ) ( p ( +g ` P ) ( s ( .r ` P ) F ) ) = ( p ( +g ` P ) ( y ( .r ` P ) F ) ) )
37 eqeq1 
 |-  ( z = ( p ( +g ` P ) ( s ( .r ` P ) F ) ) -> ( z = ( p ( +g ` P ) ( y ( .r ` P ) F ) ) <-> ( p ( +g ` P ) ( s ( .r ` P ) F ) ) = ( p ( +g ` P ) ( y ( .r ` P ) F ) ) ) )
38 37 rexbidv 
 |-  ( z = ( p ( +g ` P ) ( s ( .r ` P ) F ) ) -> ( E. y e. ( Base ` P ) z = ( p ( +g ` P ) ( y ( .r ` P ) F ) ) <-> E. y e. ( Base ` P ) ( p ( +g ` P ) ( s ( .r ` P ) F ) ) = ( p ( +g ` P ) ( y ( .r ` P ) F ) ) ) )
39 29 36 38 elabd 
 |-  ( ( ( ( ph /\ p e. ( Base ` P ) ) /\ ( Z = [ p ] ( P ~QG I ) /\ Z = { z | E. y e. ( Base ` P ) z = ( p ( +g ` P ) ( y ( .r ` P ) F ) ) } ) ) /\ s e. ( Base ` P ) ) -> ( p ( +g ` P ) ( s ( .r ` P ) F ) ) e. { z | E. y e. ( Base ` P ) z = ( p ( +g ` P ) ( y ( .r ` P ) F ) ) } )
40 simplrr 
 |-  ( ( ( ( ph /\ p e. ( Base ` P ) ) /\ ( Z = [ p ] ( P ~QG I ) /\ Z = { z | E. y e. ( Base ` P ) z = ( p ( +g ` P ) ( y ( .r ` P ) F ) ) } ) ) /\ s e. ( Base ` P ) ) -> Z = { z | E. y e. ( Base ` P ) z = ( p ( +g ` P ) ( y ( .r ` P ) F ) ) } )
41 39 40 eleqtrrd 
 |-  ( ( ( ( ph /\ p e. ( Base ` P ) ) /\ ( Z = [ p ] ( P ~QG I ) /\ Z = { z | E. y e. ( Base ` P ) z = ( p ( +g ` P ) ( y ( .r ` P ) F ) ) } ) ) /\ s e. ( Base ` P ) ) -> ( p ( +g ` P ) ( s ( .r ` P ) F ) ) e. Z )
42 simprr 
 |-  ( ( ( ph /\ p e. ( Base ` P ) ) /\ ( Z = [ p ] ( P ~QG I ) /\ Z = { z | E. y e. ( Base ` P ) z = ( p ( +g ` P ) ( y ( .r ` P ) F ) ) } ) ) -> Z = { z | E. y e. ( Base ` P ) z = ( p ( +g ` P ) ( y ( .r ` P ) F ) ) } )
43 42 eqimssd 
 |-  ( ( ( ph /\ p e. ( Base ` P ) ) /\ ( Z = [ p ] ( P ~QG I ) /\ Z = { z | E. y e. ( Base ` P ) z = ( p ( +g ` P ) ( y ( .r ` P ) F ) ) } ) ) -> Z C_ { z | E. y e. ( Base ` P ) z = ( p ( +g ` P ) ( y ( .r ` P ) F ) ) } )
44 43 sselda 
 |-  ( ( ( ( ph /\ p e. ( Base ` P ) ) /\ ( Z = [ p ] ( P ~QG I ) /\ Z = { z | E. y e. ( Base ` P ) z = ( p ( +g ` P ) ( y ( .r ` P ) F ) ) } ) ) /\ q e. Z ) -> q e. { z | E. y e. ( Base ` P ) z = ( p ( +g ` P ) ( y ( .r ` P ) F ) ) } )
45 eqeq1 
 |-  ( z = q -> ( z = ( p ( +g ` P ) ( y ( .r ` P ) F ) ) <-> q = ( p ( +g ` P ) ( y ( .r ` P ) F ) ) ) )
46 45 rexbidv 
 |-  ( z = q -> ( E. y e. ( Base ` P ) z = ( p ( +g ` P ) ( y ( .r ` P ) F ) ) <-> E. y e. ( Base ` P ) q = ( p ( +g ` P ) ( y ( .r ` P ) F ) ) ) )
47 33 eqeq2d 
 |-  ( y = s -> ( q = ( p ( +g ` P ) ( y ( .r ` P ) F ) ) <-> q = ( p ( +g ` P ) ( s ( .r ` P ) F ) ) ) )
48 47 cbvrexvw 
 |-  ( E. y e. ( Base ` P ) q = ( p ( +g ` P ) ( y ( .r ` P ) F ) ) <-> E. s e. ( Base ` P ) q = ( p ( +g ` P ) ( s ( .r ` P ) F ) ) )
49 46 48 bitrdi 
 |-  ( z = q -> ( E. y e. ( Base ` P ) z = ( p ( +g ` P ) ( y ( .r ` P ) F ) ) <-> E. s e. ( Base ` P ) q = ( p ( +g ` P ) ( s ( .r ` P ) F ) ) ) )
50 49 elabg 
 |-  ( q e. { z | E. y e. ( Base ` P ) z = ( p ( +g ` P ) ( y ( .r ` P ) F ) ) } -> ( q e. { z | E. y e. ( Base ` P ) z = ( p ( +g ` P ) ( y ( .r ` P ) F ) ) } <-> E. s e. ( Base ` P ) q = ( p ( +g ` P ) ( s ( .r ` P ) F ) ) ) )
51 50 ibi 
 |-  ( q e. { z | E. y e. ( Base ` P ) z = ( p ( +g ` P ) ( y ( .r ` P ) F ) ) } -> E. s e. ( Base ` P ) q = ( p ( +g ` P ) ( s ( .r ` P ) F ) ) )
52 44 51 syl 
 |-  ( ( ( ( ph /\ p e. ( Base ` P ) ) /\ ( Z = [ p ] ( P ~QG I ) /\ Z = { z | E. y e. ( Base ` P ) z = ( p ( +g ` P ) ( y ( .r ` P ) F ) ) } ) ) /\ q e. Z ) -> E. s e. ( Base ` P ) q = ( p ( +g ` P ) ( s ( .r ` P ) F ) ) )
53 eqtr2 
 |-  ( ( q = ( p ( +g ` P ) ( s ( .r ` P ) F ) ) /\ q = ( p ( +g ` P ) ( t ( .r ` P ) F ) ) ) -> ( p ( +g ` P ) ( s ( .r ` P ) F ) ) = ( p ( +g ` P ) ( t ( .r ` P ) F ) ) )
54 17 ringgrpd 
 |-  ( ph -> P e. Grp )
55 54 adantr 
 |-  ( ( ph /\ ( p e. ( Base ` P ) /\ s e. ( Base ` P ) /\ t e. ( Base ` P ) ) ) -> P e. Grp )
56 17 adantr 
 |-  ( ( ph /\ ( p e. ( Base ` P ) /\ s e. ( Base ` P ) /\ t e. ( Base ` P ) ) ) -> P e. Ring )
57 simpr2 
 |-  ( ( ph /\ ( p e. ( Base ` P ) /\ s e. ( Base ` P ) /\ t e. ( Base ` P ) ) ) -> s e. ( Base ` P ) )
58 19 adantr 
 |-  ( ( ph /\ ( p e. ( Base ` P ) /\ s e. ( Base ` P ) /\ t e. ( Base ` P ) ) ) -> F e. ( Base ` P ) )
59 10 12 56 57 58 ringcld 
 |-  ( ( ph /\ ( p e. ( Base ` P ) /\ s e. ( Base ` P ) /\ t e. ( Base ` P ) ) ) -> ( s ( .r ` P ) F ) e. ( Base ` P ) )
60 simpr3 
 |-  ( ( ph /\ ( p e. ( Base ` P ) /\ s e. ( Base ` P ) /\ t e. ( Base ` P ) ) ) -> t e. ( Base ` P ) )
61 10 12 56 60 58 ringcld 
 |-  ( ( ph /\ ( p e. ( Base ` P ) /\ s e. ( Base ` P ) /\ t e. ( Base ` P ) ) ) -> ( t ( .r ` P ) F ) e. ( Base ` P ) )
62 simpr1 
 |-  ( ( ph /\ ( p e. ( Base ` P ) /\ s e. ( Base ` P ) /\ t e. ( Base ` P ) ) ) -> p e. ( Base ` P ) )
63 10 11 grplcan 
 |-  ( ( P e. Grp /\ ( ( s ( .r ` P ) F ) e. ( Base ` P ) /\ ( t ( .r ` P ) F ) e. ( Base ` P ) /\ p e. ( Base ` P ) ) ) -> ( ( p ( +g ` P ) ( s ( .r ` P ) F ) ) = ( p ( +g ` P ) ( t ( .r ` P ) F ) ) <-> ( s ( .r ` P ) F ) = ( t ( .r ` P ) F ) ) )
64 55 59 61 62 63 syl13anc 
 |-  ( ( ph /\ ( p e. ( Base ` P ) /\ s e. ( Base ` P ) /\ t e. ( Base ` P ) ) ) -> ( ( p ( +g ` P ) ( s ( .r ` P ) F ) ) = ( p ( +g ` P ) ( t ( .r ` P ) F ) ) <-> ( s ( .r ` P ) F ) = ( t ( .r ` P ) F ) ) )
65 eqid 
 |-  ( 0g ` P ) = ( 0g ` P )
66 simplr2 
 |-  ( ( ( ph /\ ( p e. ( Base ` P ) /\ s e. ( Base ` P ) /\ t e. ( Base ` P ) ) ) /\ ( s ( .r ` P ) F ) = ( t ( .r ` P ) F ) ) -> s e. ( Base ` P ) )
67 simplr3 
 |-  ( ( ( ph /\ ( p e. ( Base ` P ) /\ s e. ( Base ` P ) /\ t e. ( Base ` P ) ) ) /\ ( s ( .r ` P ) F ) = ( t ( .r ` P ) F ) ) -> t e. ( Base ` P ) )
68 1 65 5 uc1pn0 
 |-  ( F e. N -> F =/= ( 0g ` P ) )
69 8 68 syl 
 |-  ( ph -> F =/= ( 0g ` P ) )
70 19 69 eldifsnd 
 |-  ( ph -> F e. ( ( Base ` P ) \ { ( 0g ` P ) } ) )
71 70 ad2antrr 
 |-  ( ( ( ph /\ ( p e. ( Base ` P ) /\ s e. ( Base ` P ) /\ t e. ( Base ` P ) ) ) /\ ( s ( .r ` P ) F ) = ( t ( .r ` P ) F ) ) -> F e. ( ( Base ` P ) \ { ( 0g ` P ) } ) )
72 15 ad2antrr 
 |-  ( ( ( ph /\ ( p e. ( Base ` P ) /\ s e. ( Base ` P ) /\ t e. ( Base ` P ) ) ) /\ ( s ( .r ` P ) F ) = ( t ( .r ` P ) F ) ) -> P e. Domn )
73 simpr 
 |-  ( ( ( ph /\ ( p e. ( Base ` P ) /\ s e. ( Base ` P ) /\ t e. ( Base ` P ) ) ) /\ ( s ( .r ` P ) F ) = ( t ( .r ` P ) F ) ) -> ( s ( .r ` P ) F ) = ( t ( .r ` P ) F ) )
74 10 65 12 66 67 71 72 73 domnrcan 
 |-  ( ( ( ph /\ ( p e. ( Base ` P ) /\ s e. ( Base ` P ) /\ t e. ( Base ` P ) ) ) /\ ( s ( .r ` P ) F ) = ( t ( .r ` P ) F ) ) -> s = t )
75 74 ex 
 |-  ( ( ph /\ ( p e. ( Base ` P ) /\ s e. ( Base ` P ) /\ t e. ( Base ` P ) ) ) -> ( ( s ( .r ` P ) F ) = ( t ( .r ` P ) F ) -> s = t ) )
76 64 75 sylbid 
 |-  ( ( ph /\ ( p e. ( Base ` P ) /\ s e. ( Base ` P ) /\ t e. ( Base ` P ) ) ) -> ( ( p ( +g ` P ) ( s ( .r ` P ) F ) ) = ( p ( +g ` P ) ( t ( .r ` P ) F ) ) -> s = t ) )
77 76 3exp2 
 |-  ( ph -> ( p e. ( Base ` P ) -> ( s e. ( Base ` P ) -> ( t e. ( Base ` P ) -> ( ( p ( +g ` P ) ( s ( .r ` P ) F ) ) = ( p ( +g ` P ) ( t ( .r ` P ) F ) ) -> s = t ) ) ) ) )
78 77 imp43 
 |-  ( ( ( ph /\ p e. ( Base ` P ) ) /\ ( s e. ( Base ` P ) /\ t e. ( Base ` P ) ) ) -> ( ( p ( +g ` P ) ( s ( .r ` P ) F ) ) = ( p ( +g ` P ) ( t ( .r ` P ) F ) ) -> s = t ) )
79 53 78 syl5 
 |-  ( ( ( ph /\ p e. ( Base ` P ) ) /\ ( s e. ( Base ` P ) /\ t e. ( Base ` P ) ) ) -> ( ( q = ( p ( +g ` P ) ( s ( .r ` P ) F ) ) /\ q = ( p ( +g ` P ) ( t ( .r ` P ) F ) ) ) -> s = t ) )
80 79 ralrimivva 
 |-  ( ( ph /\ p e. ( Base ` P ) ) -> A. s e. ( Base ` P ) A. t e. ( Base ` P ) ( ( q = ( p ( +g ` P ) ( s ( .r ` P ) F ) ) /\ q = ( p ( +g ` P ) ( t ( .r ` P ) F ) ) ) -> s = t ) )
81 oveq1 
 |-  ( s = t -> ( s ( .r ` P ) F ) = ( t ( .r ` P ) F ) )
82 81 oveq2d 
 |-  ( s = t -> ( p ( +g ` P ) ( s ( .r ` P ) F ) ) = ( p ( +g ` P ) ( t ( .r ` P ) F ) ) )
83 82 eqeq2d 
 |-  ( s = t -> ( q = ( p ( +g ` P ) ( s ( .r ` P ) F ) ) <-> q = ( p ( +g ` P ) ( t ( .r ` P ) F ) ) ) )
84 83 rmo4 
 |-  ( E* s e. ( Base ` P ) q = ( p ( +g ` P ) ( s ( .r ` P ) F ) ) <-> A. s e. ( Base ` P ) A. t e. ( Base ` P ) ( ( q = ( p ( +g ` P ) ( s ( .r ` P ) F ) ) /\ q = ( p ( +g ` P ) ( t ( .r ` P ) F ) ) ) -> s = t ) )
85 80 84 sylibr 
 |-  ( ( ph /\ p e. ( Base ` P ) ) -> E* s e. ( Base ` P ) q = ( p ( +g ` P ) ( s ( .r ` P ) F ) ) )
86 85 ad2antrr 
 |-  ( ( ( ( ph /\ p e. ( Base ` P ) ) /\ ( Z = [ p ] ( P ~QG I ) /\ Z = { z | E. y e. ( Base ` P ) z = ( p ( +g ` P ) ( y ( .r ` P ) F ) ) } ) ) /\ q e. Z ) -> E* s e. ( Base ` P ) q = ( p ( +g ` P ) ( s ( .r ` P ) F ) ) )
87 reu5 
 |-  ( E! s e. ( Base ` P ) q = ( p ( +g ` P ) ( s ( .r ` P ) F ) ) <-> ( E. s e. ( Base ` P ) q = ( p ( +g ` P ) ( s ( .r ` P ) F ) ) /\ E* s e. ( Base ` P ) q = ( p ( +g ` P ) ( s ( .r ` P ) F ) ) ) )
88 52 86 87 sylanbrc 
 |-  ( ( ( ( ph /\ p e. ( Base ` P ) ) /\ ( Z = [ p ] ( P ~QG I ) /\ Z = { z | E. y e. ( Base ` P ) z = ( p ( +g ` P ) ( y ( .r ` P ) F ) ) } ) ) /\ q e. Z ) -> E! s e. ( Base ` P ) q = ( p ( +g ` P ) ( s ( .r ` P ) F ) ) )
89 fveq2 
 |-  ( q = ( p ( +g ` P ) ( s ( .r ` P ) F ) ) -> ( D ` q ) = ( D ` ( p ( +g ` P ) ( s ( .r ` P ) F ) ) ) )
90 89 breq1d 
 |-  ( q = ( p ( +g ` P ) ( s ( .r ` P ) F ) ) -> ( ( D ` q ) < ( D ` F ) <-> ( D ` ( p ( +g ` P ) ( s ( .r ` P ) F ) ) ) < ( D ` F ) ) )
91 41 88 90 reuxfr1ds 
 |-  ( ( ( ph /\ p e. ( Base ` P ) ) /\ ( Z = [ p ] ( P ~QG I ) /\ Z = { z | E. y e. ( Base ` P ) z = ( p ( +g ` P ) ( y ( .r ` P ) F ) ) } ) ) -> ( E! q e. Z ( D ` q ) < ( D ` F ) <-> E! s e. ( Base ` P ) ( D ` ( p ( +g ` P ) ( s ( .r ` P ) F ) ) ) < ( D ` F ) ) )
92 28 91 mpbird 
 |-  ( ( ( ph /\ p e. ( Base ` P ) ) /\ ( Z = [ p ] ( P ~QG I ) /\ Z = { z | E. y e. ( Base ` P ) z = ( p ( +g ` P ) ( y ( .r ` P ) F ) ) } ) ) -> E! q e. Z ( D ` q ) < ( D ` F ) )
93 92 ex 
 |-  ( ( ph /\ p e. ( Base ` P ) ) -> ( ( Z = [ p ] ( P ~QG I ) /\ Z = { z | E. y e. ( Base ` P ) z = ( p ( +g ` P ) ( y ( .r ` P ) F ) ) } ) -> E! q e. Z ( D ` q ) < ( D ` F ) ) )
94 93 reximdva 
 |-  ( ph -> ( E. p e. ( Base ` P ) ( Z = [ p ] ( P ~QG I ) /\ Z = { z | E. y e. ( Base ` P ) z = ( p ( +g ` P ) ( y ( .r ` P ) F ) ) } ) -> E. p e. ( Base ` P ) E! q e. Z ( D ` q ) < ( D ` F ) ) )
95 21 94 mpd 
 |-  ( ph -> E. p e. ( Base ` P ) E! q e. Z ( D ` q ) < ( D ` F ) )
96 id 
 |-  ( E! q e. Z ( D ` q ) < ( D ` F ) -> E! q e. Z ( D ` q ) < ( D ` F ) )
97 96 rexlimivw 
 |-  ( E. p e. ( Base ` P ) E! q e. Z ( D ` q ) < ( D ` F ) -> E! q e. Z ( D ` q ) < ( D ` F ) )
98 95 97 syl 
 |-  ( ph -> E! q e. Z ( D ` q ) < ( D ` F ) )