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 29162

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 2736	. . . 4 ⊢ ( +_𝑣 ‘𝑈) = ( +_𝑣 ‘𝑈)
4		eqid 2736	. . . 4 ⊢ ( +_𝑣 ‘𝑊) = ( +_𝑣 ‘𝑊)
5		eqid 2736	. . . 4 ⊢ ( ·_𝑠OLD ‘𝑈) = ( ·_𝑠OLD ‘𝑈)
6		eqid 2736	. . . 4 ⊢ ( ·_𝑠OLD ‘𝑊) = ( ·_𝑠OLD ‘𝑊)
7		lnof.7	. . . 4 ⊢ 𝐿 = (𝑈 LnOp 𝑊)
8	1, 2, 3, 4, 5, 6, 7	islno 29160	. . 3 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → (𝑇 ∈ 𝐿 ↔ (𝑇:𝑋⟶𝑌 ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑇‘((𝑥( ·_𝑠OLD ‘𝑈)𝑦)( +_𝑣 ‘𝑈)𝑧)) = ((𝑥( ·_𝑠OLD ‘𝑊)(𝑇‘𝑦))( +_𝑣 ‘𝑊)(𝑇‘𝑧)))))
9	8	simprbda 500	. 2 ⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) ∧ 𝑇 ∈ 𝐿) → 𝑇:𝑋⟶𝑌)
10	9	3impa 1110	1 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) → 𝑇:𝑋⟶𝑌)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 397 ∧ w3a 1087 = wceq 1539 ∈ wcel 2104 ∀wral 3062 ⟶wf 6454 ‘cfv 6458 (class class class)co 7307 ℂcc 10915 NrmCVeccnv 28991 +_𝑣 cpv 28992 BaseSetcba 28993 ·_𝑠OLD cns 28994 LnOp clno 29147

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 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2707 ax-sep 5232 ax-nul 5239 ax-pow 5297 ax-pr 5361 ax-un 7620

This theorem depends on definitions: df-bi 206 df-an 398 df-or 846 df-3an 1089 df-tru 1542 df-fal 1552 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2887 df-ne 2942 df-ral 3063 df-rex 3072 df-rab 3287 df-v 3439 df-sbc 3722 df-dif 3895 df-un 3897 df-in 3899 df-ss 3909 df-nul 4263 df-if 4466 df-pw 4541 df-sn 4566 df-pr 4568 df-op 4572 df-uni 4845 df-br 5082 df-opab 5144 df-id 5500 df-xp 5606 df-rel 5607 df-cnv 5608 df-co 5609 df-dm 5610 df-rn 5611 df-iota 6410 df-fun 6460 df-fn 6461 df-f 6462 df-fv 6466 df-ov 7310 df-oprab 7311 df-mpo 7312 df-map 8648 df-lno 29151

This theorem is referenced by: lno0 29163 lnocoi 29164 lnoadd 29165 lnosub 29166 lnomul 29167 isblo2 29190 blof 29192 nmlno0lem 29200 nmlnoubi 29203 nmlnogt0 29204 lnon0 29205 isblo3i 29208 blocnilem 29211 blocni 29212 htthlem 29324

W3C validator