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 ⊢ X = BaseSet ⁡ U
nvrinv.2 ⊢ G = + v ⁡ U
nvrinv.4 ⊢ S = ⋅ 𝑠OLD ⁡ U
nvrinv.6 ⊢ Z = 0 vec ⁡ U
Assertion nvrinv ⊢ U ∈ NrmCVec ∧ A ∈ X → A G -1 S A = Z

Proof

Step Hyp Ref Expression
1 nvrinv.1 ⊢ X = BaseSet ⁡ U
2 nvrinv.2 ⊢ G = + v ⁡ U
3 nvrinv.4 ⊢ S = ⋅ 𝑠OLD ⁡ U
4 nvrinv.6 ⊢ Z = 0 vec ⁡ U
5 2 nvgrp ⊢ U ∈ NrmCVec → G ∈ GrpOp
6 1 2 bafval ⊢ X = ran ⁡ G
7 eqid ⊢ GId ⁡ G = GId ⁡ G
8 eqid ⊢ inv ⁡ G = inv ⁡ G
9 6 7 8 grporinv ⊢ G ∈ GrpOp ∧ A ∈ X → A G inv ⁡ G ⁡ A = GId ⁡ G
10 5 9 sylan ⊢ U ∈ NrmCVec ∧ A ∈ X → A G inv ⁡ G ⁡ A = GId ⁡ G
11 1 2 3 8 nvinv ⊢ U ∈ NrmCVec ∧ A ∈ X → -1 S A = inv ⁡ G ⁡ A
12 11 oveq2d ⊢ U ∈ NrmCVec ∧ A ∈ X → A G -1 S A = A G inv ⁡ G ⁡ A
13 2 4 0vfval ⊢ U ∈ NrmCVec → Z = GId ⁡ G
14 13 adantr ⊢ U ∈ NrmCVec ∧ A ∈ X → Z = GId ⁡ G
15 10 12 14 3eqtr4d ⊢ U ∈ NrmCVec ∧ A ∈ X → A G -1 S A = Z