Step | Hyp | Ref
| Expression |
1 | | abvfval.a |
. . . 4
β’ π΄ = (AbsValβπ
) |
2 | | abvfval.b |
. . . 4
β’ π΅ = (Baseβπ
) |
3 | | abvfval.p |
. . . 4
β’ + =
(+gβπ
) |
4 | | abvfval.t |
. . . 4
β’ Β· =
(.rβπ
) |
5 | | abvfval.z |
. . . 4
β’ 0 =
(0gβπ
) |
6 | 1, 2, 3, 4, 5 | abvfval 20320 |
. . 3
β’ (π
β Ring β π΄ = {π β ((0[,)+β) βm
π΅) β£ βπ₯ β π΅ (((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π΅ ((πβ(π₯ Β· π¦)) = ((πβπ₯) Β· (πβπ¦)) β§ (πβ(π₯ + π¦)) β€ ((πβπ₯) + (πβπ¦))))}) |
7 | 6 | eleq2d 2820 |
. 2
β’ (π
β Ring β (πΉ β π΄ β πΉ β {π β ((0[,)+β) βm
π΅) β£ βπ₯ β π΅ (((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π΅ ((πβ(π₯ Β· π¦)) = ((πβπ₯) Β· (πβπ¦)) β§ (πβ(π₯ + π¦)) β€ ((πβπ₯) + (πβπ¦))))})) |
8 | | fveq1 6845 |
. . . . . . . 8
β’ (π = πΉ β (πβπ₯) = (πΉβπ₯)) |
9 | 8 | eqeq1d 2735 |
. . . . . . 7
β’ (π = πΉ β ((πβπ₯) = 0 β (πΉβπ₯) = 0)) |
10 | 9 | bibi1d 344 |
. . . . . 6
β’ (π = πΉ β (((πβπ₯) = 0 β π₯ = 0 ) β ((πΉβπ₯) = 0 β π₯ = 0 ))) |
11 | | fveq1 6845 |
. . . . . . . . 9
β’ (π = πΉ β (πβ(π₯ Β· π¦)) = (πΉβ(π₯ Β· π¦))) |
12 | | fveq1 6845 |
. . . . . . . . . 10
β’ (π = πΉ β (πβπ¦) = (πΉβπ¦)) |
13 | 8, 12 | oveq12d 7379 |
. . . . . . . . 9
β’ (π = πΉ β ((πβπ₯) Β· (πβπ¦)) = ((πΉβπ₯) Β· (πΉβπ¦))) |
14 | 11, 13 | eqeq12d 2749 |
. . . . . . . 8
β’ (π = πΉ β ((πβ(π₯ Β· π¦)) = ((πβπ₯) Β· (πβπ¦)) β (πΉβ(π₯ Β· π¦)) = ((πΉβπ₯) Β· (πΉβπ¦)))) |
15 | | fveq1 6845 |
. . . . . . . . 9
β’ (π = πΉ β (πβ(π₯ + π¦)) = (πΉβ(π₯ + π¦))) |
16 | 8, 12 | oveq12d 7379 |
. . . . . . . . 9
β’ (π = πΉ β ((πβπ₯) + (πβπ¦)) = ((πΉβπ₯) + (πΉβπ¦))) |
17 | 15, 16 | breq12d 5122 |
. . . . . . . 8
β’ (π = πΉ β ((πβ(π₯ + π¦)) β€ ((πβπ₯) + (πβπ¦)) β (πΉβ(π₯ + π¦)) β€ ((πΉβπ₯) + (πΉβπ¦)))) |
18 | 14, 17 | anbi12d 632 |
. . . . . . 7
β’ (π = πΉ β (((πβ(π₯ Β· π¦)) = ((πβπ₯) Β· (πβπ¦)) β§ (πβ(π₯ + π¦)) β€ ((πβπ₯) + (πβπ¦))) β ((πΉβ(π₯ Β· π¦)) = ((πΉβπ₯) Β· (πΉβπ¦)) β§ (πΉβ(π₯ + π¦)) β€ ((πΉβπ₯) + (πΉβπ¦))))) |
19 | 18 | ralbidv 3171 |
. . . . . 6
β’ (π = πΉ β (βπ¦ β π΅ ((πβ(π₯ Β· π¦)) = ((πβπ₯) Β· (πβπ¦)) β§ (πβ(π₯ + π¦)) β€ ((πβπ₯) + (πβπ¦))) β βπ¦ β π΅ ((πΉβ(π₯ Β· π¦)) = ((πΉβπ₯) Β· (πΉβπ¦)) β§ (πΉβ(π₯ + π¦)) β€ ((πΉβπ₯) + (πΉβπ¦))))) |
20 | 10, 19 | anbi12d 632 |
. . . . 5
β’ (π = πΉ β ((((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π΅ ((πβ(π₯ Β· π¦)) = ((πβπ₯) Β· (πβπ¦)) β§ (πβ(π₯ + π¦)) β€ ((πβπ₯) + (πβπ¦)))) β (((πΉβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π΅ ((πΉβ(π₯ Β· π¦)) = ((πΉβπ₯) Β· (πΉβπ¦)) β§ (πΉβ(π₯ + π¦)) β€ ((πΉβπ₯) + (πΉβπ¦)))))) |
21 | 20 | ralbidv 3171 |
. . . 4
β’ (π = πΉ β (βπ₯ β π΅ (((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π΅ ((πβ(π₯ Β· π¦)) = ((πβπ₯) Β· (πβπ¦)) β§ (πβ(π₯ + π¦)) β€ ((πβπ₯) + (πβπ¦)))) β βπ₯ β π΅ (((πΉβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π΅ ((πΉβ(π₯ Β· π¦)) = ((πΉβπ₯) Β· (πΉβπ¦)) β§ (πΉβ(π₯ + π¦)) β€ ((πΉβπ₯) + (πΉβπ¦)))))) |
22 | 21 | elrab 3649 |
. . 3
β’ (πΉ β {π β ((0[,)+β) βm
π΅) β£ βπ₯ β π΅ (((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π΅ ((πβ(π₯ Β· π¦)) = ((πβπ₯) Β· (πβπ¦)) β§ (πβ(π₯ + π¦)) β€ ((πβπ₯) + (πβπ¦))))} β (πΉ β ((0[,)+β) βm
π΅) β§ βπ₯ β π΅ (((πΉβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π΅ ((πΉβ(π₯ Β· π¦)) = ((πΉβπ₯) Β· (πΉβπ¦)) β§ (πΉβ(π₯ + π¦)) β€ ((πΉβπ₯) + (πΉβπ¦)))))) |
23 | | ovex 7394 |
. . . . 5
β’
(0[,)+β) β V |
24 | 2 | fvexi 6860 |
. . . . 5
β’ π΅ β V |
25 | 23, 24 | elmap 8815 |
. . . 4
β’ (πΉ β ((0[,)+β)
βm π΅)
β πΉ:π΅βΆ(0[,)+β)) |
26 | 25 | anbi1i 625 |
. . 3
β’ ((πΉ β ((0[,)+β)
βm π΅) β§
βπ₯ β π΅ (((πΉβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π΅ ((πΉβ(π₯ Β· π¦)) = ((πΉβπ₯) Β· (πΉβπ¦)) β§ (πΉβ(π₯ + π¦)) β€ ((πΉβπ₯) + (πΉβπ¦))))) β (πΉ:π΅βΆ(0[,)+β) β§ βπ₯ β π΅ (((πΉβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π΅ ((πΉβ(π₯ Β· π¦)) = ((πΉβπ₯) Β· (πΉβπ¦)) β§ (πΉβ(π₯ + π¦)) β€ ((πΉβπ₯) + (πΉβπ¦)))))) |
27 | 22, 26 | bitri 275 |
. 2
β’ (πΉ β {π β ((0[,)+β) βm
π΅) β£ βπ₯ β π΅ (((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π΅ ((πβ(π₯ Β· π¦)) = ((πβπ₯) Β· (πβπ¦)) β§ (πβ(π₯ + π¦)) β€ ((πβπ₯) + (πβπ¦))))} β (πΉ:π΅βΆ(0[,)+β) β§ βπ₯ β π΅ (((πΉβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π΅ ((πΉβ(π₯ Β· π¦)) = ((πΉβπ₯) Β· (πΉβπ¦)) β§ (πΉβ(π₯ + π¦)) β€ ((πΉβπ₯) + (πΉβπ¦)))))) |
28 | 7, 27 | bitrdi 287 |
1
β’ (π
β Ring β (πΉ β π΄ β (πΉ:π΅βΆ(0[,)+β) β§ βπ₯ β π΅ (((πΉβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π΅ ((πΉβ(π₯ Β· π¦)) = ((πΉβπ₯) Β· (πΉβπ¦)) β§ (πΉβ(π₯ + π¦)) β€ ((πΉβπ₯) + (πΉβπ¦))))))) |