Description: The regular absolute value function on the rationals is in fact an absolute value under our definition. (Contributed by Mario Carneiro, 9-Sep-2014)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | qrng.q | |- Q = ( CCfld |`s QQ ) |
|
| qabsabv.a | |- A = ( AbsVal ` Q ) |
||
| Assertion | qabsabv | |- ( abs |` QQ ) e. A |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | qrng.q | |- Q = ( CCfld |`s QQ ) |
|
| 2 | qabsabv.a | |- A = ( AbsVal ` Q ) |
|
| 3 | absabv | |- abs e. ( AbsVal ` CCfld ) |
|
| 4 | qsubdrg | |- ( QQ e. ( SubRing ` CCfld ) /\ ( CCfld |`s QQ ) e. DivRing ) |
|
| 5 | 4 | simpli | |- QQ e. ( SubRing ` CCfld ) |
| 6 | eqid | |- ( AbsVal ` CCfld ) = ( AbsVal ` CCfld ) |
|
| 7 | 6 1 2 | abvres | |- ( ( abs e. ( AbsVal ` CCfld ) /\ QQ e. ( SubRing ` CCfld ) ) -> ( abs |` QQ ) e. A ) |
| 8 | 3 5 7 | mp2an | |- ( abs |` QQ ) e. A |