# 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 ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T ∈ L ∧ A ∈ X ∧ B ∈ 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 $⊢ − 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 ⁡ U B + v ⁡ U A = -1 ⋅ 𝑠OLD ⁡ W T ⁡ B + v ⁡ W T ⁡ A$
12 5 11 mp3anr1 $⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T ∈ L ∧ B ∈ X ∧ A ∈ X → T ⁡ -1 ⋅ 𝑠OLD ⁡ U B + v ⁡ U A = -1 ⋅ 𝑠OLD ⁡ W T ⁡ B + v ⁡ W T ⁡ A$
13 12 ancom2s $⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T ∈ L ∧ A ∈ X ∧ B ∈ X → T ⁡ -1 ⋅ 𝑠OLD ⁡ U B + v ⁡ U A = -1 ⋅ 𝑠OLD ⁡ W T ⁡ B + v ⁡ W T ⁡ A$
14 1 7 9 2 nvmval2 $⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A M B = -1 ⋅ 𝑠OLD ⁡ U B + v ⁡ U A$
15 14 3expb $⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A M B = -1 ⋅ 𝑠OLD ⁡ U B + v ⁡ U A$
16 15 3ad2antl1 $⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T ∈ L ∧ A ∈ X ∧ B ∈ X → A M B = -1 ⋅ 𝑠OLD ⁡ U B + v ⁡ U A$
17 16 fveq2d $⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T ∈ L ∧ A ∈ X ∧ B ∈ X → T ⁡ A M B = T ⁡ -1 ⋅ 𝑠OLD ⁡ U B + v ⁡ U A$
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 ffvelrn $⊢ 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 ffvelrn $⊢ 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 ⁡ A N T ⁡ B = -1 ⋅ 𝑠OLD ⁡ W T ⁡ B + v ⁡ W T ⁡ A$
27 18 22 25 26 syl3anc $⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T ∈ L ∧ A ∈ X ∧ B ∈ X → T ⁡ A N T ⁡ B = -1 ⋅ 𝑠OLD ⁡ W T ⁡ B + v ⁡ W T ⁡ A$
28 13 17 27 3eqtr4d $⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T ∈ L ∧ A ∈ X ∧ B ∈ X → T ⁡ A M B = T ⁡ A N T ⁡ B$