Metamath Proof Explorer

Theorem nvinvfval

Description: Function for the negative of a vector on a normed complex vector space, in terms of the underlying addition group inverse. (We currently do not have a separate notation for the negative of a vector.) (Contributed by NM, 27-Mar-2008) (New usage is discouraged.)

Ref Expression
Hypotheses nvinvfval.2 ⊢ G = + v ⁡ U
nvinvfval.4 ⊢ S = ⋅ 𝑠OLD ⁡ U
nvinvfval.3 ⊢ N = S ∘ 2 nd ↾ − 1 × V -1
Assertion nvinvfval ⊢ U ∈ NrmCVec → N = inv ⁡ G

Proof

Step Hyp Ref Expression
1 nvinvfval.2 ⊢ G = + v ⁡ U
2 nvinvfval.4 ⊢ S = ⋅ 𝑠OLD ⁡ U
3 nvinvfval.3 ⊢ N = S ∘ 2 nd ↾ − 1 × V -1
4 eqid ⊢ BaseSet ⁡ U = BaseSet ⁡ U
5 4 2 nvsf ⊢ U ∈ NrmCVec → S : ℂ × BaseSet ⁡ U ⟶ BaseSet ⁡ U
6 neg1cn ⊢ − 1 ∈ ℂ
7 3 curry1f ⊢ S : ℂ × BaseSet ⁡ U ⟶ BaseSet ⁡ U ∧ − 1 ∈ ℂ → N : BaseSet ⁡ U ⟶ BaseSet ⁡ U
8 5 6 7 sylancl ⊢ U ∈ NrmCVec → N : BaseSet ⁡ U ⟶ BaseSet ⁡ U
9 8 ffnd ⊢ U ∈ NrmCVec → N Fn BaseSet ⁡ U
10 1 nvgrp ⊢ U ∈ NrmCVec → G ∈ GrpOp
11 4 1 bafval ⊢ BaseSet ⁡ U = ran ⁡ G
12 eqid ⊢ inv ⁡ G = inv ⁡ G
13 11 12 grpoinvf ⊢ G ∈ GrpOp → inv ⁡ G : BaseSet ⁡ U ⟶ 1-1 onto BaseSet ⁡ U
14 f1ofn ⊢ inv ⁡ G : BaseSet ⁡ U ⟶ 1-1 onto BaseSet ⁡ U → inv ⁡ G Fn BaseSet ⁡ U
15 10 13 14 3syl ⊢ U ∈ NrmCVec → inv ⁡ G Fn BaseSet ⁡ U
16 5 ffnd ⊢ U ∈ NrmCVec → S Fn ℂ × BaseSet ⁡ U
17 16 adantr ⊢ U ∈ NrmCVec ∧ x ∈ BaseSet ⁡ U → S Fn ℂ × BaseSet ⁡ U
18 3 curry1val ⊢ S Fn ℂ × BaseSet ⁡ U ∧ − 1 ∈ ℂ → N ⁡ x = -1 S x
19 17 6 18 sylancl ⊢ U ∈ NrmCVec ∧ x ∈ BaseSet ⁡ U → N ⁡ x = -1 S x
20 4 1 2 12 nvinv ⊢ U ∈ NrmCVec ∧ x ∈ BaseSet ⁡ U → -1 S x = inv ⁡ G ⁡ x
21 19 20 eqtrd ⊢ U ∈ NrmCVec ∧ x ∈ BaseSet ⁡ U → N ⁡ x = inv ⁡ G ⁡ x
22 9 15 21 eqfnfvd ⊢ U ∈ NrmCVec → N = inv ⁡ G