Metamath Proof Explorer

Theorem 0lnfn

Description: The identically zero function is a linear Hilbert space functional. (Contributed by NM, 14-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion 0lnfn 
|- ( ~H X. { 0 } ) e. LinFn

Proof

Step Hyp Ref Expression
1 0cn 
 |-  0 e. CC
2 1 fconst6 
 |-  ( ~H X. { 0 } ) : ~H --> CC
3 hvmulcl 
 |-  ( ( x e. CC /\ y e. ~H ) -> ( x .h y ) e. ~H )
4 hvaddcl 
 |-  ( ( ( x .h y ) e. ~H /\ z e. ~H ) -> ( ( x .h y ) +h z ) e. ~H )
5 3 4 sylan 
 |-  ( ( ( x e. CC /\ y e. ~H ) /\ z e. ~H ) -> ( ( x .h y ) +h z ) e. ~H )
6 c0ex 
 |-  0 e. _V
7 6 fvconst2 
 |-  ( ( ( x .h y ) +h z ) e. ~H -> ( ( ~H X. { 0 } ) ` ( ( x .h y ) +h z ) ) = 0 )
8 5 7 syl 
 |-  ( ( ( x e. CC /\ y e. ~H ) /\ z e. ~H ) -> ( ( ~H X. { 0 } ) ` ( ( x .h y ) +h z ) ) = 0 )
9 6 fvconst2 
 |-  ( y e. ~H -> ( ( ~H X. { 0 } ) ` y ) = 0 )
10 9 oveq2d 
 |-  ( y e. ~H -> ( x x. ( ( ~H X. { 0 } ) ` y ) ) = ( x x. 0 ) )
11 mul01 
 |-  ( x e. CC -> ( x x. 0 ) = 0 )
12 10 11 sylan9eqr 
 |-  ( ( x e. CC /\ y e. ~H ) -> ( x x. ( ( ~H X. { 0 } ) ` y ) ) = 0 )
13 6 fvconst2 
 |-  ( z e. ~H -> ( ( ~H X. { 0 } ) ` z ) = 0 )
14 12 13 oveqan12d 
 |-  ( ( ( x e. CC /\ y e. ~H ) /\ z e. ~H ) -> ( ( x x. ( ( ~H X. { 0 } ) ` y ) ) + ( ( ~H X. { 0 } ) ` z ) ) = ( 0 + 0 ) )
15 00id 
 |-  ( 0 + 0 ) = 0
16 14 15 eqtrdi 
 |-  ( ( ( x e. CC /\ y e. ~H ) /\ z e. ~H ) -> ( ( x x. ( ( ~H X. { 0 } ) ` y ) ) + ( ( ~H X. { 0 } ) ` z ) ) = 0 )
17 8 16 eqtr4d 
 |-  ( ( ( x e. CC /\ y e. ~H ) /\ z e. ~H ) -> ( ( ~H X. { 0 } ) ` ( ( x .h y ) +h z ) ) = ( ( x x. ( ( ~H X. { 0 } ) ` y ) ) + ( ( ~H X. { 0 } ) ` z ) ) )
18 17 3impa 
 |-  ( ( x e. CC /\ y e. ~H /\ z e. ~H ) -> ( ( ~H X. { 0 } ) ` ( ( x .h y ) +h z ) ) = ( ( x x. ( ( ~H X. { 0 } ) ` y ) ) + ( ( ~H X. { 0 } ) ` z ) ) )
19 18 rgen3 
 |-  A. x e. CC A. y e. ~H A. z e. ~H ( ( ~H X. { 0 } ) ` ( ( x .h y ) +h z ) ) = ( ( x x. ( ( ~H X. { 0 } ) ` y ) ) + ( ( ~H X. { 0 } ) ` z ) )
20 ellnfn 
 |-  ( ( ~H X. { 0 } ) e. LinFn <-> ( ( ~H X. { 0 } ) : ~H --> CC /\ A. x e. CC A. y e. ~H A. z e. ~H ( ( ~H X. { 0 } ) ` ( ( x .h y ) +h z ) ) = ( ( x x. ( ( ~H X. { 0 } ) ` y ) ) + ( ( ~H X. { 0 } ) ` z ) ) ) )
21 2 19 20 mpbir2an 
 |-  ( ~H X. { 0 } ) e. LinFn