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 ) ) )