This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
lnof.2 ⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
lnof.7 ⊢ 𝐿 = ( 𝑈 LnOp 𝑊 )
Assertion lnof ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) → 𝑇 : 𝑋 ⟶ 𝑌 )

Proof

Step Hyp Ref Expression
1 lnof.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 lnof.2 ⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
3 lnof.7 ⊢ 𝐿 = ( 𝑈 LnOp 𝑊 )
4 eqid ⊢ ( +𝑣 ‘ 𝑈 ) = ( +𝑣 ‘ 𝑈 )
5 eqid ⊢ ( +𝑣 ‘ 𝑊 ) = ( +𝑣 ‘ 𝑊 )
6 eqid ⊢ ( ·𝑠OLD ‘ 𝑈 ) = ( ·𝑠OLD ‘ 𝑈 )
7 eqid ⊢ ( ·𝑠OLD ‘ 𝑊 ) = ( ·𝑠OLD ‘ 𝑊 )
8 1 2 4 5 6 7 3 islno ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → ( 𝑇 ∈ 𝐿 ↔ ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑇 ‘ ( ( 𝑥 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ( +𝑣 ‘ 𝑈 ) 𝑧 ) ) = ( ( 𝑥 ( ·𝑠OLD ‘ 𝑊 ) ( 𝑇 ‘ 𝑦 ) ) ( +𝑣 ‘ 𝑊 ) ( 𝑇 ‘ 𝑧 ) ) ) ) )
9 8 simprbda ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) ∧ 𝑇 ∈ 𝐿 ) → 𝑇 : 𝑋 ⟶ 𝑌 )
10 9 3impa ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) → 𝑇 : 𝑋 ⟶ 𝑌 )