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∘2nd↾−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∘2nd↾−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→NFnBaseSet⁡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 ontoBaseSet⁡U
14 f1ofn ⊢inv⁡G:BaseSet⁡U⟶1-1 ontoBaseSet⁡U→inv⁡GFnBaseSet⁡U
15 10 13 14 3syl ⊢U∈NrmCVec→inv⁡GFnBaseSet⁡U
16 5 ffnd ⊢U∈NrmCVec→SFnℂ×BaseSet⁡U
17 16 adantr ⊢U∈NrmCVec∧x∈BaseSet⁡U→SFnℂ×BaseSet⁡U
18 3 curry1val ⊢SFnℂ×BaseSet⁡U∧−1∈ℂ→N⁡x=-1Sx
19 17 6 18 sylancl ⊢U∈NrmCVec∧x∈BaseSet⁡U→N⁡x=-1Sx
20 4 1 2 12 nvinv ⊢U∈NrmCVec∧x∈BaseSet⁡U→-1Sx=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