# Metamath Proof Explorer

## Theorem lnolin

Description: Basic linearity property of a linear operator. (Contributed by NM, 4-Dec-2007) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

Ref Expression
Hypotheses lnoval.1
`|- X = ( BaseSet ` U )`
lnoval.2
`|- Y = ( BaseSet ` W )`
lnoval.3
`|- G = ( +v ` U )`
lnoval.4
`|- H = ( +v ` W )`
lnoval.5
`|- R = ( .sOLD ` U )`
lnoval.6
`|- S = ( .sOLD ` W )`
lnoval.7
`|- L = ( U LnOp W )`
Assertion lnolin
`|- ( ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) /\ ( A e. CC /\ B e. X /\ C e. X ) ) -> ( T ` ( ( A R B ) G C ) ) = ( ( A S ( T ` B ) ) H ( T ` C ) ) )`

### Proof

Step Hyp Ref Expression
1 lnoval.1
` |-  X = ( BaseSet ` U )`
2 lnoval.2
` |-  Y = ( BaseSet ` W )`
3 lnoval.3
` |-  G = ( +v ` U )`
4 lnoval.4
` |-  H = ( +v ` W )`
5 lnoval.5
` |-  R = ( .sOLD ` U )`
6 lnoval.6
` |-  S = ( .sOLD ` W )`
7 lnoval.7
` |-  L = ( U LnOp W )`
8 1 2 3 4 5 6 7 islno
` |-  ( ( U e. NrmCVec /\ W e. NrmCVec ) -> ( T e. L <-> ( T : X --> Y /\ A. u e. CC A. w e. X A. t e. X ( T ` ( ( u R w ) G t ) ) = ( ( u S ( T ` w ) ) H ( T ` t ) ) ) ) )`
9 8 biimp3a
` |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) -> ( T : X --> Y /\ A. u e. CC A. w e. X A. t e. X ( T ` ( ( u R w ) G t ) ) = ( ( u S ( T ` w ) ) H ( T ` t ) ) ) )`
10 9 simprd
` |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) -> A. u e. CC A. w e. X A. t e. X ( T ` ( ( u R w ) G t ) ) = ( ( u S ( T ` w ) ) H ( T ` t ) ) )`
11 oveq1
` |-  ( u = A -> ( u R w ) = ( A R w ) )`
12 11 fvoveq1d
` |-  ( u = A -> ( T ` ( ( u R w ) G t ) ) = ( T ` ( ( A R w ) G t ) ) )`
13 oveq1
` |-  ( u = A -> ( u S ( T ` w ) ) = ( A S ( T ` w ) ) )`
14 13 oveq1d
` |-  ( u = A -> ( ( u S ( T ` w ) ) H ( T ` t ) ) = ( ( A S ( T ` w ) ) H ( T ` t ) ) )`
15 12 14 eqeq12d
` |-  ( u = A -> ( ( T ` ( ( u R w ) G t ) ) = ( ( u S ( T ` w ) ) H ( T ` t ) ) <-> ( T ` ( ( A R w ) G t ) ) = ( ( A S ( T ` w ) ) H ( T ` t ) ) ) )`
16 oveq2
` |-  ( w = B -> ( A R w ) = ( A R B ) )`
17 16 fvoveq1d
` |-  ( w = B -> ( T ` ( ( A R w ) G t ) ) = ( T ` ( ( A R B ) G t ) ) )`
18 fveq2
` |-  ( w = B -> ( T ` w ) = ( T ` B ) )`
19 18 oveq2d
` |-  ( w = B -> ( A S ( T ` w ) ) = ( A S ( T ` B ) ) )`
20 19 oveq1d
` |-  ( w = B -> ( ( A S ( T ` w ) ) H ( T ` t ) ) = ( ( A S ( T ` B ) ) H ( T ` t ) ) )`
21 17 20 eqeq12d
` |-  ( w = B -> ( ( T ` ( ( A R w ) G t ) ) = ( ( A S ( T ` w ) ) H ( T ` t ) ) <-> ( T ` ( ( A R B ) G t ) ) = ( ( A S ( T ` B ) ) H ( T ` t ) ) ) )`
22 oveq2
` |-  ( t = C -> ( ( A R B ) G t ) = ( ( A R B ) G C ) )`
23 22 fveq2d
` |-  ( t = C -> ( T ` ( ( A R B ) G t ) ) = ( T ` ( ( A R B ) G C ) ) )`
24 fveq2
` |-  ( t = C -> ( T ` t ) = ( T ` C ) )`
25 24 oveq2d
` |-  ( t = C -> ( ( A S ( T ` B ) ) H ( T ` t ) ) = ( ( A S ( T ` B ) ) H ( T ` C ) ) )`
26 23 25 eqeq12d
` |-  ( t = C -> ( ( T ` ( ( A R B ) G t ) ) = ( ( A S ( T ` B ) ) H ( T ` t ) ) <-> ( T ` ( ( A R B ) G C ) ) = ( ( A S ( T ` B ) ) H ( T ` C ) ) ) )`
27 15 21 26 rspc3v
` |-  ( ( A e. CC /\ B e. X /\ C e. X ) -> ( A. u e. CC A. w e. X A. t e. X ( T ` ( ( u R w ) G t ) ) = ( ( u S ( T ` w ) ) H ( T ` t ) ) -> ( T ` ( ( A R B ) G C ) ) = ( ( A S ( T ` B ) ) H ( T ` C ) ) ) )`
28 10 27 mpan9
` |-  ( ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) /\ ( A e. CC /\ B e. X /\ C e. X ) ) -> ( T ` ( ( A R B ) G C ) ) = ( ( A S ( T ` B ) ) H ( T ` C ) ) )`