Step | Hyp | Ref
| Expression |
1 | | abvfval.a |
. 2
β’ π΄ = (AbsValβπ
) |
2 | | fveq2 6892 |
. . . . . 6
β’ (π = π
β (Baseβπ) = (Baseβπ
)) |
3 | | abvfval.b |
. . . . . 6
β’ π΅ = (Baseβπ
) |
4 | 2, 3 | eqtr4di 2791 |
. . . . 5
β’ (π = π
β (Baseβπ) = π΅) |
5 | 4 | oveq2d 7425 |
. . . 4
β’ (π = π
β ((0[,)+β) βm
(Baseβπ)) =
((0[,)+β) βm π΅)) |
6 | | fveq2 6892 |
. . . . . . . . 9
β’ (π = π
β (0gβπ) = (0gβπ
)) |
7 | | abvfval.z |
. . . . . . . . 9
β’ 0 =
(0gβπ
) |
8 | 6, 7 | eqtr4di 2791 |
. . . . . . . 8
β’ (π = π
β (0gβπ) = 0 ) |
9 | 8 | eqeq2d 2744 |
. . . . . . 7
β’ (π = π
β (π₯ = (0gβπ) β π₯ = 0 )) |
10 | 9 | bibi2d 343 |
. . . . . 6
β’ (π = π
β (((πβπ₯) = 0 β π₯ = (0gβπ)) β ((πβπ₯) = 0 β π₯ = 0 ))) |
11 | | fveq2 6892 |
. . . . . . . . . . 11
β’ (π = π
β (.rβπ) = (.rβπ
)) |
12 | | abvfval.t |
. . . . . . . . . . 11
β’ Β· =
(.rβπ
) |
13 | 11, 12 | eqtr4di 2791 |
. . . . . . . . . 10
β’ (π = π
β (.rβπ) = Β· ) |
14 | 13 | oveqd 7426 |
. . . . . . . . 9
β’ (π = π
β (π₯(.rβπ)π¦) = (π₯ Β· π¦)) |
15 | 14 | fveqeq2d 6900 |
. . . . . . . 8
β’ (π = π
β ((πβ(π₯(.rβπ)π¦)) = ((πβπ₯) Β· (πβπ¦)) β (πβ(π₯ Β· π¦)) = ((πβπ₯) Β· (πβπ¦)))) |
16 | | fveq2 6892 |
. . . . . . . . . . . 12
β’ (π = π
β (+gβπ) = (+gβπ
)) |
17 | | abvfval.p |
. . . . . . . . . . . 12
β’ + =
(+gβπ
) |
18 | 16, 17 | eqtr4di 2791 |
. . . . . . . . . . 11
β’ (π = π
β (+gβπ) = + ) |
19 | 18 | oveqd 7426 |
. . . . . . . . . 10
β’ (π = π
β (π₯(+gβπ)π¦) = (π₯ + π¦)) |
20 | 19 | fveq2d 6896 |
. . . . . . . . 9
β’ (π = π
β (πβ(π₯(+gβπ)π¦)) = (πβ(π₯ + π¦))) |
21 | 20 | breq1d 5159 |
. . . . . . . 8
β’ (π = π
β ((πβ(π₯(+gβπ)π¦)) β€ ((πβπ₯) + (πβπ¦)) β (πβ(π₯ + π¦)) β€ ((πβπ₯) + (πβπ¦)))) |
22 | 15, 21 | anbi12d 632 |
. . . . . . 7
β’ (π = π
β (((πβ(π₯(.rβπ)π¦)) = ((πβπ₯) Β· (πβπ¦)) β§ (πβ(π₯(+gβπ)π¦)) β€ ((πβπ₯) + (πβπ¦))) β ((πβ(π₯ Β· π¦)) = ((πβπ₯) Β· (πβπ¦)) β§ (πβ(π₯ + π¦)) β€ ((πβπ₯) + (πβπ¦))))) |
23 | 4, 22 | raleqbidv 3343 |
. . . . . 6
β’ (π = π
β (βπ¦ β (Baseβπ)((πβ(π₯(.rβπ)π¦)) = ((πβπ₯) Β· (πβπ¦)) β§ (πβ(π₯(+gβπ)π¦)) β€ ((πβπ₯) + (πβπ¦))) β βπ¦ β π΅ ((πβ(π₯ Β· π¦)) = ((πβπ₯) Β· (πβπ¦)) β§ (πβ(π₯ + π¦)) β€ ((πβπ₯) + (πβπ¦))))) |
24 | 10, 23 | anbi12d 632 |
. . . . 5
β’ (π = π
β ((((πβπ₯) = 0 β π₯ = (0gβπ)) β§ βπ¦ β (Baseβπ)((πβ(π₯(.rβπ)π¦)) = ((πβπ₯) Β· (πβπ¦)) β§ (πβ(π₯(+gβπ)π¦)) β€ ((πβπ₯) + (πβπ¦)))) β (((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π΅ ((πβ(π₯ Β· π¦)) = ((πβπ₯) Β· (πβπ¦)) β§ (πβ(π₯ + π¦)) β€ ((πβπ₯) + (πβπ¦)))))) |
25 | 4, 24 | raleqbidv 3343 |
. . . 4
β’ (π = π
β (βπ₯ β (Baseβπ)(((πβπ₯) = 0 β π₯ = (0gβπ)) β§ βπ¦ β (Baseβπ)((πβ(π₯(.rβπ)π¦)) = ((πβπ₯) Β· (πβπ¦)) β§ (πβ(π₯(+gβπ)π¦)) β€ ((πβπ₯) + (πβπ¦)))) β βπ₯ β π΅ (((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π΅ ((πβ(π₯ Β· π¦)) = ((πβπ₯) Β· (πβπ¦)) β§ (πβ(π₯ + π¦)) β€ ((πβπ₯) + (πβπ¦)))))) |
26 | 5, 25 | rabeqbidv 3450 |
. . 3
β’ (π = π
β {π β ((0[,)+β) βm
(Baseβπ)) β£
βπ₯ β
(Baseβπ)(((πβπ₯) = 0 β π₯ = (0gβπ)) β§ βπ¦ β (Baseβπ)((πβ(π₯(.rβπ)π¦)) = ((πβπ₯) Β· (πβπ¦)) β§ (πβ(π₯(+gβπ)π¦)) β€ ((πβπ₯) + (πβπ¦))))} = {π β ((0[,)+β) βm
π΅) β£ βπ₯ β π΅ (((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π΅ ((πβ(π₯ Β· π¦)) = ((πβπ₯) Β· (πβπ¦)) β§ (πβ(π₯ + π¦)) β€ ((πβπ₯) + (πβπ¦))))}) |
27 | | df-abv 20425 |
. . 3
β’ AbsVal =
(π β Ring β¦
{π β ((0[,)+β)
βm (Baseβπ)) β£ βπ₯ β (Baseβπ)(((πβπ₯) = 0 β π₯ = (0gβπ)) β§ βπ¦ β (Baseβπ)((πβ(π₯(.rβπ)π¦)) = ((πβπ₯) Β· (πβπ¦)) β§ (πβ(π₯(+gβπ)π¦)) β€ ((πβπ₯) + (πβπ¦))))}) |
28 | | ovex 7442 |
. . . 4
β’
((0[,)+β) βm π΅) β V |
29 | 28 | rabex 5333 |
. . 3
β’ {π β ((0[,)+β)
βm π΅)
β£ βπ₯ β
π΅ (((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π΅ ((πβ(π₯ Β· π¦)) = ((πβπ₯) Β· (πβπ¦)) β§ (πβ(π₯ + π¦)) β€ ((πβπ₯) + (πβπ¦))))} β V |
30 | 26, 27, 29 | fvmpt 6999 |
. 2
β’ (π
β Ring β
(AbsValβπ
) = {π β ((0[,)+β)
βm π΅)
β£ βπ₯ β
π΅ (((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π΅ ((πβ(π₯ Β· π¦)) = ((πβπ₯) Β· (πβπ¦)) β§ (πβ(π₯ + π¦)) β€ ((πβπ₯) + (πβπ¦))))}) |
31 | 1, 30 | eqtrid 2785 |
1
β’ (π
β Ring β π΄ = {π β ((0[,)+β) βm
π΅) β£ βπ₯ β π΅ (((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π΅ ((πβ(π₯ Β· π¦)) = ((πβπ₯) Β· (πβπ¦)) β§ (πβ(π₯ + π¦)) β€ ((πβπ₯) + (πβπ¦))))}) |