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}=\mathrm{AbsVal}\left({R}\right)$
abvneg.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
abvneg.p ${⊢}{N}={inv}_{g}\left({R}\right)$
Assertion abvneg ${⊢}\left({F}\in {A}\wedge {X}\in {B}\right)\to {F}\left({N}\left({X}\right)\right)={F}\left({X}\right)$

Proof

Step Hyp Ref Expression
1 abv0.a ${⊢}{A}=\mathrm{AbsVal}\left({R}\right)$
2 abvneg.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
3 abvneg.p ${⊢}{N}={inv}_{g}\left({R}\right)$
4 1 abvrcl ${⊢}{F}\in {A}\to {R}\in \mathrm{Ring}$
5 4 adantr ${⊢}\left({F}\in {A}\wedge {X}\in {B}\right)\to {R}\in \mathrm{Ring}$
6 ringgrp ${⊢}{R}\in \mathrm{Ring}\to {R}\in \mathrm{Grp}$
7 4 6 syl ${⊢}{F}\in {A}\to {R}\in \mathrm{Grp}$
8 2 3 grpinvcl ${⊢}\left({R}\in \mathrm{Grp}\wedge {X}\in {B}\right)\to {N}\left({X}\right)\in {B}$
9 7 8 sylan ${⊢}\left({F}\in {A}\wedge {X}\in {B}\right)\to {N}\left({X}\right)\in {B}$
10 simpr ${⊢}\left({F}\in {A}\wedge {X}\in {B}\right)\to {X}\in {B}$
11 eqid ${⊢}{1}_{{R}}={1}_{{R}}$
12 eqid ${⊢}{0}_{{R}}={0}_{{R}}$
13 2 11 12 ring1eq0 ${⊢}\left({R}\in \mathrm{Ring}\wedge {N}\left({X}\right)\in {B}\wedge {X}\in {B}\right)\to \left({1}_{{R}}={0}_{{R}}\to {N}\left({X}\right)={X}\right)$
14 5 9 10 13 syl3anc ${⊢}\left({F}\in {A}\wedge {X}\in {B}\right)\to \left({1}_{{R}}={0}_{{R}}\to {N}\left({X}\right)={X}\right)$
15 14 imp ${⊢}\left(\left({F}\in {A}\wedge {X}\in {B}\right)\wedge {1}_{{R}}={0}_{{R}}\right)\to {N}\left({X}\right)={X}$
16 15 fveq2d ${⊢}\left(\left({F}\in {A}\wedge {X}\in {B}\right)\wedge {1}_{{R}}={0}_{{R}}\right)\to {F}\left({N}\left({X}\right)\right)={F}\left({X}\right)$
17 2 11 ringidcl ${⊢}{R}\in \mathrm{Ring}\to {1}_{{R}}\in {B}$
18 4 17 syl ${⊢}{F}\in {A}\to {1}_{{R}}\in {B}$
19 2 3 grpinvcl ${⊢}\left({R}\in \mathrm{Grp}\wedge {1}_{{R}}\in {B}\right)\to {N}\left({1}_{{R}}\right)\in {B}$
20 7 18 19 syl2anc ${⊢}{F}\in {A}\to {N}\left({1}_{{R}}\right)\in {B}$
21 1 2 abvcl ${⊢}\left({F}\in {A}\wedge {N}\left({1}_{{R}}\right)\in {B}\right)\to {F}\left({N}\left({1}_{{R}}\right)\right)\in ℝ$
22 20 21 mpdan ${⊢}{F}\in {A}\to {F}\left({N}\left({1}_{{R}}\right)\right)\in ℝ$
23 22 recnd ${⊢}{F}\in {A}\to {F}\left({N}\left({1}_{{R}}\right)\right)\in ℂ$
24 23 sqvald ${⊢}{F}\in {A}\to {{F}\left({N}\left({1}_{{R}}\right)\right)}^{2}={F}\left({N}\left({1}_{{R}}\right)\right){F}\left({N}\left({1}_{{R}}\right)\right)$
25 eqid ${⊢}{\cdot }_{{R}}={\cdot }_{{R}}$
26 1 2 25 abvmul ${⊢}\left({F}\in {A}\wedge {N}\left({1}_{{R}}\right)\in {B}\wedge {N}\left({1}_{{R}}\right)\in {B}\right)\to {F}\left({N}\left({1}_{{R}}\right){\cdot }_{{R}}{N}\left({1}_{{R}}\right)\right)={F}\left({N}\left({1}_{{R}}\right)\right){F}\left({N}\left({1}_{{R}}\right)\right)$
27 20 20 26 mpd3an23 ${⊢}{F}\in {A}\to {F}\left({N}\left({1}_{{R}}\right){\cdot }_{{R}}{N}\left({1}_{{R}}\right)\right)={F}\left({N}\left({1}_{{R}}\right)\right){F}\left({N}\left({1}_{{R}}\right)\right)$
28 2 25 3 4 20 18 ringmneg2 ${⊢}{F}\in {A}\to {N}\left({1}_{{R}}\right){\cdot }_{{R}}{N}\left({1}_{{R}}\right)={N}\left({N}\left({1}_{{R}}\right){\cdot }_{{R}}{1}_{{R}}\right)$
29 2 25 11 3 4 18 ringnegl ${⊢}{F}\in {A}\to {N}\left({1}_{{R}}\right){\cdot }_{{R}}{1}_{{R}}={N}\left({1}_{{R}}\right)$
30 29 fveq2d ${⊢}{F}\in {A}\to {N}\left({N}\left({1}_{{R}}\right){\cdot }_{{R}}{1}_{{R}}\right)={N}\left({N}\left({1}_{{R}}\right)\right)$
31 2 3 grpinvinv ${⊢}\left({R}\in \mathrm{Grp}\wedge {1}_{{R}}\in {B}\right)\to {N}\left({N}\left({1}_{{R}}\right)\right)={1}_{{R}}$
32 7 18 31 syl2anc ${⊢}{F}\in {A}\to {N}\left({N}\left({1}_{{R}}\right)\right)={1}_{{R}}$
33 28 30 32 3eqtrd ${⊢}{F}\in {A}\to {N}\left({1}_{{R}}\right){\cdot }_{{R}}{N}\left({1}_{{R}}\right)={1}_{{R}}$
34 33 fveq2d ${⊢}{F}\in {A}\to {F}\left({N}\left({1}_{{R}}\right){\cdot }_{{R}}{N}\left({1}_{{R}}\right)\right)={F}\left({1}_{{R}}\right)$
35 24 27 34 3eqtr2d ${⊢}{F}\in {A}\to {{F}\left({N}\left({1}_{{R}}\right)\right)}^{2}={F}\left({1}_{{R}}\right)$
36 35 adantr ${⊢}\left({F}\in {A}\wedge {1}_{{R}}\ne {0}_{{R}}\right)\to {{F}\left({N}\left({1}_{{R}}\right)\right)}^{2}={F}\left({1}_{{R}}\right)$
37 1 11 12 abv1z ${⊢}\left({F}\in {A}\wedge {1}_{{R}}\ne {0}_{{R}}\right)\to {F}\left({1}_{{R}}\right)=1$
38 36 37 eqtrd ${⊢}\left({F}\in {A}\wedge {1}_{{R}}\ne {0}_{{R}}\right)\to {{F}\left({N}\left({1}_{{R}}\right)\right)}^{2}=1$
39 sq1 ${⊢}{1}^{2}=1$
40 38 39 syl6eqr ${⊢}\left({F}\in {A}\wedge {1}_{{R}}\ne {0}_{{R}}\right)\to {{F}\left({N}\left({1}_{{R}}\right)\right)}^{2}={1}^{2}$
41 1 2 abvge0 ${⊢}\left({F}\in {A}\wedge {N}\left({1}_{{R}}\right)\in {B}\right)\to 0\le {F}\left({N}\left({1}_{{R}}\right)\right)$
42 20 41 mpdan ${⊢}{F}\in {A}\to 0\le {F}\left({N}\left({1}_{{R}}\right)\right)$
43 1re ${⊢}1\in ℝ$
44 0le1 ${⊢}0\le 1$
45 sq11 ${⊢}\left(\left({F}\left({N}\left({1}_{{R}}\right)\right)\in ℝ\wedge 0\le {F}\left({N}\left({1}_{{R}}\right)\right)\right)\wedge \left(1\in ℝ\wedge 0\le 1\right)\right)\to \left({{F}\left({N}\left({1}_{{R}}\right)\right)}^{2}={1}^{2}↔{F}\left({N}\left({1}_{{R}}\right)\right)=1\right)$
46 43 44 45 mpanr12 ${⊢}\left({F}\left({N}\left({1}_{{R}}\right)\right)\in ℝ\wedge 0\le {F}\left({N}\left({1}_{{R}}\right)\right)\right)\to \left({{F}\left({N}\left({1}_{{R}}\right)\right)}^{2}={1}^{2}↔{F}\left({N}\left({1}_{{R}}\right)\right)=1\right)$
47 22 42 46 syl2anc ${⊢}{F}\in {A}\to \left({{F}\left({N}\left({1}_{{R}}\right)\right)}^{2}={1}^{2}↔{F}\left({N}\left({1}_{{R}}\right)\right)=1\right)$
48 47 biimpa ${⊢}\left({F}\in {A}\wedge {{F}\left({N}\left({1}_{{R}}\right)\right)}^{2}={1}^{2}\right)\to {F}\left({N}\left({1}_{{R}}\right)\right)=1$
49 40 48 syldan ${⊢}\left({F}\in {A}\wedge {1}_{{R}}\ne {0}_{{R}}\right)\to {F}\left({N}\left({1}_{{R}}\right)\right)=1$
50 49 adantlr ${⊢}\left(\left({F}\in {A}\wedge {X}\in {B}\right)\wedge {1}_{{R}}\ne {0}_{{R}}\right)\to {F}\left({N}\left({1}_{{R}}\right)\right)=1$
51 50 oveq1d ${⊢}\left(\left({F}\in {A}\wedge {X}\in {B}\right)\wedge {1}_{{R}}\ne {0}_{{R}}\right)\to {F}\left({N}\left({1}_{{R}}\right)\right){F}\left({X}\right)=1{F}\left({X}\right)$
52 simpl ${⊢}\left({F}\in {A}\wedge {X}\in {B}\right)\to {F}\in {A}$
53 20 adantr ${⊢}\left({F}\in {A}\wedge {X}\in {B}\right)\to {N}\left({1}_{{R}}\right)\in {B}$
54 1 2 25 abvmul ${⊢}\left({F}\in {A}\wedge {N}\left({1}_{{R}}\right)\in {B}\wedge {X}\in {B}\right)\to {F}\left({N}\left({1}_{{R}}\right){\cdot }_{{R}}{X}\right)={F}\left({N}\left({1}_{{R}}\right)\right){F}\left({X}\right)$
55 52 53 10 54 syl3anc ${⊢}\left({F}\in {A}\wedge {X}\in {B}\right)\to {F}\left({N}\left({1}_{{R}}\right){\cdot }_{{R}}{X}\right)={F}\left({N}\left({1}_{{R}}\right)\right){F}\left({X}\right)$
56 2 25 11 3 5 10 ringnegl ${⊢}\left({F}\in {A}\wedge {X}\in {B}\right)\to {N}\left({1}_{{R}}\right){\cdot }_{{R}}{X}={N}\left({X}\right)$
57 56 fveq2d ${⊢}\left({F}\in {A}\wedge {X}\in {B}\right)\to {F}\left({N}\left({1}_{{R}}\right){\cdot }_{{R}}{X}\right)={F}\left({N}\left({X}\right)\right)$
58 55 57 eqtr3d ${⊢}\left({F}\in {A}\wedge {X}\in {B}\right)\to {F}\left({N}\left({1}_{{R}}\right)\right){F}\left({X}\right)={F}\left({N}\left({X}\right)\right)$
59 58 adantr ${⊢}\left(\left({F}\in {A}\wedge {X}\in {B}\right)\wedge {1}_{{R}}\ne {0}_{{R}}\right)\to {F}\left({N}\left({1}_{{R}}\right)\right){F}\left({X}\right)={F}\left({N}\left({X}\right)\right)$
60 51 59 eqtr3d ${⊢}\left(\left({F}\in {A}\wedge {X}\in {B}\right)\wedge {1}_{{R}}\ne {0}_{{R}}\right)\to 1{F}\left({X}\right)={F}\left({N}\left({X}\right)\right)$
61 1 2 abvcl ${⊢}\left({F}\in {A}\wedge {X}\in {B}\right)\to {F}\left({X}\right)\in ℝ$
62 61 recnd ${⊢}\left({F}\in {A}\wedge {X}\in {B}\right)\to {F}\left({X}\right)\in ℂ$
63 62 mulid2d ${⊢}\left({F}\in {A}\wedge {X}\in {B}\right)\to 1{F}\left({X}\right)={F}\left({X}\right)$
64 63 adantr ${⊢}\left(\left({F}\in {A}\wedge {X}\in {B}\right)\wedge {1}_{{R}}\ne {0}_{{R}}\right)\to 1{F}\left({X}\right)={F}\left({X}\right)$
65 60 64 eqtr3d ${⊢}\left(\left({F}\in {A}\wedge {X}\in {B}\right)\wedge {1}_{{R}}\ne {0}_{{R}}\right)\to {F}\left({N}\left({X}\right)\right)={F}\left({X}\right)$
66 16 65 pm2.61dane ${⊢}\left({F}\in {A}\wedge {X}\in {B}\right)\to {F}\left({N}\left({X}\right)\right)={F}\left({X}\right)$