Theorem minveclem36 8580

Description: Lemma for minveceu 8583.

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
minveclem36	|- (((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)))

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 minveclem36

Step	Hyp	Ref	Expression
1		minvec35.a	. . . . . . . . . 10 |- A e. X
2		minvec35.u	. . . . . . . . . . . 12 |- U e. CPreHil
3	2	phnvi 8475	. . . . . . . . . . 11 |- U e. NrmCVec
4		minvec35.x	. . . . . . . . . . . 12 |- X = (Base` U)
5		minvec35.m	. . . . . . . . . . . 12 |- M = (-v` U)
6	4, 5	nvnnncan1 8268	. . . . . . . . . . 11 |- ((U e. NrmCVec /\ (A e. X /\ a e. X /\ b e. X)) -> ((AMa)M(AMb)) = (bMa))
7	3, 6	mpan 695	. . . . . . . . . 10 |- ((A e. X /\ a e. X /\ b e. X) -> ((AMa)M(AMb)) = (bMa))
8	1, 7	mp3an1 903	. . . . . . . . 9 |- ((a e. X /\ b e. X) -> ((AMa)M(AMb)) = (bMa))
9	8	fveq2d 3728	. . . . . . . 8 |- ((a e. X /\ b e. X) -> (N` ((AMa)M(AMb))) = (N` (bMa)))
10		minvec35.n	. . . . . . . . . 10 |- N = (norm` U)
11	4, 5, 10	nvsub 8295	. . . . . . . . 9 |- ((U e. NrmCVec /\ a e. X /\ b e. X) -> (N` (aMb)) = (N` (bMa)))
12	3, 11	mp3an1 903	. . . . . . . 8 |- ((a e. X /\ b e. X) -> (N` (aMb)) = (N` (bMa)))
13	9, 12	eqtr4d 1510	. . . . . . 7 |- ((a e. X /\ b e. X) -> (N` ((AMa)M(AMb))) = (N` (aMb)))
14	13	opreq1d 3975	. . . . . 6 |- ((a e. X /\ b e. X) -> ((N` ((AMa)M(AMb)))^2) = ((N` (aMb))^2))
15	14	opreq2d 3976	. . . . 5 |- ((a e. X /\ b e. X) -> (((N` ((AMa)G(AMb)))^2) + ((N` ((AMa)M(AMb)))^2)) = (((N` ((AMa)G(AMb)))^2) + ((N` (aMb))^2)))
16		minvec35.g	. . . . . . . 8 |- G = (+v` U)
17	4, 16, 5, 10	phpar2 8482	. . . . . . 7 |- ((U e. CPreHil /\ (AMa) e. X /\ (AMb) e. X) -> (((N` ((AMa)G(AMb)))^2) + ((N` ((AMa)M(AMb)))^2)) = (2 x. (((N` (AMa))^2) + ((N` (AMb))^2))))
18	2, 17	mp3an1 903	. . . . . 6 |- (((AMa) e. X /\ (AMb) e. X) -> (((N` ((AMa)G(AMb)))^2) + ((N` ((AMa)M(AMb)))^2)) = (2 x. (((N` (AMa))^2) + ((N` (AMb))^2))))
19	4, 5	nvmcl 8267	. . . . . . 7 |- ((U e. NrmCVec /\ A e. X /\ a e. X) -> (AMa) e. X)
20	3, 1, 19	mp3an12 906	. . . . . 6 |- (a e. X -> (AMa) e. X)
21	4, 5	nvmcl 8267	. . . . . . 7 |- ((U e. NrmCVec /\ A e. X /\ b e. X) -> (AMb) e. X)
22	3, 1, 21	mp3an12 906	. . . . . 6 |- (b e. X -> (AMb) e. X)
23	18, 20, 22	syl2an 454	. . . . 5 |- ((a e. X /\ b e. X) -> (((N` ((AMa)G(AMb)))^2) + ((N` ((AMa)M(AMb)))^2)) = (2 x. (((N` (AMa))^2) + ((N` (AMb))^2))))
24	15, 23	eqtr3d 1509	. . . 4 |- ((a e. X /\ b e. X) -> (((N` ((AMa)G(AMb)))^2) + ((N` (aMb))^2)) = (2 x. (((N` (AMa))^2) + ((N` (AMb))^2))))
25		opreq1 3968	. . . . . 6 |- ((N` (AMa)) = P -> ((N` (AMa))^2) = (P^2))
26		opreq1 3968	. . . . . 6 |- ((N` (AMb)) = P -> ((N` (AMb))^2) = (P^2))
27	25, 26	opreqan12d 3979	. . . . 5 |- (((N` (AMa)) = P /\ (N` (AMb)) = P) -> (((N` (AMa))^2) + ((N` (AMb))^2)) = ((P^2) + (P^2)))
28	27	opreq2d 3976	. . . 4 |- (((N` (AMa)) = P /\ (N` (AMb)) = P) -> (2 x. (((N` (AMa))^2) + ((N` (AMb))^2))) = (2 x. ((P^2) + (P^2))))
29	24, 28	sylan9eq 1527	. . 3 |- (((a e. X /\ b e. X) /\ ((N` (AMa)) = P /\ (N` (AMb)) = P)) -> (((N` ((AMa)G(AMb)))^2) + ((N` (aMb))^2)) = (2 x. ((P^2) + (P^2))))
30		2cn 5980	. . . . . . . . 9 |- 2 e. CC
31		minvec36.1	. . . . . . . . . . . . 13 |- R = {x | E.y e. Y x = -u(N` (AMy))}
32		minvec36.w	. . . . . . . . . . . . 13 |- W e. (SubSp` U)
33		minvec35.y	. . . . . . . . . . . . 13 |- Y = (Base` W)
34		minvec36.2	. . . . . . . . . . . . 13 |- P = -usup(R, RR, < )
35	31, 2, 5, 10, 4, 32, 33, 1, 34	minveclem12 8556	. . . . . . . . . . . 12 |- P e. RR
36	35	resqcl 6623	. . . . . . . . . . 11 |- (P^2) e. RR
37	36, 36	readdcl 5334	. . . . . . . . . 10 |- ((P^2) + (P^2)) e. RR
38	37	recn 5314	. . . . . . . . 9 |- ((P^2) + (P^2)) e. CC
39	30, 38	mulcl 5321	. . . . . . . 8 |- (2 x. ((P^2) + (P^2))) e. CC
40		subaddt 5375	. . . . . . . 8 |- (((2 x. ((P^2) + (P^2))) e. CC /\ ((N` ((AMa)G(AMb)))^2) e. CC /\ ((N` (aMb))^2) e. CC) -> (((2 x. ((P^2) + (P^2))) - ((N` ((AMa)G(AMb)))^2)) = ((N` (aMb))^2) <-> (((N` ((AMa)G(AMb)))^2) + ((N` (aMb))^2)) = (2 x. ((P^2) + (P^2)))))
41	39, 40	mp3an1 903	. . . . . . 7 |- ((((N` ((AMa)G(AMb)))^2) e. CC /\ ((N` (aMb))^2) e. CC) -> (((2 x. ((P^2) + (P^2))) - ((N` ((AMa)G(AMb)))^2)) = ((N` (aMb))^2) <-> (((N` ((AMa)G(AMb)))^2) + ((N` (aMb))^2)) = (2 x. ((P^2) + (P^2)))))
42		sqclt 6611	. . . . . . 7 |- ((N` ((AMa)G(AMb))) e. CC -> ((N` ((AMa)G(AMb)))^2) e. CC)
43		sqclt 6611	. . . . . . 7 |- ((N` (aMb)) e. CC -> ((N` (aMb))^2) e. CC)
44	41, 42, 43	syl2an 454	. . . . . 6 |- (((N` ((AMa)G(AMb))) e. CC /\ (N` (aMb)) e. CC) -> (((2 x. ((P^2) + (P^2))) - ((N` ((AMa)G(AMb)))^2)) = ((N` (aMb))^2) <-> (((N` ((AMa)G(AMb)))^2) + ((N` (aMb))^2)) = (2 x. ((P^2) + (P^2)))))
45	4, 10	nvcl 8287	. . . . . . . 8 |- ((U e. NrmCVec /\ ((AMa)