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 ⋅ ℎ ↾ ℂ × H norm ℎ ↾ 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 ⋅ ℎ ↾ ℂ × H norm ℎ ↾ 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 = if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ → H ∈ S ℋ ↔ if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ ∈ S ℋ
7 eqid ⊢ + ℎ ↾ if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ × if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ ⋅ ℎ ↾ ℂ × if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ norm ℎ ↾ if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ = + ℎ ↾ if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ × if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ ⋅ ℎ ↾ ℂ × if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ norm ℎ ↾ if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ
8 xpeq1 ⊢ H = if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ → H × H = if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ × H
9 xpeq2 ⊢ H = if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ → if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ × H = if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ × if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ
10 8 9 eqtrd ⊢ H = if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ → H × H = if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ × if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ
11 10 reseq2d ⊢ H = if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ → + ℎ ↾ H × H = + ℎ ↾ if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ × if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ
12 xpeq2 ⊢ H = if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ → ℂ × H = ℂ × if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ
13 12 reseq2d ⊢ H = if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ → ⋅ ℎ ↾ ℂ × H = ⋅ ℎ ↾ ℂ × if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ
14 11 13 opeq12d ⊢ H = if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ → + ℎ ↾ H × H ⋅ ℎ ↾ ℂ × H = + ℎ ↾ if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ × if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ ⋅ ℎ ↾ ℂ × if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ
15 reseq2 ⊢ H = if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ → norm ℎ ↾ H = norm ℎ ↾ if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ
16 14 15 opeq12d ⊢ H = if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ → + ℎ ↾ H × H ⋅ ℎ ↾ ℂ × H norm ℎ ↾ H = + ℎ ↾ if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ × if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ ⋅ ℎ ↾ ℂ × if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ norm ℎ ↾ if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ
17 2 16 eqtrid ⊢ H = if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ → W = + ℎ ↾ if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ × if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ ⋅ ℎ ↾ ℂ × if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ norm ℎ ↾ if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ
18 17 eleq1d ⊢ H = if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ → W ∈ SubSp ⁡ U ↔ + ℎ ↾ if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ × if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ ⋅ ℎ ↾ ℂ × if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ norm ℎ ↾ if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ ∈ SubSp ⁡ U
19 sseq1 ⊢ H = if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ → H ⊆ ℋ ↔ if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ ⊆ ℋ
20 18 19 anbi12d ⊢ H = if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ → W ∈ SubSp ⁡ U ∧ H ⊆ ℋ ↔ + ℎ ↾ if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ × if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ ⋅ ℎ ↾ ℂ × if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ norm ℎ ↾ if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ ∈ SubSp ⁡ U ∧ if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ ⊆ ℋ
21 xpeq1 ⊢ ℋ = if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ → ℋ × ℋ = if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ × ℋ
22 xpeq2 ⊢ ℋ = if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ → if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ × ℋ = if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ × if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ
23 21 22 eqtrd ⊢ ℋ = if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ → ℋ × ℋ = if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ × if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ
24 23 reseq2d ⊢ ℋ = if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ → + ℎ ↾ ℋ × ℋ = + ℎ ↾ if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ × if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ
25 xpeq2 ⊢ ℋ = if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ → ℂ × ℋ = ℂ × if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ
26 25 reseq2d ⊢ ℋ = if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ → ⋅ ℎ ↾ ℂ × ℋ = ⋅ ℎ ↾ ℂ × if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ
27 24 26 opeq12d ⊢ ℋ = if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ → + ℎ ↾ ℋ × ℋ ⋅ ℎ ↾ ℂ × ℋ = + ℎ ↾ if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ × if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ ⋅ ℎ ↾ ℂ × if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ
28 reseq2 ⊢ ℋ = if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ → norm ℎ ↾ ℋ = norm ℎ ↾ if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ
29 27 28 opeq12d ⊢ ℋ = if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ → + ℎ ↾ ℋ × ℋ ⋅ ℎ ↾ ℂ × ℋ norm ℎ ↾ ℋ = + ℎ ↾ if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ × if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ ⋅ ℎ ↾ ℂ × if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ norm ℎ ↾ if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ
30 29 eleq1d ⊢ ℋ = if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ → + ℎ ↾ ℋ × ℋ ⋅ ℎ ↾ ℂ × ℋ norm ℎ ↾ ℋ ∈ SubSp ⁡ U ↔ + ℎ ↾ if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ × if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ ⋅ ℎ ↾ ℂ × if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ norm ℎ ↾ if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ ∈ SubSp ⁡ U
31 sseq1 ⊢ ℋ = if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ → ℋ ⊆ ℋ ↔ if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ ⊆ ℋ
32 30 31 anbi12d ⊢ ℋ = if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ → + ℎ ↾ ℋ × ℋ ⋅ ℎ ↾ ℂ × ℋ norm ℎ ↾ ℋ ∈ SubSp ⁡ U ∧ ℋ ⊆ ℋ ↔ + ℎ ↾ if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ × if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ ⋅ ℎ ↾ ℂ × if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ norm ℎ ↾ if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ ∈ SubSp ⁡ U ∧ if W ∈ 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 ⊢ + ℎ ↾ if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ × if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ ⋅ ℎ ↾ ℂ × if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ norm ℎ ↾ if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ ∈ SubSp ⁡ U ∧ if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ ⊆ ℋ
56 55 simpli ⊢ + ℎ ↾ if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ × if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ ⋅ ℎ ↾ ℂ × if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ norm ℎ ↾ if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ ∈ SubSp ⁡ U
57 55 simpri ⊢ if W ∈ SubSp ⁡ U ∧ H ⊆ ℋ H ℋ ⊆ ℋ
58 1 7 56 57 hhshsslem2 ⊢ if W ∈ 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 ⊆ ℋ