Metamath Proof Explorer

Theorem 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)

Ref Expression
Hypotheses nmf.x ⊢ X = Base G
nmf.n ⊢ N = norm ⁡ G
nminv.i ⊢ I = inv g ⁡ G
Assertion nminv ⊢ G ∈ NrmGrp ∧ A ∈ X → N ⁡ I ⁡ A = N ⁡ A

Proof

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 ∈ NrmGrp → G ∈ Grp
5 4 adantr ⊢ G ∈ NrmGrp ∧ A ∈ X → G ∈ Grp
6 eqid ⊢ 0 G = 0 G
7 1 6 grpidcl ⊢ G ∈ Grp → 0 G ∈ X
8 5 7 syl ⊢ G ∈ NrmGrp ∧ A ∈ X → 0 G ∈ X
9 eqid ⊢ - G = - G
10 eqid ⊢ dist ⁡ G = dist ⁡ G
11 2 1 9 10 ngpdsr ⊢ G ∈ NrmGrp ∧ A ∈ X ∧ 0 G ∈ X → A dist ⁡ G 0 G = N ⁡ 0 G - G A
12 8 11 mpd3an3 ⊢ G ∈ NrmGrp ∧ A ∈ X → A dist ⁡ G 0 G = N ⁡ 0 G - G A
13 2 1 6 10 nmval ⊢ A ∈ X → N ⁡ A = A dist ⁡ G 0 G
14 13 adantl ⊢ G ∈ NrmGrp ∧ A ∈ X → N ⁡ A = A dist ⁡ G 0 G
15 1 9 3 6 grpinvval2 ⊢ G ∈ Grp ∧ A ∈ X → I ⁡ A = 0 G - G A
16 4 15 sylan ⊢ G ∈ NrmGrp ∧ A ∈ X → I ⁡ A = 0 G - G A
17 16 fveq2d ⊢ G ∈ NrmGrp ∧ A ∈ X → N ⁡ I ⁡ A = N ⁡ 0 G - G A
18 12 14 17 3eqtr4rd ⊢ G ∈ NrmGrp ∧ A ∈ X → N ⁡ I ⁡ A = N ⁡ A