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