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

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 ⊢ 𝑋 = ( Base ‘ 𝐺 )
nmf.n ⊢ 𝑁 = ( norm ‘ 𝐺 )
nminv.i ⊢ 𝐼 = ( invg ‘ 𝐺 )
Assertion nminv ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐼 ‘ 𝐴 ) ) = ( 𝑁 ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 nmf.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 nmf.n ⊢ 𝑁 = ( norm ‘ 𝐺 )
3 nminv.i ⊢ 𝐼 = ( invg ‘ 𝐺 )
4 ngpgrp ⊢ ( 𝐺 ∈ NrmGrp → 𝐺 ∈ Grp )
5 4 adantr ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ) → 𝐺 ∈ Grp )
6 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
7 1 6 grpidcl ⊢ ( 𝐺 ∈ Grp → ( 0g ‘ 𝐺 ) ∈ 𝑋 )
8 5 7 syl ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ) → ( 0g ‘ 𝐺 ) ∈ 𝑋 )
9 eqid ⊢ ( -g ‘ 𝐺 ) = ( -g ‘ 𝐺 )
10 eqid ⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
11 2 1 9 10 ngpdsr ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑋 ) → ( 𝐴 ( dist ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) = ( 𝑁 ‘ ( ( 0g ‘ 𝐺 ) ( -g ‘ 𝐺 ) 𝐴 ) ) )
12 8 11 mpd3an3 ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 ( dist ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) = ( 𝑁 ‘ ( ( 0g ‘ 𝐺 ) ( -g ‘ 𝐺 ) 𝐴 ) ) )
13 2 1 6 10 nmval ⊢ ( 𝐴 ∈ 𝑋 → ( 𝑁 ‘ 𝐴 ) = ( 𝐴 ( dist ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) )
14 13 adantl ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ) → ( 𝑁 ‘ 𝐴 ) = ( 𝐴 ( dist ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) )
15 1 9 3 6 grpinvval2 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( 𝐼 ‘ 𝐴 ) = ( ( 0g ‘ 𝐺 ) ( -g ‘ 𝐺 ) 𝐴 ) )
16 4 15 sylan ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ) → ( 𝐼 ‘ 𝐴 ) = ( ( 0g ‘ 𝐺 ) ( -g ‘ 𝐺 ) 𝐴 ) )
17 16 fveq2d ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐼 ‘ 𝐴 ) ) = ( 𝑁 ‘ ( ( 0g ‘ 𝐺 ) ( -g ‘ 𝐺 ) 𝐴 ) ) )
18 12 14 17 3eqtr4rd ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐼 ‘ 𝐴 ) ) = ( 𝑁 ‘ 𝐴 ) )