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 )
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 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 )
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 mulid2d
 |-  ( ( 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 ) )