Step | Hyp | Ref
| Expression |
1 | | fveq2 6846 |
. . . . 5
β’ (π = π
β (AbsValβπ) = (AbsValβπ
)) |
2 | | isufd.a |
. . . . 5
β’ π΄ = (AbsValβπ
) |
3 | 1, 2 | eqtr4di 2791 |
. . . 4
β’ (π = π
β (AbsValβπ) = π΄) |
4 | 3 | neeq1d 3000 |
. . 3
β’ (π = π
β ((AbsValβπ) β β
β π΄ β β
)) |
5 | | fveq2 6846 |
. . . . 5
β’ (π = π
β (PrmIdealβπ) = (PrmIdealβπ
)) |
6 | | isufd.i |
. . . . 5
β’ πΌ = (PrmIdealβπ
) |
7 | 5, 6 | eqtr4di 2791 |
. . . 4
β’ (π = π
β (PrmIdealβπ) = πΌ) |
8 | | fveq2 6846 |
. . . . . . 7
β’ (π = π
β (RPrimeβπ) = (RPrimeβπ
)) |
9 | | isufd.3 |
. . . . . . 7
β’ π = (RPrimeβπ
) |
10 | 8, 9 | eqtr4di 2791 |
. . . . . 6
β’ (π = π
β (RPrimeβπ) = π) |
11 | 10 | ineq2d 4176 |
. . . . 5
β’ (π = π
β (π β© (RPrimeβπ)) = (π β© π)) |
12 | 11 | neeq1d 3000 |
. . . 4
β’ (π = π
β ((π β© (RPrimeβπ)) β β
β (π β© π) β β
)) |
13 | 7, 12 | raleqbidv 3318 |
. . 3
β’ (π = π
β (βπ β (PrmIdealβπ)(π β© (RPrimeβπ)) β β
β βπ β πΌ (π β© π) β β
)) |
14 | 4, 13 | anbi12d 632 |
. 2
β’ (π = π
β (((AbsValβπ) β β
β§ βπ β (PrmIdealβπ)(π β© (RPrimeβπ)) β β
) β (π΄ β β
β§ βπ β πΌ (π β© π) β β
))) |
15 | | df-ufd 32314 |
. 2
β’ UFD =
{π β CRing β£
((AbsValβπ) β
β
β§ βπ
β (PrmIdealβπ)(π β© (RPrimeβπ)) β β
)} |
16 | 14, 15 | elrab2 3652 |
1
β’ (π
β UFD β (π
β CRing β§ (π΄ β β
β§
βπ β πΌ (π β© π) β β
))) |