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

Metamath Proof Explorer

Theorem clmnegneg

Description: Double negative of a vector. (Contributed by NM, 6-Aug-2007) (Revised by AV, 21-Sep-2021)

Ref Expression
Hypotheses clmpm1dir.v ⊢ V = Base W
clmpm1dir.s ⊢ · ˙ = ⋅ W
clmpm1dir.a ⊢ + ˙ = + W
Assertion clmnegneg ⊢ W ∈ CMod ∧ A ∈ V → -1 · ˙ -1 · ˙ A = A

Proof

Step Hyp Ref Expression
1 clmpm1dir.v ⊢ V = Base W
2 clmpm1dir.s ⊢ · ˙ = ⋅ W
3 clmpm1dir.a ⊢ + ˙ = + W
4 neg1mulneg1e1 ⊢ -1 ⁢ -1 = 1
5 4 oveq1i ⊢ -1 ⁢ -1 · ˙ A = 1 · ˙ A
6 simpl ⊢ W ∈ CMod ∧ A ∈ V → W ∈ CMod
7 eqid ⊢ Scalar ⁡ W = Scalar ⁡ W
8 eqid ⊢ Base Scalar ⁡ W = Base Scalar ⁡ W
9 7 8 clmneg1 ⊢ W ∈ CMod → − 1 ∈ Base Scalar ⁡ W
10 9 adantr ⊢ W ∈ CMod ∧ A ∈ V → − 1 ∈ Base Scalar ⁡ W
11 simpr ⊢ W ∈ CMod ∧ A ∈ V → A ∈ V
12 1 7 2 8 clmvsass ⊢ W ∈ CMod ∧ − 1 ∈ Base Scalar ⁡ W ∧ − 1 ∈ Base Scalar ⁡ W ∧ A ∈ V → -1 ⁢ -1 · ˙ A = -1 · ˙ -1 · ˙ A
13 6 10 10 11 12 syl13anc ⊢ W ∈ CMod ∧ A ∈ V → -1 ⁢ -1 · ˙ A = -1 · ˙ -1 · ˙ A
14 1 2 clmvs1 ⊢ W ∈ CMod ∧ A ∈ V → 1 · ˙ A = A
15 5 13 14 3eqtr3a ⊢ W ∈ CMod ∧ A ∈ V → -1 · ˙ -1 · ˙ A = A