Metamath Proof Explorer


Theorem ocval

Description: Value of orthogonal complement of a subset of Hilbert space. (Contributed by NM, 7-Aug-2000) (Revised by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

Ref Expression
Assertion ocval ( ๐ป โŠ† โ„‹ โ†’ ( โŠฅ โ€˜ ๐ป ) = { ๐‘ฅ โˆˆ โ„‹ โˆฃ โˆ€ ๐‘ฆ โˆˆ ๐ป ( ๐‘ฅ ยทih ๐‘ฆ ) = 0 } )

Proof

Step Hyp Ref Expression
1 ax-hilex โŠข โ„‹ โˆˆ V
2 1 elpw2 โŠข ( ๐ป โˆˆ ๐’ซ โ„‹ โ†” ๐ป โŠ† โ„‹ )
3 raleq โŠข ( ๐‘ง = ๐ป โ†’ ( โˆ€ ๐‘ฆ โˆˆ ๐‘ง ( ๐‘ฅ ยทih ๐‘ฆ ) = 0 โ†” โˆ€ ๐‘ฆ โˆˆ ๐ป ( ๐‘ฅ ยทih ๐‘ฆ ) = 0 ) )
4 3 rabbidv โŠข ( ๐‘ง = ๐ป โ†’ { ๐‘ฅ โˆˆ โ„‹ โˆฃ โˆ€ ๐‘ฆ โˆˆ ๐‘ง ( ๐‘ฅ ยทih ๐‘ฆ ) = 0 } = { ๐‘ฅ โˆˆ โ„‹ โˆฃ โˆ€ ๐‘ฆ โˆˆ ๐ป ( ๐‘ฅ ยทih ๐‘ฆ ) = 0 } )
5 df-oc โŠข โŠฅ = ( ๐‘ง โˆˆ ๐’ซ โ„‹ โ†ฆ { ๐‘ฅ โˆˆ โ„‹ โˆฃ โˆ€ ๐‘ฆ โˆˆ ๐‘ง ( ๐‘ฅ ยทih ๐‘ฆ ) = 0 } )
6 1 rabex โŠข { ๐‘ฅ โˆˆ โ„‹ โˆฃ โˆ€ ๐‘ฆ โˆˆ ๐ป ( ๐‘ฅ ยทih ๐‘ฆ ) = 0 } โˆˆ V
7 4 5 6 fvmpt โŠข ( ๐ป โˆˆ ๐’ซ โ„‹ โ†’ ( โŠฅ โ€˜ ๐ป ) = { ๐‘ฅ โˆˆ โ„‹ โˆฃ โˆ€ ๐‘ฆ โˆˆ ๐ป ( ๐‘ฅ ยทih ๐‘ฆ ) = 0 } )
8 2 7 sylbir โŠข ( ๐ป โŠ† โ„‹ โ†’ ( โŠฅ โ€˜ ๐ป ) = { ๐‘ฅ โˆˆ โ„‹ โˆฃ โˆ€ ๐‘ฆ โˆˆ ๐ป ( ๐‘ฅ ยทih ๐‘ฆ ) = 0 } )