# Metamath Proof Explorer

## Theorem abvneg

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 ) )`

### Proof

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 )`
` |-  ( ( 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 ) ) )`
` |-  ( ( 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 syl6eqr
` |-  ( ( 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 )`
` |-  ( ( ( 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 )`
` |-  ( ( 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 ) ) )`
` |-  ( ( ( 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 mulid2d
` |-  ( ( F e. A /\ X e. B ) -> ( 1 x. ( F ` X ) ) = ( F ` X ) )`
` |-  ( ( ( F e. A /\ X e. B ) /\ ( 1r ` R ) =/= ( 0g ` R ) ) -> ( 1 x. ( F ` X ) ) = ( F ` X ) )`
` |-  ( ( ( F e. A /\ X e. B ) /\ ( 1r ` R ) =/= ( 0g ` R ) ) -> ( F ` ( N ` X ) ) = ( F ` X ) )`
` |-  ( ( F e. A /\ X e. B ) -> ( F ` ( N ` X ) ) = ( F ` X ) )`