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

Metamath Proof Explorer

Theorem abvneg

Proof