Step | Hyp | Ref
| Expression |
1 | | abvf.a |
. . . . . 6
β’ π΄ = (AbsValβπ
) |
2 | 1 | abvrcl 20323 |
. . . . 5
β’ (πΉ β π΄ β π
β Ring) |
3 | | abvf.b |
. . . . . 6
β’ π΅ = (Baseβπ
) |
4 | | eqid 2733 |
. . . . . 6
β’
(+gβπ
) = (+gβπ
) |
5 | | eqid 2733 |
. . . . . 6
β’
(.rβπ
) = (.rβπ
) |
6 | | abveq0.z |
. . . . . 6
β’ 0 =
(0gβπ
) |
7 | 1, 3, 4, 5, 6 | isabv 20321 |
. . . . 5
β’ (π
β Ring β (πΉ β π΄ β (πΉ:π΅βΆ(0[,)+β) β§ βπ₯ β π΅ (((πΉβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π΅ ((πΉβ(π₯(.rβπ
)π¦)) = ((πΉβπ₯) Β· (πΉβπ¦)) β§ (πΉβ(π₯(+gβπ
)π¦)) β€ ((πΉβπ₯) + (πΉβπ¦))))))) |
8 | 2, 7 | syl 17 |
. . . 4
β’ (πΉ β π΄ β (πΉ β π΄ β (πΉ:π΅βΆ(0[,)+β) β§ βπ₯ β π΅ (((πΉβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π΅ ((πΉβ(π₯(.rβπ
)π¦)) = ((πΉβπ₯) Β· (πΉβπ¦)) β§ (πΉβ(π₯(+gβπ
)π¦)) β€ ((πΉβπ₯) + (πΉβπ¦))))))) |
9 | 8 | ibi 267 |
. . 3
β’ (πΉ β π΄ β (πΉ:π΅βΆ(0[,)+β) β§ βπ₯ β π΅ (((πΉβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π΅ ((πΉβ(π₯(.rβπ
)π¦)) = ((πΉβπ₯) Β· (πΉβπ¦)) β§ (πΉβ(π₯(+gβπ
)π¦)) β€ ((πΉβπ₯) + (πΉβπ¦)))))) |
10 | | simpl 484 |
. . . 4
β’ ((((πΉβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π΅ ((πΉβ(π₯(.rβπ
)π¦)) = ((πΉβπ₯) Β· (πΉβπ¦)) β§ (πΉβ(π₯(+gβπ
)π¦)) β€ ((πΉβπ₯) + (πΉβπ¦)))) β ((πΉβπ₯) = 0 β π₯ = 0 )) |
11 | 10 | ralimi 3083 |
. . 3
β’
(βπ₯ β
π΅ (((πΉβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π΅ ((πΉβ(π₯(.rβπ
)π¦)) = ((πΉβπ₯) Β· (πΉβπ¦)) β§ (πΉβ(π₯(+gβπ
)π¦)) β€ ((πΉβπ₯) + (πΉβπ¦)))) β βπ₯ β π΅ ((πΉβπ₯) = 0 β π₯ = 0 )) |
12 | 9, 11 | simpl2im 505 |
. 2
β’ (πΉ β π΄ β βπ₯ β π΅ ((πΉβπ₯) = 0 β π₯ = 0 )) |
13 | | fveqeq2 6855 |
. . . 4
β’ (π₯ = π β ((πΉβπ₯) = 0 β (πΉβπ) = 0)) |
14 | | eqeq1 2737 |
. . . 4
β’ (π₯ = π β (π₯ = 0 β π = 0 )) |
15 | 13, 14 | bibi12d 346 |
. . 3
β’ (π₯ = π β (((πΉβπ₯) = 0 β π₯ = 0 ) β ((πΉβπ) = 0 β π = 0 ))) |
16 | 15 | rspccva 3582 |
. 2
β’
((βπ₯ β
π΅ ((πΉβπ₯) = 0 β π₯ = 0 ) β§ π β π΅) β ((πΉβπ) = 0 β π = 0 )) |
17 | 12, 16 | sylan 581 |
1
β’ ((πΉ β π΄ β§ π β π΅) β ((πΉβπ) = 0 β π = 0 )) |