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

Metamath Proof Explorer

Theorem nvnegneg

Description: Double negative of a vector. (Contributed by NM, 4-Dec-2007) (New usage is discouraged.)

Ref Expression
Hypotheses nvnegneg.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
nvnegneg.4 ⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
Assertion nvnegneg ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( - 1 𝑆 ( - 1 𝑆 𝐴 ) ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 nvnegneg.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 nvnegneg.4 ⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
3 neg1cn ⊢ - 1 ∈ ℂ
4 1 2 nvscl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ - 1 ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) → ( - 1 𝑆 𝐴 ) ∈ 𝑋 )
5 3 4 mp3an2 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( - 1 𝑆 𝐴 ) ∈ 𝑋 )
6 eqid ⊢ ( +𝑣 ‘ 𝑈 ) = ( +𝑣 ‘ 𝑈 )
7 eqid ⊢ ( inv ‘ ( +𝑣 ‘ 𝑈 ) ) = ( inv ‘ ( +𝑣 ‘ 𝑈 ) )
8 1 6 2 7 nvinv ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( - 1 𝑆 𝐴 ) ∈ 𝑋 ) → ( - 1 𝑆 ( - 1 𝑆 𝐴 ) ) = ( ( inv ‘ ( +𝑣 ‘ 𝑈 ) ) ‘ ( - 1 𝑆 𝐴 ) ) )
9 5 8 syldan ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( - 1 𝑆 ( - 1 𝑆 𝐴 ) ) = ( ( inv ‘ ( +𝑣 ‘ 𝑈 ) ) ‘ ( - 1 𝑆 𝐴 ) ) )
10 1 6 2 7 nvinv ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( - 1 𝑆 𝐴 ) = ( ( inv ‘ ( +𝑣 ‘ 𝑈 ) ) ‘ 𝐴 ) )
11 10 fveq2d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( ( inv ‘ ( +𝑣 ‘ 𝑈 ) ) ‘ ( - 1 𝑆 𝐴 ) ) = ( ( inv ‘ ( +𝑣 ‘ 𝑈 ) ) ‘ ( ( inv ‘ ( +𝑣 ‘ 𝑈 ) ) ‘ 𝐴 ) ) )
12 6 nvgrp ⊢ ( 𝑈 ∈ NrmCVec → ( +𝑣 ‘ 𝑈 ) ∈ GrpOp )
13 1 6 bafval ⊢ 𝑋 = ran ( +𝑣 ‘ 𝑈 )
14 13 7 grpo2inv ⊢ ( ( ( +𝑣 ‘ 𝑈 ) ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ( ( inv ‘ ( +𝑣 ‘ 𝑈 ) ) ‘ ( ( inv ‘ ( +𝑣 ‘ 𝑈 ) ) ‘ 𝐴 ) ) = 𝐴 )
15 12 14 sylan ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( ( inv ‘ ( +𝑣 ‘ 𝑈 ) ) ‘ ( ( inv ‘ ( +𝑣 ‘ 𝑈 ) ) ‘ 𝐴 ) ) = 𝐴 )
16 9 11 15 3eqtrd ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( - 1 𝑆 ( - 1 𝑆 𝐴 ) ) = 𝐴 )