Theorem nmsub

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

	Ref	Expression
Hypotheses	nmf.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
	nmf.n	⊢ 𝑁 = ( norm ‘ 𝐺 )
	nmmtri.m	⊢ − = ( -g ‘ 𝐺 )
Assertion	nmsub	⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 − 𝐵 ) ) = ( 𝑁 ‘ ( 𝐵 − 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		nmf.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
2		nmf.n	⊢ 𝑁 = ( norm ‘ 𝐺 )
3		nmmtri.m	⊢ − = ( -g ‘ 𝐺 )
4		simp1	⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝐺 ∈ NrmGrp )
5		ngpgrp	⊢ ( 𝐺 ∈ NrmGrp → 𝐺 ∈ Grp )
6	4 5	syl	⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝐺 ∈ Grp )
7		simp3	⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝐵 ∈ 𝑋 )
8		simp2	⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝐴 ∈ 𝑋 )
9		eqid	⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
10	1 3 9	grpinvsub	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( ( invg ‘ 𝐺 ) ‘ ( 𝐵 − 𝐴 ) ) = ( 𝐴 − 𝐵 ) )
11	6 7 8 10	syl3anc	⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( invg ‘ 𝐺 ) ‘ ( 𝐵 − 𝐴 ) ) = ( 𝐴 − 𝐵 ) )
12	11	fveq2d	⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( ( invg ‘ 𝐺 ) ‘ ( 𝐵 − 𝐴 ) ) ) = ( 𝑁 ‘ ( 𝐴 − 𝐵 ) ) )
13	1 3	grpsubcl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝐵 − 𝐴 ) ∈ 𝑋 )
14	6 7 8 13	syl3anc	⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐵 − 𝐴 ) ∈ 𝑋 )
15	1 2 9	nminv	⊢ ( ( 𝐺 ∈ NrmGrp ∧ ( 𝐵 − 𝐴 ) ∈ 𝑋 ) → ( 𝑁 ‘ ( ( invg ‘ 𝐺 ) ‘ ( 𝐵 − 𝐴 ) ) ) = ( 𝑁 ‘ ( 𝐵 − 𝐴 ) ) )
16	4 14 15	syl2anc	⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( ( invg ‘ 𝐺 ) ‘ ( 𝐵 − 𝐴 ) ) ) = ( 𝑁 ‘ ( 𝐵 − 𝐴 ) ) )
17	12 16	eqtr3d	⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 − 𝐵 ) ) = ( 𝑁 ‘ ( 𝐵 − 𝐴 ) ) )