Theorem nvvc 8318

Description: The vector space component of a normed complex vector space.

Hypothesis

Ref	Expression
nvvc.1	|- W = (1st` U)

Assertion

Ref	Expression
nvvc	|- (U e. NrmCVec -> W e. CVec)

Proof of Theorem nvvc

Step	Hyp	Ref	Expression
1		nvvc.1	. . 3 |- W = (1st` U)
2	1	fveq2i 3784	. . . 4 |- (1st` W) = (1st` (1st` U))
3		eqid 1522	. . . . 5 |- (+v` U) = (+v` U)
4	3	vafval 8306	. . . 4 |- (+v` U) = (1st` (1st` U))
5	2, 4	eqtr4i 1545	. . 3 |- (1st` W) = (+v` U)
6	1	fveq2i 3784	. . . 4 |- (2nd` W) = (2nd` (1st` U))
7		eqid 1522	. . . . 5 |- (.s` U) = (.s` U)
8	7	smfval 8308	. . . 4 |- (.s` U) = (2nd` (1st` U))
9	6, 8	eqtr4i 1545	. . 3 |- (2nd` W) = (.s` U)
10	1, 5, 9	nvvop 8312	. 2 |- (U e. NrmCVec -> W = <.(1st` W), (2nd` W)>.)
11		eqid 1522	. . . . . 6 |- (Base` U) = (Base` U)
12	11, 5	bafval 8307	. . . . 5 |- (Base` U) = ran (1st` W)
13	12	eqcomi 1526	. . . 4 |- ran (1st` W) = (Base` U)
14		eqid 1522	. . . . . 6 |- (0v` U) = (0v` U)
15	5, 14	0vfval 8309	. . . . 5 |- (0v` U) = (Id` (1st` W))
16	15	eqcomi 1526	. . . 4 |- (Id` (1st` W)) = (0v` U)
17		eqid 1522	. . . . . 6 |- (norm` U) = (norm` U)
18	17	nmfval 8310	. . . . 5 |- (norm` U) = (2nd` U)
19	18	eqcomi 1526	. . . 4 |- (2nd` U) = (norm` U)
20	13, 5, 9, 16, 19	nvi 8317	. . 3 |- (U e. NrmCVec -> (<.(1st` W), (2nd` W)>. e. CVec /\ (2nd` U):ran (1st` W)-->RR /\ A.x e. ran (1st` W)((((2nd` U)` x) = 0 -> x = (Id` (1st` W))) /\ A.y e. CC ((2nd` U)` (y(2nd` W)x)) = ((abs` y) x. ((2nd` U)` x)) /\ A.y e. ran (1st` W)((2nd` U)` (x(1st` W)y)) <_ (((2nd` U)` x) + ((2nd` U)` y)))))
21	20	3simp1d 806	. 2 |- (U e. NrmCVec -> <.(1st` W), (2nd` W)>. e. CVec)
22	10, 21	eqeltrd 1595	1 |- (U e. NrmCVec -> W e. CVec)

Syntax hints:   -> wi 3   /\ w3a 787   = wceq 997   e. wcel 999  A.wral 1692  <.cop 2463   class class class wbr 2674  ran crn 3228  -->wf 3235  ` cfv 3239  (class class class)co 4021  1stc1st 4135  2ndc2nd 4136  CCcc 5297  RRcr 5298  0cc0 5299   + caddc 5302   x. cmul 5304   <_ cle 5360  abscabs 6840  Idcgi 8119  CVeccvc 8248  NrmCVeccnv 8287  +vcpv 8288  Basecba 8289  .scns 8290  0vcn0v 8291  normcnm 8293

This theorem is referenced by:  nvabl 8319  nvsf 8322  nvscl 8331  nvsid 8332  nvsass 8333  nvdi 8335  nvdir 8336  nv2 8337  nv0 8342  nvsz 8343  nvinv 8344  nvoprne 8390  sm1cnilem 8431  ipid 8447  phop 8561  ip0i 8568  ipdirilem 8572  hlvc 8681

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1003  ax-gen 1004  ax-8 1005  ax-9 1006  ax-10 1007  ax-11 1008  ax-12 1009  ax-13 1010  ax-14 1011  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019  ax-9o 1164  ax-10o 1182  ax-16 1252  ax-11o 1260  ax-ext 1504  ax-sep 2758  ax-nul 2765  ax-pow 2798  ax-pr 2835  ax-un 2922

This theorem depends on definitions:  df-bi 154  df-or 231  df-an 232  df-3an 789  df-ex 1022  df-sb 1214  df-eu 1424  df-mo 1425  df-clab 1510  df-cleq 1515  df-clel 1518  df-ne 1634  df-ral 1696  df-rex 1697  df-rab 1699  df-v 1859  df-sbc 1989  df-dif 2100  df-un 2101  df-in 2102  df-ss 2104  df-nul 2332  df-pw 2454  df-sn 2464  df-pr 2465  df-op 2468  df-uni 2558  df-br 2675  df-opab 2722  df-id 2891  df-xp 3241  df-rel 3242  df-cnv 3243  df-co 3244  df-dm 3245  df-rn 3246  df-res 3247  df-ima 3248  df-fun 3249  df-fn 3250  df-f 3251  df-fo 3253  df-fv 3255  df-opr 4023  df-oprab 4024  df-1st 4137  df-2nd 4138  df-grp 8122  df-gid 8123  df-nv 8295  df-va 8298  df-ba 8299  df-sm 8300  df-0v 8301  df-nm 8303

Copyright terms: Public domain