Step | Hyp | Ref
| Expression |
1 | | uc1pval.c |
. 2
β’ πΆ =
(Unic1pβπ
) |
2 | | fveq2 6846 |
. . . . . . . 8
β’ (π = π
β (Poly1βπ) =
(Poly1βπ
)) |
3 | | uc1pval.p |
. . . . . . . 8
β’ π = (Poly1βπ
) |
4 | 2, 3 | eqtr4di 2791 |
. . . . . . 7
β’ (π = π
β (Poly1βπ) = π) |
5 | 4 | fveq2d 6850 |
. . . . . 6
β’ (π = π
β
(Baseβ(Poly1βπ)) = (Baseβπ)) |
6 | | uc1pval.b |
. . . . . 6
β’ π΅ = (Baseβπ) |
7 | 5, 6 | eqtr4di 2791 |
. . . . 5
β’ (π = π
β
(Baseβ(Poly1βπ)) = π΅) |
8 | 4 | fveq2d 6850 |
. . . . . . . 8
β’ (π = π
β
(0gβ(Poly1βπ)) = (0gβπ)) |
9 | | uc1pval.z |
. . . . . . . 8
β’ 0 =
(0gβπ) |
10 | 8, 9 | eqtr4di 2791 |
. . . . . . 7
β’ (π = π
β
(0gβ(Poly1βπ)) = 0 ) |
11 | 10 | neeq2d 3001 |
. . . . . 6
β’ (π = π
β (π β
(0gβ(Poly1βπ)) β π β 0 )) |
12 | | fveq2 6846 |
. . . . . . . . . 10
β’ (π = π
β ( deg1 βπ) = ( deg1
βπ
)) |
13 | | uc1pval.d |
. . . . . . . . . 10
β’ π· = ( deg1
βπ
) |
14 | 12, 13 | eqtr4di 2791 |
. . . . . . . . 9
β’ (π = π
β ( deg1 βπ) = π·) |
15 | 14 | fveq1d 6848 |
. . . . . . . 8
β’ (π = π
β (( deg1 βπ)βπ) = (π·βπ)) |
16 | 15 | fveq2d 6850 |
. . . . . . 7
β’ (π = π
β ((coe1βπ)β(( deg1
βπ)βπ)) =
((coe1βπ)β(π·βπ))) |
17 | | fveq2 6846 |
. . . . . . . 8
β’ (π = π
β (Unitβπ) = (Unitβπ
)) |
18 | | uc1pval.u |
. . . . . . . 8
β’ π = (Unitβπ
) |
19 | 17, 18 | eqtr4di 2791 |
. . . . . . 7
β’ (π = π
β (Unitβπ) = π) |
20 | 16, 19 | eleq12d 2828 |
. . . . . 6
β’ (π = π
β (((coe1βπ)β(( deg1
βπ)βπ)) β (Unitβπ) β
((coe1βπ)β(π·βπ)) β π)) |
21 | 11, 20 | anbi12d 632 |
. . . . 5
β’ (π = π
β ((π β
(0gβ(Poly1βπ)) β§ ((coe1βπ)β(( deg1
βπ)βπ)) β (Unitβπ)) β (π β 0 β§
((coe1βπ)β(π·βπ)) β π))) |
22 | 7, 21 | rabeqbidv 3423 |
. . . 4
β’ (π = π
β {π β
(Baseβ(Poly1βπ)) β£ (π β
(0gβ(Poly1βπ)) β§ ((coe1βπ)β(( deg1
βπ)βπ)) β (Unitβπ))} = {π β π΅ β£ (π β 0 β§
((coe1βπ)β(π·βπ)) β π)}) |
23 | | df-uc1p 25519 |
. . . 4
β’
Unic1p = (π β V β¦ {π β
(Baseβ(Poly1βπ)) β£ (π β
(0gβ(Poly1βπ)) β§ ((coe1βπ)β(( deg1
βπ)βπ)) β (Unitβπ))}) |
24 | 6 | fvexi 6860 |
. . . . 5
β’ π΅ β V |
25 | 24 | rabex 5293 |
. . . 4
β’ {π β π΅ β£ (π β 0 β§
((coe1βπ)β(π·βπ)) β π)} β V |
26 | 22, 23, 25 | fvmpt 6952 |
. . 3
β’ (π
β V β
(Unic1pβπ
)
= {π β π΅ β£ (π β 0 β§
((coe1βπ)β(π·βπ)) β π)}) |
27 | | fvprc 6838 |
. . . 4
β’ (Β¬
π
β V β
(Unic1pβπ
)
= β
) |
28 | | ssrab2 4041 |
. . . . . 6
β’ {π β π΅ β£ (π β 0 β§
((coe1βπ)β(π·βπ)) β π)} β π΅ |
29 | | fvprc 6838 |
. . . . . . . . . 10
β’ (Β¬
π
β V β
(Poly1βπ
)
= β
) |
30 | 3, 29 | eqtrid 2785 |
. . . . . . . . 9
β’ (Β¬
π
β V β π = β
) |
31 | 30 | fveq2d 6850 |
. . . . . . . 8
β’ (Β¬
π
β V β
(Baseβπ) =
(Baseββ
)) |
32 | | base0 17096 |
. . . . . . . 8
β’ β
=
(Baseββ
) |
33 | 31, 32 | eqtr4di 2791 |
. . . . . . 7
β’ (Β¬
π
β V β
(Baseβπ) =
β
) |
34 | 6, 33 | eqtrid 2785 |
. . . . . 6
β’ (Β¬
π
β V β π΅ = β
) |
35 | 28, 34 | sseqtrid 4000 |
. . . . 5
β’ (Β¬
π
β V β {π β π΅ β£ (π β 0 β§
((coe1βπ)β(π·βπ)) β π)} β β
) |
36 | | ss0 4362 |
. . . . 5
β’ ({π β π΅ β£ (π β 0 β§
((coe1βπ)β(π·βπ)) β π)} β β
β {π β π΅ β£ (π β 0 β§
((coe1βπ)β(π·βπ)) β π)} = β
) |
37 | 35, 36 | syl 17 |
. . . 4
β’ (Β¬
π
β V β {π β π΅ β£ (π β 0 β§
((coe1βπ)β(π·βπ)) β π)} = β
) |
38 | 27, 37 | eqtr4d 2776 |
. . 3
β’ (Β¬
π
β V β
(Unic1pβπ
)
= {π β π΅ β£ (π β 0 β§
((coe1βπ)β(π·βπ)) β π)}) |
39 | 26, 38 | pm2.61i 182 |
. 2
β’
(Unic1pβπ
) = {π β π΅ β£ (π β 0 β§
((coe1βπ)β(π·βπ)) β π)} |
40 | 1, 39 | eqtri 2761 |
1
β’ πΆ = {π β π΅ β£ (π β 0 β§
((coe1βπ)β(π·βπ)) β π)} |