nminv

Description: The norm of a negated element is the same as the norm of the original element. (Contributed by Mario Carneiro, 4-Oct-2015)

Step	Hyp	Ref	Expression
1		nmf.x	$⊢ X = {Base}_{G}$
2		nmf.n	$⊢ N = norm (G)$
3		nminv.i	$⊢ I = {inv}_{g} (G)$
4		ngpgrp	$⊢ G \in NrmGrp \to G \in Grp$
5	4	adantr	$⊢ (G \in NrmGrp \land A \in X) \to G \in Grp$
6		eqid	$⊢ 0_{G} = 0_{G}$
7	1 6	grpidcl	$⊢ G \in Grp \to 0_{G} \in X$
8	5 7	syl	$⊢ (G \in NrmGrp \land A \in X) \to 0_{G} \in X$
9		eqid	$⊢ -_{G} = -_{G}$
10		eqid	$⊢ dist (G) = dist (G)$
11	2 1 9 10	ngpdsr	$⊢ (G \in NrmGrp \land A \in X \land 0_{G} \in X) \to A dist (G) 0_{G} = N (0_{G} -_{G} A)$
12	8 11	mpd3an3	$⊢ (G \in NrmGrp \land A \in X) \to A dist (G) 0_{G} = N (0_{G} -_{G} A)$
13	2 1 6 10	nmval	$⊢ A \in X \to N (A) = A dist (G) 0_{G}$
14	13	adantl	$⊢ (G \in NrmGrp \land A \in X) \to N (A) = A dist (G) 0_{G}$
15	1 9 3 6	grpinvval2	$⊢ (G \in Grp \land A \in X) \to I (A) = 0_{G} -_{G} A$
16	4 15	sylan	$⊢ (G \in NrmGrp \land A \in X) \to I (A) = 0_{G} -_{G} A$
17	16	fveq2d	$⊢ (G \in NrmGrp \land A \in X) \to N (I (A)) = N (0_{G} -_{G} A)$
18	12 14 17	3eqtr4rd	$⊢ (G \in NrmGrp \land A \in X) \to N (I (A)) = N (A)$

Metamath Proof Explorer