Theorem minveclem19 8563

Description: Lemma for minvecex 8578.

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
minvec17.h	|- (j e. NN -> (H` j) = (AM(f` j)))
minvec18.g	|- G = (+v` U)
minvec19.s	|- S = (.s` U)
minvec19.2	|- P = -usup(R, RR, < )

Assertion

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

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

Proof of Theorem minveclem19

Step	Hyp	Ref	Expression
1		minvec10.1	. . 3 |- R = {x | E.y e. Y x = -u(N` (AMy))}
2		minvec10.u	. . 3 |- U e. CPreHil
3		minvec10.m	. . 3 |- M = (-v` U)
4		minvec10.n	. . 3 |- N = (norm` U)
5		minvec10.x	. . 3 |- X = (Base` U)
6		minvec10.w1	. . 3 |- W e. (SubSp` U)
7		minvec10.y	. . 3 |- Y = (Base` W)
8		minvec10.a	. . 3 |- A e. X
9		minvec19.2	. . 3 |- P = -usup(R, RR, < )
10		minvec18.g	. . 3 |- G = (+v` U)
11		minvec19.s	. . 3 |- S = (.s` U)
12	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11	minveclem16 8560	. 2 |- (((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)))))))
13		minvec17.h	. . . . . . . . 9 |- (j e. NN -> (H` j) = (AM(f` j)))
14	13	minveclem6 8550	. . . . . . . 8 |- (n e. NN -> (H` n) = (AM(f` n)))
15	13	minveclem6 8550	. . . . . . . 8 |- (m e. NN -> (H` m) = (AM(f` m)))
16	14, 15	opreqan12d 3979	. . . . . . 7 |- ((n e. NN /\ m e. NN) -> ((H` n)G(H` m)) = ((AM(f` n))G(AM(f` m))))
17	16	ad2ant2l 408	. . . . . 6 |- (((f:NN-->Y /\ n e. NN) /\ (f:NN-->Y /\ m e. NN)) -> ((H` n)G(H` m)) = ((AM(f` n))G(AM(f` m))))
18	2	phnvi 8475	. . . . . . . 8 |- U e. NrmCVec
19	8, 8	pm3.2i 285	. . . . . . . 8 |- (A e. X /\ A e. X)
20	5, 10, 3	nvaddsub4 8281	. . . . . . . 8 |- ((U e. NrmCVec /\ (A e. X /\ A e. X) /\ ((f` n) e. X /\ (f` m) e. X)) -> ((AGA)M((f` n)G(f` m))) = ((AM(f` n))G(AM(f` m))))
21	18, 19, 20	mp3an12 906	. . . . . . 7 |- (((f` n) e. X /\ (f` m) e. X) -> ((AGA)M((f` n)G(f` m))) = ((AM(f` n))G(AM(f` m))))
22	2, 6, 7, 5	minveclem4 8548	. . . . . . 7 |- ((f:NN-->Y /\ n e. NN) -> (f` n) e. X)
23	2, 6, 7, 5	minveclem4 8548	. . . . . . 7 |- ((f:NN-->Y /\ m e. NN) -> (f` m) e. X)
24	21, 22, 23	syl2an 454	. . . . . 6 |- (((f:NN-->Y /\ n e. NN) /\ (f:NN-->Y /\ m e. NN)) -> ((AGA)M((f` n)G(f` m))) = ((AM(f` n))G(AM(f` m))))
25	17, 24	eqtr4d 1510	. . . . 5 |- (((f:NN-->Y /\ n e. NN) /\ (f:NN-->Y /\ m e. NN)) -> ((H` n)G(H` m)) = ((AGA)M((f` n)G(f` m))))
26	5, 10, 11	nv2 8253	. . . . . . 7 |- ((U e. NrmCVec /\ A e. X) -> (AGA) = (2SA))
27	18, 8, 26	mp2an 697	. . . . . 6 |- (AGA) = (2SA)
28	27	opreq1i 3971	. . . . 5 |- ((AGA)M((f` n)G(f` m))) = ((2SA)M((f` n)G(f` m)))
29	25, 28	syl6eq 1523	. . . 4 |- (((f:NN-->Y /\ n e. NN) /\ (f:NN-->Y /\ m e. NN)) -> ((H` n)G(H` m)) = ((2SA)M((f` n)G(f` m))))
30	5, 10	nvgcl 8239	. . . . . . 7 |- ((U e. NrmCVec /\ (f` n) e. X /\ (f` m) e. X) -> ((f` n)G(f` m)) e. X)
31	18, 30	mp3an1 903	. . . . . 6 |- (((f` n) e. X /\ (f` m) e. X) -> ((f` n)G(f` m)) e. X)
32		2cn 5980	. . . . . . . . . 10 |- 2 e. CC
33		2ne0 5990	. . . . . . . . . 10 |- 2 =/= 0
34	32, 33	reccl 5713	. . . . . . . . 9 |- (1 / 2) e. CC
35	5, 11	nvscl 8247	. . . . . . . . 9 |- ((U e. NrmCVec /\ (1 / 2) e. CC /\ ((f` n)G(f` m)) e. X) -> ((1 / 2)S((f` n)G(f` m))) e. X)
36	18, 34, 35	mp3an12 906	. . . . . . . 8 |- (((f` n)G(f` m)) e. X -> ((1 / 2)S((f` n)G(f` m))) e. X)
37	5, 3, 11	nvmdi 8270	. . . . . . . . . 10 |- ((U e. NrmCVec /\ (2 e. CC /\ A e. X /\ ((1 / 2)S((f` n)G(f` m))) e. X)) -> (2S(AM((1 / 2)S((f` n)G(f` m))))) = ((2SA)M(2S((1 / 2)S((f` n)G(f` m))))))
38	18, 37	mpan 695	. . . . . . . . 9 |- ((2 e. CC /\ A e. X /\ ((1 / 2)S((f` n)G(f` m))) e. X) -> (2S(AM((1 / 2)S((f` n)G(f` m))))) = ((2SA)M(2S((1 / 2)S((f` n)G(f` m))))))
39	32, 8, 38	mp3an12 906	. . . . . . . 8 |- (((1 / 2)S((f` n)G(f` m))) e. X -> (2S(AM((1 / 2)S((f` n)G(f` m))))) = ((2SA)M(2S((1 / 2)S((f` n)G(f` m))))))
40	36, 39	syl 10	. . . . . . 7 |- (((f` n)G(f` m)) e. X -> (2S(AM((1 / 2)S((f` n)G(f` m))))) = ((2SA)M(2S((1 / 2)S((f` n)G(f` m))))))
41	5, 11	nvsass 8249	. . . . . . . . . . 11 |- ((U e. NrmCVec /\ (2 e. CC /\ (1 / 2) e. CC /\ ((f` n)G(f` m)) e. X)) -> ((2 x. (1 / 2))S((f` n)G(f` m))) = (2S((1 / 2)S((f` n)G(f` m)))))
42	18, 41	mpan 695	. . . . . . . . . 10 |- ((2 e. CC /\ (1 / 2) e. CC /\ ((f` n)G(f` m)) e. X) -> ((2 x. (1 / 2))S((f` n)G(f` m))) = (2S((1 / 2)S((f` n)G(f` m)))))
43	32, 34, 42	mp3an12 906	. . . . . . . . 9 |- (((f` n)G(f` m)) e. X -> ((2 x. (1 / 2))S((f` n)G(f` m))) = (2S((1 / 2)S((f` n)G(f` m)))))
44	5, 11	nvsid 8248	. . . . . . . . . . 11 |- ((U e. NrmCVec /\ ((f` n)G(f` m)) e. X) -> (1S((f` n)G(f` m))) = ((f` n)G(f` m)))
45	18, 44	mpan 695	. . . . . . . . . 10 |- (((f` n)G(f` m)) e. X -> (1S((f` n)G(f` m))) = ((f` n)G(f` m)))
46	32, 33	recid 5733	. . . . . . . . . . 11 |- (2 x. (1 / 2)) = 1
47	46	opreq1i 3971	. . . . . . . . . 10 |- ((2 x. (1 / 2))S((f` n)G(f` m))) = (1S((f` n)G(f` m)))
48	45, 47	syl5eq 1519	. . . . . . . . 9 |- (((f` n)G(f` m)) e. X -> ((2 x. (1 / 2))S((f` n)G(f` m))) = ((f` n)G(f` m)))
49	43, 48	eqtr3d 1509	. . . . . . . 8 |- (((f` n)G(f` m)) e. X -> (2S((1 / 2)S((f`