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