This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Description: The absolute value of a negative is the same as that of the positive. (Contributed by Mario Carneiro, 8-Sep-2014)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | abv0.a | |- A = ( AbsVal ` R ) |
|
| abvneg.b | |- B = ( Base ` R ) |
||
| abvneg.p | |- N = ( invg ` R ) |
||
| Assertion | abvneg | |- ( ( F e. A /\ X e. B ) -> ( F ` ( N ` X ) ) = ( F ` X ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | abv0.a | |- A = ( AbsVal ` R ) |
|
| 2 | abvneg.b | |- B = ( Base ` R ) |
|
| 3 | abvneg.p | |- N = ( invg ` R ) |
|
| 4 | 1 | abvrcl | |- ( F e. A -> R e. Ring ) |
| 5 | 4 | adantr | |- ( ( F e. A /\ X e. B ) -> R e. Ring ) |
| 6 | ringgrp | |- ( R e. Ring -> R e. Grp ) |
|
| 7 | 4 6 | syl | |- ( F e. A -> R e. Grp ) |
| 8 | 2 3 | grpinvcl | |- ( ( R e. Grp /\ X e. B ) -> ( N ` X ) e. B ) |
| 9 | 7 8 | sylan | |- ( ( F e. A /\ X e. B ) -> ( N ` X ) e. B ) |
| 10 | simpr | |- ( ( F e. A /\ X e. B ) -> X e. B ) |
|
| 11 | eqid | |- ( 1r ` R ) = ( 1r ` R ) |
|
| 12 | eqid | |- ( 0g ` R ) = ( 0g ` R ) |
|
| 13 | 2 11 12 | ring1eq0 | |- ( ( R e. Ring /\ ( N ` X ) e. B /\ X e. B ) -> ( ( 1r ` R ) = ( 0g ` R ) -> ( N ` X ) = X ) ) |
| 14 | 5 9 10 13 | syl3anc | |- ( ( F e. A /\ X e. B ) -> ( ( 1r ` R ) = ( 0g ` R ) -> ( N ` X ) = X ) ) |
| 15 | 14 | imp | |- ( ( ( F e. A /\ X e. B ) /\ ( 1r ` R ) = ( 0g ` R ) ) -> ( N ` X ) = X ) |
| 16 | 15 | fveq2d | |- ( ( ( F e. A /\ X e. B ) /\ ( 1r ` R ) = ( 0g ` R ) ) -> ( F ` ( N ` X ) ) = ( F ` X ) ) |
| 17 | 2 11 | ringidcl | |- ( R e. Ring -> ( 1r ` R ) e. B ) |
| 18 | 4 17 | syl | |- ( F e. A -> ( 1r ` R ) e. B ) |
| 19 | 2 3 | grpinvcl | |- ( ( R e. Grp /\ ( 1r ` R ) e. B ) -> ( N ` ( 1r ` R ) ) e. B ) |
| 20 | 7 18 19 | syl2anc | |- ( F e. A -> ( N ` ( 1r ` R ) ) e. B ) |
| 21 | 1 2 | abvcl | |- ( ( F e. A /\ ( N ` ( 1r ` R ) ) e. B ) -> ( F ` ( N ` ( 1r ` R ) ) ) e. RR ) |
| 22 | 20 21 | mpdan | |- ( F e. A -> ( F ` ( N ` ( 1r ` R ) ) ) e. RR ) |
| 23 | 22 | recnd | |- ( F e. A -> ( F ` ( N ` ( 1r ` R ) ) ) e. CC ) |
| 24 | 23 | sqvald | |- ( F e. A -> ( ( F ` ( N ` ( 1r ` R ) ) ) ^ 2 ) = ( ( F ` ( N ` ( 1r ` R ) ) ) x. ( F ` ( N ` ( 1r ` R ) ) ) ) ) |
| 25 | eqid | |- ( .r ` R ) = ( .r ` R ) |
|
| 26 | 1 2 25 | abvmul | |- ( ( F e. A /\ ( N ` ( 1r ` R ) ) e. B /\ ( N ` ( 1r ` R ) ) e. B ) -> ( F ` ( ( N ` ( 1r ` R ) ) ( .r ` R ) ( N ` ( 1r ` R ) ) ) ) = ( ( F ` ( N ` ( 1r ` R ) ) ) x. ( F ` ( N ` ( 1r ` R ) ) ) ) ) |
| 27 | 20 20 26 | mpd3an23 | |- ( F e. A -> ( F ` ( ( N ` ( 1r ` R ) ) ( .r ` R ) ( N ` ( 1r ` R ) ) ) ) = ( ( F ` ( N ` ( 1r ` R ) ) ) x. ( F ` ( N ` ( 1r ` R ) ) ) ) ) |
| 28 | 2 25 3 4 20 18 | ringmneg2 | |- ( F e. A -> ( ( N ` ( 1r ` R ) ) ( .r ` R ) ( N ` ( 1r ` R ) ) ) = ( N ` ( ( N ` ( 1r ` R ) ) ( .r ` R ) ( 1r ` R ) ) ) ) |
| 29 | 2 25 11 3 4 18 | ringnegl | |- ( F e. A -> ( ( N ` ( 1r ` R ) ) ( .r ` R ) ( 1r ` R ) ) = ( N ` ( 1r ` R ) ) ) |
| 30 | 29 | fveq2d | |- ( F e. A -> ( N ` ( ( N ` ( 1r ` R ) ) ( .r ` R ) ( 1r ` R ) ) ) = ( N ` ( N ` ( 1r ` R ) ) ) ) |
| 31 | 2 3 | grpinvinv | |- ( ( R e. Grp /\ ( 1r ` R ) e. B ) -> ( N ` ( N ` ( 1r ` R ) ) ) = ( 1r ` R ) ) |
| 32 | 7 18 31 | syl2anc | |- ( F e. A -> ( N ` ( N ` ( 1r ` R ) ) ) = ( 1r ` R ) ) |
| 33 | 28 30 32 | 3eqtrd | |- ( F e. A -> ( ( N ` ( 1r ` R ) ) ( .r ` R ) ( N ` ( 1r ` R ) ) ) = ( 1r ` R ) ) |
| 34 | 33 | fveq2d | |- ( F e. A -> ( F ` ( ( N ` ( 1r ` R ) ) ( .r ` R ) ( N ` ( 1r ` R ) ) ) ) = ( F ` ( 1r ` R ) ) ) |
| 35 | 24 27 34 | 3eqtr2d | |- ( F e. A -> ( ( F ` ( N ` ( 1r ` R ) ) ) ^ 2 ) = ( F ` ( 1r ` R ) ) ) |
| 36 | 35 | adantr | |- ( ( F e. A /\ ( 1r ` R ) =/= ( 0g ` R ) ) -> ( ( F ` ( N ` ( 1r ` R ) ) ) ^ 2 ) = ( F ` ( 1r ` R ) ) ) |
| 37 | 1 11 12 | abv1z | |- ( ( F e. A /\ ( 1r ` R ) =/= ( 0g ` R ) ) -> ( F ` ( 1r ` R ) ) = 1 ) |
| 38 | 36 37 | eqtrd | |- ( ( F e. A /\ ( 1r ` R ) =/= ( 0g ` R ) ) -> ( ( F ` ( N ` ( 1r ` R ) ) ) ^ 2 ) = 1 ) |
| 39 | sq1 | |- ( 1 ^ 2 ) = 1 |
|
| 40 | 38 39 | eqtr4di | |- ( ( F e. A /\ ( 1r ` R ) =/= ( 0g ` R ) ) -> ( ( F ` ( N ` ( 1r ` R ) ) ) ^ 2 ) = ( 1 ^ 2 ) ) |
| 41 | 1 2 | abvge0 | |- ( ( F e. A /\ ( N ` ( 1r ` R ) ) e. B ) -> 0 <_ ( F ` ( N ` ( 1r ` R ) ) ) ) |
| 42 | 20 41 | mpdan | |- ( F e. A -> 0 <_ ( F ` ( N ` ( 1r ` R ) ) ) ) |
| 43 | 1re | |- 1 e. RR |
|
| 44 | 0le1 | |- 0 <_ 1 |
|
| 45 | sq11 | |- ( ( ( ( F ` ( N ` ( 1r ` R ) ) ) e. RR /\ 0 <_ ( F ` ( N ` ( 1r ` R ) ) ) ) /\ ( 1 e. RR /\ 0 <_ 1 ) ) -> ( ( ( F ` ( N ` ( 1r ` R ) ) ) ^ 2 ) = ( 1 ^ 2 ) <-> ( F ` ( N ` ( 1r ` R ) ) ) = 1 ) ) |
|
| 46 | 43 44 45 | mpanr12 | |- ( ( ( F ` ( N ` ( 1r ` R ) ) ) e. RR /\ 0 <_ ( F ` ( N ` ( 1r ` R ) ) ) ) -> ( ( ( F ` ( N ` ( 1r ` R ) ) ) ^ 2 ) = ( 1 ^ 2 ) <-> ( F ` ( N ` ( 1r ` R ) ) ) = 1 ) ) |
| 47 | 22 42 46 | syl2anc | |- ( F e. A -> ( ( ( F ` ( N ` ( 1r ` R ) ) ) ^ 2 ) = ( 1 ^ 2 ) <-> ( F ` ( N ` ( 1r ` R ) ) ) = 1 ) ) |
| 48 | 47 | biimpa | |- ( ( F e. A /\ ( ( F ` ( N ` ( 1r ` R ) ) ) ^ 2 ) = ( 1 ^ 2 ) ) -> ( F ` ( N ` ( 1r ` R ) ) ) = 1 ) |
| 49 | 40 48 | syldan | |- ( ( F e. A /\ ( 1r ` R ) =/= ( 0g ` R ) ) -> ( F ` ( N ` ( 1r ` R ) ) ) = 1 ) |
| 50 | 49 | adantlr | |- ( ( ( F e. A /\ X e. B ) /\ ( 1r ` R ) =/= ( 0g ` R ) ) -> ( F ` ( N ` ( 1r ` R ) ) ) = 1 ) |
| 51 | 50 | oveq1d | |- ( ( ( F e. A /\ X e. B ) /\ ( 1r ` R ) =/= ( 0g ` R ) ) -> ( ( F ` ( N ` ( 1r ` R ) ) ) x. ( F ` X ) ) = ( 1 x. ( F ` X ) ) ) |
| 52 | simpl | |- ( ( F e. A /\ X e. B ) -> F e. A ) |
|
| 53 | 20 | adantr | |- ( ( F e. A /\ X e. B ) -> ( N ` ( 1r ` R ) ) e. B ) |
| 54 | 1 2 25 | abvmul | |- ( ( F e. A /\ ( N ` ( 1r ` R ) ) e. B /\ X e. B ) -> ( F ` ( ( N ` ( 1r ` R ) ) ( .r ` R ) X ) ) = ( ( F ` ( N ` ( 1r ` R ) ) ) x. ( F ` X ) ) ) |
| 55 | 52 53 10 54 | syl3anc | |- ( ( F e. A /\ X e. B ) -> ( F ` ( ( N ` ( 1r ` R ) ) ( .r ` R ) X ) ) = ( ( F ` ( N ` ( 1r ` R ) ) ) x. ( F ` X ) ) ) |
| 56 | 2 25 11 3 5 10 | ringnegl | |- ( ( F e. A /\ X e. B ) -> ( ( N ` ( 1r ` R ) ) ( .r ` R ) X ) = ( N ` X ) ) |
| 57 | 56 | fveq2d | |- ( ( F e. A /\ X e. B ) -> ( F ` ( ( N ` ( 1r ` R ) ) ( .r ` R ) X ) ) = ( F ` ( N ` X ) ) ) |
| 58 | 55 57 | eqtr3d | |- ( ( F e. A /\ X e. B ) -> ( ( F ` ( N ` ( 1r ` R ) ) ) x. ( F ` X ) ) = ( F ` ( N ` X ) ) ) |
| 59 | 58 | adantr | |- ( ( ( F e. A /\ X e. B ) /\ ( 1r ` R ) =/= ( 0g ` R ) ) -> ( ( F ` ( N ` ( 1r ` R ) ) ) x. ( F ` X ) ) = ( F ` ( N ` X ) ) ) |
| 60 | 51 59 | eqtr3d | |- ( ( ( F e. A /\ X e. B ) /\ ( 1r ` R ) =/= ( 0g ` R ) ) -> ( 1 x. ( F ` X ) ) = ( F ` ( N ` X ) ) ) |
| 61 | 1 2 | abvcl | |- ( ( F e. A /\ X e. B ) -> ( F ` X ) e. RR ) |
| 62 | 61 | recnd | |- ( ( F e. A /\ X e. B ) -> ( F ` X ) e. CC ) |
| 63 | 62 | mullidd | |- ( ( F e. A /\ X e. B ) -> ( 1 x. ( F ` X ) ) = ( F ` X ) ) |
| 64 | 63 | adantr | |- ( ( ( F e. A /\ X e. B ) /\ ( 1r ` R ) =/= ( 0g ` R ) ) -> ( 1 x. ( F ` X ) ) = ( F ` X ) ) |
| 65 | 60 64 | eqtr3d | |- ( ( ( F e. A /\ X e. B ) /\ ( 1r ` R ) =/= ( 0g ` R ) ) -> ( F ` ( N ` X ) ) = ( F ` X ) ) |
| 66 | 16 65 | pm2.61dane | |- ( ( F e. A /\ X e. B ) -> ( F ` ( N ` X ) ) = ( F ` X ) ) |