HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem minveclem18 8493
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
minvec17.h |- (j e. NN -> (H` j) = (AM(f` j)))
minvec18.g |- G = (+v` U)
Assertion
Ref Expression
minveclem18 |- (((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)G(H` m)))^2)) = ((N` ((f` n)M(f` m)))^2))
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   x,U,y   x,W,y   f,Y,j,m,n,x,y
Proof of Theorem minveclem18
StepHypRef Expression
1 minvec10.u . . . . 5 |- U e. CPreHil
2 minvec10.x . . . . . 6 |- X = (Base` U)
3 minvec18.g . . . . . 6 |- G = (+v` U)
4 minvec10.m . . . . . 6 |- M = (-v` U)
5 minvec10.n . . . . . 6 |- N = (norm` U)
62, 3, 4, 5phpar2 8413 . . . . 5 |- ((U e. CPreHil /\ (H` n) e. X /\ (H` m) e. X) -> (((N` ((H` n)G(H` m)))^2) + ((N` ((H` n)M(H` m)))^2)) = (2 x. (((N` (H` n))^2) + ((N` (H` m))^2))))
71, 6mp3an1 900 . . . 4 |- (((H` n) e. X /\ (H` m) e. X) -> (((N` ((H` n)G(H` m)))^2) + ((N` ((H` n)M(H` m)))^2)) = (2 x. (((N` (H` n))^2) + ((N` (H` m))^2))))
8 subaddt 5347 . . . . 5 |- (((2 x. (((N` (H` n))^2) + ((N` (H` m))^2))) e. CC /\ ((N` ((H` n)G(H` m)))^2) e. CC /\ ((N` ((H` n)M(H` m)))^2) e. CC) -> (((2 x. (((N` (H` n))^2) + ((N` (H` m))^2))) - ((N` ((H` n)G(H` m)))^2)) = ((N` ((H` n)M(H` m)))^2) <-> (((N` ((H` n)G(H` m)))^2) + ((N` ((H` n)M(H` m)))^2)) = (2 x. (((N` (H` n))^2) + ((N` (H` m))^2)))))
9 axaddcl 5243 . . . . . . 7 |- ((((N` (H` n))^2) e. CC /\ ((N` (H` m))^2) e. CC) -> (((N` (H` n))^2) + ((N` (H` m))^2)) e. CC)
101phnvi 8406 . . . . . . . . . 10 |- U e. NrmCVec
112, 5nvcl 8227 . . . . . . . . . 10 |- ((U e. NrmCVec /\ (H` n) e. X) -> (N` (H` n)) e. RR)
1210, 11mpan 693 . . . . . . . . 9 |- ((H` n) e. X -> (N` (H` n)) e. RR)
1312recnd 5287 . . . . . . . 8 |- ((H` n) e. X -> (N` (H` n)) e. CC)
14 sqclt 6542 . . . . . . . 8 |- ((N` (H` n)) e. CC -> ((N` (H` n))^2) e. CC)
1513, 14syl 10 . . . . . . 7 |- ((H` n) e. X -> ((N` (H` n))^2) e. CC)
162, 5nvcl 8227 . . . . . . . . . 10 |- ((U e. NrmCVec /\ (H` m) e. X) -> (N` (H` m)) e. RR)
1710, 16mpan 693 . . . . . . . . 9 |- ((H` m) e. X -> (N` (H` m)) e. RR)
1817recnd 5287 . . . . . . . 8 |- ((H` m) e. X -> (N` (H` m)) e. CC)
19 sqclt 6542 . . . . . . . 8 |- ((N` (H` m)) e. CC -> ((N` (H` m))^2) e. CC)
2018, 19syl 10 . . . . . . 7 |- ((H` m) e. X -> ((N` (H` m))^2) e. CC)
219, 15, 20syl2an 454 . . . . . 6 |- (((H` n) e. X /\ (H` m) e. X) -> (((N` (H` n))^2) + ((N` (H` m))^2)) e. CC)
22 2cn 5927 . . . . . . 7 |- 2 e. CC
23 axmulcl 5245 . . . . . . 7 |- ((2 e. CC /\ (((N` (H` n))^2) + ((N` (H` m))^2)) e. CC) -> (2 x. (((N` (H` n))^2) + ((N` (H` m))^2))) e. CC)
2422, 23mpan 693 . . . . . 6 |- ((((N` (H` n))^2) + ((N` (H` m))^2)) e. CC -> (2 x. (((N` (H` n))^2) + ((N` (H` m))^2))) e. CC)
2521, 24syl 10 . . . . 5 |- (((H` n) e. X /\ (H` m) e. X) -> (2 x. (((N` (H` n))^2) + ((N` (H` m))^2))) e. CC)
262, 3nvgcl 8179 . . . . . . . . 9 |- ((U e. NrmCVec /\ (H` n) e. X /\ (H` m) e. X) -> ((H` n)G(H` m)) e. X)
2710, 26mp3an1 900 . . . . . . . 8 |- (((H` n) e. X /\ (H` m) e. X) -> ((H` n)G(H` m)) e. X)
282, 5nvcl 8227 . . . . . . . . 9 |- ((U e. NrmCVec /\ ((H` n)G(H` m)) e. X) -> (N` ((H` n)G(H` m))) e. RR)
2910, 28mpan 693 . . . . . . . 8 |- (((H` n)G(H` m)) e. X -> (N` ((H` n)G(H` m))) e. RR)
3027, 29syl 10 . . . . . . 7 |- (((H` n) e. X /\ (H` m) e. X) -> (N` ((H` n)G(H` m))) e. RR)
3130recnd 5287 . . . . . 6 |- (((H` n) e. X /\ (H` m) e. X) -> (N` ((H` n)G(H` m))) e. CC)
32 sqclt 6542 . . . . . 6 |- ((N` ((H` n)G(H` m))) e. CC -> ((N` ((H` n)G(H` m)))^2) e. CC)
3331, 32syl 10 . . . . 5 |- (((H` n) e. X /\ (H` m) e. X) -> ((N` ((H` n)G(H` m)))^2) e. CC)
342, 4nvmcl 8207 . . . . . . . . 9 |- ((U e. NrmCVec /\ (H` n) e. X /\ (H` m) e. X) -> ((H` n)M(H` m)) e. X)
3510, 34mp3an1 900 . . . . . . . 8 |- (((H` n) e. X /\ (H` m) e. X) -> ((H` n)M(H` m)) e. X)
362, 5nvcl 8227 . . . . . . . . 9 |- ((U e. NrmCVec /\ ((H` n)M(H` m)) e. X) -> (N` ((H` n)M(H` m))) e. RR)
3710, 36mpan 693 . . . . . . . 8 |- (((H` n)M(H` m)) e. X -> (N` ((H` n)M(H` m))) e. RR)
3835, 37syl 10 . . . . . . 7 |- (((H` n) e. X /\ (H` m) e. X) -> (N` ((H` n)M(H` m))) e. RR)
3938recnd 5287 . . . . . 6 |- (((H` n) e. X /\ (H` m) e. X) -> (N` ((H` n)M(H` m))) e. CC)
40 sqclt 6542 . . . . . 6 |- ((N` ((H` n)M(H` m))) e. CC -> ((N` ((H` n)M(H` m)))^2) e. CC)
4139, 40syl 10 . . . . 5 |- (((H` n) e. X /\ (H` m) e. X) -> ((N` ((H` n)M(H` m)))^2) e. CC)
428, 25, 33, 41syl3anc 856 . . . 4 |- (((H` n) e. X /\ (H` m) e. X) -> (((2 x. (((N` (H` n))^2) + ((N` (H` m))^2))) - ((N` ((H` n)G(H` m)))^2)) = ((N` ((H` n)M(H` m)))^2) <-> (((N` ((H` n)G(H` m)))^2) + ((N` ((H` n)