Metamath Proof Explorer

Theorem q1peqb

Description: Characterizing property of the polynomial quotient. (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 โ€˜ ๐‘ƒ )
q1peqb.c โŠข ๐ถ = ( Unic1p โ€˜ ๐‘… )
Assertion q1peqb ( ( ๐‘… โˆˆ Ring โˆง ๐น โˆˆ ๐ต โˆง ๐บ โˆˆ ๐ถ ) โ†’ ( ( ๐‘‹ โˆˆ ๐ต โˆง ( ๐ท โ€˜ ( ๐น โˆ’ ( ๐‘‹ ยท ๐บ ) ) ) < ( ๐ท โ€˜ ๐บ ) ) โ†” ( ๐น ๐‘„ ๐บ ) = ๐‘‹ ) )

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 q1peqb.c โŠข ๐ถ = ( Unic1p โ€˜ ๐‘… )
8 elex โŠข ( ๐‘‹ โˆˆ ๐ต โ†’ ๐‘‹ โˆˆ V )
9 8 adantr โŠข ( ( ๐‘‹ โˆˆ ๐ต โˆง ( ๐ท โ€˜ ( ๐น โˆ’ ( ๐‘‹ ยท ๐บ ) ) ) < ( ๐ท โ€˜ ๐บ ) ) โ†’ ๐‘‹ โˆˆ V )
10 9 a1i โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐น โˆˆ ๐ต โˆง ๐บ โˆˆ ๐ถ ) โ†’ ( ( ๐‘‹ โˆˆ ๐ต โˆง ( ๐ท โ€˜ ( ๐น โˆ’ ( ๐‘‹ ยท ๐บ ) ) ) < ( ๐ท โ€˜ ๐บ ) ) โ†’ ๐‘‹ โˆˆ V ) )
11 ovex โŠข ( ๐น ๐‘„ ๐บ ) โˆˆ V
12 eleq1 โŠข ( ( ๐น ๐‘„ ๐บ ) = ๐‘‹ โ†’ ( ( ๐น ๐‘„ ๐บ ) โˆˆ V โ†” ๐‘‹ โˆˆ V ) )
13 11 12 mpbii โŠข ( ( ๐น ๐‘„ ๐บ ) = ๐‘‹ โ†’ ๐‘‹ โˆˆ V )
14 13 a1i โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐น โˆˆ ๐ต โˆง ๐บ โˆˆ ๐ถ ) โ†’ ( ( ๐น ๐‘„ ๐บ ) = ๐‘‹ โ†’ ๐‘‹ โˆˆ V ) )
15 simpr โŠข ( ( ( ๐‘… โˆˆ Ring โˆง ๐น โˆˆ ๐ต โˆง ๐บ โˆˆ ๐ถ ) โˆง ๐‘‹ โˆˆ V ) โ†’ ๐‘‹ โˆˆ V )
16 eqid โŠข ( 0g โ€˜ ๐‘ƒ ) = ( 0g โ€˜ ๐‘ƒ )
17 simp1 โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐น โˆˆ ๐ต โˆง ๐บ โˆˆ ๐ถ ) โ†’ ๐‘… โˆˆ Ring )
18 simp2 โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐น โˆˆ ๐ต โˆง ๐บ โˆˆ ๐ถ ) โ†’ ๐น โˆˆ ๐ต )
19 2 3 7 uc1pcl โŠข ( ๐บ โˆˆ ๐ถ โ†’ ๐บ โˆˆ ๐ต )
20 19 3ad2ant3 โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐น โˆˆ ๐ต โˆง ๐บ โˆˆ ๐ถ ) โ†’ ๐บ โˆˆ ๐ต )
21 2 16 7 uc1pn0 โŠข ( ๐บ โˆˆ ๐ถ โ†’ ๐บ โ‰  ( 0g โ€˜ ๐‘ƒ ) )
22 21 3ad2ant3 โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐น โˆˆ ๐ต โˆง ๐บ โˆˆ ๐ถ ) โ†’ ๐บ โ‰  ( 0g โ€˜ ๐‘ƒ ) )
23 eqid โŠข ( Unit โ€˜ ๐‘… ) = ( Unit โ€˜ ๐‘… )
24 4 23 7 uc1pldg โŠข ( ๐บ โˆˆ ๐ถ โ†’ ( ( coe1 โ€˜ ๐บ ) โ€˜ ( ๐ท โ€˜ ๐บ ) ) โˆˆ ( Unit โ€˜ ๐‘… ) )
25 24 3ad2ant3 โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐น โˆˆ ๐ต โˆง ๐บ โˆˆ ๐ถ ) โ†’ ( ( coe1 โ€˜ ๐บ ) โ€˜ ( ๐ท โ€˜ ๐บ ) ) โˆˆ ( Unit โ€˜ ๐‘… ) )
26 2 4 3 5 16 6 17 18 20 22 25 23 ply1divalg2 โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐น โˆˆ ๐ต โˆง ๐บ โˆˆ ๐ถ ) โ†’ โˆƒ! ๐‘ž โˆˆ ๐ต ( ๐ท โ€˜ ( ๐น โˆ’ ( ๐‘ž ยท ๐บ ) ) ) < ( ๐ท โ€˜ ๐บ ) )
27 df-reu โŠข ( โˆƒ! ๐‘ž โˆˆ ๐ต ( ๐ท โ€˜ ( ๐น โˆ’ ( ๐‘ž ยท ๐บ ) ) ) < ( ๐ท โ€˜ ๐บ ) โ†” โˆƒ! ๐‘ž ( ๐‘ž โˆˆ ๐ต โˆง ( ๐ท โ€˜ ( ๐น โˆ’ ( ๐‘ž ยท ๐บ ) ) ) < ( ๐ท โ€˜ ๐บ ) ) )
28 26 27 sylib โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐น โˆˆ ๐ต โˆง ๐บ โˆˆ ๐ถ ) โ†’ โˆƒ! ๐‘ž ( ๐‘ž โˆˆ ๐ต โˆง ( ๐ท โ€˜ ( ๐น โˆ’ ( ๐‘ž ยท ๐บ ) ) ) < ( ๐ท โ€˜ ๐บ ) ) )
29 28 adantr โŠข ( ( ( ๐‘… โˆˆ Ring โˆง ๐น โˆˆ ๐ต โˆง ๐บ โˆˆ ๐ถ ) โˆง ๐‘‹ โˆˆ V ) โ†’ โˆƒ! ๐‘ž ( ๐‘ž โˆˆ ๐ต โˆง ( ๐ท โ€˜ ( ๐น โˆ’ ( ๐‘ž ยท ๐บ ) ) ) < ( ๐ท โ€˜ ๐บ ) ) )
30 eleq1 โŠข ( ๐‘ž = ๐‘‹ โ†’ ( ๐‘ž โˆˆ ๐ต โ†” ๐‘‹ โˆˆ ๐ต ) )
31 oveq1 โŠข ( ๐‘ž = ๐‘‹ โ†’ ( ๐‘ž ยท ๐บ ) = ( ๐‘‹ ยท ๐บ ) )
32 31 oveq2d โŠข ( ๐‘ž = ๐‘‹ โ†’ ( ๐น โˆ’ ( ๐‘ž ยท ๐บ ) ) = ( ๐น โˆ’ ( ๐‘‹ ยท ๐บ ) ) )
33 32 fveq2d โŠข ( ๐‘ž = ๐‘‹ โ†’ ( ๐ท โ€˜ ( ๐น โˆ’ ( ๐‘ž ยท ๐บ ) ) ) = ( ๐ท โ€˜ ( ๐น โˆ’ ( ๐‘‹ ยท ๐บ ) ) ) )
34 33 breq1d โŠข ( ๐‘ž = ๐‘‹ โ†’ ( ( ๐ท โ€˜ ( ๐น โˆ’ ( ๐‘ž ยท ๐บ ) ) ) < ( ๐ท โ€˜ ๐บ ) โ†” ( ๐ท โ€˜ ( ๐น โˆ’ ( ๐‘‹ ยท ๐บ ) ) ) < ( ๐ท โ€˜ ๐บ ) ) )
35 30 34 anbi12d โŠข ( ๐‘ž = ๐‘‹ โ†’ ( ( ๐‘ž โˆˆ ๐ต โˆง ( ๐ท โ€˜ ( ๐น โˆ’ ( ๐‘ž ยท ๐บ ) ) ) < ( ๐ท โ€˜ ๐บ ) ) โ†” ( ๐‘‹ โˆˆ ๐ต โˆง ( ๐ท โ€˜ ( ๐น โˆ’ ( ๐‘‹ ยท ๐บ ) ) ) < ( ๐ท โ€˜ ๐บ ) ) ) )
36 35 adantl โŠข ( ( ( ( ๐‘… โˆˆ Ring โˆง ๐น โˆˆ ๐ต โˆง ๐บ โˆˆ ๐ถ ) โˆง ๐‘‹ โˆˆ V ) โˆง ๐‘ž = ๐‘‹ ) โ†’ ( ( ๐‘ž โˆˆ ๐ต โˆง ( ๐ท โ€˜ ( ๐น โˆ’ ( ๐‘ž ยท ๐บ ) ) ) < ( ๐ท โ€˜ ๐บ ) ) โ†” ( ๐‘‹ โˆˆ ๐ต โˆง ( ๐ท โ€˜ ( ๐น โˆ’ ( ๐‘‹ ยท ๐บ ) ) ) < ( ๐ท โ€˜ ๐บ ) ) ) )
37 15 29 36 iota2d โŠข ( ( ( ๐‘… โˆˆ Ring โˆง ๐น โˆˆ ๐ต โˆง ๐บ โˆˆ ๐ถ ) โˆง ๐‘‹ โˆˆ V ) โ†’ ( ( ๐‘‹ โˆˆ ๐ต โˆง ( ๐ท โ€˜ ( ๐น โˆ’ ( ๐‘‹ ยท ๐บ ) ) ) < ( ๐ท โ€˜ ๐บ ) ) โ†” ( โ„ฉ ๐‘ž ( ๐‘ž โˆˆ ๐ต โˆง ( ๐ท โ€˜ ( ๐น โˆ’ ( ๐‘ž ยท ๐บ ) ) ) < ( ๐ท โ€˜ ๐บ ) ) ) = ๐‘‹ ) )
38 1 2 3 4 5 6 q1pval โŠข ( ( ๐น โˆˆ ๐ต โˆง ๐บ โˆˆ ๐ต ) โ†’ ( ๐น ๐‘„ ๐บ ) = ( โ„ฉ ๐‘ž โˆˆ ๐ต ( ๐ท โ€˜ ( ๐น โˆ’ ( ๐‘ž ยท ๐บ ) ) ) < ( ๐ท โ€˜ ๐บ ) ) )
39 18 20 38 syl2anc โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐น โˆˆ ๐ต โˆง ๐บ โˆˆ ๐ถ ) โ†’ ( ๐น ๐‘„ ๐บ ) = ( โ„ฉ ๐‘ž โˆˆ ๐ต ( ๐ท โ€˜ ( ๐น โˆ’ ( ๐‘ž ยท ๐บ ) ) ) < ( ๐ท โ€˜ ๐บ ) ) )
40 df-riota โŠข ( โ„ฉ ๐‘ž โˆˆ ๐ต ( ๐ท โ€˜ ( ๐น โˆ’ ( ๐‘ž ยท ๐บ ) ) ) < ( ๐ท โ€˜ ๐บ ) ) = ( โ„ฉ ๐‘ž ( ๐‘ž โˆˆ ๐ต โˆง ( ๐ท โ€˜ ( ๐น โˆ’ ( ๐‘ž ยท ๐บ ) ) ) < ( ๐ท โ€˜ ๐บ ) ) )
41 39 40 eqtrdi โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐น โˆˆ ๐ต โˆง ๐บ โˆˆ ๐ถ ) โ†’ ( ๐น ๐‘„ ๐บ ) = ( โ„ฉ ๐‘ž ( ๐‘ž โˆˆ ๐ต โˆง ( ๐ท โ€˜ ( ๐น โˆ’ ( ๐‘ž ยท ๐บ ) ) ) < ( ๐ท โ€˜ ๐บ ) ) ) )
42 41 adantr โŠข ( ( ( ๐‘… โˆˆ Ring โˆง ๐น โˆˆ ๐ต โˆง ๐บ โˆˆ ๐ถ ) โˆง ๐‘‹ โˆˆ V ) โ†’ ( ๐น ๐‘„ ๐บ ) = ( โ„ฉ ๐‘ž ( ๐‘ž โˆˆ ๐ต โˆง ( ๐ท โ€˜ ( ๐น โˆ’ ( ๐‘ž ยท ๐บ ) ) ) < ( ๐ท โ€˜ ๐บ ) ) ) )
43 42 eqeq1d โŠข ( ( ( ๐‘… โˆˆ Ring โˆง ๐น โˆˆ ๐ต โˆง ๐บ โˆˆ ๐ถ ) โˆง ๐‘‹ โˆˆ V ) โ†’ ( ( ๐น ๐‘„ ๐บ ) = ๐‘‹ โ†” ( โ„ฉ ๐‘ž ( ๐‘ž โˆˆ ๐ต โˆง ( ๐ท โ€˜ ( ๐น โˆ’ ( ๐‘ž ยท ๐บ ) ) ) < ( ๐ท โ€˜ ๐บ ) ) ) = ๐‘‹ ) )
44 37 43 bitr4d โŠข ( ( ( ๐‘… โˆˆ Ring โˆง ๐น โˆˆ ๐ต โˆง ๐บ โˆˆ ๐ถ ) โˆง ๐‘‹ โˆˆ V ) โ†’ ( ( ๐‘‹ โˆˆ ๐ต โˆง ( ๐ท โ€˜ ( ๐น โˆ’ ( ๐‘‹ ยท ๐บ ) ) ) < ( ๐ท โ€˜ ๐บ ) ) โ†” ( ๐น ๐‘„ ๐บ ) = ๐‘‹ ) )
45 44 ex โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐น โˆˆ ๐ต โˆง ๐บ โˆˆ ๐ถ ) โ†’ ( ๐‘‹ โˆˆ V โ†’ ( ( ๐‘‹ โˆˆ ๐ต โˆง ( ๐ท โ€˜ ( ๐น โˆ’ ( ๐‘‹ ยท ๐บ ) ) ) < ( ๐ท โ€˜ ๐บ ) ) โ†” ( ๐น ๐‘„ ๐บ ) = ๐‘‹ ) ) )
46 10 14 45 pm5.21ndd โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐น โˆˆ ๐ต โˆง ๐บ โˆˆ ๐ถ ) โ†’ ( ( ๐‘‹ โˆˆ ๐ต โˆง ( ๐ท โ€˜ ( ๐น โˆ’ ( ๐‘‹ ยท ๐บ ) ) ) < ( ๐ท โ€˜ ๐บ ) ) โ†” ( ๐น ๐‘„ ๐บ ) = ๐‘‹ ) )