This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lnomul

Description: Scalar multiplication property of a linear operator. (Contributed by NM, 5-Dec-2007) (Revised by Mario Carneiro, 19-Nov-2013) (New usage is discouraged.)

Ref Expression
Hypotheses lnomul.1 
|- X = ( BaseSet ` U )
lnomul.5 
|- R = ( .sOLD ` U )
lnomul.6 
|- S = ( .sOLD ` W )
lnomul.7 
|- L = ( U LnOp W )
Assertion lnomul 
|- ( ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) /\ ( A e. CC /\ B e. X ) ) -> ( T ` ( A R B ) ) = ( A S ( T ` B ) ) )

Proof

Step Hyp Ref Expression
1 lnomul.1 
 |-  X = ( BaseSet ` U )
2 lnomul.5 
 |-  R = ( .sOLD ` U )
3 lnomul.6 
 |-  S = ( .sOLD ` W )
4 lnomul.7 
 |-  L = ( U LnOp W )
5 simpl 
 |-  ( ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) /\ ( A e. CC /\ B e. X ) ) -> ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) )
6 simprl 
 |-  ( ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) /\ ( A e. CC /\ B e. X ) ) -> A e. CC )
7 simprr 
 |-  ( ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) /\ ( A e. CC /\ B e. X ) ) -> B e. X )
8 simpl1 
 |-  ( ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) /\ ( A e. CC /\ B e. X ) ) -> U e. NrmCVec )
9 eqid 
 |-  ( 0vec ` U ) = ( 0vec ` U )
10 1 9 nvzcl 
 |-  ( U e. NrmCVec -> ( 0vec ` U ) e. X )
11 8 10 syl 
 |-  ( ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) /\ ( A e. CC /\ B e. X ) ) -> ( 0vec ` U ) e. X )
12 eqid 
 |-  ( BaseSet ` W ) = ( BaseSet ` W )
13 eqid 
 |-  ( +v ` U ) = ( +v ` U )
14 eqid 
 |-  ( +v ` W ) = ( +v ` W )
15 1 12 13 14 2 3 4 lnolin 
 |-  ( ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) /\ ( A e. CC /\ B e. X /\ ( 0vec ` U ) e. X ) ) -> ( T ` ( ( A R B ) ( +v ` U ) ( 0vec ` U ) ) ) = ( ( A S ( T ` B ) ) ( +v ` W ) ( T ` ( 0vec ` U ) ) ) )
16 5 6 7 11 15 syl13anc 
 |-  ( ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) /\ ( A e. CC /\ B e. X ) ) -> ( T ` ( ( A R B ) ( +v ` U ) ( 0vec ` U ) ) ) = ( ( A S ( T ` B ) ) ( +v ` W ) ( T ` ( 0vec ` U ) ) ) )
17 1 2 nvscl 
 |-  ( ( U e. NrmCVec /\ A e. CC /\ B e. X ) -> ( A R B ) e. X )
18 8 6 7 17 syl3anc 
 |-  ( ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) /\ ( A e. CC /\ B e. X ) ) -> ( A R B ) e. X )
19 1 13 9 nv0rid 
 |-  ( ( U e. NrmCVec /\ ( A R B ) e. X ) -> ( ( A R B ) ( +v ` U ) ( 0vec ` U ) ) = ( A R B ) )
20 8 18 19 syl2anc 
 |-  ( ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) /\ ( A e. CC /\ B e. X ) ) -> ( ( A R B ) ( +v ` U ) ( 0vec ` U ) ) = ( A R B ) )
21 20 fveq2d 
 |-  ( ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) /\ ( A e. CC /\ B e. X ) ) -> ( T ` ( ( A R B ) ( +v ` U ) ( 0vec ` U ) ) ) = ( T ` ( A R B ) ) )
22 eqid 
 |-  ( 0vec ` W ) = ( 0vec ` W )
23 1 12 9 22 4 lno0 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) -> ( T ` ( 0vec ` U ) ) = ( 0vec ` W ) )
24 23 oveq2d 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) -> ( ( A S ( T ` B ) ) ( +v ` W ) ( T ` ( 0vec ` U ) ) ) = ( ( A S ( T ` B ) ) ( +v ` W ) ( 0vec ` W ) ) )
25 24 adantr 
 |-  ( ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) /\ ( A e. CC /\ B e. X ) ) -> ( ( A S ( T ` B ) ) ( +v ` W ) ( T ` ( 0vec ` U ) ) ) = ( ( A S ( T ` B ) ) ( +v ` W ) ( 0vec ` W ) ) )
26 simpl2 
 |-  ( ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) /\ ( A e. CC /\ B e. X ) ) -> W e. NrmCVec )
27 1 12 4 lnof 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) -> T : X --> ( BaseSet ` W ) )
28 27 adantr 
 |-  ( ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) /\ ( A e. CC /\ B e. X ) ) -> T : X --> ( BaseSet ` W ) )
29 28 7 ffvelcdmd 
 |-  ( ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) /\ ( A e. CC /\ B e. X ) ) -> ( T ` B ) e. ( BaseSet ` W ) )
30 12 3 nvscl 
 |-  ( ( W e. NrmCVec /\ A e. CC /\ ( T ` B ) e. ( BaseSet ` W ) ) -> ( A S ( T ` B ) ) e. ( BaseSet ` W ) )
31 26 6 29 30 syl3anc 
 |-  ( ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) /\ ( A e. CC /\ B e. X ) ) -> ( A S ( T ` B ) ) e. ( BaseSet ` W ) )
32 12 14 22 nv0rid 
 |-  ( ( W e. NrmCVec /\ ( A S ( T ` B ) ) e. ( BaseSet ` W ) ) -> ( ( A S ( T ` B ) ) ( +v ` W ) ( 0vec ` W ) ) = ( A S ( T ` B ) ) )
33 26 31 32 syl2anc 
 |-  ( ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) /\ ( A e. CC /\ B e. X ) ) -> ( ( A S ( T ` B ) ) ( +v ` W ) ( 0vec ` W ) ) = ( A S ( T ` B ) ) )
34 25 33 eqtrd 
 |-  ( ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) /\ ( A e. CC /\ B e. X ) ) -> ( ( A S ( T ` B ) ) ( +v ` W ) ( T ` ( 0vec ` U ) ) ) = ( A S ( T ` B ) ) )
35 16 21 34 3eqtr3d 
 |-  ( ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) /\ ( A e. CC /\ B e. X ) ) -> ( T ` ( A R B ) ) = ( A S ( T ` B ) ) )