Metamath Proof Explorer

Theorem lnosub

Description: Subtraction 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 lnosub.1 
|- X = ( BaseSet ` U )
lnosub.5 
|- M = ( -v ` U )
lnosub.6 
|- N = ( -v ` W )
lnosub.7 
|- L = ( U LnOp W )
Assertion lnosub 
|- ( ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) /\ ( A e. X /\ B e. X ) ) -> ( T ` ( A M B ) ) = ( ( T ` A ) N ( T ` B ) ) )

Proof

Step Hyp Ref Expression
1 lnosub.1 
 |-  X = ( BaseSet ` U )
2 lnosub.5 
 |-  M = ( -v ` U )
3 lnosub.6 
 |-  N = ( -v ` W )
4 lnosub.7 
 |-  L = ( U LnOp W )
5 neg1cn 
 |-  -u 1 e. CC
6 eqid 
 |-  ( BaseSet ` W ) = ( BaseSet ` W )
7 eqid 
 |-  ( +v ` U ) = ( +v ` U )
8 eqid 
 |-  ( +v ` W ) = ( +v ` W )
9 eqid 
 |-  ( .sOLD ` U ) = ( .sOLD ` U )
10 eqid 
 |-  ( .sOLD ` W ) = ( .sOLD ` W )
11 1 6 7 8 9 10 4 lnolin 
 |-  ( ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) /\ ( -u 1 e. CC /\ B e. X /\ A e. X ) ) -> ( T ` ( ( -u 1 ( .sOLD ` U ) B ) ( +v ` U ) A ) ) = ( ( -u 1 ( .sOLD ` W ) ( T ` B ) ) ( +v ` W ) ( T ` A ) ) )
12 5 11 mp3anr1 
 |-  ( ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) /\ ( B e. X /\ A e. X ) ) -> ( T ` ( ( -u 1 ( .sOLD ` U ) B ) ( +v ` U ) A ) ) = ( ( -u 1 ( .sOLD ` W ) ( T ` B ) ) ( +v ` W ) ( T ` A ) ) )
13 12 ancom2s 
 |-  ( ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) /\ ( A e. X /\ B e. X ) ) -> ( T ` ( ( -u 1 ( .sOLD ` U ) B ) ( +v ` U ) A ) ) = ( ( -u 1 ( .sOLD ` W ) ( T ` B ) ) ( +v ` W ) ( T ` A ) ) )
14 1 7 9 2 nvmval2 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A M B ) = ( ( -u 1 ( .sOLD ` U ) B ) ( +v ` U ) A ) )
15 14 3expb 
 |-  ( ( U e. NrmCVec /\ ( A e. X /\ B e. X ) ) -> ( A M B ) = ( ( -u 1 ( .sOLD ` U ) B ) ( +v ` U ) A ) )
16 15 3ad2antl1 
 |-  ( ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) /\ ( A e. X /\ B e. X ) ) -> ( A M B ) = ( ( -u 1 ( .sOLD ` U ) B ) ( +v ` U ) A ) )
17 16 fveq2d 
 |-  ( ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) /\ ( A e. X /\ B e. X ) ) -> ( T ` ( A M B ) ) = ( T ` ( ( -u 1 ( .sOLD ` U ) B ) ( +v ` U ) A ) ) )
18 simpl2 
 |-  ( ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) /\ ( A e. X /\ B e. X ) ) -> W e. NrmCVec )
19 1 6 4 lnof 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) -> T : X --> ( BaseSet ` W ) )
20 simpl 
 |-  ( ( A e. X /\ B e. X ) -> A e. X )
21 ffvelrn 
 |-  ( ( T : X --> ( BaseSet ` W ) /\ A e. X ) -> ( T ` A ) e. ( BaseSet ` W ) )
22 19 20 21 syl2an 
 |-  ( ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) /\ ( A e. X /\ B e. X ) ) -> ( T ` A ) e. ( BaseSet ` W ) )
23 simpr 
 |-  ( ( A e. X /\ B e. X ) -> B e. X )
24 ffvelrn 
 |-  ( ( T : X --> ( BaseSet ` W ) /\ B e. X ) -> ( T ` B ) e. ( BaseSet ` W ) )
25 19 23 24 syl2an 
 |-  ( ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) /\ ( A e. X /\ B e. X ) ) -> ( T ` B ) e. ( BaseSet ` W ) )
26 6 8 10 3 nvmval2 
 |-  ( ( W e. NrmCVec /\ ( T ` A ) e. ( BaseSet ` W ) /\ ( T ` B ) e. ( BaseSet ` W ) ) -> ( ( T ` A ) N ( T ` B ) ) = ( ( -u 1 ( .sOLD ` W ) ( T ` B ) ) ( +v ` W ) ( T ` A ) ) )
27 18 22 25 26 syl3anc 
 |-  ( ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) /\ ( A e. X /\ B e. X ) ) -> ( ( T ` A ) N ( T ` B ) ) = ( ( -u 1 ( .sOLD ` W ) ( T ` B ) ) ( +v ` W ) ( T ` A ) ) )
28 13 17 27 3eqtr4d 
 |-  ( ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) /\ ( A e. X /\ B e. X ) ) -> ( T ` ( A M B ) ) = ( ( T ` A ) N ( T ` B ) ) )