Metamath Proof Explorer


Theorem isch2

Description: Closed subspace H of a Hilbert space. Definition of Beran p. 107. (Contributed by NM, 17-Aug-1999) (Revised by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

Ref Expression
Assertion isch2 H C H S f x f : H f v x x H

Proof

Step Hyp Ref Expression
1 isch H C H S v H H
2 alcom f x f H f v x x H x f f H f v x x H
3 19.23v f f H f v x x H f f H f v x x H
4 vex x V
5 4 elima2 x v H f f H f v x
6 5 imbi1i x v H x H f f H f v x x H
7 3 6 bitr4i f f H f v x x H x v H x H
8 7 albii x f f H f v x x H x x v H x H
9 dfss2 v H H x x v H x H
10 8 9 bitr4i x f f H f v x x H v H H
11 2 10 bitri f x f H f v x x H v H H
12 nnex V
13 elmapg H S V f H f : H
14 12 13 mpan2 H S f H f : H
15 14 anbi1d H S f H f v x f : H f v x
16 15 imbi1d H S f H f v x x H f : H f v x x H
17 16 2albidv H S f x f H f v x x H f x f : H f v x x H
18 11 17 bitr3id H S v H H f x f : H f v x x H
19 18 pm5.32i H S v H H H S f x f : H f v x x H
20 1 19 bitri H C H S f x f : H f v x x H