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 30684

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 30682	. . 3 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → (𝑇 ∈ 𝐿 ↔ (𝑇:𝑋⟶𝑌 ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑇‘((𝑥( ·_𝑠OLD ‘𝑈)𝑦)( +_𝑣 ‘𝑈)𝑧)) = ((𝑥( ·_𝑠OLD ‘𝑊)(𝑇‘𝑦))( +_𝑣 ‘𝑊)(𝑇‘𝑧)))))
9	8	simprbda 498	. 2 ⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) ∧ 𝑇 ∈ 𝐿) → 𝑇:𝑋⟶𝑌)
10	9	3impa 1109	1 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) → 𝑇:𝑋⟶𝑌)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ∀wral 3044 ⟶wf 6507 ‘cfv 6511 (class class class)co 7387 ℂcc 11066 NrmCVeccnv 30513 +_𝑣 cpv 30514 BaseSetcba 30515 ·_𝑠OLD cns 30516 LnOp clno 30669

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-sep 5251 ax-nul 5261 ax-pow 5320 ax-pr 5387 ax-un 7711

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-ral 3045 df-rex 3054 df-rab 3406 df-v 3449 df-sbc 3754 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-nul 4297 df-if 4489 df-pw 4565 df-sn 4590 df-pr 4592 df-op 4596 df-uni 4872 df-br 5108 df-opab 5170 df-id 5533 df-xp 5644 df-rel 5645 df-cnv 5646 df-co 5647 df-dm 5648 df-rn 5649 df-iota 6464 df-fun 6513 df-fn 6514 df-f 6515 df-fv 6519 df-ov 7390 df-oprab 7391 df-mpo 7392 df-map 8801 df-lno 30673

This theorem is referenced by: lno0 30685 lnocoi 30686 lnoadd 30687 lnosub 30688 lnomul 30689 isblo2 30712 blof 30714 nmlno0lem 30722 nmlnoubi 30725 nmlnogt0 30726 lnon0 30727 isblo3i 30730 blocnilem 30733 blocni 30734 htthlem 30846

W3C validator