Theorem minveclem38 8513

Description: Lemma for minveceu 8514.

Hypotheses

Ref	Expression
minvec35.x	|- X = (Base` U)
minvec35.g	|- G = (+v` U)
minvec35.m	|- M = (-v` U)
minvec35.s	|- S = (.s` U)
minvec35.n	|- N = (norm` U)
minvec35.y	|- Y = (Base` W)
minvec35.u	|- U e. CPreHil
minvec35.a	|- A e. X
minvec36.w	|- W e. (SubSp` U)
minvec36.2	|- P = -usup(R, RR, < )
minvec36.1	|- R = {x | E.y e. Y x = -u(N` (AMy))}

Assertion

Ref	Expression
minveclem38	|- (((a e. Y /\ b e. Y) /\ ((N` (AMa)) = P /\ (N` (AMb)) = P)) -> (N` (aMb)) <_ 0)

Distinct variable groups:   x,y,A   x,G,y   x,M,y   x,N,y   x,S,y   x,U,y   x,W,y   x,Y,y   a,b,x,y

Proof of Theorem minveclem38

Step	Hyp	Ref	Expression
1		minvec35.x	. . . . . 6 |- X = (Base` U)
2		minvec35.g	. . . . . 6 |- G = (+v` U)
3		minvec35.m	. . . . . 6 |- M = (-v` U)
4		minvec35.s	. . . . . 6 |- S = (.s` U)
5		minvec35.n	. . . . . 6 |- N = (norm` U)
6		minvec35.y	. . . . . 6 |- Y = (Base` W)
7		minvec35.u	. . . . . 6 |- U e. CPreHil
8		minvec35.a	. . . . . 6 |- A e. X
9		minvec36.w	. . . . . 6 |- W e. (SubSp` U)
10		minvec36.2	. . . . . 6 |- P = -usup(R, RR, < )
11		minvec36.1	. . . . . 6 |- R = {x | E.y e. Y x = -u(N` (AMy))}
12	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11	minveclem36 8511	. . . . 5 |- (((a e. X /\ b e. X) /\ ((N` (AMa)) = P /\ (N` (AMb)) = P)) -> ((N` (aMb))^2) = ((2 x. ((P^2) + (P^2))) - ((N` ((AMa)G(AMb)))^2)))
13	7, 9, 6, 1	minveclem3 8478	. . . . . . 7 |- Y (_ X
14	13	sseli 2055	. . . . . 6 |- (a e. Y -> a e. X)
15	13	sseli 2055	. . . . . 6 |- (b e. Y -> b e. X)
16	14, 15	anim12i 333	. . . . 5 |- ((a e. Y /\ b e. Y) -> (a e. X /\ b e. X))
17	12, 16	sylan 448	. . . 4 |- (((a e. Y /\ b e. Y) /\ ((N` (AMa)) = P /\ (N` (AMb)) = P)) -> ((N` (aMb))^2) = ((2 x. ((P^2) + (P^2))) - ((N` ((AMa)G(AMb)))^2)))
18	11, 7, 3, 5, 1, 9, 6, 8, 10	minveclem12 8487	. . . . . . . . . . 11 |- P e. RR
19	18	resqcl 6554	. . . . . . . . . 10 |- (P^2) e. RR
20		4re 5929	. . . . . . . . . . . 12 |- 4 e. RR
21		0re 5412	. . . . . . . . . . . . 13 |- 0 e. RR
22		4pos 5939	. . . . . . . . . . . . 13 |- 0 < 4
23	21, 20, 22	ltlei 5554	. . . . . . . . . . . 12 |- 0 <_ 4
24	20, 23	pm3.2i 285	. . . . . . . . . . 11 |- (4 e. RR /\ 0 <_ 4)
25		lemul2it 5795	. . . . . . . . . . 11 |- ((((P^2) e. RR /\ ((N` (AM((1 / 2)S(aGb))))^2) e. RR /\ (4 e. RR /\ 0 <_ 4)) /\ (P^2) <_ ((N` (AM((1 / 2)S(aGb))))^2)) -> (4 x. (P^2)) <_ (4 x. ((N` (AM((1 / 2)S(aGb))))^2)))
26	24, 25	mp3anl3 909	. . . . . . . . . 10 |- ((((P^2) e. RR /\ ((N` (AM((1 / 2)S(aGb))))^2) e. RR) /\ (P^2) <_ ((N` (AM((1 / 2)S(aGb))))^2)) -> (4 x. (P^2)) <_ (4 x. ((N` (AM((1 / 2)S(aGb))))^2)))
27	19, 26	mpanl1 704	. . . . . . . . 9 |- ((((N` (AM((1 / 2)S(aGb))))^2) e. RR /\ (P^2) <_ ((N` (AM((1 / 2)S(aGb))))^2)) -> (4 x. (P^2)) <_ (4 x. ((N` (AM((1 / 2)S(aGb))))^2)))
28	7	phnvi 8406	. . . . . . . . . . . . . . 15 |- U e. NrmCVec
29	1, 2	nvgcl 8179	. . . . . . . . . . . . . . 15 |- ((U e. NrmCVec /\ a e. X /\ b e. X) -> (aGb) e. X)
30	28, 29	mp3an1 900	. . . . . . . . . . . . . 14 |- ((a e. X /\ b e. X) -> (aGb) e. X)
31	30, 14, 15	syl2an 454	. . . . . . . . . . . . 13 |- ((a e. Y /\ b e. Y) -> (aGb) e. X)
32		2cn 5927	. . . . . . . . . . . . . . 15 |- 2 e. CC
33		2ne0 5937	. . . . . . . . . . . . . . 15 |- 2 =/= 0
34	32, 33	reccl 5682	. . . . . . . . . . . . . 14 |- (1 / 2) e. CC
35	1, 4	nvscl 8187	. . . . . . . . . . . . . 14 |- ((U e. NrmCVec /\ (1 / 2) e. CC /\ (aGb) e. X) -> ((1 / 2)S(aGb)) e. X)
36	28, 34, 35	mp3an12 903	. . . . . . . . . . . . 13 |- ((aGb) e. X -> ((1 / 2)S(aGb)) e. X)
37	31, 36	syl 10	. . . . . . . . . . . 12 |- ((a e. Y /\ b e. Y) -> ((1 / 2)S(aGb)) e. X)
38	1, 3	nvmcl 8207	. . . . . . . . . . . . 13 |- ((U e. NrmCVec /\ A e. X /\ ((1 / 2)S(aGb)) e. X) -> (AM((1 / 2)S(aGb))) e. X)
39	28, 8, 38	mp3an12 903	. . . . . . . . . . . 12 |- (((1 / 2)S(aGb)) e. X -> (AM((1 / 2)S(aGb))) e. X)
40	37, 39	syl 10	. . . . . . . . . . 11 |- ((a e. Y /\ b e. Y) -> (AM((1 / 2)S(aGb))) e. X)
41	1, 5	nvcl 8227	. . . . . . . . . . . 12 |- ((U e. NrmCVec /\ (AM((1 / 2)S(aGb))) e. X) -> (N` (AM((1 / 2)S(aGb)))) e. RR)
42	28, 41	mpan 693	. . . . . . . . . . 11 |- ((AM((1 / 2)S(aGb))) e. X -> (N` (AM((1 / 2)S(aGb)))) e. RR)
43	40, 42	syl 10	. . . . . . . . . 10 |- ((a e. Y /\ b e. Y) -> (N` (AM((1 / 2)S(aGb)))) e. RR)
44		resqclt 6552	. . . . . . . . . 10 |- ((N` (AM((1 / 2)S(aGb)))) e. RR -> ((N` (AM((1 / 2)S(aGb))))^2) e. RR)
45	43, 44	syl 10	. . . . . . . . 9 |- ((a e. Y /\ b e. Y) -> ((N` (AM((1 / 2)S(aGb))))^2) e. RR)
46	11, 7, 3, 5, 1, 9, 6, 8, 10	minveclem14 8489	. . . . . . . . . . 11 |- 0 <_ P
47		le2sqit 6563	. . . . . . . . . . 11 |- (((P e. RR /\ 0 <_ P) /\ ((N` (AM((1 / 2)S(aGb)))) e. RR /\ P <_ (N` (AM((1 / 2)S(aGb)))))) -> (P^2) <_ ((N` (AM((1 / 2)S(aGb))))^2))
48	18, 46, 47	mpanl12 706	. . . . . . . . . 10 |- (((N` (AM((1 / 2)S(aGb)))) e. RR /\ P <_ (N` (AM((1 / 2)S(aGb))))) -> (P^2) <_ ((N` (AM((1 / 2)S(aGb))))^2))
49	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11	minveclem37 8512	. . . . . . . . . 10 |- ((a e. Y /\ b e. Y) -> P <_ (N` (AM((1 / 2)S(aGb)))))
50	48, 43, 49	sylanc 471	. . . . . . . . 9 |- ((a e. Y /\ b e. Y) -> (P^2) <_ ((N` (AM((1 / 2)S(aGb))))^2))
51	27, 45, 50	sylanc 471	. . . . . . . 8 |- ((a e. Y /\ b e. Y) -> (4 x. (P^2)) <_ (4 x. ((N` (AM((1 / 2)S(aGb))))^2)))
52	19	recn 5286	. . . . . . . . . 10 |- (P^2) e. CC
53	32, 32, 52	mulass 5297	. . . . . . . . 9 |- ((2 x. 2) x. (P^2)) = (2 x. (2 x. (P^2)))
54		2t2e4 5969	. . . . . . . . . 10 |- (2 x. 2) = 4
55	54	opreq1i 3956	. . . . . . . . 9 |- ((2 x. 2) x. (P^2)) = (4 x. (P^2))
56	52	2times 5950	. . . . . . . . . 10 |- (2 x. (P^2)) = ((P^2) + (P^2))
57	56	opreq2i 3957	. . . . . . . . 9 |- (2 x. (2 x. (P^2))) = (2 x. ((P^2) + (P^2)))
58	53, 55, 57	3eqtr3r 1496	. . . . . . . 8 |- (2 x. ((P^2) + (P^2))) = (4 x. (P^2))
59	51, 58	syl5eqbr 2638	. . . . . . 7 |- ((a e. Y /\ b e. Y) -> (2 x. ((P^2) + (P^2))) <_ (4 x. ((N` (AM((1 / 2)S(aGb))))^2)))
60	43	recnd 5287	. . . . . . . . . 10 |- ((a e. Y /\ b e. Y) -> (N` (AM((1 / 2)S(aGb)))) e. CC)
61		sqmult 6543	. . . . . . . . . . 11 |- ((2 e. CC /\ (N` (AM((1 / 2)S(aGb)))) e. CC) -> ((2 x. (N` (AM((1 / 2)S(aGb)))))^2) = ((2^2) x. ((N` (