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