Metamath Proof Explorer


Theorem q1pval

Description: Value of the univariate polynomial quotient function. (Contributed by Stefan O'Rear, 28-Mar-2015)

Ref Expression
Hypotheses q1pval.q โŠข ๐‘„ = ( quot1p โ€˜ ๐‘… )
q1pval.p โŠข ๐‘ƒ = ( Poly1 โ€˜ ๐‘… )
q1pval.b โŠข ๐ต = ( Base โ€˜ ๐‘ƒ )
q1pval.d โŠข ๐ท = ( deg1 โ€˜ ๐‘… )
q1pval.m โŠข โˆ’ = ( -g โ€˜ ๐‘ƒ )
q1pval.t โŠข ยท = ( .r โ€˜ ๐‘ƒ )
Assertion q1pval ( ( ๐น โˆˆ ๐ต โˆง ๐บ โˆˆ ๐ต ) โ†’ ( ๐น ๐‘„ ๐บ ) = ( โ„ฉ ๐‘ž โˆˆ ๐ต ( ๐ท โ€˜ ( ๐น โˆ’ ( ๐‘ž ยท ๐บ ) ) ) < ( ๐ท โ€˜ ๐บ ) ) )

Proof

Step Hyp Ref Expression
1 q1pval.q โŠข ๐‘„ = ( quot1p โ€˜ ๐‘… )
2 q1pval.p โŠข ๐‘ƒ = ( Poly1 โ€˜ ๐‘… )
3 q1pval.b โŠข ๐ต = ( Base โ€˜ ๐‘ƒ )
4 q1pval.d โŠข ๐ท = ( deg1 โ€˜ ๐‘… )
5 q1pval.m โŠข โˆ’ = ( -g โ€˜ ๐‘ƒ )
6 q1pval.t โŠข ยท = ( .r โ€˜ ๐‘ƒ )
7 2 3 elbasfv โŠข ( ๐บ โˆˆ ๐ต โ†’ ๐‘… โˆˆ V )
8 fveq2 โŠข ( ๐‘Ÿ = ๐‘… โ†’ ( Poly1 โ€˜ ๐‘Ÿ ) = ( Poly1 โ€˜ ๐‘… ) )
9 8 2 eqtr4di โŠข ( ๐‘Ÿ = ๐‘… โ†’ ( Poly1 โ€˜ ๐‘Ÿ ) = ๐‘ƒ )
10 9 csbeq1d โŠข ( ๐‘Ÿ = ๐‘… โ†’ โฆ‹ ( Poly1 โ€˜ ๐‘Ÿ ) / ๐‘ โฆŒ โฆ‹ ( Base โ€˜ ๐‘ ) / ๐‘ โฆŒ ( ๐‘“ โˆˆ ๐‘ , ๐‘” โˆˆ ๐‘ โ†ฆ ( โ„ฉ ๐‘ž โˆˆ ๐‘ ( ( deg1 โ€˜ ๐‘Ÿ ) โ€˜ ( ๐‘“ ( -g โ€˜ ๐‘ ) ( ๐‘ž ( .r โ€˜ ๐‘ ) ๐‘” ) ) ) < ( ( deg1 โ€˜ ๐‘Ÿ ) โ€˜ ๐‘” ) ) ) = โฆ‹ ๐‘ƒ / ๐‘ โฆŒ โฆ‹ ( Base โ€˜ ๐‘ ) / ๐‘ โฆŒ ( ๐‘“ โˆˆ ๐‘ , ๐‘” โˆˆ ๐‘ โ†ฆ ( โ„ฉ ๐‘ž โˆˆ ๐‘ ( ( deg1 โ€˜ ๐‘Ÿ ) โ€˜ ( ๐‘“ ( -g โ€˜ ๐‘ ) ( ๐‘ž ( .r โ€˜ ๐‘ ) ๐‘” ) ) ) < ( ( deg1 โ€˜ ๐‘Ÿ ) โ€˜ ๐‘” ) ) ) )
11 2 fvexi โŠข ๐‘ƒ โˆˆ V
12 11 a1i โŠข ( ๐‘Ÿ = ๐‘… โ†’ ๐‘ƒ โˆˆ V )
13 fveq2 โŠข ( ๐‘ = ๐‘ƒ โ†’ ( Base โ€˜ ๐‘ ) = ( Base โ€˜ ๐‘ƒ ) )
14 13 adantl โŠข ( ( ๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐‘ƒ ) โ†’ ( Base โ€˜ ๐‘ ) = ( Base โ€˜ ๐‘ƒ ) )
15 14 3 eqtr4di โŠข ( ( ๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐‘ƒ ) โ†’ ( Base โ€˜ ๐‘ ) = ๐ต )
16 15 csbeq1d โŠข ( ( ๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐‘ƒ ) โ†’ โฆ‹ ( Base โ€˜ ๐‘ ) / ๐‘ โฆŒ ( ๐‘“ โˆˆ ๐‘ , ๐‘” โˆˆ ๐‘ โ†ฆ ( โ„ฉ ๐‘ž โˆˆ ๐‘ ( ( deg1 โ€˜ ๐‘Ÿ ) โ€˜ ( ๐‘“ ( -g โ€˜ ๐‘ ) ( ๐‘ž ( .r โ€˜ ๐‘ ) ๐‘” ) ) ) < ( ( deg1 โ€˜ ๐‘Ÿ ) โ€˜ ๐‘” ) ) ) = โฆ‹ ๐ต / ๐‘ โฆŒ ( ๐‘“ โˆˆ ๐‘ , ๐‘” โˆˆ ๐‘ โ†ฆ ( โ„ฉ ๐‘ž โˆˆ ๐‘ ( ( deg1 โ€˜ ๐‘Ÿ ) โ€˜ ( ๐‘“ ( -g โ€˜ ๐‘ ) ( ๐‘ž ( .r โ€˜ ๐‘ ) ๐‘” ) ) ) < ( ( deg1 โ€˜ ๐‘Ÿ ) โ€˜ ๐‘” ) ) ) )
17 3 fvexi โŠข ๐ต โˆˆ V
18 17 a1i โŠข ( ( ๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐‘ƒ ) โ†’ ๐ต โˆˆ V )
19 simpr โŠข ( ( ( ๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐‘ƒ ) โˆง ๐‘ = ๐ต ) โ†’ ๐‘ = ๐ต )
20 fveq2 โŠข ( ๐‘Ÿ = ๐‘… โ†’ ( deg1 โ€˜ ๐‘Ÿ ) = ( deg1 โ€˜ ๐‘… ) )
21 20 ad2antrr โŠข ( ( ( ๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐‘ƒ ) โˆง ๐‘ = ๐ต ) โ†’ ( deg1 โ€˜ ๐‘Ÿ ) = ( deg1 โ€˜ ๐‘… ) )
22 21 4 eqtr4di โŠข ( ( ( ๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐‘ƒ ) โˆง ๐‘ = ๐ต ) โ†’ ( deg1 โ€˜ ๐‘Ÿ ) = ๐ท )
23 fveq2 โŠข ( ๐‘ = ๐‘ƒ โ†’ ( -g โ€˜ ๐‘ ) = ( -g โ€˜ ๐‘ƒ ) )
24 23 ad2antlr โŠข ( ( ( ๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐‘ƒ ) โˆง ๐‘ = ๐ต ) โ†’ ( -g โ€˜ ๐‘ ) = ( -g โ€˜ ๐‘ƒ ) )
25 24 5 eqtr4di โŠข ( ( ( ๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐‘ƒ ) โˆง ๐‘ = ๐ต ) โ†’ ( -g โ€˜ ๐‘ ) = โˆ’ )
26 eqidd โŠข ( ( ( ๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐‘ƒ ) โˆง ๐‘ = ๐ต ) โ†’ ๐‘“ = ๐‘“ )
27 fveq2 โŠข ( ๐‘ = ๐‘ƒ โ†’ ( .r โ€˜ ๐‘ ) = ( .r โ€˜ ๐‘ƒ ) )
28 27 ad2antlr โŠข ( ( ( ๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐‘ƒ ) โˆง ๐‘ = ๐ต ) โ†’ ( .r โ€˜ ๐‘ ) = ( .r โ€˜ ๐‘ƒ ) )
29 28 6 eqtr4di โŠข ( ( ( ๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐‘ƒ ) โˆง ๐‘ = ๐ต ) โ†’ ( .r โ€˜ ๐‘ ) = ยท )
30 29 oveqd โŠข ( ( ( ๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐‘ƒ ) โˆง ๐‘ = ๐ต ) โ†’ ( ๐‘ž ( .r โ€˜ ๐‘ ) ๐‘” ) = ( ๐‘ž ยท ๐‘” ) )
31 25 26 30 oveq123d โŠข ( ( ( ๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐‘ƒ ) โˆง ๐‘ = ๐ต ) โ†’ ( ๐‘“ ( -g โ€˜ ๐‘ ) ( ๐‘ž ( .r โ€˜ ๐‘ ) ๐‘” ) ) = ( ๐‘“ โˆ’ ( ๐‘ž ยท ๐‘” ) ) )
32 22 31 fveq12d โŠข ( ( ( ๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐‘ƒ ) โˆง ๐‘ = ๐ต ) โ†’ ( ( deg1 โ€˜ ๐‘Ÿ ) โ€˜ ( ๐‘“ ( -g โ€˜ ๐‘ ) ( ๐‘ž ( .r โ€˜ ๐‘ ) ๐‘” ) ) ) = ( ๐ท โ€˜ ( ๐‘“ โˆ’ ( ๐‘ž ยท ๐‘” ) ) ) )
33 22 fveq1d โŠข ( ( ( ๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐‘ƒ ) โˆง ๐‘ = ๐ต ) โ†’ ( ( deg1 โ€˜ ๐‘Ÿ ) โ€˜ ๐‘” ) = ( ๐ท โ€˜ ๐‘” ) )
34 32 33 breq12d โŠข ( ( ( ๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐‘ƒ ) โˆง ๐‘ = ๐ต ) โ†’ ( ( ( deg1 โ€˜ ๐‘Ÿ ) โ€˜ ( ๐‘“ ( -g โ€˜ ๐‘ ) ( ๐‘ž ( .r โ€˜ ๐‘ ) ๐‘” ) ) ) < ( ( deg1 โ€˜ ๐‘Ÿ ) โ€˜ ๐‘” ) โ†” ( ๐ท โ€˜ ( ๐‘“ โˆ’ ( ๐‘ž ยท ๐‘” ) ) ) < ( ๐ท โ€˜ ๐‘” ) ) )
35 19 34 riotaeqbidv โŠข ( ( ( ๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐‘ƒ ) โˆง ๐‘ = ๐ต ) โ†’ ( โ„ฉ ๐‘ž โˆˆ ๐‘ ( ( deg1 โ€˜ ๐‘Ÿ ) โ€˜ ( ๐‘“ ( -g โ€˜ ๐‘ ) ( ๐‘ž ( .r โ€˜ ๐‘ ) ๐‘” ) ) ) < ( ( deg1 โ€˜ ๐‘Ÿ ) โ€˜ ๐‘” ) ) = ( โ„ฉ ๐‘ž โˆˆ ๐ต ( ๐ท โ€˜ ( ๐‘“ โˆ’ ( ๐‘ž ยท ๐‘” ) ) ) < ( ๐ท โ€˜ ๐‘” ) ) )
36 19 19 35 mpoeq123dv โŠข ( ( ( ๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐‘ƒ ) โˆง ๐‘ = ๐ต ) โ†’ ( ๐‘“ โˆˆ ๐‘ , ๐‘” โˆˆ ๐‘ โ†ฆ ( โ„ฉ ๐‘ž โˆˆ ๐‘ ( ( deg1 โ€˜ ๐‘Ÿ ) โ€˜ ( ๐‘“ ( -g โ€˜ ๐‘ ) ( ๐‘ž ( .r โ€˜ ๐‘ ) ๐‘” ) ) ) < ( ( deg1 โ€˜ ๐‘Ÿ ) โ€˜ ๐‘” ) ) ) = ( ๐‘“ โˆˆ ๐ต , ๐‘” โˆˆ ๐ต โ†ฆ ( โ„ฉ ๐‘ž โˆˆ ๐ต ( ๐ท โ€˜ ( ๐‘“ โˆ’ ( ๐‘ž ยท ๐‘” ) ) ) < ( ๐ท โ€˜ ๐‘” ) ) ) )
37 18 36 csbied โŠข ( ( ๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐‘ƒ ) โ†’ โฆ‹ ๐ต / ๐‘ โฆŒ ( ๐‘“ โˆˆ ๐‘ , ๐‘” โˆˆ ๐‘ โ†ฆ ( โ„ฉ ๐‘ž โˆˆ ๐‘ ( ( deg1 โ€˜ ๐‘Ÿ ) โ€˜ ( ๐‘“ ( -g โ€˜ ๐‘ ) ( ๐‘ž ( .r โ€˜ ๐‘ ) ๐‘” ) ) ) < ( ( deg1 โ€˜ ๐‘Ÿ ) โ€˜ ๐‘” ) ) ) = ( ๐‘“ โˆˆ ๐ต , ๐‘” โˆˆ ๐ต โ†ฆ ( โ„ฉ ๐‘ž โˆˆ ๐ต ( ๐ท โ€˜ ( ๐‘“ โˆ’ ( ๐‘ž ยท ๐‘” ) ) ) < ( ๐ท โ€˜ ๐‘” ) ) ) )
38 16 37 eqtrd โŠข ( ( ๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐‘ƒ ) โ†’ โฆ‹ ( Base โ€˜ ๐‘ ) / ๐‘ โฆŒ ( ๐‘“ โˆˆ ๐‘ , ๐‘” โˆˆ ๐‘ โ†ฆ ( โ„ฉ ๐‘ž โˆˆ ๐‘ ( ( deg1 โ€˜ ๐‘Ÿ ) โ€˜ ( ๐‘“ ( -g โ€˜ ๐‘ ) ( ๐‘ž ( .r โ€˜ ๐‘ ) ๐‘” ) ) ) < ( ( deg1 โ€˜ ๐‘Ÿ ) โ€˜ ๐‘” ) ) ) = ( ๐‘“ โˆˆ ๐ต , ๐‘” โˆˆ ๐ต โ†ฆ ( โ„ฉ ๐‘ž โˆˆ ๐ต ( ๐ท โ€˜ ( ๐‘“ โˆ’ ( ๐‘ž ยท ๐‘” ) ) ) < ( ๐ท โ€˜ ๐‘” ) ) ) )
39 12 38 csbied โŠข ( ๐‘Ÿ = ๐‘… โ†’ โฆ‹ ๐‘ƒ / ๐‘ โฆŒ โฆ‹ ( Base โ€˜ ๐‘ ) / ๐‘ โฆŒ ( ๐‘“ โˆˆ ๐‘ , ๐‘” โˆˆ ๐‘ โ†ฆ ( โ„ฉ ๐‘ž โˆˆ ๐‘ ( ( deg1 โ€˜ ๐‘Ÿ ) โ€˜ ( ๐‘“ ( -g โ€˜ ๐‘ ) ( ๐‘ž ( .r โ€˜ ๐‘ ) ๐‘” ) ) ) < ( ( deg1 โ€˜ ๐‘Ÿ ) โ€˜ ๐‘” ) ) ) = ( ๐‘“ โˆˆ ๐ต , ๐‘” โˆˆ ๐ต โ†ฆ ( โ„ฉ ๐‘ž โˆˆ ๐ต ( ๐ท โ€˜ ( ๐‘“ โˆ’ ( ๐‘ž ยท ๐‘” ) ) ) < ( ๐ท โ€˜ ๐‘” ) ) ) )
40 10 39 eqtrd โŠข ( ๐‘Ÿ = ๐‘… โ†’ โฆ‹ ( Poly1 โ€˜ ๐‘Ÿ ) / ๐‘ โฆŒ โฆ‹ ( Base โ€˜ ๐‘ ) / ๐‘ โฆŒ ( ๐‘“ โˆˆ ๐‘ , ๐‘” โˆˆ ๐‘ โ†ฆ ( โ„ฉ ๐‘ž โˆˆ ๐‘ ( ( deg1 โ€˜ ๐‘Ÿ ) โ€˜ ( ๐‘“ ( -g โ€˜ ๐‘ ) ( ๐‘ž ( .r โ€˜ ๐‘ ) ๐‘” ) ) ) < ( ( deg1 โ€˜ ๐‘Ÿ ) โ€˜ ๐‘” ) ) ) = ( ๐‘“ โˆˆ ๐ต , ๐‘” โˆˆ ๐ต โ†ฆ ( โ„ฉ ๐‘ž โˆˆ ๐ต ( ๐ท โ€˜ ( ๐‘“ โˆ’ ( ๐‘ž ยท ๐‘” ) ) ) < ( ๐ท โ€˜ ๐‘” ) ) ) )
41 df-q1p โŠข quot1p = ( ๐‘Ÿ โˆˆ V โ†ฆ โฆ‹ ( Poly1 โ€˜ ๐‘Ÿ ) / ๐‘ โฆŒ โฆ‹ ( Base โ€˜ ๐‘ ) / ๐‘ โฆŒ ( ๐‘“ โˆˆ ๐‘ , ๐‘” โˆˆ ๐‘ โ†ฆ ( โ„ฉ ๐‘ž โˆˆ ๐‘ ( ( deg1 โ€˜ ๐‘Ÿ ) โ€˜ ( ๐‘“ ( -g โ€˜ ๐‘ ) ( ๐‘ž ( .r โ€˜ ๐‘ ) ๐‘” ) ) ) < ( ( deg1 โ€˜ ๐‘Ÿ ) โ€˜ ๐‘” ) ) ) )
42 17 17 mpoex โŠข ( ๐‘“ โˆˆ ๐ต , ๐‘” โˆˆ ๐ต โ†ฆ ( โ„ฉ ๐‘ž โˆˆ ๐ต ( ๐ท โ€˜ ( ๐‘“ โˆ’ ( ๐‘ž ยท ๐‘” ) ) ) < ( ๐ท โ€˜ ๐‘” ) ) ) โˆˆ V
43 40 41 42 fvmpt โŠข ( ๐‘… โˆˆ V โ†’ ( quot1p โ€˜ ๐‘… ) = ( ๐‘“ โˆˆ ๐ต , ๐‘” โˆˆ ๐ต โ†ฆ ( โ„ฉ ๐‘ž โˆˆ ๐ต ( ๐ท โ€˜ ( ๐‘“ โˆ’ ( ๐‘ž ยท ๐‘” ) ) ) < ( ๐ท โ€˜ ๐‘” ) ) ) )
44 1 43 eqtrid โŠข ( ๐‘… โˆˆ V โ†’ ๐‘„ = ( ๐‘“ โˆˆ ๐ต , ๐‘” โˆˆ ๐ต โ†ฆ ( โ„ฉ ๐‘ž โˆˆ ๐ต ( ๐ท โ€˜ ( ๐‘“ โˆ’ ( ๐‘ž ยท ๐‘” ) ) ) < ( ๐ท โ€˜ ๐‘” ) ) ) )
45 7 44 syl โŠข ( ๐บ โˆˆ ๐ต โ†’ ๐‘„ = ( ๐‘“ โˆˆ ๐ต , ๐‘” โˆˆ ๐ต โ†ฆ ( โ„ฉ ๐‘ž โˆˆ ๐ต ( ๐ท โ€˜ ( ๐‘“ โˆ’ ( ๐‘ž ยท ๐‘” ) ) ) < ( ๐ท โ€˜ ๐‘” ) ) ) )
46 45 adantl โŠข ( ( ๐น โˆˆ ๐ต โˆง ๐บ โˆˆ ๐ต ) โ†’ ๐‘„ = ( ๐‘“ โˆˆ ๐ต , ๐‘” โˆˆ ๐ต โ†ฆ ( โ„ฉ ๐‘ž โˆˆ ๐ต ( ๐ท โ€˜ ( ๐‘“ โˆ’ ( ๐‘ž ยท ๐‘” ) ) ) < ( ๐ท โ€˜ ๐‘” ) ) ) )
47 id โŠข ( ๐‘“ = ๐น โ†’ ๐‘“ = ๐น )
48 oveq2 โŠข ( ๐‘” = ๐บ โ†’ ( ๐‘ž ยท ๐‘” ) = ( ๐‘ž ยท ๐บ ) )
49 47 48 oveqan12d โŠข ( ( ๐‘“ = ๐น โˆง ๐‘” = ๐บ ) โ†’ ( ๐‘“ โˆ’ ( ๐‘ž ยท ๐‘” ) ) = ( ๐น โˆ’ ( ๐‘ž ยท ๐บ ) ) )
50 49 fveq2d โŠข ( ( ๐‘“ = ๐น โˆง ๐‘” = ๐บ ) โ†’ ( ๐ท โ€˜ ( ๐‘“ โˆ’ ( ๐‘ž ยท ๐‘” ) ) ) = ( ๐ท โ€˜ ( ๐น โˆ’ ( ๐‘ž ยท ๐บ ) ) ) )
51 fveq2 โŠข ( ๐‘” = ๐บ โ†’ ( ๐ท โ€˜ ๐‘” ) = ( ๐ท โ€˜ ๐บ ) )
52 51 adantl โŠข ( ( ๐‘“ = ๐น โˆง ๐‘” = ๐บ ) โ†’ ( ๐ท โ€˜ ๐‘” ) = ( ๐ท โ€˜ ๐บ ) )
53 50 52 breq12d โŠข ( ( ๐‘“ = ๐น โˆง ๐‘” = ๐บ ) โ†’ ( ( ๐ท โ€˜ ( ๐‘“ โˆ’ ( ๐‘ž ยท ๐‘” ) ) ) < ( ๐ท โ€˜ ๐‘” ) โ†” ( ๐ท โ€˜ ( ๐น โˆ’ ( ๐‘ž ยท ๐บ ) ) ) < ( ๐ท โ€˜ ๐บ ) ) )
54 53 riotabidv โŠข ( ( ๐‘“ = ๐น โˆง ๐‘” = ๐บ ) โ†’ ( โ„ฉ ๐‘ž โˆˆ ๐ต ( ๐ท โ€˜ ( ๐‘“ โˆ’ ( ๐‘ž ยท ๐‘” ) ) ) < ( ๐ท โ€˜ ๐‘” ) ) = ( โ„ฉ ๐‘ž โˆˆ ๐ต ( ๐ท โ€˜ ( ๐น โˆ’ ( ๐‘ž ยท ๐บ ) ) ) < ( ๐ท โ€˜ ๐บ ) ) )
55 54 adantl โŠข ( ( ( ๐น โˆˆ ๐ต โˆง ๐บ โˆˆ ๐ต ) โˆง ( ๐‘“ = ๐น โˆง ๐‘” = ๐บ ) ) โ†’ ( โ„ฉ ๐‘ž โˆˆ ๐ต ( ๐ท โ€˜ ( ๐‘“ โˆ’ ( ๐‘ž ยท ๐‘” ) ) ) < ( ๐ท โ€˜ ๐‘” ) ) = ( โ„ฉ ๐‘ž โˆˆ ๐ต ( ๐ท โ€˜ ( ๐น โˆ’ ( ๐‘ž ยท ๐บ ) ) ) < ( ๐ท โ€˜ ๐บ ) ) )
56 simpl โŠข ( ( ๐น โˆˆ ๐ต โˆง ๐บ โˆˆ ๐ต ) โ†’ ๐น โˆˆ ๐ต )
57 simpr โŠข ( ( ๐น โˆˆ ๐ต โˆง ๐บ โˆˆ ๐ต ) โ†’ ๐บ โˆˆ ๐ต )
58 riotaex โŠข ( โ„ฉ ๐‘ž โˆˆ ๐ต ( ๐ท โ€˜ ( ๐น โˆ’ ( ๐‘ž ยท ๐บ ) ) ) < ( ๐ท โ€˜ ๐บ ) ) โˆˆ V
59 58 a1i โŠข ( ( ๐น โˆˆ ๐ต โˆง ๐บ โˆˆ ๐ต ) โ†’ ( โ„ฉ ๐‘ž โˆˆ ๐ต ( ๐ท โ€˜ ( ๐น โˆ’ ( ๐‘ž ยท ๐บ ) ) ) < ( ๐ท โ€˜ ๐บ ) ) โˆˆ V )
60 46 55 56 57 59 ovmpod โŠข ( ( ๐น โˆˆ ๐ต โˆง ๐บ โˆˆ ๐ต ) โ†’ ( ๐น ๐‘„ ๐บ ) = ( โ„ฉ ๐‘ž โˆˆ ๐ต ( ๐ท โ€˜ ( ๐น โˆ’ ( ๐‘ž ยท ๐บ ) ) ) < ( ๐ท โ€˜ ๐บ ) ) )