lnof - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > lnof		Structured version Visualization version GIF version

Theorem lnof 30685

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

**Hypotheses**
Ref	Expression
lnof.1	⊢ 𝑋 = (BaseSet‘𝑈)
lnof.2	⊢ 𝑌 = (BaseSet‘𝑊)
lnof.7	⊢ 𝐿 = (𝑈 LnOp 𝑊)

**Assertion**
Ref	Expression
lnof	⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) → 𝑇:𝑋⟶𝑌)

Proof of Theorem lnof Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

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

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 394 ∧ w3a 1084 = wceq 1534 ∈ wcel 2100 ∀wral 3054 ⟶wf 6552 ‘cfv 6556 (class class class)co 7427 ℂcc 11157 NrmCVeccnv 30514 +_𝑣 cpv 30515 BaseSetcba 30516 ·_𝑠OLD cns 30517 LnOp clno 30670

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2102 ax-9 2110 ax-10 2133 ax-11 2150 ax-12 2170 ax-ext 2700 ax-sep 5305 ax-nul 5312 ax-pow 5371 ax-pr 5435 ax-un 7748

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2062 df-mo 2532 df-eu 2561 df-clab 2707 df-cleq 2721 df-clel 2806 df-nfc 2881 df-ne 2934 df-ral 3055 df-rex 3064 df-rab 3429 df-v 3474 df-sbc 3788 df-dif 3961 df-un 3963 df-in 3965 df-ss 3975 df-nul 4334 df-if 4535 df-pw 4610 df-sn 4635 df-pr 4637 df-op 4641 df-uni 4917 df-br 5155 df-opab 5217 df-id 5582 df-xp 5690 df-rel 5691 df-cnv 5692 df-co 5693 df-dm 5694 df-rn 5695 df-iota 6508 df-fun 6558 df-fn 6559 df-f 6560 df-fv 6564 df-ov 7430 df-oprab 7431 df-mpo 7432 df-map 8861 df-lno 30674

This theorem is referenced by: lno0 30686 lnocoi 30687 lnoadd 30688 lnosub 30689 lnomul 30690 isblo2 30713 blof 30715 nmlno0lem 30723 nmlnoubi 30726 nmlnogt0 30727 lnon0 30728 isblo3i 30731 blocnilem 30734 blocni 30735 htthlem 30847

W3C validator