Metamath Proof Explorer

Theorem lnoadd

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

Ref Expression
Hypotheses lnoadd.1 
|- X = ( BaseSet ` U )
lnoadd.5 
|- G = ( +v ` U )
lnoadd.6 
|- H = ( +v ` W )
lnoadd.7 
|- L = ( U LnOp W )
Assertion lnoadd 
|- ( ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) /\ ( A e. X /\ B e. X ) ) -> ( T ` ( A G B ) ) = ( ( T ` A ) H ( T ` B ) ) )

Proof

Step Hyp Ref Expression
1 lnoadd.1 
 |-  X = ( BaseSet ` U )
2 lnoadd.5 
 |-  G = ( +v ` U )
3 lnoadd.6 
 |-  H = ( +v ` W )
4 lnoadd.7 
 |-  L = ( U LnOp W )
5 ax-1cn 
 |-  1 e. CC
6 eqid 
 |-  ( BaseSet ` W ) = ( BaseSet ` W )
7 eqid 
 |-  ( .sOLD ` U ) = ( .sOLD ` U )
8 eqid 
 |-  ( .sOLD ` W ) = ( .sOLD ` W )
9 1 6 2 3 7 8 4 lnolin 
 |-  ( ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) /\ ( 1 e. CC /\ A e. X /\ B e. X ) ) -> ( T ` ( ( 1 ( .sOLD ` U ) A ) G B ) ) = ( ( 1 ( .sOLD ` W ) ( T ` A ) ) H ( T ` B ) ) )
10 5 9 mp3anr1 
 |-  ( ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) /\ ( A e. X /\ B e. X ) ) -> ( T ` ( ( 1 ( .sOLD ` U ) A ) G B ) ) = ( ( 1 ( .sOLD ` W ) ( T ` A ) ) H ( T ` B ) ) )
11 simp1 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) -> U e. NrmCVec )
12 simpl 
 |-  ( ( A e. X /\ B e. X ) -> A e. X )
13 1 7 nvsid 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( 1 ( .sOLD ` U ) A ) = A )
14 11 12 13 syl2an 
 |-  ( ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) /\ ( A e. X /\ B e. X ) ) -> ( 1 ( .sOLD ` U ) A ) = A )
15 14 fvoveq1d 
 |-  ( ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) /\ ( A e. X /\ B e. X ) ) -> ( T ` ( ( 1 ( .sOLD ` U ) A ) G B ) ) = ( T ` ( A G B ) ) )
16 simpl2 
 |-  ( ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) /\ ( A e. X /\ B e. X ) ) -> W e. NrmCVec )
17 1 6 4 lnof 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) -> T : X --> ( BaseSet ` W ) )
18 ffvelrn 
 |-  ( ( T : X --> ( BaseSet ` W ) /\ A e. X ) -> ( T ` A ) e. ( BaseSet ` W ) )
19 17 12 18 syl2an 
 |-  ( ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) /\ ( A e. X /\ B e. X ) ) -> ( T ` A ) e. ( BaseSet ` W ) )
20 6 8 nvsid 
 |-  ( ( W e. NrmCVec /\ ( T ` A ) e. ( BaseSet ` W ) ) -> ( 1 ( .sOLD ` W ) ( T ` A ) ) = ( T ` A ) )
21 16 19 20 syl2anc 
 |-  ( ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) /\ ( A e. X /\ B e. X ) ) -> ( 1 ( .sOLD ` W ) ( T ` A ) ) = ( T ` A ) )
22 21 oveq1d 
 |-  ( ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) /\ ( A e. X /\ B e. X ) ) -> ( ( 1 ( .sOLD ` W ) ( T ` A ) ) H ( T ` B ) ) = ( ( T ` A ) H ( T ` B ) ) )
23 10 15 22 3eqtr3d 
 |-  ( ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) /\ ( A e. X /\ B e. X ) ) -> ( T ` ( A G B ) ) = ( ( T ` A ) H ( T ` B ) ) )