nmsub

Description: The norm of the difference between two elements. (Contributed by Mario Carneiro, 4-Oct-2015)

	Ref	Expression
Hypotheses	nmf.x	$⊢ X = {Base}_{G}$
	nmf.n	$⊢ N = norm (G)$
	nmmtri.m	$⊢ \underset{˙}{-} = -_{G}$
Assertion	nmsub	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to N (A \underset{˙}{-} B) = N (B \underset{˙}{-} A)$

Step	Hyp	Ref	Expression
1		nmf.x	$⊢ X = {Base}_{G}$
2		nmf.n	$⊢ N = norm (G)$
3		nmmtri.m	$⊢ \underset{˙}{-} = -_{G}$
4		simp1	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to G \in NrmGrp$
5		ngpgrp	$⊢ G \in NrmGrp \to G \in Grp$
6	4 5	syl	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to G \in Grp$
7		simp3	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to B \in X$
8		simp2	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to A \in X$
9		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
10	1 3 9	grpinvsub	$⊢ (G \in Grp \land B \in X \land A \in X) \to {inv}_{g} (G) (B \underset{˙}{-} A) = A \underset{˙}{-} B$
11	6 7 8 10	syl3anc	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to {inv}_{g} (G) (B \underset{˙}{-} A) = A \underset{˙}{-} B$
12	11	fveq2d	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to N ({inv}_{g} (G) (B \underset{˙}{-} A)) = N (A \underset{˙}{-} B)$
13	1 3	grpsubcl	$⊢ (G \in Grp \land B \in X \land A \in X) \to B \underset{˙}{-} A \in X$
14	6 7 8 13	syl3anc	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to B \underset{˙}{-} A \in X$
15	1 2 9	nminv	$⊢ (G \in NrmGrp \land B \underset{˙}{-} A \in X) \to N ({inv}_{g} (G) (B \underset{˙}{-} A)) = N (B \underset{˙}{-} A)$
16	4 14 15	syl2anc	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to N ({inv}_{g} (G) (B \underset{˙}{-} A)) = N (B \underset{˙}{-} A)$
17	12 16	eqtr3d	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to N (A \underset{˙}{-} B) = N (B \underset{˙}{-} A)$

Metamath Proof Explorer