Theorem minveclem9 8549

Description: Lemma for minvecex 8574.

Hypotheses

Ref	Expression
minvec9.u	|- U e. CPreHil
minvec9.m	|- M = (-v` U)
minvec9.n	|- N = (norm` U)
minvec9.x	|- X = (Base` U)
minvec9.w1	|- W e. (SubSp` U)
minvec9.y	|- Y = (Base` W)
minvec9.d	|- D = (IndMet` W)
minvec9.j	|- J e. V
minvec9.k	|- (m e. NN -> (J` m) = (N` ((f` m)Ma)))

Assertion

Ref	Expression
minveclem9	|- (((f:NN-->Y /\ f(~~>m` D)a) /\ a e. Y) -> J ~~> 0)

Distinct variable groups:   D,m   m,J   m,Y   f,a,m

Proof of Theorem minveclem9

Step	Hyp	Ref	Expression
1		minvec9.u	. . . . . . . . . . 11 |- U e. CPreHil
2	1	phnvi 8471	. . . . . . . . . 10 |- U e. NrmCVec
3		minvec9.w1	. . . . . . . . . 10 |- W e. (SubSp` U)
4		eqid 1478	. . . . . . . . . . 11 |- (SubSp` U) = (SubSp` U)
5	4	sspnv 8381	. . . . . . . . . 10 |- ((U e. NrmCVec /\ W e. (SubSp` U)) -> W e. NrmCVec)
6	2, 3, 5	mp2an 699	. . . . . . . . 9 |- W e. NrmCVec
7		minvec9.d	. . . . . . . . . 10 |- D = (IndMet` W)
8	7	imsmet 8320	. . . . . . . . 9 |- (W e. NrmCVec -> D e. Met)
9	6, 8	ax-mp 7	. . . . . . . 8 |- D e. Met
10		minvec9.y	. . . . . . . . . 10 |- Y = (Base` W)
11	10, 7, 6	imsbai 8318	. . . . . . . . 9 |- Y = dom dom D
12		eqidd 1479	. . . . . . . . 9 |- (m e. NN -> (f` m) = (f` m))
13	11, 12	lmcvgnns 7940	. . . . . . . 8 |- (((D e. Met /\ a e. Y) /\ (f(~~>m` D)a /\ u e. RR+)) -> E.k e. NN A.m e. NN (k <_ m -> ((f` m)Da) < u))
14	9, 13	mpanl1 708	. . . . . . 7 |- ((a e. Y /\ (f(~~>m` D)a /\ u e. RR+)) -> E.k e. NN A.m e. NN (k <_ m -> ((f` m)Da) < u))
15	14	an1s 488	. . . . . 6 |- ((f(~~>m` D)a /\ (a e. Y /\ u e. RR+)) -> E.k e. NN A.m e. NN (k <_ m -> ((f` m)Da) < u))
16	15	anassrs 443	. . . . 5 |- (((f(~~>m` D)a /\ a e. Y) /\ u e. RR+) -> E.k e. NN A.m e. NN (k <_ m -> ((f` m)Da) < u))
17	16	adantlll 398	. . . 4 |- ((((f:NN-->Y /\ f(~~>m` D)a) /\ a e. Y) /\ u e. RR+) -> E.k e. NN A.m e. NN (k <_ m -> ((f` m)Da) < u))
18		eqid 1478	. . . . . . . . . . . . . . 15 |- (IndMet` U) = (IndMet` U)
19	10, 18, 7, 4	sspimsval 8395	. . . . . . . . . . . . . 14 |- (((U e. NrmCVec /\ W e. (SubSp` U)) /\ ((f` m) e. Y /\ a e. Y)) -> ((f` m)Da) = ((f` m)(IndMet` U)a))
20	2, 3, 19	mpanl12 710	. . . . . . . . . . . . 13 |- (((f` m) e. Y /\ a e. Y) -> ((f` m)Da) = ((f` m)(IndMet` U)a))
21		minvec9.x	. . . . . . . . . . . . . . . . 17 |- X = (Base` U)
22		minvec9.m	. . . . . . . . . . . . . . . . 17 |- M = (-v` U)
23		minvec9.n	. . . . . . . . . . . . . . . . 17 |- N = (norm` U)
24	21, 22, 23, 18	imsdval 8313	. . . . . . . . . . . . . . . 16 |- ((U e. NrmCVec /\ (f` m) e. X /\ a e. X) -> ((f` m)(IndMet` U)a) = (N` ((f` m)Ma)))
25	2, 24	mp3an1 905	. . . . . . . . . . . . . . 15 |- (((f` m) e. X /\ a e. X) -> ((f` m)(IndMet` U)a) = (N` ((f` m)Ma)))
26		absidt 6862	. . . . . . . . . . . . . . . 16 |- (((N` ((f` m)Ma)) e. RR /\ 0 <_ (N` ((f` m)Ma))) -> (abs` (N` ((f` m)Ma))) = (N` ((f` m)Ma)))
27	21, 22	nvmcl 8263	. . . . . . . . . . . . . . . . . 18 |- ((U e. NrmCVec /\ (f` m) e. X /\ a e. X) -> ((f` m)Ma) e. X)
28	2, 27	mp3an1 905	. . . . . . . . . . . . . . . . 17 |- (((f` m) e. X /\ a e. X) -> ((f` m)Ma) e. X)
29	21, 23	nvcl 8283	. . . . . . . . . . . . . . . . . 18 |- ((U e. NrmCVec /\ ((f` m)Ma) e. X) -> (N` ((f` m)Ma)) e. RR)
30	2, 29	mpan 697	. . . . . . . . . . . . . . . . 17 |- (((f` m)Ma) e. X -> (N` ((f` m)Ma)) e. RR)
31	28, 30	syl 10	. . . . . . . . . . . . . . . 16 |- (((f` m) e. X /\ a e. X) -> (N` ((f` m)Ma)) e. RR)
32	21, 23	nvge0 8298	. . . . . . . . . . . . . . . . . 18 |- ((U e. NrmCVec /\ ((f` m)Ma) e. X) -> 0 <_ (N` ((f` m)Ma)))
33	2, 32	mpan 697	. . . . . . . . . . . . . . . . 17 |- (((f` m)Ma) e. X -> 0 <_ (N` ((f` m)Ma)))
34	28, 33	syl 10	. . . . . . . . . . . . . . . 16 |- (((f` m) e. X /\ a e. X) -> 0 <_ (N` ((f` m)Ma)))
35	26, 31, 34	sylanc 473	. . . . . . . . . . . . . . 15 |- (((f` m) e. X /\ a e. X) -> (abs` (N` ((f` m)Ma))) = (N` ((f` m)Ma)))
36	25, 35	eqtr4d 1513	. . . . . . . . . . . . . 14 |- (((f` m) e. X /\ a e. X) -> ((f` m)(IndMet` U)a) = (abs` (N` ((f` m)Ma))))
37	1, 3, 10, 21	minveclem3 8543	. . . . . . . . . . . . . . 15 |- Y (_ X
38	37	sseli 2068	. . . . . . . . . . . . . 14 |- ((f` m) e. Y -> (f` m) e. X)
39	37	sseli 2068	. . . . . . . . . . . . . 14 |- (a e. Y -> a e. X)
40	36, 38, 39	syl2an 456	. . . . . . . . . . . . 13 |- (((f` m) e. Y /\ a e. Y) -> ((f` m)(IndMet` U)a) = (abs` (N` ((f` m)Ma))))
41	20, 40	eqtrd 1510	. . . . . . . . . . . 12 |- (((f` m) e. Y /\ a e. Y) -> ((f` m)Da) = (abs` (N` ((f` m)Ma))))
42		ffvelrn 3820	. . . . . . . . . . . 12 |- ((f:NN-->Y /\ m e. NN) -> (f` m) e. Y)
43	41, 42	sylan 450	. . . . . . . . . . 11 |- (((f:NN-->Y /\ m e. NN) /\ a e. Y) -> ((f` m)Da) = (abs` (N` ((f` m)Ma))))
44	43	an1rs 491	. . . . . . . . . 10 |- (((f:NN-->Y /\ a e. Y) /\ m e. NN) -> ((f` m)Da) = (abs` (N` ((f` m)Ma))))
45	44	breq1d 2634	. . . . . . . . 9 |- (((f:NN-->Y /\ a e. Y) /\ m e. NN) -> (((f` m)Da) < u <-> (abs` (N` ((f` m)Ma))) < u))
46	45	imbi2d 614	. . . . . . . 8 |- (((f:NN-->Y /\ a e. Y) /\ m e. NN) -> ((k <_ m -> ((f` m)Da) < u) <-> (k <_ m -> (abs` (N` ((f` m)Ma))) < u)))
47	46	ralbidva 1662	. . . . . . 7 |- ((f:NN-->Y /\ a e. Y) -> (A.m e. NN (k <_ m -> ((f` m)Da) < u) <-> A.m e. NN (k <_ m -> (abs` (N` ((f` m)Ma))) < u)))
48	47	rexbidv 1667	. . . . . 6 |- ((f:NN-->Y /\ a e. Y) -> (E.k e. NN A.m e. NN (k <_ m -> ((f` m)Da) < u) <-> E.k e. NN A.m e. NN (k <_ m -> (abs` (N` ((f` m)Ma))) < u)))
49	48	adantlr 395	. . . . 5 |- (((f:NN-->Y /\ f(~~>m` D)a) /\ a e. Y) -> (E.k e. NN A.m e. NN (k <_ m -> ((f` m)Da) < u) <-> E.k e. NN A.m e. NN (k <_ m -> (abs` (N` ((f` m)Ma))) < u)))
50	49	adantr 391	. . . 4 |- ((((f:NN-->Y /\ f(~~>m` D)a) /\ a e. Y) /\ u e. RR+) -> (E.k e. NN A.m e. NN (k <_ m -> ((f` m)Da) < u) <-> E.k e. NN A.m e. NN (k <_ m -> (abs` (N` ((f` m)Ma))) < u)))
51	17, 50	mpbid 195	. . 3 |- ((((f:NN-->Y /\ f(~~>m` D)a) /\ a e. Y) /\ u e. RR+) -> E.k e. NN A.m e. NN (k <_ m -> (abs` (N` ((f` m)Ma))) < u))
52	51	r19.21aiva 1717	. 2 |- (((f:NN-->Y /\ f(~~>m` D)a) /\ a e. Y) -> A.u e. RR+ E.k e. NN A.m e. NN (k <_ m -> (abs` (N` ((f` m)Ma))) < u))
53	31	recnd 5327	. . . . . . 7 |- (((f` m) e. X /\ a e. X) -> (N` ((f` m)Ma)) e. CC)
54	1, 3, 10, 21	minveclem4 8544	. . . . . . 7 |- ((f:NN-->Y /\ m e. NN) -> (f` m) e. X)
55	53, 54, 39	syl2an 456	. . . . . 6 |- (((f:NN-->Y /\ m e. NN) /\ a e. Y) -> (N` ((f` m)Ma)) e. CC)
56	55	an1rs 491	. . . . 5 |- (((f:NN-->Y /\ a e. Y) /\ m e. NN) -> (N` ((f` m)Ma)) e. CC