Theorem nvlinv

Description: Minus a vector plus itself. (Contributed by NM, 4-Dec-2007) (Revised by Mario Carneiro, 21-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nvrinv.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
	nvrinv.2	⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
	nvrinv.4	⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
	nvrinv.6	⊢ 𝑍 = ( 0vec ‘ 𝑈 )
Assertion	nvlinv	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( ( - 1 𝑆 𝐴 ) 𝐺 𝐴 ) = 𝑍 )

Proof

Step	Hyp	Ref	Expression
1		nvrinv.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2		nvrinv.2	⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
3		nvrinv.4	⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
4		nvrinv.6	⊢ 𝑍 = ( 0vec ‘ 𝑈 )
5	2	nvgrp	⊢ ( 𝑈 ∈ NrmCVec → 𝐺 ∈ GrpOp )
6	1 2	bafval	⊢ 𝑋 = ran 𝐺
7		eqid	⊢ ( GId ‘ 𝐺 ) = ( GId ‘ 𝐺 )
8		eqid	⊢ ( inv ‘ 𝐺 ) = ( inv ‘ 𝐺 )
9	6 7 8	grpolinv	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ( ( ( inv ‘ 𝐺 ) ‘ 𝐴 ) 𝐺 𝐴 ) = ( GId ‘ 𝐺 ) )
10	5 9	sylan	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( ( ( inv ‘ 𝐺 ) ‘ 𝐴 ) 𝐺 𝐴 ) = ( GId ‘ 𝐺 ) )
11	1 2 3 8	nvinv	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( - 1 𝑆 𝐴 ) = ( ( inv ‘ 𝐺 ) ‘ 𝐴 ) )
12	11	oveq1d	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( ( - 1 𝑆 𝐴 ) 𝐺 𝐴 ) = ( ( ( inv ‘ 𝐺 ) ‘ 𝐴 ) 𝐺 𝐴 ) )
13	2 4	0vfval	⊢ ( 𝑈 ∈ NrmCVec → 𝑍 = ( GId ‘ 𝐺 ) )
14	13	adantr	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → 𝑍 = ( GId ‘ 𝐺 ) )
15	10 12 14	3eqtr4d	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( ( - 1 𝑆 𝐴 ) 𝐺 𝐴 ) = 𝑍 )