HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem minveclem30 8570
Description: Lemma for minvecex 8574.
Hypotheses
Ref Expression
minvec10.1 |- R = {x | E.y e. Y x = -u(N` (AMy))}
minvec10.u |- U e. CPreHil
minvec10.m |- M = (-v` U)
minvec10.n |- N = (norm` U)
minvec10.x |- X = (Base` U)
minvec10.w1 |- W e. (SubSp` U)
minvec10.y |- Y = (Base` W)
minvec10.a |- A e. X
minvec30.2 |- P = -usup(R, RR, < )
minvec30.hf |- (j e. NN -> (F` j) = (N` (AM(f` j))))
minvec30.d |- D = (IndMet` W)
minvec30.jv |- J e. V
minvec30.j |- (m e. NN -> (J` m) = (N` ((f` m)Ma)))
minvec30.fv |- F e. V
minvec30.tv |- T e. V
minvec30.t |- (m e. NN -> (T` m) = ((F` m) + (N` ((f` m)Ma))))
Assertion
Ref Expression
minveclem30 |- (((f:NN-->Y /\ f(~~>m` D)a) /\ (F ~~> P /\ a e. Y)) -> T ~~> P)
Distinct variable groups:   f,j,m,x,y,A   m,a,D   j,a,F,m   f,M,j,m,x,y   f,N,j,m,x,y   f,a,P,j,m   R,a   x,U,y   x,W,y   x,a,y,Y,f,j,m   m,J   T,m
Proof of Theorem minveclem30
StepHypRef Expression
1 1z 6161 . . . . 5 |- 1 e. ZZ
2 minvec30.fv . . . . . 6 |- F e. V
3 minvec30.jv . . . . . 6 |- J e. V
4 minvec30.tv . . . . . 6 |- T e. V
5 minvec10.1 . . . . . . . 8 |- R = {x | E.y e. Y x = -u(N` (AMy))}
6 minvec10.u . . . . . . . 8 |- U e. CPreHil
7 minvec10.m . . . . . . . 8 |- M = (-v` U)
8 minvec10.n . . . . . . . 8 |- N = (norm` U)
9 minvec10.x . . . . . . . 8 |- X = (Base` U)
10 minvec10.w1 . . . . . . . 8 |- W e. (SubSp` U)
11 minvec10.y . . . . . . . 8 |- Y = (Base` W)
12 minvec10.a . . . . . . . 8 |- A e. X
13 minvec30.2 . . . . . . . 8 |- P = -usup(R, RR, < )
145, 6, 7, 8, 9, 10, 11, 12, 13minveclem12 8552 . . . . . . 7 |- P e. RR
1514elisseti 1821 . . . . . 6 |- P e. V
16 0cn 5340 . . . . . . 7 |- 0 e. CC
1716elisseti 1821 . . . . . 6 |- 0 e. V
182, 3, 4, 15, 17climadd 7117 . . . . 5 |- (((F ~~> P /\ J ~~> 0) /\ (1 e. ZZ /\ A.m e. (ZZ>` 1)((F` m) e. CC /\ (J` m) e. CC /\ (T` m) = ((F` m) + (J` m))))) -> T ~~> (P + 0))
191, 18mpanr1 711 . . . 4 |- (((F ~~> P /\ J ~~> 0) /\ A.m e. (ZZ>` 1)((F` m) e. CC /\ (J` m) e. CC /\ (T` m) = ((F` m) + (J` m)))) -> T ~~> (P + 0))
20 nnuz 6440 . . . . 5 |- NN = (ZZ>` 1)
21 raleq1 1789 . . . . 5 |- (NN = (ZZ>` 1) -> (A.m e. NN ((F` m) e. CC /\ (J` m) e. CC /\ (T` m) = ((F` m) + (J` m))) <-> A.m e. (ZZ>` 1)((F` m) e. CC /\ (J` m) e. CC /\ (T` m) = ((F` m) + (J` m)))))
2220, 21ax-mp 7 . . . 4 |- (A.m e. NN ((F` m) e. CC /\ (J` m) e. CC /\ (T` m) = ((F` m) + (J` m))) <-> A.m e. (ZZ>` 1)((F` m) e. CC /\ (J` m) e. CC /\ (T` m) = ((F` m) + (J` m))))
2319, 22sylan2b 454 . . 3 |- (((F ~~> P /\ J ~~> 0) /\ A.m e. NN ((F` m) e. CC /\ (J` m) e. CC /\ (T` m) = ((F` m) + (J` m)))) -> T ~~> (P + 0))
24 simprl 416 . . . 4 |- (((f:NN-->Y /\ f(~~>m` D)a) /\ (F ~~> P /\ a e. Y)) -> F ~~> P)
25 minvec30.d . . . . . 6 |- D = (IndMet` W)
26 minvec30.j . . . . . 6 |- (m e. NN -> (J` m) = (N` ((f` m)Ma)))
276, 7, 8, 9, 10, 11, 25, 3, 26minveclem9 8549 . . . . 5 |- (((f:NN-->Y /\ f(~~>m` D)a) /\ a e. Y) -> J ~~> 0)
2827adantrl 396 . . . 4 |- (((f:NN-->Y /\ f(~~>m` D)a) /\ (F ~~> P /\ a e. Y)) -> J ~~> 0)
2924, 28jca 288 . . 3 |- (((f:NN-->Y /\ f(~~>m` D)a) /\ (F ~~> P /\ a e. Y)) -> (F ~~> P /\ J ~~> 0))
30 minvec30.hf . . . . . . . . 9 |- (j e. NN -> (F` j) = (N` (AM(f` j))))
315, 6, 7, 8, 9, 10, 11, 12, 30minveclem22 8562 . . . . . . . 8 |- ((f:NN-->Y /\ m e. NN) -> (F` m) e. RR)
3231recnd 5327 . . . . . . 7 |- ((f:NN-->Y /\ m e. NN) -> (F` m) e. CC)
3332adantlr 395 . . . . . 6 |- (((f:NN-->Y /\ f(~~>m` D)a) /\ m e. NN) -> (F` m) e. CC)
3433adantlr 395 . . . . 5 |- ((((f:NN-->Y /\ f(~~>m` D)a) /\ (F ~~> P /\ a e. Y)) /\ m e. NN) -> (F` m) e. CC)
3526adantl 390 . . . . . . . . 9 |- (((f:NN-->Y /\ a e. Y) /\ m e. NN) -> (J` m) = (N` ((f` m)Ma)))
366phnvi 8471 . . . . . . . . . . . . 13 |- U e. NrmCVec
379, 7nvmcl 8263 . . . . . . . . . . . . 13 |- ((U e. NrmCVec /\ (f` m) e. X /\ a e. X) -> ((f` m)Ma) e. X)
3836, 37mp3an1 905 . . . . . . . . . . . 12 |- (((f` m) e. X /\ a e. X) -> ((f` m)Ma) e. X)
399, 8nvcl 8283 . . . . . . . . . . . . 13 |- ((U e. NrmCVec /\ ((f` m)Ma) e. X) -> (N` ((f` m)Ma)) e. RR)
4036, 39mpan 697 . . . . . . . . . . . 12 |- (((f` m)Ma) e. X -> (N` ((f` m)Ma)) e. RR)
4138, 40syl 10 . . . . . . . . . . 11 |- (((f` m) e. X /\ a e. X) -> (N` ((f` m)Ma)) e. RR)
426, 10, 11, 9minveclem4 8544 . . . . . . . . . . 11 |- ((f:NN-->Y /\ m e. NN) -> (f` m) e. X)
436, 10, 11, 9minveclem3 8543 . . . . . . . . . . . 12 |- Y (_ X
4443sseli 2068 . . . . . . . . . . 11 |- (a e. Y -> a e. X)
4541, 42, 44syl2an 456 . . . . . . . . . 10 |- (((f:NN-->Y /\ m e. NN) /\ a e. Y) -> (N` ((f` m)Ma)) e. RR)
4645an1rs 491 . . . . . . . . 9 |- (((f:NN-->Y /\ a e. Y) /\ m e. NN) -> (N` ((f` m)Ma)) e. RR)
4735, 46eqeltrd 1551 . . . . . . . 8 |- (((f:NN-->Y /\ a e. Y) /\ m e. NN) -> (J` m) e. RR)
4847recnd 5327 . . . . . . 7 |- (((f:NN-->Y /\ a e. Y) /\ m e. NN) -> (J` m) e. CC)
4948adantllr 399 . . . . . 6 |- ((((f:NN-->Y /\ f(~~>m` D)a) /\ a e. Y) /\ m e. NN) -> (J` m) e. CC)
5049adantlrl 400 . . . . 5 |- ((((f:NN-->Y /\ f(~~>m` D)a) /\ (F ~~> P /\ a e. Y)) /\ m e. NN) -> (J` m) e. CC)
51 minvec30.t . . . . . . 7 |- (m e. NN -> (T` m) = ((F` m) + (N` ((f` m)Ma))))
5226opreq2d 3982 . . . . . . 7 |- (m e. NN -> ((F` m) + (J` m)) = ((F` m) + (N` ((f` m)Ma))))
5351, 52eqtr4d 1513 . . . . . 6 |- (m e. NN -> (T` m) = ((F` m) + (J` m)))
5453adantl 390 . . . . 5 |- ((((f:NN-->Y /\ f(~~>m` D)a) /\ (F ~~> P /\ a e. Y)) /\ m e. NN) -> (T` m) = ((F` m) + (J` m)))
5534, 50, 543jca 821 . . . 4 |- ((((f:NN-->Y /\ f(~~>m` D)a) /\ (F ~~> P /\ a e. Y)) /\ m e. NN) -> ((F` m) e. CC /\ (J` m) e. CC /\ (T` m) = ((F` m) + (J` m))))
5655r19.21aiva 1717 . . 3 |- (((f:NN-->Y /\ f(~~>m` D)a) /\ (F ~~> P /\ a e. Y)) -> A.m e. NN ((F` m) e. CC /\ (J` m) e. CC /\ (T` m) = ((F` m) + (J` m))))
5723, 29, 56sylanc 473 . 2 |- (((f:NN-->Y /\ f(~~>m` D)a) /\ (F ~~> P /\ a e. Y)) -> T ~~> (P + 0))
5814recn 5326 . . 3 |- P e. CC
5958addid1 5342 . 2 |- (P + 0) = P
6057, 59syl6breq 2659 1 |- (((f:NN-->Y /\ f(~~>m` D)a) /\ (F ~~> P /\ a e. Y)) -> T ~~> P)
Colors of variables: wff set class
Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   /\ w3a 777   = wceq 958   e. wcel 960  {cab 1466  A.wral 1648  E.wrex 1649  Vcvv 1814   class class class wbr 2624  -->wf 3184  ` cfv 3188  (class class class)co 3969  supcsup 4582  CCcc 5244  RRcr 5245  0cc0 5246  1c1 5247   + caddc 5249  -ucneg 5305  NNcn 5308  ZZcz 5310   < clt 5498  ZZ>cuz 6418   ~~> cli 6974  ~~>mclm 7916  NrmCVeccnv 8199  Basecba 8201  -vcnsb 8204  normcnm 8205  IndMetcims 8206  SubSpcss 8376  CPreHilcphl 8467
This theorem is referenced by:  minveclem31 8571