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 ⊢ X = BaseSet ⁡ U
nvnegneg.4 ⊢ S = ⋅ 𝑠OLD ⁡ U
Assertion nvnegneg ⊢ U ∈ NrmCVec ∧ A ∈ X → -1 S -1 S A = A

Proof

Step Hyp Ref Expression
1 nvnegneg.1 ⊢ X = BaseSet ⁡ U
2 nvnegneg.4 ⊢ S = ⋅ 𝑠OLD ⁡ U
3 neg1cn ⊢ − 1 ∈ ℂ
4 1 2 nvscl ⊢ U ∈ NrmCVec ∧ − 1 ∈ ℂ ∧ A ∈ X → -1 S A ∈ X
5 3 4 mp3an2 ⊢ U ∈ NrmCVec ∧ A ∈ X → -1 S A ∈ X
6 eqid ⊢ + v ⁡ U = + v ⁡ U
7 eqid ⊢ inv ⁡ + v ⁡ U = inv ⁡ + v ⁡ U
8 1 6 2 7 nvinv ⊢ U ∈ NrmCVec ∧ -1 S A ∈ X → -1 S -1 S A = inv ⁡ + v ⁡ U ⁡ -1 S A
9 5 8 syldan ⊢ U ∈ NrmCVec ∧ A ∈ X → -1 S -1 S A = inv ⁡ + v ⁡ U ⁡ -1 S A
10 1 6 2 7 nvinv ⊢ U ∈ NrmCVec ∧ A ∈ X → -1 S A = inv ⁡ + v ⁡ U ⁡ A
11 10 fveq2d ⊢ U ∈ NrmCVec ∧ A ∈ X → inv ⁡ + v ⁡ U ⁡ -1 S A = inv ⁡ + v ⁡ U ⁡ inv ⁡ + v ⁡ U ⁡ A
12 6 nvgrp ⊢ U ∈ NrmCVec → + v ⁡ U ∈ GrpOp
13 1 6 bafval ⊢ X = ran ⁡ + v ⁡ U
14 13 7 grpo2inv ⊢ + v ⁡ U ∈ GrpOp ∧ A ∈ X → inv ⁡ + v ⁡ U ⁡ inv ⁡ + v ⁡ U ⁡ A = A
15 12 14 sylan ⊢ U ∈ NrmCVec ∧ A ∈ X → inv ⁡ + v ⁡ U ⁡ inv ⁡ + v ⁡ U ⁡ A = A
16 9 11 15 3eqtrd ⊢ U ∈ NrmCVec ∧ A ∈ X → -1 S -1 S A = A