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 |
โข ( ( ๐น โ ๐ต โง ๐บ โ ๐ต ) โ ( ๐น ๐ ๐บ ) = ( โฉ ๐ โ ๐ต ( ๐ท โ ( ๐น โ ( ๐ ยท ๐บ ) ) ) < ( ๐ท โ ๐บ ) ) ) |