Metamath Proof Explorer

Theorem lnof

Description: A linear operator is a mapping. (Contributed by NM, 4-Dec-2007) (Revised by Mario Carneiro, 18-Nov-2013) (New usage is discouraged.)

Ref Expression
Hypotheses lnof.1 ⊢ X = BaseSet ⁡ U
lnof.2 ⊢ Y = BaseSet ⁡ W
lnof.7 ⊢ L = U LnOp W
Assertion lnof ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T ∈ L → T : X ⟶ Y

Proof

Step Hyp Ref Expression
1 lnof.1 ⊢ X = BaseSet ⁡ U
2 lnof.2 ⊢ Y = BaseSet ⁡ W
3 lnof.7 ⊢ L = U LnOp W
4 eqid ⊢ + v ⁡ U = + v ⁡ U
5 eqid ⊢ + v ⁡ W = + v ⁡ W
6 eqid ⊢ ⋅ 𝑠OLD ⁡ U = ⋅ 𝑠OLD ⁡ U
7 eqid ⊢ ⋅ 𝑠OLD ⁡ W = ⋅ 𝑠OLD ⁡ W
8 1 2 4 5 6 7 3 islno ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec → T ∈ L ↔ T : X ⟶ Y ∧ ∀ x ∈ ℂ ∀ y ∈ X ∀ z ∈ X T ⁡ x ⋅ 𝑠OLD ⁡ U y + v ⁡ U z = x ⋅ 𝑠OLD ⁡ W T ⁡ y + v ⁡ W T ⁡ z
9 8 simprbda ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T ∈ L → T : X ⟶ Y
10 9 3impa ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T ∈ L → T : X ⟶ Y