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

Metamath Proof Explorer

Theorem nvrinv

Description: A vector minus 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 nvrinv ( ( 𝑈 ∈ 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 grporinv ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝐺 ( ( inv ‘ 𝐺 ) ‘ 𝐴 ) ) = ( GId ‘ 𝐺 ) )
10 5 9 sylan ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝐺 ( ( inv ‘ 𝐺 ) ‘ 𝐴 ) ) = ( GId ‘ 𝐺 ) )
11 1 2 3 8 nvinv ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( - 1 𝑆 𝐴 ) = ( ( inv ‘ 𝐺 ) ‘ 𝐴 ) )
12 11 oveq2d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝐺 ( - 1 𝑆 𝐴 ) ) = ( 𝐴 𝐺 ( ( inv ‘ 𝐺 ) ‘ 𝐴 ) ) )
13 2 4 0vfval ⊢ ( 𝑈 ∈ NrmCVec → 𝑍 = ( GId ‘ 𝐺 ) )
14 13 adantr ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → 𝑍 = ( GId ‘ 𝐺 ) )
15 10 12 14 3eqtr4d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝐺 ( - 1 𝑆 𝐴 ) ) = 𝑍 )