Step | Hyp | Ref
| Expression |
1 | | q1pval.p |
. . . . 5
โข ๐ = (Poly1โ๐
) |
2 | | q1pval.b |
. . . . 5
โข ๐ต = (Baseโ๐) |
3 | 1, 2 | elbasfv 16959 |
. . . 4
โข (๐บ โ ๐ต โ ๐
โ V) |
4 | | q1pval.q |
. . . . 5
โข ๐ =
(quot1pโ๐
) |
5 | | fveq2 6800 |
. . . . . . . . 9
โข (๐ = ๐
โ (Poly1โ๐) =
(Poly1โ๐
)) |
6 | 5, 1 | eqtr4di 2794 |
. . . . . . . 8
โข (๐ = ๐
โ (Poly1โ๐) = ๐) |
7 | 6 | csbeq1d 3841 |
. . . . . . 7
โข (๐ = ๐
โ
โฆ(Poly1โ๐) / ๐โฆโฆ(Baseโ๐) / ๐โฆ(๐ โ ๐, ๐ โ ๐ โฆ (โฉ๐ โ ๐ (( deg1 โ๐)โ(๐(-gโ๐)(๐(.rโ๐)๐))) < (( deg1 โ๐)โ๐))) = โฆ๐ / ๐โฆโฆ(Baseโ๐) / ๐โฆ(๐ โ ๐, ๐ โ ๐ โฆ (โฉ๐ โ ๐ (( deg1 โ๐)โ(๐(-gโ๐)(๐(.rโ๐)๐))) < (( deg1 โ๐)โ๐)))) |
8 | 1 | fvexi 6814 |
. . . . . . . . 9
โข ๐ โ V |
9 | 8 | a1i 11 |
. . . . . . . 8
โข (๐ = ๐
โ ๐ โ V) |
10 | | fveq2 6800 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ (Baseโ๐) = (Baseโ๐)) |
11 | 10 | adantl 483 |
. . . . . . . . . . 11
โข ((๐ = ๐
โง ๐ = ๐) โ (Baseโ๐) = (Baseโ๐)) |
12 | 11, 2 | eqtr4di 2794 |
. . . . . . . . . 10
โข ((๐ = ๐
โง ๐ = ๐) โ (Baseโ๐) = ๐ต) |
13 | 12 | csbeq1d 3841 |
. . . . . . . . 9
โข ((๐ = ๐
โง ๐ = ๐) โ โฆ(Baseโ๐) / ๐โฆ(๐ โ ๐, ๐ โ ๐ โฆ (โฉ๐ โ ๐ (( deg1 โ๐)โ(๐(-gโ๐)(๐(.rโ๐)๐))) < (( deg1 โ๐)โ๐))) = โฆ๐ต / ๐โฆ(๐ โ ๐, ๐ โ ๐ โฆ (โฉ๐ โ ๐ (( deg1 โ๐)โ(๐(-gโ๐)(๐(.rโ๐)๐))) < (( deg1 โ๐)โ๐)))) |
14 | 2 | fvexi 6814 |
. . . . . . . . . . 11
โข ๐ต โ V |
15 | 14 | a1i 11 |
. . . . . . . . . 10
โข ((๐ = ๐
โง ๐ = ๐) โ ๐ต โ V) |
16 | | simpr 486 |
. . . . . . . . . . 11
โข (((๐ = ๐
โง ๐ = ๐) โง ๐ = ๐ต) โ ๐ = ๐ต) |
17 | | fveq2 6800 |
. . . . . . . . . . . . . . . 16
โข (๐ = ๐
โ ( deg1 โ๐) = ( deg1
โ๐
)) |
18 | 17 | ad2antrr 724 |
. . . . . . . . . . . . . . 15
โข (((๐ = ๐
โง ๐ = ๐) โง ๐ = ๐ต) โ ( deg1 โ๐) = ( deg1
โ๐
)) |
19 | | q1pval.d |
. . . . . . . . . . . . . . 15
โข ๐ท = ( deg1
โ๐
) |
20 | 18, 19 | eqtr4di 2794 |
. . . . . . . . . . . . . 14
โข (((๐ = ๐
โง ๐ = ๐) โง ๐ = ๐ต) โ ( deg1 โ๐) = ๐ท) |
21 | | fveq2 6800 |
. . . . . . . . . . . . . . . . 17
โข (๐ = ๐ โ (-gโ๐) = (-gโ๐)) |
22 | 21 | ad2antlr 725 |
. . . . . . . . . . . . . . . 16
โข (((๐ = ๐
โง ๐ = ๐) โง ๐ = ๐ต) โ (-gโ๐) = (-gโ๐)) |
23 | | q1pval.m |
. . . . . . . . . . . . . . . 16
โข โ =
(-gโ๐) |
24 | 22, 23 | eqtr4di 2794 |
. . . . . . . . . . . . . . 15
โข (((๐ = ๐
โง ๐ = ๐) โง ๐ = ๐ต) โ (-gโ๐) = โ ) |
25 | | eqidd 2737 |
. . . . . . . . . . . . . . 15
โข (((๐ = ๐
โง ๐ = ๐) โง ๐ = ๐ต) โ ๐ = ๐) |
26 | | fveq2 6800 |
. . . . . . . . . . . . . . . . . 18
โข (๐ = ๐ โ (.rโ๐) = (.rโ๐)) |
27 | 26 | ad2antlr 725 |
. . . . . . . . . . . . . . . . 17
โข (((๐ = ๐
โง ๐ = ๐) โง ๐ = ๐ต) โ (.rโ๐) = (.rโ๐)) |
28 | | q1pval.t |
. . . . . . . . . . . . . . . . 17
โข ยท =
(.rโ๐) |
29 | 27, 28 | eqtr4di 2794 |
. . . . . . . . . . . . . . . 16
โข (((๐ = ๐
โง ๐ = ๐) โง ๐ = ๐ต) โ (.rโ๐) = ยท ) |
30 | 29 | oveqd 7320 |
. . . . . . . . . . . . . . 15
โข (((๐ = ๐
โง ๐ = ๐) โง ๐ = ๐ต) โ (๐(.rโ๐)๐) = (๐ ยท ๐)) |
31 | 24, 25, 30 | oveq123d 7324 |
. . . . . . . . . . . . . 14
โข (((๐ = ๐
โง ๐ = ๐) โง ๐ = ๐ต) โ (๐(-gโ๐)(๐(.rโ๐)๐)) = (๐ โ (๐ ยท ๐))) |
32 | 20, 31 | fveq12d 6807 |
. . . . . . . . . . . . 13
โข (((๐ = ๐
โง ๐ = ๐) โง ๐ = ๐ต) โ (( deg1 โ๐)โ(๐(-gโ๐)(๐(.rโ๐)๐))) = (๐ทโ(๐ โ (๐ ยท ๐)))) |
33 | 20 | fveq1d 6802 |
. . . . . . . . . . . . 13
โข (((๐ = ๐
โง ๐ = ๐) โง ๐ = ๐ต) โ (( deg1 โ๐)โ๐) = (๐ทโ๐)) |
34 | 32, 33 | breq12d 5094 |
. . . . . . . . . . . 12
โข (((๐ = ๐
โง ๐ = ๐) โง ๐ = ๐ต) โ ((( deg1 โ๐)โ(๐(-gโ๐)(๐(.rโ๐)๐))) < (( deg1 โ๐)โ๐) โ (๐ทโ(๐ โ (๐ ยท ๐))) < (๐ทโ๐))) |
35 | 16, 34 | riotaeqbidv 7263 |
. . . . . . . . . . 11
โข (((๐ = ๐
โง ๐ = ๐) โง ๐ = ๐ต) โ (โฉ๐ โ ๐ (( deg1 โ๐)โ(๐(-gโ๐)(๐(.rโ๐)๐))) < (( deg1 โ๐)โ๐)) = (โฉ๐ โ ๐ต (๐ทโ(๐ โ (๐ ยท ๐))) < (๐ทโ๐))) |
36 | 16, 16, 35 | mpoeq123dv 7378 |
. . . . . . . . . 10
โข (((๐ = ๐
โง ๐ = ๐) โง ๐ = ๐ต) โ (๐ โ ๐, ๐ โ ๐ โฆ (โฉ๐ โ ๐ (( deg1 โ๐)โ(๐(-gโ๐)(๐(.rโ๐)๐))) < (( deg1 โ๐)โ๐))) = (๐ โ ๐ต, ๐ โ ๐ต โฆ (โฉ๐ โ ๐ต (๐ทโ(๐ โ (๐ ยท ๐))) < (๐ทโ๐)))) |
37 | 15, 36 | csbied 3875 |
. . . . . . . . 9
โข ((๐ = ๐
โง ๐ = ๐) โ โฆ๐ต / ๐โฆ(๐ โ ๐, ๐ โ ๐ โฆ (โฉ๐ โ ๐ (( deg1 โ๐)โ(๐(-gโ๐)(๐(.rโ๐)๐))) < (( deg1 โ๐)โ๐))) = (๐ โ ๐ต, ๐ โ ๐ต โฆ (โฉ๐ โ ๐ต (๐ทโ(๐ โ (๐ ยท ๐))) < (๐ทโ๐)))) |
38 | 13, 37 | eqtrd 2776 |
. . . . . . . 8
โข ((๐ = ๐
โง ๐ = ๐) โ โฆ(Baseโ๐) / ๐โฆ(๐ โ ๐, ๐ โ ๐ โฆ (โฉ๐ โ ๐ (( deg1 โ๐)โ(๐(-gโ๐)(๐(.rโ๐)๐))) < (( deg1 โ๐)โ๐))) = (๐ โ ๐ต, ๐ โ ๐ต โฆ (โฉ๐ โ ๐ต (๐ทโ(๐ โ (๐ ยท ๐))) < (๐ทโ๐)))) |
39 | 9, 38 | csbied 3875 |
. . . . . . 7
โข (๐ = ๐
โ โฆ๐ / ๐โฆโฆ(Baseโ๐) / ๐โฆ(๐ โ ๐, ๐ โ ๐ โฆ (โฉ๐ โ ๐ (( deg1 โ๐)โ(๐(-gโ๐)(๐(.rโ๐)๐))) < (( deg1 โ๐)โ๐))) = (๐ โ ๐ต, ๐ โ ๐ต โฆ (โฉ๐ โ ๐ต (๐ทโ(๐ โ (๐ ยท ๐))) < (๐ทโ๐)))) |
40 | 7, 39 | eqtrd 2776 |
. . . . . 6
โข (๐ = ๐
โ
โฆ(Poly1โ๐) / ๐โฆโฆ(Baseโ๐) / ๐โฆ(๐ โ ๐, ๐ โ ๐ โฆ (โฉ๐ โ ๐ (( deg1 โ๐)โ(๐(-gโ๐)(๐(.rโ๐)๐))) < (( deg1 โ๐)โ๐))) = (๐ โ ๐ต, ๐ โ ๐ต โฆ (โฉ๐ โ ๐ต (๐ทโ(๐ โ (๐ ยท ๐))) < (๐ทโ๐)))) |
41 | | df-q1p 25338 |
. . . . . 6
โข
quot1p = (๐ โ V โฆ
โฆ(Poly1โ๐) / ๐โฆโฆ(Baseโ๐) / ๐โฆ(๐ โ ๐, ๐ โ ๐ โฆ (โฉ๐ โ ๐ (( deg1 โ๐)โ(๐(-gโ๐)(๐(.rโ๐)๐))) < (( deg1 โ๐)โ๐)))) |
42 | 14, 14 | mpoex 7948 |
. . . . . 6
โข (๐ โ ๐ต, ๐ โ ๐ต โฆ (โฉ๐ โ ๐ต (๐ทโ(๐ โ (๐ ยท ๐))) < (๐ทโ๐))) โ V |
43 | 40, 41, 42 | fvmpt 6903 |
. . . . 5
โข (๐
โ V โ
(quot1pโ๐
)
= (๐ โ ๐ต, ๐ โ ๐ต โฆ (โฉ๐ โ ๐ต (๐ทโ(๐ โ (๐ ยท ๐))) < (๐ทโ๐)))) |
44 | 4, 43 | eqtrid 2788 |
. . . 4
โข (๐
โ V โ ๐ = (๐ โ ๐ต, ๐ โ ๐ต โฆ (โฉ๐ โ ๐ต (๐ทโ(๐ โ (๐ ยท ๐))) < (๐ทโ๐)))) |
45 | 3, 44 | syl 17 |
. . 3
โข (๐บ โ ๐ต โ ๐ = (๐ โ ๐ต, ๐ โ ๐ต โฆ (โฉ๐ โ ๐ต (๐ทโ(๐ โ (๐ ยท ๐))) < (๐ทโ๐)))) |
46 | 45 | adantl 483 |
. 2
โข ((๐น โ ๐ต โง ๐บ โ ๐ต) โ ๐ = (๐ โ ๐ต, ๐ โ ๐ต โฆ (โฉ๐ โ ๐ต (๐ทโ(๐ โ (๐ ยท ๐))) < (๐ทโ๐)))) |
47 | | id 22 |
. . . . . . 7
โข (๐ = ๐น โ ๐ = ๐น) |
48 | | oveq2 7311 |
. . . . . . 7
โข (๐ = ๐บ โ (๐ ยท ๐) = (๐ ยท ๐บ)) |
49 | 47, 48 | oveqan12d 7322 |
. . . . . 6
โข ((๐ = ๐น โง ๐ = ๐บ) โ (๐ โ (๐ ยท ๐)) = (๐น โ (๐ ยท ๐บ))) |
50 | 49 | fveq2d 6804 |
. . . . 5
โข ((๐ = ๐น โง ๐ = ๐บ) โ (๐ทโ(๐ โ (๐ ยท ๐))) = (๐ทโ(๐น โ (๐ ยท ๐บ)))) |
51 | | fveq2 6800 |
. . . . . 6
โข (๐ = ๐บ โ (๐ทโ๐) = (๐ทโ๐บ)) |
52 | 51 | adantl 483 |
. . . . 5
โข ((๐ = ๐น โง ๐ = ๐บ) โ (๐ทโ๐) = (๐ทโ๐บ)) |
53 | 50, 52 | breq12d 5094 |
. . . 4
โข ((๐ = ๐น โง ๐ = ๐บ) โ ((๐ทโ(๐ โ (๐ ยท ๐))) < (๐ทโ๐) โ (๐ทโ(๐น โ (๐ ยท ๐บ))) < (๐ทโ๐บ))) |
54 | 53 | riotabidv 7262 |
. . 3
โข ((๐ = ๐น โง ๐ = ๐บ) โ (โฉ๐ โ ๐ต (๐ทโ(๐ โ (๐ ยท ๐))) < (๐ทโ๐)) = (โฉ๐ โ ๐ต (๐ทโ(๐น โ (๐ ยท ๐บ))) < (๐ทโ๐บ))) |
55 | 54 | adantl 483 |
. 2
โข (((๐น โ ๐ต โง ๐บ โ ๐ต) โง (๐ = ๐น โง ๐ = ๐บ)) โ (โฉ๐ โ ๐ต (๐ทโ(๐ โ (๐ ยท ๐))) < (๐ทโ๐)) = (โฉ๐ โ ๐ต (๐ทโ(๐น โ (๐ ยท ๐บ))) < (๐ทโ๐บ))) |
56 | | simpl 484 |
. 2
โข ((๐น โ ๐ต โง ๐บ โ ๐ต) โ ๐น โ ๐ต) |
57 | | simpr 486 |
. 2
โข ((๐น โ ๐ต โง ๐บ โ ๐ต) โ ๐บ โ ๐ต) |
58 | | riotaex 7264 |
. . 3
โข
(โฉ๐
โ ๐ต (๐ทโ(๐น โ (๐ ยท ๐บ))) < (๐ทโ๐บ)) โ V |
59 | 58 | a1i 11 |
. 2
โข ((๐น โ ๐ต โง ๐บ โ ๐ต) โ (โฉ๐ โ ๐ต (๐ทโ(๐น โ (๐ ยท ๐บ))) < (๐ทโ๐บ)) โ V) |
60 | 46, 55, 56, 57, 59 | ovmpod 7453 |
1
โข ((๐น โ ๐ต โง ๐บ โ ๐ต) โ (๐น๐๐บ) = (โฉ๐ โ ๐ต (๐ทโ(๐น โ (๐ ยท ๐บ))) < (๐ทโ๐บ))) |