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=ULnOpW
Assertion lnosub ⊢U∈NrmCVec∧W∈NrmCVec∧T∈L∧A∈X∧B∈X→T⁡AMB=T⁡ANT⁡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=ULnOpW
5 neg1cn ⊢−1∈ℂ
6 eqid ⊢BaseSet⁡W=BaseSet⁡W
7 eqid ⊢+v⁡U=+v⁡U
8 eqid ⊢+v⁡W=+v⁡W
9 eqid ⊢⋅𝑠OLD⁡U=⋅𝑠OLD⁡U
10 eqid ⊢⋅𝑠OLD⁡W=⋅𝑠OLD⁡W
11 1 6 7 8 9 10 4 lnolin ⊢U∈NrmCVec∧W∈NrmCVec∧T∈L∧−1∈ℂ∧B∈X∧A∈X→T⁡-1⋅𝑠OLD⁡UB+v⁡UA=-1⋅𝑠OLD⁡WT⁡B+v⁡WT⁡A
12 5 11 mp3anr1 ⊢U∈NrmCVec∧W∈NrmCVec∧T∈L∧B∈X∧A∈X→T⁡-1⋅𝑠OLD⁡UB+v⁡UA=-1⋅𝑠OLD⁡WT⁡B+v⁡WT⁡A
13 12 ancom2s ⊢U∈NrmCVec∧W∈NrmCVec∧T∈L∧A∈X∧B∈X→T⁡-1⋅𝑠OLD⁡UB+v⁡UA=-1⋅𝑠OLD⁡WT⁡B+v⁡WT⁡A
14 1 7 9 2 nvmval2 ⊢U∈NrmCVec∧A∈X∧B∈X→AMB=-1⋅𝑠OLD⁡UB+v⁡UA
15 14 3expb ⊢U∈NrmCVec∧A∈X∧B∈X→AMB=-1⋅𝑠OLD⁡UB+v⁡UA
16 15 3ad2antl1 ⊢U∈NrmCVec∧W∈NrmCVec∧T∈L∧A∈X∧B∈X→AMB=-1⋅𝑠OLD⁡UB+v⁡UA
17 16 fveq2d ⊢U∈NrmCVec∧W∈NrmCVec∧T∈L∧A∈X∧B∈X→T⁡AMB=T⁡-1⋅𝑠OLD⁡UB+v⁡UA
18 simpl2 ⊢U∈NrmCVec∧W∈NrmCVec∧T∈L∧A∈X∧B∈X→W∈NrmCVec
19 1 6 4 lnof ⊢U∈NrmCVec∧W∈NrmCVec∧T∈L→T:X⟶BaseSet⁡W
20 simpl ⊢A∈X∧B∈X→A∈X
21 ffvelcdm ⊢T:X⟶BaseSet⁡W∧A∈X→T⁡A∈BaseSet⁡W
22 19 20 21 syl2an ⊢U∈NrmCVec∧W∈NrmCVec∧T∈L∧A∈X∧B∈X→T⁡A∈BaseSet⁡W
23 simpr ⊢A∈X∧B∈X→B∈X
24 ffvelcdm ⊢T:X⟶BaseSet⁡W∧B∈X→T⁡B∈BaseSet⁡W
25 19 23 24 syl2an ⊢U∈NrmCVec∧W∈NrmCVec∧T∈L∧A∈X∧B∈X→T⁡B∈BaseSet⁡W
26 6 8 10 3 nvmval2 ⊢W∈NrmCVec∧T⁡A∈BaseSet⁡W∧T⁡B∈BaseSet⁡W→T⁡ANT⁡B=-1⋅𝑠OLD⁡WT⁡B+v⁡WT⁡A
27 18 22 25 26 syl3anc ⊢U∈NrmCVec∧W∈NrmCVec∧T∈L∧A∈X∧B∈X→T⁡ANT⁡B=-1⋅𝑠OLD⁡WT⁡B+v⁡WT⁡A
28 13 17 27 3eqtr4d ⊢U∈NrmCVec∧W∈NrmCVec∧T∈L∧A∈X∧B∈X→T⁡AMB=T⁡ANT⁡B