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 ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T ∈ L ∧ A ∈ X ∧ B ∈ 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 ∈ ℂ
6 eqid ⊢ BaseSet ⁡ W = BaseSet ⁡ W
7 eqid ⊢ ⋅ 𝑠OLD ⁡ U = ⋅ 𝑠OLD ⁡ U
8 eqid ⊢ ⋅ 𝑠OLD ⁡ W = ⋅ 𝑠OLD ⁡ W
9 1 6 2 3 7 8 4 lnolin ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T ∈ L ∧ 1 ∈ ℂ ∧ A ∈ X ∧ B ∈ X → T ⁡ 1 ⋅ 𝑠OLD ⁡ U A G B = 1 ⋅ 𝑠OLD ⁡ W T ⁡ A H T ⁡ B
10 5 9 mp3anr1 ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T ∈ L ∧ A ∈ X ∧ B ∈ X → T ⁡ 1 ⋅ 𝑠OLD ⁡ U A G B = 1 ⋅ 𝑠OLD ⁡ W T ⁡ A H T ⁡ B
11 simp1 ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T ∈ L → U ∈ NrmCVec
12 simpl ⊢ A ∈ X ∧ B ∈ X → A ∈ X
13 1 7 nvsid ⊢ U ∈ NrmCVec ∧ A ∈ X → 1 ⋅ 𝑠OLD ⁡ U A = A
14 11 12 13 syl2an ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T ∈ L ∧ A ∈ X ∧ B ∈ X → 1 ⋅ 𝑠OLD ⁡ U A = A
15 14 fvoveq1d ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T ∈ L ∧ A ∈ X ∧ B ∈ X → T ⁡ 1 ⋅ 𝑠OLD ⁡ U A G B = T ⁡ A G B
16 simpl2 ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T ∈ L ∧ A ∈ X ∧ B ∈ X → W ∈ NrmCVec
17 1 6 4 lnof ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T ∈ L → T : X ⟶ BaseSet ⁡ W
18 ffvelrn ⊢ T : X ⟶ BaseSet ⁡ W ∧ A ∈ X → T ⁡ A ∈ BaseSet ⁡ W
19 17 12 18 syl2an ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T ∈ L ∧ A ∈ X ∧ B ∈ X → T ⁡ A ∈ BaseSet ⁡ W
20 6 8 nvsid ⊢ W ∈ NrmCVec ∧ T ⁡ A ∈ BaseSet ⁡ W → 1 ⋅ 𝑠OLD ⁡ W T ⁡ A = T ⁡ A
21 16 19 20 syl2anc ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T ∈ L ∧ A ∈ X ∧ B ∈ X → 1 ⋅ 𝑠OLD ⁡ W T ⁡ A = T ⁡ A
22 21 oveq1d ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T ∈ L ∧ A ∈ X ∧ B ∈ X → 1 ⋅ 𝑠OLD ⁡ W T ⁡ A H T ⁡ B = T ⁡ A H T ⁡ B
23 10 15 22 3eqtr3d ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T ∈ L ∧ A ∈ X ∧ B ∈ X → T ⁡ A G B = T ⁡ A H T ⁡ B