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 30844

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

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1092 = wceq 1547 ∈ wcel 2119 ∀wral 3053 ⟶wf 6481 ‘cfv 6485 (class class class)co 7356 ℂcc 11027 NrmCVeccnv 30673 +_𝑣 cpv 30674 BaseSetcba 30675 ·_𝑠OLD cns 30676 LnOp clno 30829

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-10 2152 ax-11 2168 ax-12 2189 ax-ext 2711 ax-sep 5218 ax-nul 5228 ax-pow 5294 ax-pr 5362 ax-un 7678

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2543 df-eu 2573 df-clab 2718 df-cleq 2731 df-clel 2814 df-nfc 2888 df-ne 2935 df-ral 3054 df-rex 3064 df-rab 3392 df-v 3433 df-sbc 3724 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-nul 4262 df-if 4455 df-pw 4531 df-sn 4556 df-pr 4558 df-op 4562 df-uni 4839 df-br 5073 df-opab 5135 df-id 5513 df-xp 5624 df-rel 5625 df-cnv 5626 df-co 5627 df-dm 5628 df-rn 5629 df-iota 6441 df-fun 6487 df-fn 6488 df-f 6489 df-fv 6493 df-ov 7359 df-oprab 7360 df-mpo 7361 df-map 8765 df-lno 30833

This theorem is referenced by: lno0 30845 lnocoi 30846 lnoadd 30847 lnosub 30848 lnomul 30849 isblo2 30872 blof 30874 nmlno0lem 30882 nmlnoubi 30885 nmlnogt0 30886 lnon0 30887 isblo3i 30890 blocnilem 30893 blocni 30894 htthlem 31006

W3C validator