Theorem minveclem16 8491

Description: Lemma for minvecex 8509.

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
minvec12.2	|- P = -usup(R, RR, < )
minvec16.g	|- G = (+v` U)
minvec16.s	|- S = (.s` U)

Assertion

Ref	Expression
minveclem16	|- (((f:NN-->Y /\ n e. NN) /\ (f:NN-->Y /\ m e. NN)) -> (2 x. P) <_ (N` (2S(AM((1 / 2)S((f` n)G(f` m)))))))

Distinct variable groups:   f,m,x,y,A   m,n,x,y   x,G,y   f,n,M,m,x,y   f,N,m,n,x,y   P,f,m,n   x,S,y   x,U,y   x,W,y   f,Y,m,n,x,y

Proof of Theorem minveclem16

Step	Hyp	Ref	Expression
1		minvec10.u	. . . . . 6 |- U e. CPreHil
2	1	phnvi 8406	. . . . 5 |- U e. NrmCVec
3		minvec10.w1	. . . . 5 |- W e. (SubSp` U)
4		minvec10.y	. . . . . 6 |- Y = (Base` W)
5		minvec16.g	. . . . . 6 |- G = (+v` U)
6		eqid 1468	. . . . . 6 |- (+v` W) = (+v` W)
7		eqid 1468	. . . . . 6 |- (SubSp` U) = (SubSp` U)
8	4, 5, 6, 7	sspgval 8322	. . . . 5 |- (((U e. NrmCVec /\ W e. (SubSp` U)) /\ ((f` n) e. Y /\ (f` m) e. Y)) -> ((f` n)(+v` W)(f` m)) = ((f` n)G(f` m)))
9	2, 3, 8	mpanl12 706	. . . 4 |- (((f` n) e. Y /\ (f` m) e. Y) -> ((f` n)(+v` W)(f` m)) = ((f` n)G(f` m)))
10	1, 3	minveclem1 8476	. . . . 5 |- W e. NrmCVec
11	4, 6	nvgcl 8179	. . . . 5 |- ((W e. NrmCVec /\ (f` n) e. Y /\ (f` m) e. Y) -> ((f` n)(+v` W)(f` m)) e. Y)
12	10, 11	mp3an1 900	. . . 4 |- (((f` n) e. Y /\ (f` m) e. Y) -> ((f` n)(+v` W)(f` m)) e. Y)
13	9, 12	eqeltrrd 1541	. . 3 |- (((f` n) e. Y /\ (f` m) e. Y) -> ((f` n)G(f` m)) e. Y)
14		2cn 5927	. . . . . . . 8 |- 2 e. CC
15		2ne0 5937	. . . . . . . 8 |- 2 =/= 0
16	14, 15	reccl 5682	. . . . . . 7 |- (1 / 2) e. CC
17		minvec16.s	. . . . . . . . 9 |- S = (.s` U)
18		eqid 1468	. . . . . . . . 9 |- (.s` W) = (.s` W)
19	4, 17, 18, 7	sspsval 8324	. . . . . . . 8 |- (((U e. NrmCVec /\ W e. (SubSp` U)) /\ ((1 / 2) e. CC /\ ((f` n)G(f` m)) e. Y)) -> ((1 / 2)(.s` W)((f` n)G(f` m))) = ((1 / 2)S((f` n)G(f` m))))
20	2, 3, 19	mpanl12 706	. . . . . . 7 |- (((1 / 2) e. CC /\ ((f` n)G(f` m)) e. Y) -> ((1 / 2)(.s` W)((f` n)G(f` m))) = ((1 / 2)S((f` n)G(f` m))))
21	16, 20	mpan 693	. . . . . 6 |- (((f` n)G(f` m)) e. Y -> ((1 / 2)(.s` W)((f` n)G(f` m))) = ((1 / 2)S((f` n)G(f` m))))
22	4, 18	nvscl 8187	. . . . . . 7 |- ((W e. NrmCVec /\ (1 / 2) e. CC /\ ((f` n)G(f` m)) e. Y) -> ((1 / 2)(.s` W)((f` n)G(f` m))) e. Y)
23	10, 16, 22	mp3an12 903	. . . . . 6 |- (((f` n)G(f` m)) e. Y -> ((1 / 2)(.s` W)((f` n)G(f` m))) e. Y)
24	21, 23	eqeltrrd 1541	. . . . 5 |- (((f` n)G(f` m)) e. Y -> ((1 / 2)S((f` n)G(f` m))) e. Y)
25		minvec10.1	. . . . . . . 8 |- R = {x | E.y e. Y x = -u(N` (AMy))}
26		minvec10.m	. . . . . . . 8 |- M = (-v` U)
27		minvec10.n	. . . . . . . 8 |- N = (norm` U)
28		minvec10.x	. . . . . . . 8 |- X = (Base` U)
29		minvec10.a	. . . . . . . 8 |- A e. X
30		minvec12.2	. . . . . . . 8 |- P = -usup(R, RR, < )
31	25, 1, 26, 27, 28, 3, 4, 29, 30	minveclem12 8487	. . . . . . 7 |- P e. RR
32		2re 5926	. . . . . . . . 9 |- 2 e. RR
33		0re 5412	. . . . . . . . . 10 |- 0 e. RR
34		2pos 5936	. . . . . . . . . 10 |- 0 < 2
35	33, 32, 34	ltlei 5554	. . . . . . . . 9 |- 0 <_ 2
36	32, 35	pm3.2i 285	. . . . . . . 8 |- (2 e. RR /\ 0 <_ 2)
37		lemul2it 5795	. . . . . . . 8 |- (((P e. RR /\ (N` (AM((1 / 2)S((f` n)G(f` m))))) e. RR /\ (2 e. RR /\ 0 <_ 2)) /\ P <_ (N` (AM((1 / 2)S((f` n)G(f` m)))))) -> (2 x. P) <_ (2 x. (N` (AM((1 / 2)S((f` n)G(f` m)))))))
38	36, 37	mp3anl3 909	. . . . . . 7 |- (((P e. RR /\ (N` (AM((1 / 2)S((f` n)G(f` m))))) e. RR) /\ P <_ (N` (AM((1 / 2)S((f` n)G(f` m)))))) -> (2 x. P) <_ (2 x. (N` (AM((1 / 2)S((f` n)G(f` m)))))))
39	31, 38	mpanl1 704	. . . . . 6 |- (((N` (AM((1 / 2)S((f` n)G(f` m))))) e. RR /\ P <_ (N` (AM((1 / 2)S((f` n)G(f` m)))))) -> (2 x. P) <_ (2 x. (N` (AM((1 / 2)S((f` n)G(f` m)))))))
40	1, 3, 4, 28	minveclem3 8478	. . . . . . . . 9 |- Y (_ X
41	40	sseli 2055	. . . . . . . 8 |- (((1 / 2)S((f` n)G(f` m))) e. Y -> ((1 / 2)S((f` n)G(f` m))) e. X)
42	28, 26	nvmcl 8207	. . . . . . . . 9 |- ((U e. NrmCVec /\ A e. X /\ ((1 / 2)S((f` n)G(f` m))) e. X) -> (AM((1 / 2)S((f` n)G(f` m)))) e. X)
43	2, 29, 42	mp3an12 903	. . . . . . . 8 |- (((1 / 2)S((f` n)G(f` m))) e. X -> (AM((1 / 2)S((f` n)G(f` m)))) e. X)
44	41, 43	syl 10	. . . . . . 7 |- (((1 / 2)S((f` n)G(f` m))) e. Y -> (AM((1 / 2)S((f` n)G(f` m)))) e. X)
45	28, 27	nvcl 8227	. . . . . . . 8 |- ((U e. NrmCVec /\ (AM((1 / 2)S((f` n)G(f` m)))) e. X) -> (N` (AM((1 / 2)S((f` n)G(f` m))))) e. RR)
46	2, 45	mpan 693	. . . . . . 7 |- ((AM((1 / 2)S((f` n)G(f` m)))) e. X -> (N` (AM((1 / 2)S((f` n)G(f` m))))) e. RR)
47	44, 46	syl 10	. . . . . 6 |- (((1 / 2)S((f` n)G(f` m))) e. Y -> (N` (AM((1 / 2)S((f` n)G(f` m))))) e. RR)
48	25, 1, 26, 27, 28, 3, 4, 29, 30	minveclem13 8488	. . . . . 6 |- (((1 / 2)S((f` n)G(f` m))) e. Y -> P <_ (N` (AM((1 / 2)S((f` n)G(f` m))))))
49	39, 47, 48	sylanc 471	. . . . 5 |- (((1 / 2)S((f` n)G(f` m))) e. Y -> (2 x. P) <_ (2 x. (N` (AM((1 / 2)S((f` n)G(f` m)))))))
50	24, 49	syl 10	. . . 4 |- (((f` n)G(f` m)) e. Y -> (2 x. P) <_ (2 x. (N` (AM((1 / 2)S((f` n)G(f` m)))))))
51	40	sseli 2055	. . . . 5 |- (((f` n)G(f` m)) e. Y -> ((f` n)G(f` m)) e. X)
52	28, 17	nvscl 8187	. . . . . . . 8 |- ((U e. NrmCVec /\ (1 / 2) e. CC /\ ((f` n)G(f` m)) e. X) -> ((1 / 2)S((f` n)G(f` m))) e. X)
53	2, 16, 52	mp3an12 903	. . . . . . 7 |- (((f` n)G(f` m)) e. X -> ((1 / 2)S((f` n)G(f` m))) e. X)
54	53, 43