Metamath Proof Explorer

Theorem bralnfn

Description: The Dirac bra function is a linear functional. (Contributed by NM, 23-May-2006) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

Ref Expression
Assertion bralnfn 
|- ( A e. ~H -> ( bra ` A ) e. LinFn )

Proof

Step Hyp Ref Expression
1 brafn 
 |-  ( A e. ~H -> ( bra ` A ) : ~H --> CC )
2 simpll 
 |-  ( ( ( A e. ~H /\ x e. CC ) /\ ( y e. ~H /\ z e. ~H ) ) -> A e. ~H )
3 hvmulcl 
 |-  ( ( x e. CC /\ y e. ~H ) -> ( x .h y ) e. ~H )
4 3 ad2ant2lr 
 |-  ( ( ( A e. ~H /\ x e. CC ) /\ ( y e. ~H /\ z e. ~H ) ) -> ( x .h y ) e. ~H )
5 simprr 
 |-  ( ( ( A e. ~H /\ x e. CC ) /\ ( y e. ~H /\ z e. ~H ) ) -> z e. ~H )
6 braadd 
 |-  ( ( A e. ~H /\ ( x .h y ) e. ~H /\ z e. ~H ) -> ( ( bra ` A ) ` ( ( x .h y ) +h z ) ) = ( ( ( bra ` A ) ` ( x .h y ) ) + ( ( bra ` A ) ` z ) ) )
7 2 4 5 6 syl3anc 
 |-  ( ( ( A e. ~H /\ x e. CC ) /\ ( y e. ~H /\ z e. ~H ) ) -> ( ( bra ` A ) ` ( ( x .h y ) +h z ) ) = ( ( ( bra ` A ) ` ( x .h y ) ) + ( ( bra ` A ) ` z ) ) )
8 bramul 
 |-  ( ( A e. ~H /\ x e. CC /\ y e. ~H ) -> ( ( bra ` A ) ` ( x .h y ) ) = ( x x. ( ( bra ` A ) ` y ) ) )
9 8 3expa 
 |-  ( ( ( A e. ~H /\ x e. CC ) /\ y e. ~H ) -> ( ( bra ` A ) ` ( x .h y ) ) = ( x x. ( ( bra ` A ) ` y ) ) )
10 9 adantrr 
 |-  ( ( ( A e. ~H /\ x e. CC ) /\ ( y e. ~H /\ z e. ~H ) ) -> ( ( bra ` A ) ` ( x .h y ) ) = ( x x. ( ( bra ` A ) ` y ) ) )
11 10 oveq1d 
 |-  ( ( ( A e. ~H /\ x e. CC ) /\ ( y e. ~H /\ z e. ~H ) ) -> ( ( ( bra ` A ) ` ( x .h y ) ) + ( ( bra ` A ) ` z ) ) = ( ( x x. ( ( bra ` A ) ` y ) ) + ( ( bra ` A ) ` z ) ) )
12 7 11 eqtrd 
 |-  ( ( ( A e. ~H /\ x e. CC ) /\ ( y e. ~H /\ z e. ~H ) ) -> ( ( bra ` A ) ` ( ( x .h y ) +h z ) ) = ( ( x x. ( ( bra ` A ) ` y ) ) + ( ( bra ` A ) ` z ) ) )
13 12 ralrimivva 
 |-  ( ( A e. ~H /\ x e. CC ) -> A. y e. ~H A. z e. ~H ( ( bra ` A ) ` ( ( x .h y ) +h z ) ) = ( ( x x. ( ( bra ` A ) ` y ) ) + ( ( bra ` A ) ` z ) ) )
14 13 ralrimiva 
 |-  ( A e. ~H -> A. x e. CC A. y e. ~H A. z e. ~H ( ( bra ` A ) ` ( ( x .h y ) +h z ) ) = ( ( x x. ( ( bra ` A ) ` y ) ) + ( ( bra ` A ) ` z ) ) )
15 ellnfn 
 |-  ( ( bra ` A ) e. LinFn <-> ( ( bra ` A ) : ~H --> CC /\ A. x e. CC A. y e. ~H A. z e. ~H ( ( bra ` A ) ` ( ( x .h y ) +h z ) ) = ( ( x x. ( ( bra ` A ) ` y ) ) + ( ( bra ` A ) ` z ) ) ) )
16 1 14 15 sylanbrc 
 |-  ( A e. ~H -> ( bra ` A ) e. LinFn )