Theorem minveclem21 8509

Description: Lemma for minvecex 8522.

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
minvec20.h	|- (j e. NN -> (H` j) = (AM(f` j)))
minvec20.f	|- (j e. NN -> (F` j) = (N` (H` j)))
minvec21.2	|- P = -usup(R, RR, < )

Assertion

Ref	Expression
minveclem21	|- (((f:NN-->Y /\ n e. NN) /\ (f:NN-->Y /\ m e. NN)) -> ((N` ((f` n)M(f` m)))^2) <_ ((2 x. (((F` n)^2) + ((F` m)^2))) - ((2 x. P)^2)))

Distinct variable groups:   f,j,m,x,y,A   m,n,x,y,j   j,F,m,n   j,H   f,n,M,j,m,x,y   f,N,j,m,n,x,y   P,f,j,m,n   x,U,y   x,W,y   f,Y,j,m,n,x,y

Proof of Theorem minveclem21

Step	Hyp	Ref	Expression
1		minvec20.f	. . . . . . . . 9 |- (j e. NN -> (F` j) = (N` (H` j)))
2	1	minveclem7 8495	. . . . . . . 8 |- (n e. NN -> (F` n) = (N` (H` n)))
3	2	opreq1d 3966	. . . . . . 7 |- (n e. NN -> ((F` n)^2) = ((N` (H` n))^2))
4	1	minveclem7 8495	. . . . . . . 8 |- (m e. NN -> (F` m) = (N` (H` m)))
5	4	opreq1d 3966	. . . . . . 7 |- (m e. NN -> ((F` m)^2) = ((N` (H` m))^2))
6	3, 5	opreqan12d 3970	. . . . . 6 |- ((n e. NN /\ m e. NN) -> (((F` n)^2) + ((F` m)^2)) = (((N` (H` n))^2) + ((N` (H` m))^2)))
7	6	opreq2d 3967	. . . . 5 |- ((n e. NN /\ m e. NN) -> (2 x. (((F` n)^2) + ((F` m)^2))) = (2 x. (((N` (H` n))^2) + ((N` (H` m))^2))))
8	7	opreq1d 3966	. . . 4 |- ((n e. NN /\ m e. NN) -> ((2 x. (((F` n)^2) + ((F` m)^2))) - ((N` ((H` n)(+v` U)(H` m)))^2)) = ((2 x. (((N` (H` n))^2) + ((N` (H` m))^2))) - ((N` ((H` n)(+v` U)(H` m)))^2)))
9	8	ad2ant2l 408	. . 3 |- (((f:NN-->Y /\ n e. NN) /\ (f:NN-->Y /\ m e. NN)) -> ((2 x. (((F` n)^2) + ((F` m)^2))) - ((N` ((H` n)(+v` U)(H` m)))^2)) = ((2 x. (((N` (H` n))^2) + ((N` (H` m))^2))) - ((N` ((H` n)(+v` U)(H` m)))^2)))
10		minvec10.1	. . . 4 |- R = {x | E.y e. Y x = -u(N` (AMy))}
11		minvec10.u	. . . 4 |- U e. CPreHil
12		minvec10.m	. . . 4 |- M = (-v` U)
13		minvec10.n	. . . 4 |- N = (norm` U)
14		minvec10.x	. . . 4 |- X = (Base` U)
15		minvec10.w1	. . . 4 |- W e. (SubSp` U)
16		minvec10.y	. . . 4 |- Y = (Base` W)
17		minvec10.a	. . . 4 |- A e. X
18		minvec20.h	. . . 4 |- (j e. NN -> (H` j) = (AM(f` j)))
19		eqid 1473	. . . 4 |- (+v` U) = (+v` U)
20	10, 11, 12, 13, 14, 15, 16, 17, 18, 19	minveclem18 8506	. . 3 |- (((f:NN-->Y /\ n e. NN) /\ (f:NN-->Y /\ m e. NN)) -> ((2 x. (((N` (H` n))^2) + ((N` (H` m))^2))) - ((N` ((H` n)(+v` U)(H` m)))^2)) = ((N` ((f` n)M(f` m)))^2))
21	9, 20	eqtr2d 1505	. 2 |- (((f:NN-->Y /\ n e. NN) /\ (f:NN-->Y /\ m e. NN)) -> ((N` ((f` n)M(f` m)))^2) = ((2 x. (((F` n)^2) + ((F` m)^2))) - ((N` ((H` n)(+v` U)(H` m)))^2)))
22		2re 5934	. . . . . 6 |- 2 e. RR
23		minvec21.2	. . . . . . 7 |- P = -usup(R, RR, < )
24	10, 11, 12, 13, 14, 15, 16, 17, 23	minveclem12 8500	. . . . . 6 |- P e. RR
25	22, 24	remulcl 5315	. . . . 5 |- (2 x. P) e. RR
26		0re 5420	. . . . . . 7 |- 0 e. RR
27		2pos 5944	. . . . . . 7 |- 0 < 2
28	26, 22, 27	ltlei 5562	. . . . . 6 |- 0 <_ 2
29	10, 11, 12, 13, 14, 15, 16, 17, 23	minveclem14 8502	. . . . . 6 |- 0 <_ P
30	22, 24	mulge0 5589	. . . . . 6 |- ((0 <_ 2 /\ 0 <_ P) -> 0 <_ (2 x. P))
31	28, 29, 30	mp2an 696	. . . . 5 |- 0 <_ (2 x. P)
32		le2sqit 6571	. . . . 5 |- ((((2 x. P) e. RR /\ 0 <_ (2 x. P)) /\ ((N` ((H` n)(+v` U)(H` m))) e. RR /\ (2 x. P) <_ (N` ((H` n)(+v` U)(H` m))))) -> ((2 x. P)^2) <_ ((N` ((H` n)(+v` U)(H` m)))^2))
33	25, 31, 32	mpanl12 707	. . . 4 |- (((N` ((H` n)(+v` U)(H` m))) e. RR /\ (2 x. P) <_ (N` ((H` n)(+v` U)(H` m)))) -> ((2 x. P)^2) <_ ((N` ((H` n)(+v` U)(H` m)))^2))
34	11	phnvi 8419	. . . . . . 7 |- U e. NrmCVec
35	14, 19	nvgcl 8191	. . . . . . 7 |- ((U e. NrmCVec /\ (H` n) e. X /\ (H` m) e. X) -> ((H` n)(+v` U)(H` m)) e. X)
36	34, 35	mp3an1 901	. . . . . 6 |- (((H` n) e. X /\ (H` m) e. X) -> ((H` n)(+v` U)(H` m)) e. X)
37	14, 13	nvcl 8239	. . . . . . 7 |- ((U e. NrmCVec /\ ((H` n)(+v` U)(H` m)) e. X) -> (N` ((H` n)(+v` U)(H` m))) e. RR)
38	34, 37	mpan 694	. . . . . 6 |- (((H` n)(+v` U)(H` m)) e. X -> (N` ((H` n)(+v` U)(H` m))) e. RR)
39	36, 38	syl 10	. . . . 5 |- (((H` n) e. X /\ (H` m) e. X) -> (N` ((H` n)(+v` U)(H` m))) e. RR)
40	10, 11, 12, 13, 14, 15, 16, 17, 18	minveclem17 8505	. . . . 5 |- ((f:NN-->Y /\ n e. NN) -> (H` n) e. X)
41	10, 11, 12, 13, 14, 15, 16, 17, 18	minveclem17 8505	. . . . 5 |- ((f:NN-->Y /\ m e. NN) -> (H` m) e. X)
42	39, 40, 41	syl2an 454	. . . 4 |- (((f:NN-->Y /\ n e. NN) /\ (f:NN-->Y /\ m e. NN)) -> (N` ((H` n)(+v` U)(H` m))) e. RR)
43		eqid 1473	. . . . 5 |- (.s` U) = (.s` U)
44	10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 43, 23	minveclem19 8507	. . . 4 |- (((f:NN-->Y /\ n e. NN) /\ (f:NN-->Y /\ m e. NN)) -> (2 x. P) <_ (N` ((H` n)(+v` U)(H` m))))
45	33, 42, 44	sylanc 471	. . 3 |- (((f:NN-->Y /\ n e. NN) /\ (f:NN-->Y /\ m e. NN)) -> ((2 x. P)^2) <_ ((N` ((H` n)(+v` U)(H` m)))^2))
46	25	resqcl 6562	. . . . 5 |- ((2 x. P)^2) e. RR
47		lesub2t 5642	. . . . 5 |- ((((2 x. P)^2) e. RR /\ ((N` ((H` n)(+v` U)(H` m)))^2) e. RR /\ (2 x. (((F` n)^2) + ((F` m)^2))) e. RR) -> (((2 x. P)^2) <_ ((N` ((H` n)(+v` U)(H` m)))^2) <-> ((2 x. (((F` n)^2) + ((F` m)^2))) - ((N` ((H` n)(+v` U)(H` m)))^2)) <_ ((2 x. (((F` n)^2) + ((F` m)^2))) - ((2 x. P)^2))))
48	46, 47	mp3an1 901	. . . 4 |- ((((N` ((H` n)(+v` U)(H` m)))^2) e. RR /\ (2 x. (