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 syl5eq 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