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	\|- T : ~H --> ~H
	Assertion	ho01i	\|- ( A. x e. ~H A. y e. ~H ( ( T ` x ) .ih y ) = 0 <-> T = 0hop )

Proof

Step	Hyp	Ref	Expression
1		ho0.1	\|- T : ~H --> ~H
2		ffn	\|- ( T : ~H --> ~H -> T Fn ~H )
3	1 2	ax-mp	\|- T Fn ~H
4		ax-hv0cl	\|- 0h e. ~H
5	4	elexi	\|- 0h e. _V
6	5	fconst	\|- ( ~H X. { 0h } ) : ~H --> { 0h }
7		ffn	\|- ( ( ~H X. { 0h } ) : ~H --> { 0h } -> ( ~H X. { 0h } ) Fn ~H )
8	6 7	ax-mp	\|- ( ~H X. { 0h } ) Fn ~H
9		eqfnfv	\|- ( ( T Fn ~H /\ ( ~H X. { 0h } ) Fn ~H ) -> ( T = ( ~H X. { 0h } ) <-> A. x e. ~H ( T ` x ) = ( ( ~H X. { 0h } ) ` x ) ) )
10	3 8 9	mp2an	\|- ( T = ( ~H X. { 0h } ) <-> A. x e. ~H ( T ` x ) = ( ( ~H X. { 0h } ) ` x ) )
11		df0op2	\|- 0hop = ( ~H X. 0H )
12		df-ch0	\|- 0H = { 0h }
13	12	xpeq2i	\|- ( ~H X. 0H ) = ( ~H X. { 0h } )
14	11 13	eqtri	\|- 0hop = ( ~H X. { 0h } )
15	14	eqeq2i	\|- ( T = 0hop <-> T = ( ~H X. { 0h } ) )
16	1	ffvelcdmi	\|- ( x e. ~H -> ( T ` x ) e. ~H )
17		hial0	\|- ( ( T ` x ) e. ~H -> ( A. y e. ~H ( ( T ` x ) .ih y ) = 0 <-> ( T ` x ) = 0h ) )
18	16 17	syl	\|- ( x e. ~H -> ( A. y e. ~H ( ( T ` x ) .ih y ) = 0 <-> ( T ` x ) = 0h ) )
19	5	fvconst2	\|- ( x e. ~H -> ( ( ~H X. { 0h } ) ` x ) = 0h )
20	19	eqeq2d	\|- ( x e. ~H -> ( ( T ` x ) = ( ( ~H X. { 0h } ) ` x ) <-> ( T ` x ) = 0h ) )
21	18 20	bitr4d	\|- ( x e. ~H -> ( A. y e. ~H ( ( T ` x ) .ih y ) = 0 <-> ( T ` x ) = ( ( ~H X. { 0h } ) ` x ) ) )
22	21	ralbiia	\|- ( A. x e. ~H A. y e. ~H ( ( T ` x ) .ih y ) = 0 <-> A. x e. ~H ( T ` x ) = ( ( ~H X. { 0h } ) ` x ) )
23	10 15 22	3bitr4ri	\|- ( A. x e. ~H A. y e. ~H ( ( T ` x ) .ih y ) = 0 <-> T = 0hop )

Metamath Proof Explorer

Theorem ho01i

Proof