This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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