Step | Hyp | Ref
| Expression |
1 | | df-rprm 20152 |
. 2
β’ RPrime =
(π β V β¦
β¦(Baseβπ) / πβ¦{π β (π β ((Unitβπ) βͺ {(0gβπ)})) β£ βπ₯ β π βπ¦ β π [(β₯rβπ) / π](ππ(π₯(.rβπ)π¦) β (πππ₯ β¨ πππ¦))}) |
2 | | fvexd 6861 |
. . 3
β’ (π = π
β (Baseβπ) β V) |
3 | | simpr 486 |
. . . . . . 7
β’ ((π = π
β§ π = (Baseβπ)) β π = (Baseβπ)) |
4 | | fveq2 6846 |
. . . . . . . 8
β’ (π = π
β (Baseβπ) = (Baseβπ
)) |
5 | 4 | adantr 482 |
. . . . . . 7
β’ ((π = π
β§ π = (Baseβπ)) β (Baseβπ) = (Baseβπ
)) |
6 | 3, 5 | eqtrd 2773 |
. . . . . 6
β’ ((π = π
β§ π = (Baseβπ)) β π = (Baseβπ
)) |
7 | | rprmval.b |
. . . . . 6
β’ π΅ = (Baseβπ
) |
8 | 6, 7 | eqtr4di 2791 |
. . . . 5
β’ ((π = π
β§ π = (Baseβπ)) β π = π΅) |
9 | | fveq2 6846 |
. . . . . . . 8
β’ (π = π
β (Unitβπ) = (Unitβπ
)) |
10 | | rprmval.u |
. . . . . . . 8
β’ π = (Unitβπ
) |
11 | 9, 10 | eqtr4di 2791 |
. . . . . . 7
β’ (π = π
β (Unitβπ) = π) |
12 | | fveq2 6846 |
. . . . . . . . 9
β’ (π = π
β (0gβπ) = (0gβπ
)) |
13 | | rprmval.1 |
. . . . . . . . 9
β’ 0 =
(0gβπ
) |
14 | 12, 13 | eqtr4di 2791 |
. . . . . . . 8
β’ (π = π
β (0gβπ) = 0 ) |
15 | 14 | sneqd 4602 |
. . . . . . 7
β’ (π = π
β {(0gβπ)} = { 0 }) |
16 | 11, 15 | uneq12d 4128 |
. . . . . 6
β’ (π = π
β ((Unitβπ) βͺ {(0gβπ)}) = (π βͺ { 0 })) |
17 | 16 | adantr 482 |
. . . . 5
β’ ((π = π
β§ π = (Baseβπ)) β ((Unitβπ) βͺ {(0gβπ)}) = (π βͺ { 0 })) |
18 | 8, 17 | difeq12d 4087 |
. . . 4
β’ ((π = π
β§ π = (Baseβπ)) β (π β ((Unitβπ) βͺ {(0gβπ)})) = (π΅ β (π βͺ { 0 }))) |
19 | | fvexd 6861 |
. . . . . . 7
β’ ((π = π
β§ π = (Baseβπ)) β (β₯rβπ) β V) |
20 | | eqidd 2734 |
. . . . . . . . 9
β’ (((π = π
β§ π = (Baseβπ)) β§ π = (β₯rβπ)) β π = π) |
21 | | simpr 486 |
. . . . . . . . . . 11
β’ (((π = π
β§ π = (Baseβπ)) β§ π = (β₯rβπ)) β π = (β₯rβπ)) |
22 | | fveq2 6846 |
. . . . . . . . . . . 12
β’ (π = π
β (β₯rβπ) =
(β₯rβπ
)) |
23 | 22 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π = π
β§ π = (Baseβπ)) β§ π = (β₯rβπ)) β
(β₯rβπ) = (β₯rβπ
)) |
24 | 21, 23 | eqtrd 2773 |
. . . . . . . . . 10
β’ (((π = π
β§ π = (Baseβπ)) β§ π = (β₯rβπ)) β π = (β₯rβπ
)) |
25 | | rprmval.d |
. . . . . . . . . 10
β’ β₯ =
(β₯rβπ
) |
26 | 24, 25 | eqtr4di 2791 |
. . . . . . . . 9
β’ (((π = π
β§ π = (Baseβπ)) β§ π = (β₯rβπ)) β π = β₯ ) |
27 | | fveq2 6846 |
. . . . . . . . . . . 12
β’ (π = π
β (.rβπ) = (.rβπ
)) |
28 | | rprmval.m |
. . . . . . . . . . . 12
β’ Β· =
(.rβπ
) |
29 | 27, 28 | eqtr4di 2791 |
. . . . . . . . . . 11
β’ (π = π
β (.rβπ) = Β· ) |
30 | 29 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π = π
β§ π = (Baseβπ)) β§ π = (β₯rβπ)) β
(.rβπ) =
Β·
) |
31 | 30 | oveqd 7378 |
. . . . . . . . 9
β’ (((π = π
β§ π = (Baseβπ)) β§ π = (β₯rβπ)) β (π₯(.rβπ)π¦) = (π₯ Β· π¦)) |
32 | 20, 26, 31 | breq123d 5123 |
. . . . . . . 8
β’ (((π = π
β§ π = (Baseβπ)) β§ π = (β₯rβπ)) β (ππ(π₯(.rβπ)π¦) β π β₯ (π₯ Β· π¦))) |
33 | 26 | breqd 5120 |
. . . . . . . . 9
β’ (((π = π
β§ π = (Baseβπ)) β§ π = (β₯rβπ)) β (πππ₯ β π β₯ π₯)) |
34 | 26 | breqd 5120 |
. . . . . . . . 9
β’ (((π = π
β§ π = (Baseβπ)) β§ π = (β₯rβπ)) β (πππ¦ β π β₯ π¦)) |
35 | 33, 34 | orbi12d 918 |
. . . . . . . 8
β’ (((π = π
β§ π = (Baseβπ)) β§ π = (β₯rβπ)) β ((πππ₯ β¨ πππ¦) β (π β₯ π₯ β¨ π β₯ π¦))) |
36 | 32, 35 | imbi12d 345 |
. . . . . . 7
β’ (((π = π
β§ π = (Baseβπ)) β§ π = (β₯rβπ)) β ((ππ(π₯(.rβπ)π¦) β (πππ₯ β¨ πππ¦)) β (π β₯ (π₯ Β· π¦) β (π β₯ π₯ β¨ π β₯ π¦)))) |
37 | 19, 36 | sbcied 3788 |
. . . . . 6
β’ ((π = π
β§ π = (Baseβπ)) β
([(β₯rβπ) / π](ππ(π₯(.rβπ)π¦) β (πππ₯ β¨ πππ¦)) β (π β₯ (π₯ Β· π¦) β (π β₯ π₯ β¨ π β₯ π¦)))) |
38 | 8, 37 | raleqbidv 3318 |
. . . . 5
β’ ((π = π
β§ π = (Baseβπ)) β (βπ¦ β π [(β₯rβπ) / π](ππ(π₯(.rβπ)π¦) β (πππ₯ β¨ πππ¦)) β βπ¦ β π΅ (π β₯ (π₯ Β· π¦) β (π β₯ π₯ β¨ π β₯ π¦)))) |
39 | 8, 38 | raleqbidv 3318 |
. . . 4
β’ ((π = π
β§ π = (Baseβπ)) β (βπ₯ β π βπ¦ β π [(β₯rβπ) / π](ππ(π₯(.rβπ)π¦) β (πππ₯ β¨ πππ¦)) β βπ₯ β π΅ βπ¦ β π΅ (π β₯ (π₯ Β· π¦) β (π β₯ π₯ β¨ π β₯ π¦)))) |
40 | 18, 39 | rabeqbidv 3423 |
. . 3
β’ ((π = π
β§ π = (Baseβπ)) β {π β (π β ((Unitβπ) βͺ {(0gβπ)})) β£ βπ₯ β π βπ¦ β π [(β₯rβπ) / π](ππ(π₯(.rβπ)π¦) β (πππ₯ β¨ πππ¦))} = {π β (π΅ β (π βͺ { 0 })) β£ βπ₯ β π΅ βπ¦ β π΅ (π β₯ (π₯ Β· π¦) β (π β₯ π₯ β¨ π β₯ π¦))}) |
41 | 2, 40 | csbied 3897 |
. 2
β’ (π = π
β β¦(Baseβπ) / πβ¦{π β (π β ((Unitβπ) βͺ {(0gβπ)})) β£ βπ₯ β π βπ¦ β π [(β₯rβπ) / π](ππ(π₯(.rβπ)π¦) β (πππ₯ β¨ πππ¦))} = {π β (π΅ β (π βͺ { 0 })) β£ βπ₯ β π΅ βπ¦ β π΅ (π β₯ (π₯ Β· π¦) β (π β₯ π₯ β¨ π β₯ π¦))}) |
42 | | elex 3465 |
. 2
β’ (π
β π β π
β V) |
43 | 7 | fvexi 6860 |
. . . . 5
β’ π΅ β V |
44 | 43 | difexi 5289 |
. . . 4
β’ (π΅ β (π βͺ { 0 })) β
V |
45 | 44 | rabex 5293 |
. . 3
β’ {π β (π΅ β (π βͺ { 0 })) β£ βπ₯ β π΅ βπ¦ β π΅ (π β₯ (π₯ Β· π¦) β (π β₯ π₯ β¨ π β₯ π¦))} β V |
46 | 45 | a1i 11 |
. 2
β’ (π
β π β {π β (π΅ β (π βͺ { 0 })) β£ βπ₯ β π΅ βπ¦ β π΅ (π β₯ (π₯ Β· π¦) β (π β₯ π₯ β¨ π β₯ π¦))} β V) |
47 | 1, 41, 42, 46 | fvmptd3 6975 |
1
β’ (π
β π β (RPrimeβπ
) = {π β (π΅ β (π βͺ { 0 })) β£ βπ₯ β π΅ βπ¦ β π΅ (π β₯ (π₯ Β· π¦) β (π β₯ π₯ β¨ π β₯ π¦))}) |