Metamath Proof Explorer

Theorem ho01i

Description: A condition implying that a Hilbert space operator is identically zero. Lemma 3.2(S8) of Beran p. 95. (Contributed by NM, 28-Jan-2006) (New usage is discouraged.)

Ref Expression
Hypothesis ho0.1 โŠข ๐‘‡ : โ„‹ โŸถ โ„‹
Assertion ho01i ( โˆ€ ๐‘ฅ โˆˆ โ„‹ โˆ€ ๐‘ฆ โˆˆ โ„‹ ( ( ๐‘‡ โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) = 0 โ†” ๐‘‡ = 0hop )

Proof

Step Hyp Ref Expression
1 ho0.1 โŠข ๐‘‡ : โ„‹ โŸถ โ„‹
2 ffn โŠข ( ๐‘‡ : โ„‹ โŸถ โ„‹ โ†’ ๐‘‡ Fn โ„‹ )
3 1 2 ax-mp โŠข ๐‘‡ Fn โ„‹
4 ax-hv0cl โŠข 0โ„Ž โˆˆ โ„‹
5 4 elexi โŠข 0โ„Ž โˆˆ V
6 5 fconst โŠข ( โ„‹ ร— { 0โ„Ž } ) : โ„‹ โŸถ { 0โ„Ž }
7 ffn โŠข ( ( โ„‹ ร— { 0โ„Ž } ) : โ„‹ โŸถ { 0โ„Ž } โ†’ ( โ„‹ ร— { 0โ„Ž } ) Fn โ„‹ )
8 6 7 ax-mp โŠข ( โ„‹ ร— { 0โ„Ž } ) Fn โ„‹
9 eqfnfv โŠข ( ( ๐‘‡ Fn โ„‹ โˆง ( โ„‹ ร— { 0โ„Ž } ) Fn โ„‹ ) โ†’ ( ๐‘‡ = ( โ„‹ ร— { 0โ„Ž } ) โ†” โˆ€ ๐‘ฅ โˆˆ โ„‹ ( ๐‘‡ โ€˜ ๐‘ฅ ) = ( ( โ„‹ ร— { 0โ„Ž } ) โ€˜ ๐‘ฅ ) ) )
10 3 8 9 mp2an โŠข ( ๐‘‡ = ( โ„‹ ร— { 0โ„Ž } ) โ†” โˆ€ ๐‘ฅ โˆˆ โ„‹ ( ๐‘‡ โ€˜ ๐‘ฅ ) = ( ( โ„‹ ร— { 0โ„Ž } ) โ€˜ ๐‘ฅ ) )
11 df0op2 โŠข 0hop = ( โ„‹ ร— 0โ„‹ )
12 df-ch0 โŠข 0โ„‹ = { 0โ„Ž }
13 12 xpeq2i โŠข ( โ„‹ ร— 0โ„‹ ) = ( โ„‹ ร— { 0โ„Ž } )
14 11 13 eqtri โŠข 0hop = ( โ„‹ ร— { 0โ„Ž } )
15 14 eqeq2i โŠข ( ๐‘‡ = 0hop โ†” ๐‘‡ = ( โ„‹ ร— { 0โ„Ž } ) )
16 1 ffvelcdmi โŠข ( ๐‘ฅ โˆˆ โ„‹ โ†’ ( ๐‘‡ โ€˜ ๐‘ฅ ) โˆˆ โ„‹ )
17 hial0 โŠข ( ( ๐‘‡ โ€˜ ๐‘ฅ ) โˆˆ โ„‹ โ†’ ( โˆ€ ๐‘ฆ โˆˆ โ„‹ ( ( ๐‘‡ โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) = 0 โ†” ( ๐‘‡ โ€˜ ๐‘ฅ ) = 0โ„Ž ) )
18 16 17 syl โŠข ( ๐‘ฅ โˆˆ โ„‹ โ†’ ( โˆ€ ๐‘ฆ โˆˆ โ„‹ ( ( ๐‘‡ โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) = 0 โ†” ( ๐‘‡ โ€˜ ๐‘ฅ ) = 0โ„Ž ) )
19 5 fvconst2 โŠข ( ๐‘ฅ โˆˆ โ„‹ โ†’ ( ( โ„‹ ร— { 0โ„Ž } ) โ€˜ ๐‘ฅ ) = 0โ„Ž )
20 19 eqeq2d โŠข ( ๐‘ฅ โˆˆ โ„‹ โ†’ ( ( ๐‘‡ โ€˜ ๐‘ฅ ) = ( ( โ„‹ ร— { 0โ„Ž } ) โ€˜ ๐‘ฅ ) โ†” ( ๐‘‡ โ€˜ ๐‘ฅ ) = 0โ„Ž ) )
21 18 20 bitr4d โŠข ( ๐‘ฅ โˆˆ โ„‹ โ†’ ( โˆ€ ๐‘ฆ โˆˆ โ„‹ ( ( ๐‘‡ โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) = 0 โ†” ( ๐‘‡ โ€˜ ๐‘ฅ ) = ( ( โ„‹ ร— { 0โ„Ž } ) โ€˜ ๐‘ฅ ) ) )
22 21 ralbiia โŠข ( โˆ€ ๐‘ฅ โˆˆ โ„‹ โˆ€ ๐‘ฆ โˆˆ โ„‹ ( ( ๐‘‡ โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) = 0 โ†” โˆ€ ๐‘ฅ โˆˆ โ„‹ ( ๐‘‡ โ€˜ ๐‘ฅ ) = ( ( โ„‹ ร— { 0โ„Ž } ) โ€˜ ๐‘ฅ ) )
23 10 15 22 3bitr4ri โŠข ( โˆ€ ๐‘ฅ โˆˆ โ„‹ โˆ€ ๐‘ฆ โˆˆ โ„‹ ( ( ๐‘‡ โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) = 0 โ†” ๐‘‡ = 0hop )