Metamath Proof Explorer

Theorem hhsssh

Description: The predicate " H is a subspace of Hilbert space." (Contributed by NM, 25-Mar-2008) (New usage is discouraged.)

Ref Expression
Hypotheses hhsst.1 ⊢U=+ℎ⋅ℎnormℎ
hhsst.2 ⊢W=+ℎ↾H×H⋅ℎ↾ℂ×Hnormℎ↾H
Assertion hhsssh ⊢H∈Sℋ↔W∈SubSp⁡U∧H⊆ℋ

Proof

Step Hyp Ref Expression
1 hhsst.1 ⊢U=+ℎ⋅ℎnormℎ
2 hhsst.2 ⊢W=+ℎ↾H×H⋅ℎ↾ℂ×Hnormℎ↾H
3 1 2 hhsst ⊢H∈Sℋ→W∈SubSp⁡U
4 shss ⊢H∈Sℋ→H⊆ℋ
5 3 4 jca ⊢H∈Sℋ→W∈SubSp⁡U∧H⊆ℋ
6 eleq1 ⊢H=ifW∈SubSp⁡U∧H⊆ℋHℋ→H∈Sℋ↔ifW∈SubSp⁡U∧H⊆ℋHℋ∈Sℋ
7 eqid ⊢+ℎ↾ifW∈SubSp⁡U∧H⊆ℋHℋ×ifW∈SubSp⁡U∧H⊆ℋHℋ⋅ℎ↾ℂ×ifW∈SubSp⁡U∧H⊆ℋHℋnormℎ↾ifW∈SubSp⁡U∧H⊆ℋHℋ=+ℎ↾ifW∈SubSp⁡U∧H⊆ℋHℋ×ifW∈SubSp⁡U∧H⊆ℋHℋ⋅ℎ↾ℂ×ifW∈SubSp⁡U∧H⊆ℋHℋnormℎ↾ifW∈SubSp⁡U∧H⊆ℋHℋ
8 xpeq1 ⊢H=ifW∈SubSp⁡U∧H⊆ℋHℋ→H×H=ifW∈SubSp⁡U∧H⊆ℋHℋ×H
9 xpeq2 ⊢H=ifW∈SubSp⁡U∧H⊆ℋHℋ→ifW∈SubSp⁡U∧H⊆ℋHℋ×H=ifW∈SubSp⁡U∧H⊆ℋHℋ×ifW∈SubSp⁡U∧H⊆ℋHℋ
10 8 9 eqtrd ⊢H=ifW∈SubSp⁡U∧H⊆ℋHℋ→H×H=ifW∈SubSp⁡U∧H⊆ℋHℋ×ifW∈SubSp⁡U∧H⊆ℋHℋ
11 10 reseq2d ⊢H=ifW∈SubSp⁡U∧H⊆ℋHℋ→+ℎ↾H×H=+ℎ↾ifW∈SubSp⁡U∧H⊆ℋHℋ×ifW∈SubSp⁡U∧H⊆ℋHℋ
12 xpeq2 ⊢H=ifW∈SubSp⁡U∧H⊆ℋHℋ→ℂ×H=ℂ×ifW∈SubSp⁡U∧H⊆ℋHℋ
13 12 reseq2d ⊢H=ifW∈SubSp⁡U∧H⊆ℋHℋ→⋅ℎ↾ℂ×H=⋅ℎ↾ℂ×ifW∈SubSp⁡U∧H⊆ℋHℋ
14 11 13 opeq12d ⊢H=ifW∈SubSp⁡U∧H⊆ℋHℋ→+ℎ↾H×H⋅ℎ↾ℂ×H=+ℎ↾ifW∈SubSp⁡U∧H⊆ℋHℋ×ifW∈SubSp⁡U∧H⊆ℋHℋ⋅ℎ↾ℂ×ifW∈SubSp⁡U∧H⊆ℋHℋ
15 reseq2 ⊢H=ifW∈SubSp⁡U∧H⊆ℋHℋ→normℎ↾H=normℎ↾ifW∈SubSp⁡U∧H⊆ℋHℋ
16 14 15 opeq12d ⊢H=ifW∈SubSp⁡U∧H⊆ℋHℋ→+ℎ↾H×H⋅ℎ↾ℂ×Hnormℎ↾H=+ℎ↾ifW∈SubSp⁡U∧H⊆ℋHℋ×ifW∈SubSp⁡U∧H⊆ℋHℋ⋅ℎ↾ℂ×ifW∈SubSp⁡U∧H⊆ℋHℋnormℎ↾ifW∈SubSp⁡U∧H⊆ℋHℋ
17 2 16 eqtrid ⊢H=ifW∈SubSp⁡U∧H⊆ℋHℋ→W=+ℎ↾ifW∈SubSp⁡U∧H⊆ℋHℋ×ifW∈SubSp⁡U∧H⊆ℋHℋ⋅ℎ↾ℂ×ifW∈SubSp⁡U∧H⊆ℋHℋnormℎ↾ifW∈SubSp⁡U∧H⊆ℋHℋ
18 17 eleq1d ⊢H=ifW∈SubSp⁡U∧H⊆ℋHℋ→W∈SubSp⁡U↔+ℎ↾ifW∈SubSp⁡U∧H⊆ℋHℋ×ifW∈SubSp⁡U∧H⊆ℋHℋ⋅ℎ↾ℂ×ifW∈SubSp⁡U∧H⊆ℋHℋnormℎ↾ifW∈SubSp⁡U∧H⊆ℋHℋ∈SubSp⁡U
19 sseq1 ⊢H=ifW∈SubSp⁡U∧H⊆ℋHℋ→H⊆ℋ↔ifW∈SubSp⁡U∧H⊆ℋHℋ⊆ℋ
20 18 19 anbi12d ⊢H=ifW∈SubSp⁡U∧H⊆ℋHℋ→W∈SubSp⁡U∧H⊆ℋ↔+ℎ↾ifW∈SubSp⁡U∧H⊆ℋHℋ×ifW∈SubSp⁡U∧H⊆ℋHℋ⋅ℎ↾ℂ×ifW∈SubSp⁡U∧H⊆ℋHℋnormℎ↾ifW∈SubSp⁡U∧H⊆ℋHℋ∈SubSp⁡U∧ifW∈SubSp⁡U∧H⊆ℋHℋ⊆ℋ
21 xpeq1 ⊢ℋ=ifW∈SubSp⁡U∧H⊆ℋHℋ→ℋ×ℋ=ifW∈SubSp⁡U∧H⊆ℋHℋ×ℋ
22 xpeq2 ⊢ℋ=ifW∈SubSp⁡U∧H⊆ℋHℋ→ifW∈SubSp⁡U∧H⊆ℋHℋ×ℋ=ifW∈SubSp⁡U∧H⊆ℋHℋ×ifW∈SubSp⁡U∧H⊆ℋHℋ
23 21 22 eqtrd ⊢ℋ=ifW∈SubSp⁡U∧H⊆ℋHℋ→ℋ×ℋ=ifW∈SubSp⁡U∧H⊆ℋHℋ×ifW∈SubSp⁡U∧H⊆ℋHℋ
24 23 reseq2d ⊢ℋ=ifW∈SubSp⁡U∧H⊆ℋHℋ→+ℎ↾ℋ×ℋ=+ℎ↾ifW∈SubSp⁡U∧H⊆ℋHℋ×ifW∈SubSp⁡U∧H⊆ℋHℋ
25 xpeq2 ⊢ℋ=ifW∈SubSp⁡U∧H⊆ℋHℋ→ℂ×ℋ=ℂ×ifW∈SubSp⁡U∧H⊆ℋHℋ
26 25 reseq2d ⊢ℋ=ifW∈SubSp⁡U∧H⊆ℋHℋ→⋅ℎ↾ℂ×ℋ=⋅ℎ↾ℂ×ifW∈SubSp⁡U∧H⊆ℋHℋ
27 24 26 opeq12d ⊢ℋ=ifW∈SubSp⁡U∧H⊆ℋHℋ→+ℎ↾ℋ×ℋ⋅ℎ↾ℂ×ℋ=+ℎ↾ifW∈SubSp⁡U∧H⊆ℋHℋ×ifW∈SubSp⁡U∧H⊆ℋHℋ⋅ℎ↾ℂ×ifW∈SubSp⁡U∧H⊆ℋHℋ
28 reseq2 ⊢ℋ=ifW∈SubSp⁡U∧H⊆ℋHℋ→normℎ↾ℋ=normℎ↾ifW∈SubSp⁡U∧H⊆ℋHℋ
29 27 28 opeq12d ⊢ℋ=ifW∈SubSp⁡U∧H⊆ℋHℋ→+ℎ↾ℋ×ℋ⋅ℎ↾ℂ×ℋnormℎ↾ℋ=+ℎ↾ifW∈SubSp⁡U∧H⊆ℋHℋ×ifW∈SubSp⁡U∧H⊆ℋHℋ⋅ℎ↾ℂ×ifW∈SubSp⁡U∧H⊆ℋHℋnormℎ↾ifW∈SubSp⁡U∧H⊆ℋHℋ
30 29 eleq1d ⊢ℋ=ifW∈SubSp⁡U∧H⊆ℋHℋ→+ℎ↾ℋ×ℋ⋅ℎ↾ℂ×ℋnormℎ↾ℋ∈SubSp⁡U↔+ℎ↾ifW∈SubSp⁡U∧H⊆ℋHℋ×ifW∈SubSp⁡U∧H⊆ℋHℋ⋅ℎ↾ℂ×ifW∈SubSp⁡U∧H⊆ℋHℋnormℎ↾ifW∈SubSp⁡U∧H⊆ℋHℋ∈SubSp⁡U
31 sseq1 ⊢ℋ=ifW∈SubSp⁡U∧H⊆ℋHℋ→ℋ⊆ℋ↔ifW∈SubSp⁡U∧H⊆ℋHℋ⊆ℋ
32 30 31 anbi12d ⊢ℋ=ifW∈SubSp⁡U∧H⊆ℋHℋ→+ℎ↾ℋ×ℋ⋅ℎ↾ℂ×ℋnormℎ↾ℋ∈SubSp⁡U∧ℋ⊆ℋ↔+ℎ↾ifW∈SubSp⁡U∧H⊆ℋHℋ×ifW∈SubSp⁡U∧H⊆ℋHℋ⋅ℎ↾ℂ×ifW∈SubSp⁡U∧H⊆ℋHℋnormℎ↾ifW∈SubSp⁡U∧H⊆ℋHℋ∈SubSp⁡U∧ifW∈SubSp⁡U∧H⊆ℋHℋ⊆ℋ
33 ax-hfvadd ⊢+ℎ:ℋ×ℋ⟶ℋ
34 ffn ⊢+ℎ:ℋ×ℋ⟶ℋ→+ℎFnℋ×ℋ
35 fnresdm ⊢+ℎFnℋ×ℋ→+ℎ↾ℋ×ℋ=+ℎ
36 33 34 35 mp2b ⊢+ℎ↾ℋ×ℋ=+ℎ
37 ax-hfvmul ⊢⋅ℎ:ℂ×ℋ⟶ℋ
38 ffn ⊢⋅ℎ:ℂ×ℋ⟶ℋ→⋅ℎFnℂ×ℋ
39 fnresdm ⊢⋅ℎFnℂ×ℋ→⋅ℎ↾ℂ×ℋ=⋅ℎ
40 37 38 39 mp2b ⊢⋅ℎ↾ℂ×ℋ=⋅ℎ
41 36 40 opeq12i ⊢+ℎ↾ℋ×ℋ⋅ℎ↾ℂ×ℋ=+ℎ⋅ℎ
42 normf ⊢normℎ:ℋ⟶ℝ
43 ffn ⊢normℎ:ℋ⟶ℝ→normℎFnℋ
44 fnresdm ⊢normℎFnℋ→normℎ↾ℋ=normℎ
45 42 43 44 mp2b ⊢normℎ↾ℋ=normℎ
46 41 45 opeq12i ⊢+ℎ↾ℋ×ℋ⋅ℎ↾ℂ×ℋnormℎ↾ℋ=+ℎ⋅ℎnormℎ
47 46 1 eqtr4i ⊢+ℎ↾ℋ×ℋ⋅ℎ↾ℂ×ℋnormℎ↾ℋ=U
48 1 hhnv ⊢U∈NrmCVec
49 eqid ⊢SubSp⁡U=SubSp⁡U
50 49 sspid ⊢U∈NrmCVec→U∈SubSp⁡U
51 48 50 ax-mp ⊢U∈SubSp⁡U
52 47 51 eqeltri ⊢+ℎ↾ℋ×ℋ⋅ℎ↾ℂ×ℋnormℎ↾ℋ∈SubSp⁡U
53 ssid ⊢ℋ⊆ℋ
54 52 53 pm3.2i ⊢+ℎ↾ℋ×ℋ⋅ℎ↾ℂ×ℋnormℎ↾ℋ∈SubSp⁡U∧ℋ⊆ℋ
55 20 32 54 elimhyp ⊢+ℎ↾ifW∈SubSp⁡U∧H⊆ℋHℋ×ifW∈SubSp⁡U∧H⊆ℋHℋ⋅ℎ↾ℂ×ifW∈SubSp⁡U∧H⊆ℋHℋnormℎ↾ifW∈SubSp⁡U∧H⊆ℋHℋ∈SubSp⁡U∧ifW∈SubSp⁡U∧H⊆ℋHℋ⊆ℋ
56 55 simpli ⊢+ℎ↾ifW∈SubSp⁡U∧H⊆ℋHℋ×ifW∈SubSp⁡U∧H⊆ℋHℋ⋅ℎ↾ℂ×ifW∈SubSp⁡U∧H⊆ℋHℋnormℎ↾ifW∈SubSp⁡U∧H⊆ℋHℋ∈SubSp⁡U
57 55 simpri ⊢ifW∈SubSp⁡U∧H⊆ℋHℋ⊆ℋ
58 1 7 56 57 hhshsslem2 ⊢ifW∈SubSp⁡U∧H⊆ℋHℋ∈Sℋ
59 6 58 dedth ⊢W∈SubSp⁡U∧H⊆ℋ→H∈Sℋ
60 5 59 impbii ⊢H∈Sℋ↔W∈SubSp⁡U∧H⊆ℋ