Theorem hhsssh 9059

Description: The predicate "H is a subspace of Hilbert space."

Hypotheses

Ref	Expression
hhsst.1	|- U = <.<. +h , .h >., normh>.
hhsst.2	|- W = <.<.( +h |` (H X. H)), ( .h |` (CC X. H))>., (normh |` H)>.

Assertion

Ref	Expression
hhsssh	|- (H e. SH <-> (W e. (SubSp` U) /\ H (_ H~))

Proof of Theorem hhsssh

Step	Hyp	Ref	Expression
1		hhsst.1	. . . 4 |- U = <.<. +h , .h >., normh>.
2		hhsst.2	. . . 4 |- W = <.<.( +h |` (H X. H)), ( .h |` (CC X. H))>., (normh |` H)>.
3	1, 2	hhsst 9056	. . 3 |- (H e. SH -> W e. (SubSp` U))
4		shss 9000	. . 3 |- (H e. SH -> H (_ H~)
5	3, 4	jca 288	. 2 |- (H e. SH -> (W e. (SubSp` U) /\ H (_ H~))
6		eleq1 1526	. . 3 |- (H = if((W e. (SubSp` U) /\ H (_ H~), H, H~) -> (H e. SH <-> if((W e. (SubSp` U) /\ H (_ H~), H, H~) e. SH))
7		eqid 1468	. . . 4 |- <.<.( +h |` (if((W e. (SubSp` U) /\ H (_ H~), H, H~) X. if((W e. (SubSp` U) /\ H (_ H~), H, H~))), ( .h |` (CC X. if((W e. (SubSp` U) /\ H (_ H~), H, H~)))>., (normh |` if((W e. (SubSp` U) /\ H (_ H~), H, H~))>. = <.<.( +h |` (if((W e. (SubSp` U) /\ H (_ H~), H, H~) X. if((W e. (SubSp` U) /\ H (_ H~), H, H~))), ( .h |` (CC X. if((W e. (SubSp` U) /\ H (_ H~), H, H~)))>., (normh |` if((W e. (SubSp` U) /\ H (_ H~), H, H~))>.
8		xpeq1 3190	. . . . . . . . . . . . 13 |- (H = if((W e. (SubSp` U) /\ H (_ H~), H, H~) -> (H X. H) = (if((W e. (SubSp` U) /\ H (_ H~), H, H~) X. H))
9		xpeq2 3191	. . . . . . . . . . . . 13 |- (H = if((W e. (SubSp` U) /\ H (_ H~), H, H~) -> (if((W e. (SubSp` U) /\ H (_ H~), H, H~) X. H) = (if((W e. (SubSp` U) /\ H (_ H~), H, H~) X. if((W e. (SubSp` U) /\ H (_ H~), H, H~)))
10	8, 9	eqtrd 1499	. . . . . . . . . . . 12 |- (H = if((W e. (SubSp` U) /\ H (_ H~), H, H~) -> (H X. H) = (if((W e. (SubSp` U) /\ H (_ H~), H, H~) X. if((W e. (SubSp` U) /\ H (_ H~), H, H~)))
11		reseq2 3353	. . . . . . . . . . . 12 |- ((H X. H) = (if((W e. (SubSp` U) /\ H (_ H~), H, H~) X. if((W e. (SubSp` U) /\ H (_ H~), H, H~)) -> ( +h |` (H X. H)) = ( +h |` (if((W e. (SubSp` U) /\ H (_ H~), H, H~) X. if((W e. (SubSp` U) /\ H (_ H~), H, H~))))
12	10, 11	syl 10	. . . . . . . . . . 11 |- (H = if((W e. (SubSp` U) /\ H (_ H~), H, H~) -> ( +h |` (H X. H)) = ( +h |` (if((W e. (SubSp` U) /\ H (_ H~), H, H~) X. if((W e. (SubSp` U) /\ H (_ H~), H, H~))))
13		xpeq2 3191	. . . . . . . . . . . 12 |- (H = if((W e. (SubSp` U) /\ H (_ H~), H, H~) -> (CC X. H) = (CC X. if((W e. (SubSp` U) /\ H (_ H~), H, H~)))
14		reseq2 3353	. . . . . . . . . . . 12 |- ((CC X. H) = (CC X. if((W e. (SubSp` U) /\ H (_ H~), H, H~)) -> ( .h |` (CC X. H)) = ( .h |` (CC X. if((W e. (SubSp` U) /\ H (_ H~), H, H~))))
15	13, 14	syl 10	. . . . . . . . . . 11 |- (H = if((W e. (SubSp` U) /\ H (_ H~), H, H~) -> ( .h |` (CC X. H)) = ( .h |` (CC X. if((W e. (SubSp` U) /\ H (_ H~), H, H~))))
16	12, 15	opeq12d 2486	. . . . . . . . . 10 |- (H = if((W e. (SubSp` U) /\ H (_ H~), H, H~) -> <.( +h |` (H X. H)), ( .h |` (CC X. H))>. = <.( +h |` (if((W e. (SubSp` U) /\ H (_ H~), H, H~) X. if((W e. (SubSp` U) /\ H (_ H~), H, H~))), ( .h |` (CC X. if((W e. (SubSp` U) /\ H (_ H~), H, H~)))>.)
17		reseq2 3353	. . . . . . . . . 10 |- (H = if((W e. (SubSp` U) /\ H (_ H~), H, H~) -> (normh |` H) = (normh |` if((W e. (SubSp` U) /\ H (_ H~), H, H~)))
18	16, 17	opeq12d 2486	. . . . . . . . 9 |- (H = if((W e. (SubSp` U) /\ H (_ H~), H, H~) -> <.<.( +h |` (H X. H)), ( .h |` (CC X. H))>., (normh |` H)>. = <.<.( +h |` (if((W e. (SubSp` U) /\ H (_ H~), H, H~) X. if((W e. (SubSp` U) /\ H (_ H~), H, H~))), ( .h |` (CC X. if((W e. (SubSp` U) /\ H (_ H~), H, H~)))>., (normh |` if((W e. (SubSp` U) /\ H (_ H~), H, H~))>.)
19	18, 2	syl5eq 1511	. . . . . . . 8 |- (H = if((W e. (SubSp` U) /\ H (_ H~), H, H~) -> W = <.<.( +h |` (if((W e. (SubSp` U) /\ H (_ H~), H, H~) X. if((W e. (SubSp` U) /\ H (_ H~), H, H~))), ( .h |` (CC X. if((W e. (SubSp` U) /\ H (_ H~), H, H~)))>., (normh |` if((W e. (SubSp` U) /\ H (_ H~), H, H~))>.)
20	19	eleq1d 1532	. . . . . . 7 |- (H = if((W e. (SubSp` U) /\ H (_ H~), H, H~) -> (W e. (SubSp` U) <-> <.<.( +h |` (if((W e. (SubSp` U) /\ H (_ H~), H, H~) X. if((W e. (SubSp` U) /\ H (_ H~), H, H~))), ( .h |` (CC X. if((W e. (SubSp` U) /\ H (_ H~), H, H~)))>., (normh |` if((W e. (SubSp` U) /\ H (_ H~), H, H~))>. e. (SubSp` U)))
21		sseq1 2072	. . . . . . 7 |- (H = if((W e. (SubSp` U) /\ H (_ H~), H, H~) -> (H (_ H~ <-> if((W e. (SubSp` U) /\ H (_ H~), H, H~) (_ H~))
22	20, 21	anbi12d 626	. . . . . 6 |- (H = if((W e. (SubSp` U) /\ H (_ H~), H, H~) -> ((W e. (SubSp` U) /\ H (_ H~) <-> (<.<.( +h |` (if((W e. (SubSp` U) /\ H (_ H~), H, H~) X. if((W e. (SubSp` U) /\ H (_ H~), H, H~))), ( .h |` (CC X. if((W e. (SubSp` U) /\ H (_ H~), H, H~)))>., (normh |` if((W e. (SubSp` U) /\ H (_ H~), H, H~))>. e. (SubSp` U) /\ if((W e. (SubSp` U) /\ H (_ H~), H, H~) (_ H~)))
23		xpeq1 3190	. . . . . . . . . . . 12 |- (H~ = if((W e. (SubSp` U) /\ H (_ H~), H, H~) -> (H~ X. H~) = (if((W e. (SubSp` U) /\ H (_ H~), H, H~) X. H~))
24		xpeq2 3191	. . . . . . . . . . . 12 |- (H~ = if((W e. (SubSp` U) /\ H (_ H~), H, H~) -> (if((W e. (SubSp` U) /\ H (_ H~), H, H~) X. H~) = (if((W e. (SubSp` U) /\ H (_ H~), H, H~) X. if((W e. (SubSp` U) /\ H (_ H~), H, H~)))
25	23, 24	eqtrd 1499	. . . . . . . . . . 11 |- (H~ = if((W e. (SubSp` U) /\ H (_ H~), H, H~) -> (H~ X. H~) = (if((W e. (SubSp` U) /\ H (_ H~), H, H~) X. if((W e. (SubSp` U) /\ H (_ H~), H, H~)))
26		reseq2 3353	. . . . . . . . . . 11 |- ((H~ X. H~) = (if((W e. (SubSp` U) /\ H (_ H~), H, H~) X. if((W e. (SubSp` U) /\ H (_ H~), H, H~)) -> ( +h |` (H~ X. H~)) = ( +h |` (if((W e. (SubSp` U) /\ H (_ H~), H, H~) X. if((W e. (SubSp` U) /\ H (_ H~), H, H~)