# Metamath Proof Explorer

## Theorem lnfnl

Description: Basic linearity property of a linear functional. (Contributed by NM, 11-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion lnfnl
`|- ( ( ( T e. LinFn /\ A e. CC ) /\ ( B e. ~H /\ C e. ~H ) ) -> ( T ` ( ( A .h B ) +h C ) ) = ( ( A x. ( T ` B ) ) + ( T ` C ) ) )`

### Proof

Step Hyp Ref Expression
1 ellnfn
` |-  ( T e. LinFn <-> ( T : ~H --> CC /\ A. x e. CC A. y e. ~H A. z e. ~H ( T ` ( ( x .h y ) +h z ) ) = ( ( x x. ( T ` y ) ) + ( T ` z ) ) ) )`
2 1 simprbi
` |-  ( T e. LinFn -> A. x e. CC A. y e. ~H A. z e. ~H ( T ` ( ( x .h y ) +h z ) ) = ( ( x x. ( T ` y ) ) + ( T ` z ) ) )`
3 oveq1
` |-  ( x = A -> ( x .h y ) = ( A .h y ) )`
4 3 fvoveq1d
` |-  ( x = A -> ( T ` ( ( x .h y ) +h z ) ) = ( T ` ( ( A .h y ) +h z ) ) )`
5 oveq1
` |-  ( x = A -> ( x x. ( T ` y ) ) = ( A x. ( T ` y ) ) )`
6 5 oveq1d
` |-  ( x = A -> ( ( x x. ( T ` y ) ) + ( T ` z ) ) = ( ( A x. ( T ` y ) ) + ( T ` z ) ) )`
7 4 6 eqeq12d
` |-  ( x = A -> ( ( T ` ( ( x .h y ) +h z ) ) = ( ( x x. ( T ` y ) ) + ( T ` z ) ) <-> ( T ` ( ( A .h y ) +h z ) ) = ( ( A x. ( T ` y ) ) + ( T ` z ) ) ) )`
8 oveq2
` |-  ( y = B -> ( A .h y ) = ( A .h B ) )`
9 8 fvoveq1d
` |-  ( y = B -> ( T ` ( ( A .h y ) +h z ) ) = ( T ` ( ( A .h B ) +h z ) ) )`
10 fveq2
` |-  ( y = B -> ( T ` y ) = ( T ` B ) )`
11 10 oveq2d
` |-  ( y = B -> ( A x. ( T ` y ) ) = ( A x. ( T ` B ) ) )`
12 11 oveq1d
` |-  ( y = B -> ( ( A x. ( T ` y ) ) + ( T ` z ) ) = ( ( A x. ( T ` B ) ) + ( T ` z ) ) )`
13 9 12 eqeq12d
` |-  ( y = B -> ( ( T ` ( ( A .h y ) +h z ) ) = ( ( A x. ( T ` y ) ) + ( T ` z ) ) <-> ( T ` ( ( A .h B ) +h z ) ) = ( ( A x. ( T ` B ) ) + ( T ` z ) ) ) )`
14 oveq2
` |-  ( z = C -> ( ( A .h B ) +h z ) = ( ( A .h B ) +h C ) )`
15 14 fveq2d
` |-  ( z = C -> ( T ` ( ( A .h B ) +h z ) ) = ( T ` ( ( A .h B ) +h C ) ) )`
16 fveq2
` |-  ( z = C -> ( T ` z ) = ( T ` C ) )`
17 16 oveq2d
` |-  ( z = C -> ( ( A x. ( T ` B ) ) + ( T ` z ) ) = ( ( A x. ( T ` B ) ) + ( T ` C ) ) )`
18 15 17 eqeq12d
` |-  ( z = C -> ( ( T ` ( ( A .h B ) +h z ) ) = ( ( A x. ( T ` B ) ) + ( T ` z ) ) <-> ( T ` ( ( A .h B ) +h C ) ) = ( ( A x. ( T ` B ) ) + ( T ` C ) ) ) )`
19 7 13 18 rspc3v
` |-  ( ( A e. CC /\ B e. ~H /\ C e. ~H ) -> ( A. x e. CC A. y e. ~H A. z e. ~H ( T ` ( ( x .h y ) +h z ) ) = ( ( x x. ( T ` y ) ) + ( T ` z ) ) -> ( T ` ( ( A .h B ) +h C ) ) = ( ( A x. ( T ` B ) ) + ( T ` C ) ) ) )`
20 2 19 syl5
` |-  ( ( A e. CC /\ B e. ~H /\ C e. ~H ) -> ( T e. LinFn -> ( T ` ( ( A .h B ) +h C ) ) = ( ( A x. ( T ` B ) ) + ( T ` C ) ) ) )`
21 20 3expb
` |-  ( ( A e. CC /\ ( B e. ~H /\ C e. ~H ) ) -> ( T e. LinFn -> ( T ` ( ( A .h B ) +h C ) ) = ( ( A x. ( T ` B ) ) + ( T ` C ) ) ) )`
22 21 impcom
` |-  ( ( T e. LinFn /\ ( A e. CC /\ ( B e. ~H /\ C e. ~H ) ) ) -> ( T ` ( ( A .h B ) +h C ) ) = ( ( A x. ( T ` B ) ) + ( T ` C ) ) )`
23 22 anassrs
` |-  ( ( ( T e. LinFn /\ A e. CC ) /\ ( B e. ~H /\ C e. ~H ) ) -> ( T ` ( ( A .h B ) +h C ) ) = ( ( A x. ( T ` B ) ) + ( T ` C ) ) )`