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	⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑁 ‘ 𝑋 ) ) = ( 𝐹 ‘ 𝑋 ) )