# 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 )`
` |-  ( ( ( 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`