This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐴 = ( AbsVal ‘ 𝑅 )
abvneg.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
abvneg.p ⊢ 𝑁 = ( invg ‘ 𝑅 )
Assertion abvneg ( ( 𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑁 ‘ 𝑋 ) ) = ( 𝐹 ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 abv0.a ⊢ 𝐴 = ( AbsVal ‘ 𝑅 )
2 abvneg.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
3 abvneg.p ⊢ 𝑁 = ( invg ‘ 𝑅 )
4 1 abvrcl ⊢ ( 𝐹 ∈ 𝐴 → 𝑅 ∈ Ring )
5 4 adantr ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) → 𝑅 ∈ Ring )
6 ringgrp ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
7 4 6 syl ⊢ ( 𝐹 ∈ 𝐴 → 𝑅 ∈ Grp )
8 2 3 grpinvcl ⊢ ( ( 𝑅 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 ‘ 𝑋 ) ∈ 𝐵 )
9 7 8 sylan ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 ‘ 𝑋 ) ∈ 𝐵 )
10 simpr ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
11 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
12 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
13 2 11 12 ring1eq0 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 ‘ 𝑋 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) → ( 𝑁 ‘ 𝑋 ) = 𝑋 ) )
14 5 9 10 13 syl3anc ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) → ( ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) → ( 𝑁 ‘ 𝑋 ) = 𝑋 ) )
15 14 imp ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) ) → ( 𝑁 ‘ 𝑋 ) = 𝑋 )
16 15 fveq2d ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) ) → ( 𝐹 ‘ ( 𝑁 ‘ 𝑋 ) ) = ( 𝐹 ‘ 𝑋 ) )
17 2 11 ringidcl ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
18 4 17 syl ⊢ ( 𝐹 ∈ 𝐴 → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
19 2 3 grpinvcl ⊢ ( ( 𝑅 ∈ Grp ∧ ( 1r ‘ 𝑅 ) ∈ 𝐵 ) → ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ∈ 𝐵 )
20 7 18 19 syl2anc ⊢ ( 𝐹 ∈ 𝐴 → ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ∈ 𝐵 )
21 1 2 abvcl ⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ) ∈ ℝ )
22 20 21 mpdan ⊢ ( 𝐹 ∈ 𝐴 → ( 𝐹 ‘ ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ) ∈ ℝ )
23 22 recnd ⊢ ( 𝐹 ∈ 𝐴 → ( 𝐹 ‘ ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ) ∈ ℂ )
24 23 sqvald ⊢ ( 𝐹 ∈ 𝐴 → ( ( 𝐹 ‘ ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ) ↑ 2 ) = ( ( 𝐹 ‘ ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ) · ( 𝐹 ‘ ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ) ) )
25 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
26 1 2 25 abvmul ⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ∈ 𝐵 ∧ ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ∈ 𝐵 ) → ( 𝐹 ‘ ( ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑅 ) ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ) ) = ( ( 𝐹 ‘ ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ) · ( 𝐹 ‘ ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ) ) )
27 20 20 26 mpd3an23 ⊢ ( 𝐹 ∈ 𝐴 → ( 𝐹 ‘ ( ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑅 ) ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ) ) = ( ( 𝐹 ‘ ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ) · ( 𝐹 ‘ ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ) ) )
28 2 25 3 4 20 18 ringmneg2 ⊢ ( 𝐹 ∈ 𝐴 → ( ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑅 ) ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ) = ( 𝑁 ‘ ( ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ) )
29 2 25 11 3 4 18 ringnegl ⊢ ( 𝐹 ∈ 𝐴 → ( ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) )
30 29 fveq2d ⊢ ( 𝐹 ∈ 𝐴 → ( 𝑁 ‘ ( ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ) = ( 𝑁 ‘ ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ) )
31 2 3 grpinvinv ⊢ ( ( 𝑅 ∈ Grp ∧ ( 1r ‘ 𝑅 ) ∈ 𝐵 ) → ( 𝑁 ‘ ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ) = ( 1r ‘ 𝑅 ) )
32 7 18 31 syl2anc ⊢ ( 𝐹 ∈ 𝐴 → ( 𝑁 ‘ ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ) = ( 1r ‘ 𝑅 ) )
33 28 30 32 3eqtrd ⊢ ( 𝐹 ∈ 𝐴 → ( ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑅 ) ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ) = ( 1r ‘ 𝑅 ) )
34 33 fveq2d ⊢ ( 𝐹 ∈ 𝐴 → ( 𝐹 ‘ ( ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑅 ) ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ) ) = ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) )
35 24 27 34 3eqtr2d ⊢ ( 𝐹 ∈ 𝐴 → ( ( 𝐹 ‘ ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ) ↑ 2 ) = ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) )
36 35 adantr ⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) → ( ( 𝐹 ‘ ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ) ↑ 2 ) = ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) )
37 1 11 12 abv1z ⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) → ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) = 1 )
38 36 37 eqtrd ⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) → ( ( 𝐹 ‘ ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ) ↑ 2 ) = 1 )
39 sq1 ⊢ ( 1 ↑ 2 ) = 1
40 38 39 eqtr4di ⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) → ( ( 𝐹 ‘ ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ) ↑ 2 ) = ( 1 ↑ 2 ) )
41 1 2 abvge0 ⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ∈ 𝐵 ) → 0 ≤ ( 𝐹 ‘ ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ) )
42 20 41 mpdan ⊢ ( 𝐹 ∈ 𝐴 → 0 ≤ ( 𝐹 ‘ ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ) )
43 1re ⊢ 1 ∈ ℝ
44 0le1 ⊢ 0 ≤ 1
45 sq11 ⊢ ( ( ( ( 𝐹 ‘ ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ) ∈ ℝ ∧ 0 ≤ ( 𝐹 ‘ ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ) ) ∧ ( 1 ∈ ℝ ∧ 0 ≤ 1 ) ) → ( ( ( 𝐹 ‘ ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ) ↑ 2 ) = ( 1 ↑ 2 ) ↔ ( 𝐹 ‘ ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ) = 1 ) )
46 43 44 45 mpanr12 ⊢ ( ( ( 𝐹 ‘ ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ) ∈ ℝ ∧ 0 ≤ ( 𝐹 ‘ ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ) ) → ( ( ( 𝐹 ‘ ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ) ↑ 2 ) = ( 1 ↑ 2 ) ↔ ( 𝐹 ‘ ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ) = 1 ) )
47 22 42 46 syl2anc ⊢ ( 𝐹 ∈ 𝐴 → ( ( ( 𝐹 ‘ ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ) ↑ 2 ) = ( 1 ↑ 2 ) ↔ ( 𝐹 ‘ ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ) = 1 ) )
48 47 biimpa ⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( ( 𝐹 ‘ ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ) ↑ 2 ) = ( 1 ↑ 2 ) ) → ( 𝐹 ‘ ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ) = 1 )
49 40 48 syldan ⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) → ( 𝐹 ‘ ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ) = 1 )
50 49 adantlr ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) → ( 𝐹 ‘ ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ) = 1 )
51 50 oveq1d ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) → ( ( 𝐹 ‘ ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ) · ( 𝐹 ‘ 𝑋 ) ) = ( 1 · ( 𝐹 ‘ 𝑋 ) ) )
52 simpl ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) → 𝐹 ∈ 𝐴 )
53 20 adantr ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ∈ 𝐵 )
54 1 2 25 abvmul ⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ ( ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑅 ) 𝑋 ) ) = ( ( 𝐹 ‘ ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ) · ( 𝐹 ‘ 𝑋 ) ) )
55 52 53 10 54 syl3anc ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ ( ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑅 ) 𝑋 ) ) = ( ( 𝐹 ‘ ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ) · ( 𝐹 ‘ 𝑋 ) ) )
56 2 25 11 3 5 10 ringnegl ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑅 ) 𝑋 ) = ( 𝑁 ‘ 𝑋 ) )
57 56 fveq2d ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ ( ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑅 ) 𝑋 ) ) = ( 𝐹 ‘ ( 𝑁 ‘ 𝑋 ) ) )
58 55 57 eqtr3d ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝐹 ‘ ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ) · ( 𝐹 ‘ 𝑋 ) ) = ( 𝐹 ‘ ( 𝑁 ‘ 𝑋 ) ) )
59 58 adantr ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) → ( ( 𝐹 ‘ ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ) · ( 𝐹 ‘ 𝑋 ) ) = ( 𝐹 ‘ ( 𝑁 ‘ 𝑋 ) ) )
60 51 59 eqtr3d ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) → ( 1 · ( 𝐹 ‘ 𝑋 ) ) = ( 𝐹 ‘ ( 𝑁 ‘ 𝑋 ) ) )
61 1 2 abvcl ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑋 ) ∈ ℝ )
62 61 recnd ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑋 ) ∈ ℂ )
63 62 mullidd ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) → ( 1 · ( 𝐹 ‘ 𝑋 ) ) = ( 𝐹 ‘ 𝑋 ) )
64 63 adantr ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) → ( 1 · ( 𝐹 ‘ 𝑋 ) ) = ( 𝐹 ‘ 𝑋 ) )
65 60 64 eqtr3d ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) → ( 𝐹 ‘ ( 𝑁 ‘ 𝑋 ) ) = ( 𝐹 ‘ 𝑋 ) )
66 16 65 pm2.61dane ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑁 ‘ 𝑋 ) ) = ( 𝐹 ‘ 𝑋 ) )