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	⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
	nvinvfval.4	⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
	nvinvfval.3	⊢ 𝑁 = ( 𝑆 ∘ ◡ ( 2nd ↾ ( { - 1 } × V ) ) )
Assertion	nvinvfval	⊢ ( 𝑈 ∈ NrmCVec → 𝑁 = ( inv ‘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		nvinvfval.2	⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
2		nvinvfval.4	⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
3		nvinvfval.3	⊢ 𝑁 = ( 𝑆 ∘ ◡ ( 2nd ↾ ( { - 1 } × V ) ) )
4		eqid	⊢ ( BaseSet ‘ 𝑈 ) = ( BaseSet ‘ 𝑈 )
5	4 2	nvsf	⊢ ( 𝑈 ∈ NrmCVec → 𝑆 : ( ℂ × ( BaseSet ‘ 𝑈 ) ) ⟶ ( BaseSet ‘ 𝑈 ) )
6		neg1cn	⊢ - 1 ∈ ℂ
7	3	curry1f	⊢ ( ( 𝑆 : ( ℂ × ( BaseSet ‘ 𝑈 ) ) ⟶ ( BaseSet ‘ 𝑈 ) ∧ - 1 ∈ ℂ ) → 𝑁 : ( BaseSet ‘ 𝑈 ) ⟶ ( BaseSet ‘ 𝑈 ) )
8	5 6 7	sylancl	⊢ ( 𝑈 ∈ NrmCVec → 𝑁 : ( BaseSet ‘ 𝑈 ) ⟶ ( BaseSet ‘ 𝑈 ) )
9	8	ffnd	⊢ ( 𝑈 ∈ NrmCVec → 𝑁 Fn ( BaseSet ‘ 𝑈 ) )
10	1	nvgrp	⊢ ( 𝑈 ∈ NrmCVec → 𝐺 ∈ GrpOp )
11	4 1	bafval	⊢ ( BaseSet ‘ 𝑈 ) = ran 𝐺
12		eqid	⊢ ( inv ‘ 𝐺 ) = ( inv ‘ 𝐺 )
13	11 12	grpoinvf	⊢ ( 𝐺 ∈ GrpOp → ( inv ‘ 𝐺 ) : ( BaseSet ‘ 𝑈 ) –1-1-onto→ ( BaseSet ‘ 𝑈 ) )
14		f1ofn	⊢ ( ( inv ‘ 𝐺 ) : ( BaseSet ‘ 𝑈 ) –1-1-onto→ ( BaseSet ‘ 𝑈 ) → ( inv ‘ 𝐺 ) Fn ( BaseSet ‘ 𝑈 ) )
15	10 13 14	3syl	⊢ ( 𝑈 ∈ NrmCVec → ( inv ‘ 𝐺 ) Fn ( BaseSet ‘ 𝑈 ) )
16	5	ffnd	⊢ ( 𝑈 ∈ NrmCVec → 𝑆 Fn ( ℂ × ( BaseSet ‘ 𝑈 ) ) )
17	16	adantr	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ) → 𝑆 Fn ( ℂ × ( BaseSet ‘ 𝑈 ) ) )
18	3	curry1val	⊢ ( ( 𝑆 Fn ( ℂ × ( BaseSet ‘ 𝑈 ) ) ∧ - 1 ∈ ℂ ) → ( 𝑁 ‘ 𝑥 ) = ( - 1 𝑆 𝑥 ) )
19	17 6 18	sylancl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ) → ( 𝑁 ‘ 𝑥 ) = ( - 1 𝑆 𝑥 ) )
20	4 1 2 12	nvinv	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ) → ( - 1 𝑆 𝑥 ) = ( ( inv ‘ 𝐺 ) ‘ 𝑥 ) )
21	19 20	eqtrd	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ) → ( 𝑁 ‘ 𝑥 ) = ( ( inv ‘ 𝐺 ) ‘ 𝑥 ) )
22	9 15 21	eqfnfvd	⊢ ( 𝑈 ∈ NrmCVec → 𝑁 = ( inv ‘ 𝐺 ) )