Metamath Proof Explorer

Theorem ncvs1

Description: From any nonzero vector of a normed subcomplex vector space, construct a collinear vector whose norm is one. (Contributed by NM, 6-Dec-2007) (Revised by AV, 8-Oct-2021)

Ref Expression
Hypotheses ncvs1.x 
|- X = ( Base ` G )
ncvs1.n 
|- N = ( norm ` G )
ncvs1.z 
|- .0. = ( 0g ` G )
ncvs1.s 
|- .x. = ( .s ` G )
ncvs1.f 
|- F = ( Scalar ` G )
ncvs1.k 
|- K = ( Base ` F )
Assertion ncvs1 
|- ( ( G e. ( NrmVec i^i CVec ) /\ ( A e. X /\ A =/= .0. ) /\ ( 1 / ( N ` A ) ) e. K ) -> ( N ` ( ( 1 / ( N ` A ) ) .x. A ) ) = 1 )

Proof

Step Hyp Ref Expression
1 ncvs1.x 
 |-  X = ( Base ` G )
2 ncvs1.n 
 |-  N = ( norm ` G )
3 ncvs1.z 
 |-  .0. = ( 0g ` G )
4 ncvs1.s 
 |-  .x. = ( .s ` G )
5 ncvs1.f 
 |-  F = ( Scalar ` G )
6 ncvs1.k 
 |-  K = ( Base ` F )
7 simp1 
 |-  ( ( G e. ( NrmVec i^i CVec ) /\ ( A e. X /\ A =/= .0. ) /\ ( 1 / ( N ` A ) ) e. K ) -> G e. ( NrmVec i^i CVec ) )
8 simp3 
 |-  ( ( G e. ( NrmVec i^i CVec ) /\ ( A e. X /\ A =/= .0. ) /\ ( 1 / ( N ` A ) ) e. K ) -> ( 1 / ( N ` A ) ) e. K )
9 elin 
 |-  ( G e. ( NrmVec i^i CVec ) <-> ( G e. NrmVec /\ G e. CVec ) )
10 nvcnlm 
 |-  ( G e. NrmVec -> G e. NrmMod )
11 nlmngp 
 |-  ( G e. NrmMod -> G e. NrmGrp )
12 10 11 syl 
 |-  ( G e. NrmVec -> G e. NrmGrp )
13 12 adantr 
 |-  ( ( G e. NrmVec /\ G e. CVec ) -> G e. NrmGrp )
14 9 13 sylbi 
 |-  ( G e. ( NrmVec i^i CVec ) -> G e. NrmGrp )
15 simpl 
 |-  ( ( A e. X /\ A =/= .0. ) -> A e. X )
16 14 15 anim12i 
 |-  ( ( G e. ( NrmVec i^i CVec ) /\ ( A e. X /\ A =/= .0. ) ) -> ( G e. NrmGrp /\ A e. X ) )
17 1 2 nmcl 
 |-  ( ( G e. NrmGrp /\ A e. X ) -> ( N ` A ) e. RR )
18 16 17 syl 
 |-  ( ( G e. ( NrmVec i^i CVec ) /\ ( A e. X /\ A =/= .0. ) ) -> ( N ` A ) e. RR )
19 1 2 3 nmeq0 
 |-  ( ( G e. NrmGrp /\ A e. X ) -> ( ( N ` A ) = 0 <-> A = .0. ) )
20 19 bicomd 
 |-  ( ( G e. NrmGrp /\ A e. X ) -> ( A = .0. <-> ( N ` A ) = 0 ) )
21 14 20 sylan 
 |-  ( ( G e. ( NrmVec i^i CVec ) /\ A e. X ) -> ( A = .0. <-> ( N ` A ) = 0 ) )
22 21 necon3bid 
 |-  ( ( G e. ( NrmVec i^i CVec ) /\ A e. X ) -> ( A =/= .0. <-> ( N ` A ) =/= 0 ) )
23 22 biimpd 
 |-  ( ( G e. ( NrmVec i^i CVec ) /\ A e. X ) -> ( A =/= .0. -> ( N ` A ) =/= 0 ) )
24 23 impr 
 |-  ( ( G e. ( NrmVec i^i CVec ) /\ ( A e. X /\ A =/= .0. ) ) -> ( N ` A ) =/= 0 )
25 18 24 rereccld 
 |-  ( ( G e. ( NrmVec i^i CVec ) /\ ( A e. X /\ A =/= .0. ) ) -> ( 1 / ( N ` A ) ) e. RR )
26 25 3adant3 
 |-  ( ( G e. ( NrmVec i^i CVec ) /\ ( A e. X /\ A =/= .0. ) /\ ( 1 / ( N ` A ) ) e. K ) -> ( 1 / ( N ` A ) ) e. RR )
27 8 26 elind 
 |-  ( ( G e. ( NrmVec i^i CVec ) /\ ( A e. X /\ A =/= .0. ) /\ ( 1 / ( N ` A ) ) e. K ) -> ( 1 / ( N ` A ) ) e. ( K i^i RR ) )
28 1re 
 |-  1 e. RR
29 0le1 
 |-  0 <_ 1
30 28 29 pm3.2i 
 |-  ( 1 e. RR /\ 0 <_ 1 )
31 30 a1i 
 |-  ( ( G e. ( NrmVec i^i CVec ) /\ ( A e. X /\ A =/= .0. ) ) -> ( 1 e. RR /\ 0 <_ 1 ) )
32 simprr 
 |-  ( ( G e. ( NrmVec i^i CVec ) /\ ( A e. X /\ A =/= .0. ) ) -> A =/= .0. )
33 1 2 3 nmgt0 
 |-  ( ( G e. NrmGrp /\ A e. X ) -> ( A =/= .0. <-> 0 < ( N ` A ) ) )
34 16 33 syl 
 |-  ( ( G e. ( NrmVec i^i CVec ) /\ ( A e. X /\ A =/= .0. ) ) -> ( A =/= .0. <-> 0 < ( N ` A ) ) )
35 32 34 mpbid 
 |-  ( ( G e. ( NrmVec i^i CVec ) /\ ( A e. X /\ A =/= .0. ) ) -> 0 < ( N ` A ) )
36 31 18 35 jca32 
 |-  ( ( G e. ( NrmVec i^i CVec ) /\ ( A e. X /\ A =/= .0. ) ) -> ( ( 1 e. RR /\ 0 <_ 1 ) /\ ( ( N ` A ) e. RR /\ 0 < ( N ` A ) ) ) )
37 36 3adant3 
 |-  ( ( G e. ( NrmVec i^i CVec ) /\ ( A e. X /\ A =/= .0. ) /\ ( 1 / ( N ` A ) ) e. K ) -> ( ( 1 e. RR /\ 0 <_ 1 ) /\ ( ( N ` A ) e. RR /\ 0 < ( N ` A ) ) ) )
38 divge0 
 |-  ( ( ( 1 e. RR /\ 0 <_ 1 ) /\ ( ( N ` A ) e. RR /\ 0 < ( N ` A ) ) ) -> 0 <_ ( 1 / ( N ` A ) ) )
39 37 38 syl 
 |-  ( ( G e. ( NrmVec i^i CVec ) /\ ( A e. X /\ A =/= .0. ) /\ ( 1 / ( N ` A ) ) e. K ) -> 0 <_ ( 1 / ( N ` A ) ) )
40 simp2l 
 |-  ( ( G e. ( NrmVec i^i CVec ) /\ ( A e. X /\ A =/= .0. ) /\ ( 1 / ( N ` A ) ) e. K ) -> A e. X )
41 1 2 4 5 6 ncvsge0 
 |-  ( ( G e. ( NrmVec i^i CVec ) /\ ( ( 1 / ( N ` A ) ) e. ( K i^i RR ) /\ 0 <_ ( 1 / ( N ` A ) ) ) /\ A e. X ) -> ( N ` ( ( 1 / ( N ` A ) ) .x. A ) ) = ( ( 1 / ( N ` A ) ) x. ( N ` A ) ) )
42 7 27 39 40 41 syl121anc 
 |-  ( ( G e. ( NrmVec i^i CVec ) /\ ( A e. X /\ A =/= .0. ) /\ ( 1 / ( N ` A ) ) e. K ) -> ( N ` ( ( 1 / ( N ` A ) ) .x. A ) ) = ( ( 1 / ( N ` A ) ) x. ( N ` A ) ) )
43 16 3adant3 
 |-  ( ( G e. ( NrmVec i^i CVec ) /\ ( A e. X /\ A =/= .0. ) /\ ( 1 / ( N ` A ) ) e. K ) -> ( G e. NrmGrp /\ A e. X ) )
44 43 17 syl 
 |-  ( ( G e. ( NrmVec i^i CVec ) /\ ( A e. X /\ A =/= .0. ) /\ ( 1 / ( N ` A ) ) e. K ) -> ( N ` A ) e. RR )
45 44 recnd 
 |-  ( ( G e. ( NrmVec i^i CVec ) /\ ( A e. X /\ A =/= .0. ) /\ ( 1 / ( N ` A ) ) e. K ) -> ( N ` A ) e. CC )
46 24 3adant3 
 |-  ( ( G e. ( NrmVec i^i CVec ) /\ ( A e. X /\ A =/= .0. ) /\ ( 1 / ( N ` A ) ) e. K ) -> ( N ` A ) =/= 0 )
47 45 46 recid2d 
 |-  ( ( G e. ( NrmVec i^i CVec ) /\ ( A e. X /\ A =/= .0. ) /\ ( 1 / ( N ` A ) ) e. K ) -> ( ( 1 / ( N ` A ) ) x. ( N ` A ) ) = 1 )
48 42 47 eqtrd 
 |-  ( ( G e. ( NrmVec i^i CVec ) /\ ( A e. X /\ A =/= .0. ) /\ ( 1 / ( N ` A ) ) e. K ) -> ( N ` ( ( 1 / ( N ` A ) ) .x. A ) ) = 1 )