Theorem sspph 8515

Description: A subspace of an inner product space is an inner product space.

Hypothesis

Ref	Expression
sspph.h	|- H = (SubSp` U)

Assertion

Ref	Expression
sspph	|- ((U e. CPreHil /\ W e. H) -> W e. CPreHil)

Proof of Theorem sspph

Step	Hyp	Ref	Expression
1		sspph.h	. . . . 5 |- H = (SubSp` U)
2	1	sspnv 8385	. . . 4 |- ((U e. NrmCVec /\ W e. H) -> W e. NrmCVec)
3		phnv 8473	. . . 4 |- (U e. CPreHil -> U e. NrmCVec)
4	2, 3	sylan 448	. . 3 |- ((U e. CPreHil /\ W e. H) -> W e. NrmCVec)
5		eqid 1475	. . . . . . . . . . . 12 |- (Base` U) = (Base` U)
6		eqid 1475	. . . . . . . . . . . 12 |- (Base` W) = (Base` W)
7	5, 6, 1	sspba 8386	. . . . . . . . . . 11 |- ((U e. NrmCVec /\ W e. H) -> (Base` W) (_ (Base` U))
8	7	sseld 2067	. . . . . . . . . 10 |- ((U e. NrmCVec /\ W e. H) -> (x e. (Base` W) -> x e. (Base` U)))
9	7	sseld 2067	. . . . . . . . . 10 |- ((U e. NrmCVec /\ W e. H) -> (y e. (Base` W) -> y e. (Base` U)))
10	8, 9	anim12d 558	. . . . . . . . 9 |- ((U e. NrmCVec /\ W e. H) -> ((x e. (Base` W) /\ y e. (Base` W)) -> (x e. (Base` U) /\ y e. (Base` U))))
11	10, 3	sylan 448	. . . . . . . 8 |- ((U e. CPreHil /\ W e. H) -> ((x e. (Base` W) /\ y e. (Base` W)) -> (x e. (Base` U) /\ y e. (Base` U))))
12	11	imp 350	. . . . . . 7 |- (((U e. CPreHil /\ W e. H) /\ (x e. (Base` W) /\ y e. (Base` W))) -> (x e. (Base` U) /\ y e. (Base` U)))
13		eqid 1475	. . . . . . . . . 10 |- (+v` U) = (+v` U)
14		eqid 1475	. . . . . . . . . 10 |- (-v` U) = (-v` U)
15		eqid 1475	. . . . . . . . . 10 |- (norm` U) = (norm` U)
16	5, 13, 14, 15	phpar2 8482	. . . . . . . . 9 |- ((U e. CPreHil /\ x e. (Base` U) /\ y e. (Base` U)) -> ((((norm` U)` (x(+v` U)y))^2) + (((norm` U)` (x(-v` U)y))^2)) = (2 x. ((((norm` U)` x)^2) + (((norm` U)` y)^2))))
17	16	3expb 834	. . . . . . . 8 |- ((U e. CPreHil /\ (x e. (Base` U) /\ y e. (Base` U))) -> ((((norm` U)` (x(+v` U)y))^2) + (((norm` U)` (x(-v` U)y))^2)) = (2 x. ((((norm` U)` x)^2) + (((norm` U)` y)^2))))
18	17	adantlr 393	. . . . . . 7 |- (((U e. CPreHil /\ W e. H) /\ (x e. (Base` U) /\ y e. (Base` U))) -> ((((norm` U)` (x(+v` U)y))^2) + (((norm` U)` (x(-v` U)y))^2)) = (2 x. ((((norm` U)` x)^2) + (((norm` U)` y)^2))))
19	12, 18	syldan 467	. . . . . 6 |- (((U e. CPreHil /\ W e. H) /\ (x e. (Base` W) /\ y e. (Base` W))) -> ((((norm` U)` (x(+v` U)y))^2) + (((norm` U)` (x(-v` U)y))^2)) = (2 x. ((((norm` U)` x)^2) + (((norm` U)` y)^2))))
20		eqid 1475	. . . . . . . . . . . . . 14 |- (+v` W) = (+v` W)
21	6, 20	nvgcl 8239	. . . . . . . . . . . . 13 |- ((W e. NrmCVec /\ x e. (Base` W) /\ y e. (Base` W)) -> (x(+v` W)y) e. (Base` W))
22	21	3expb 834	. . . . . . . . . . . 12 |- ((W e. NrmCVec /\ (x e. (Base` W) /\ y e. (Base` W))) -> (x(+v` W)y) e. (Base` W))
23	22, 2	sylan 448	. . . . . . . . . . 11 |- (((U e. NrmCVec /\ W e. H) /\ (x e. (Base` W) /\ y e. (Base` W))) -> (x(+v` W)y) e. (Base` W))
24		eqid 1475	. . . . . . . . . . . . 13 |- (norm` W) = (norm` W)
25	6, 15, 24, 1	sspnval 8396	. . . . . . . . . . . 12 |- ((U e. NrmCVec /\ W e. H /\ (x(+v` W)y) e. (Base` W)) -> ((norm` W)` (x(+v` W)y)) = ((norm` U)` (x(+v` W)y)))
26	25	3expa 833	. . . . . . . . . . 11 |- (((U e. NrmCVec /\ W e. H) /\ (x(+v` W)y) e. (Base` W)) -> ((norm` W)` (x(+v` W)y)) = ((norm` U)` (x(+v` W)y)))
27	23, 26	syldan 467	. . . . . . . . . 10 |- (((U e. NrmCVec /\ W e. H) /\ (x e. (Base` W) /\ y e. (Base` W))) -> ((norm` W)` (x(+v` W)y)) = ((norm` U)` (x(+v` W)y)))
28	27	opreq1d 3975	. . . . . . . . 9 |- (((U e. NrmCVec /\ W e. H) /\ (x e. (Base` W) /\ y e. (Base` W))) -> (((norm` W)` (x(+v` W)y))^2) = (((norm` U)` (x(+v` W)y))^2))
29	6, 13, 20, 1	sspgval 8388	. . . . . . . . . . 11 |- (((U e. NrmCVec /\ W e. H) /\ (x e. (Base` W) /\ y e. (Base` W))) -> (x(+v` W)y) = (x(+v` U)y))
30	29	fveq2d 3728	. . . . . . . . . 10 |- (((U e. NrmCVec /\ W e. H) /\ (x e. (Base` W) /\ y e. (Base` W))) -> ((norm` U)` (x(+v` W)y)) = ((norm` U)` (x(+v` U)y)))
31	30	opreq1d 3975	. . . . . . . . 9 |- (((U e. NrmCVec /\ W e. H) /\ (x e. (Base` W) /\ y e. (Base` W))) -> (((norm` U)` (x(+v` W)y))^2) = (((norm` U)` (x(+v` U)y))^2))
32	28, 31	eqtrd 1507	. . . . . . . 8 |- (((U e. NrmCVec /\ W e. H) /\ (x e. (Base` W) /\ y e. (Base` W))) -> (((norm` W)` (x(+v` W)y))^2) = (((norm` U)` (x(+v` U)y))^2))
33		eqid 1475	. . . . . . . . . . . . . 14 |- (-v` W) = (-v` W)
34	6, 33	nvmcl 8267	. . . . . . . . . . . . 13 |- ((W e. NrmCVec /\ x e. (Base` W) /\ y e. (Base` W)) -> (x(-v` W)y) e. (Base` W))
35	34	3expb 834	. . . . . . . . . . . 12 |- ((W e. NrmCVec /\ (x e. (Base` W) /\ y e. (Base` W))) -> (x(-v` W)y) e. (Base` W))
36	35, 2	sylan 448	. . . . . . . . . . 11 |- (((U e. NrmCVec /\ W e. H) /\ (x e. (Base` W) /\ y e. (Base` W))) -> (x(-v` W)y) e. (Base` W))
37	6, 15, 24, 1	sspnval 8396	. . . . . . . . . . . 12 |- ((U e. NrmCVec /\ W e. H /\ (x(-v` W)y) e. (Base` W)) -> ((norm` W)` (x(-v` W)y)) = ((norm` U)` (x(-v` W)y)))
38	37	3expa 833	. . . . . . . . . . 11 |- (((U e. NrmCVec /\ W e. H) /\ (x(-v` W)y) e. (Base` W)) -> ((norm` W)` (x(-v` W)y)) = ((norm` U)` (x(-v` W)y)))
39	36, 38	syldan 467	. . . . . . . . . 10 |- (((U e. NrmCVec /\ W e. H) /\ (x e. (Base` W) /\ y e. (Base` W))) -> ((norm` W)` (x(-v` W)y)) = ((norm` U)` (x(-v` W)y)))
40	6, 14, 33, 1	sspmval 8392	. . . . . . . . . . 11 |- (((U e. NrmCVec /\ W e. H) /\ (x e. (Base` W) /\ y e. (Base` W))) -> (x(-v` W)y) = (x(-v` U)y))
41	40	fveq2d 3728	. . . . . . . . . 10 |- (((U e. NrmCVec /\ W e. H) /\ (x e. (Base` W) /\ y e. (Base` W))) -> ((norm` U)` (x(-v` W)y)) = ((norm` U)` (x(-v` U)y)))
42	39, 41	eqtrd 1507	. . . . . . . . 9 |- (((U e. NrmCVec /\ W e. H) /\ (x e. (Base` W) /\ y e. (Base` W))) -> ((norm` W)` (x(-v` W)y)) = ((norm` U)` (x(-v` U)y)))
43	42	opreq1d 3975	. . . . . . . 8 |- (((U e. NrmCVec /\ W e. H) /\ (x e. (Base` W) /\ y e. (Base` W))) -> (((norm` W)` (x(-v` W)y))^2) = (((norm` U)` (x(-v` U)y))^2))
44	32, 43	opreq12d 3978	. . . . . . 7 |- (((U e. NrmCVec /\ W e. H) /\ (x e. (Base` W) /\ y e. (Base` W))) -> ((((norm` W)` (x(+v` W)y))^2) + (((norm` W)` (x(-v` W)y))^2)) = ((((norm` U)`