HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  nlelshi Structured version   Visualization version   GIF version

Theorem nlelshi 31051
Description: The null space of a linear functional is a subspace. (Contributed by NM, 11-Feb-2006.) (Revised by Mario Carneiro, 17-Nov-2013.) (New usage is discouraged.)
Hypothesis
Ref Expression
nlelsh.1 𝑇 ∈ LinFn
Assertion
Ref Expression
nlelshi (nullβ€˜π‘‡) ∈ Sβ„‹

Proof of Theorem nlelshi
Dummy variables π‘₯ 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ax-hv0cl 29994 . . 3 0β„Ž ∈ β„‹
2 nlelsh.1 . . . 4 𝑇 ∈ LinFn
32lnfn0i 31033 . . 3 (π‘‡β€˜0β„Ž) = 0
42lnfnfi 31032 . . . 4 𝑇: β„‹βŸΆβ„‚
5 elnlfn 30919 . . . 4 (𝑇: β„‹βŸΆβ„‚ β†’ (0β„Ž ∈ (nullβ€˜π‘‡) ↔ (0β„Ž ∈ β„‹ ∧ (π‘‡β€˜0β„Ž) = 0)))
64, 5ax-mp 5 . . 3 (0β„Ž ∈ (nullβ€˜π‘‡) ↔ (0β„Ž ∈ β„‹ ∧ (π‘‡β€˜0β„Ž) = 0))
71, 3, 6mpbir2an 710 . 2 0β„Ž ∈ (nullβ€˜π‘‡)
8 nlfnval 30872 . . . . . . . . . 10 (𝑇: β„‹βŸΆβ„‚ β†’ (nullβ€˜π‘‡) = (◑𝑇 β€œ {0}))
94, 8ax-mp 5 . . . . . . . . 9 (nullβ€˜π‘‡) = (◑𝑇 β€œ {0})
10 cnvimass 6037 . . . . . . . . 9 (◑𝑇 β€œ {0}) βŠ† dom 𝑇
119, 10eqsstri 3982 . . . . . . . 8 (nullβ€˜π‘‡) βŠ† dom 𝑇
124fdmi 6684 . . . . . . . 8 dom 𝑇 = β„‹
1311, 12sseqtri 3984 . . . . . . 7 (nullβ€˜π‘‡) βŠ† β„‹
1413sseli 3944 . . . . . 6 (π‘₯ ∈ (nullβ€˜π‘‡) β†’ π‘₯ ∈ β„‹)
1513sseli 3944 . . . . . 6 (𝑦 ∈ (nullβ€˜π‘‡) β†’ 𝑦 ∈ β„‹)
16 hvaddcl 30003 . . . . . 6 ((π‘₯ ∈ β„‹ ∧ 𝑦 ∈ β„‹) β†’ (π‘₯ +β„Ž 𝑦) ∈ β„‹)
1714, 15, 16syl2an 597 . . . . 5 ((π‘₯ ∈ (nullβ€˜π‘‡) ∧ 𝑦 ∈ (nullβ€˜π‘‡)) β†’ (π‘₯ +β„Ž 𝑦) ∈ β„‹)
182lnfnaddi 31034 . . . . . . . 8 ((π‘₯ ∈ β„‹ ∧ 𝑦 ∈ β„‹) β†’ (π‘‡β€˜(π‘₯ +β„Ž 𝑦)) = ((π‘‡β€˜π‘₯) + (π‘‡β€˜π‘¦)))
1914, 15, 18syl2an 597 . . . . . . 7 ((π‘₯ ∈ (nullβ€˜π‘‡) ∧ 𝑦 ∈ (nullβ€˜π‘‡)) β†’ (π‘‡β€˜(π‘₯ +β„Ž 𝑦)) = ((π‘‡β€˜π‘₯) + (π‘‡β€˜π‘¦)))
20 elnlfn 30919 . . . . . . . . . 10 (𝑇: β„‹βŸΆβ„‚ β†’ (π‘₯ ∈ (nullβ€˜π‘‡) ↔ (π‘₯ ∈ β„‹ ∧ (π‘‡β€˜π‘₯) = 0)))
214, 20ax-mp 5 . . . . . . . . 9 (π‘₯ ∈ (nullβ€˜π‘‡) ↔ (π‘₯ ∈ β„‹ ∧ (π‘‡β€˜π‘₯) = 0))
2221simprbi 498 . . . . . . . 8 (π‘₯ ∈ (nullβ€˜π‘‡) β†’ (π‘‡β€˜π‘₯) = 0)
23 elnlfn 30919 . . . . . . . . . 10 (𝑇: β„‹βŸΆβ„‚ β†’ (𝑦 ∈ (nullβ€˜π‘‡) ↔ (𝑦 ∈ β„‹ ∧ (π‘‡β€˜π‘¦) = 0)))
244, 23ax-mp 5 . . . . . . . . 9 (𝑦 ∈ (nullβ€˜π‘‡) ↔ (𝑦 ∈ β„‹ ∧ (π‘‡β€˜π‘¦) = 0))
2524simprbi 498 . . . . . . . 8 (𝑦 ∈ (nullβ€˜π‘‡) β†’ (π‘‡β€˜π‘¦) = 0)
2622, 25oveqan12d 7380 . . . . . . 7 ((π‘₯ ∈ (nullβ€˜π‘‡) ∧ 𝑦 ∈ (nullβ€˜π‘‡)) β†’ ((π‘‡β€˜π‘₯) + (π‘‡β€˜π‘¦)) = (0 + 0))
2719, 26eqtrd 2773 . . . . . 6 ((π‘₯ ∈ (nullβ€˜π‘‡) ∧ 𝑦 ∈ (nullβ€˜π‘‡)) β†’ (π‘‡β€˜(π‘₯ +β„Ž 𝑦)) = (0 + 0))
28 00id 11338 . . . . . 6 (0 + 0) = 0
2927, 28eqtrdi 2789 . . . . 5 ((π‘₯ ∈ (nullβ€˜π‘‡) ∧ 𝑦 ∈ (nullβ€˜π‘‡)) β†’ (π‘‡β€˜(π‘₯ +β„Ž 𝑦)) = 0)
30 elnlfn 30919 . . . . . 6 (𝑇: β„‹βŸΆβ„‚ β†’ ((π‘₯ +β„Ž 𝑦) ∈ (nullβ€˜π‘‡) ↔ ((π‘₯ +β„Ž 𝑦) ∈ β„‹ ∧ (π‘‡β€˜(π‘₯ +β„Ž 𝑦)) = 0)))
314, 30ax-mp 5 . . . . 5 ((π‘₯ +β„Ž 𝑦) ∈ (nullβ€˜π‘‡) ↔ ((π‘₯ +β„Ž 𝑦) ∈ β„‹ ∧ (π‘‡β€˜(π‘₯ +β„Ž 𝑦)) = 0))
3217, 29, 31sylanbrc 584 . . . 4 ((π‘₯ ∈ (nullβ€˜π‘‡) ∧ 𝑦 ∈ (nullβ€˜π‘‡)) β†’ (π‘₯ +β„Ž 𝑦) ∈ (nullβ€˜π‘‡))
3332rgen2 3191 . . 3 βˆ€π‘₯ ∈ (nullβ€˜π‘‡)βˆ€π‘¦ ∈ (nullβ€˜π‘‡)(π‘₯ +β„Ž 𝑦) ∈ (nullβ€˜π‘‡)
34 hvmulcl 30004 . . . . . 6 ((π‘₯ ∈ β„‚ ∧ 𝑦 ∈ β„‹) β†’ (π‘₯ Β·β„Ž 𝑦) ∈ β„‹)
3515, 34sylan2 594 . . . . 5 ((π‘₯ ∈ β„‚ ∧ 𝑦 ∈ (nullβ€˜π‘‡)) β†’ (π‘₯ Β·β„Ž 𝑦) ∈ β„‹)
362lnfnmuli 31035 . . . . . . 7 ((π‘₯ ∈ β„‚ ∧ 𝑦 ∈ β„‹) β†’ (π‘‡β€˜(π‘₯ Β·β„Ž 𝑦)) = (π‘₯ Β· (π‘‡β€˜π‘¦)))
3715, 36sylan2 594 . . . . . 6 ((π‘₯ ∈ β„‚ ∧ 𝑦 ∈ (nullβ€˜π‘‡)) β†’ (π‘‡β€˜(π‘₯ Β·β„Ž 𝑦)) = (π‘₯ Β· (π‘‡β€˜π‘¦)))
3825oveq2d 7377 . . . . . . 7 (𝑦 ∈ (nullβ€˜π‘‡) β†’ (π‘₯ Β· (π‘‡β€˜π‘¦)) = (π‘₯ Β· 0))
39 mul01 11342 . . . . . . 7 (π‘₯ ∈ β„‚ β†’ (π‘₯ Β· 0) = 0)
4038, 39sylan9eqr 2795 . . . . . 6 ((π‘₯ ∈ β„‚ ∧ 𝑦 ∈ (nullβ€˜π‘‡)) β†’ (π‘₯ Β· (π‘‡β€˜π‘¦)) = 0)
4137, 40eqtrd 2773 . . . . 5 ((π‘₯ ∈ β„‚ ∧ 𝑦 ∈ (nullβ€˜π‘‡)) β†’ (π‘‡β€˜(π‘₯ Β·β„Ž 𝑦)) = 0)
42 elnlfn 30919 . . . . . 6 (𝑇: β„‹βŸΆβ„‚ β†’ ((π‘₯ Β·β„Ž 𝑦) ∈ (nullβ€˜π‘‡) ↔ ((π‘₯ Β·β„Ž 𝑦) ∈ β„‹ ∧ (π‘‡β€˜(π‘₯ Β·β„Ž 𝑦)) = 0)))
434, 42ax-mp 5 . . . . 5 ((π‘₯ Β·β„Ž 𝑦) ∈ (nullβ€˜π‘‡) ↔ ((π‘₯ Β·β„Ž 𝑦) ∈ β„‹ ∧ (π‘‡β€˜(π‘₯ Β·β„Ž 𝑦)) = 0))
4435, 41, 43sylanbrc 584 . . . 4 ((π‘₯ ∈ β„‚ ∧ 𝑦 ∈ (nullβ€˜π‘‡)) β†’ (π‘₯ Β·β„Ž 𝑦) ∈ (nullβ€˜π‘‡))
4544rgen2 3191 . . 3 βˆ€π‘₯ ∈ β„‚ βˆ€π‘¦ ∈ (nullβ€˜π‘‡)(π‘₯ Β·β„Ž 𝑦) ∈ (nullβ€˜π‘‡)
4633, 45pm3.2i 472 . 2 (βˆ€π‘₯ ∈ (nullβ€˜π‘‡)βˆ€π‘¦ ∈ (nullβ€˜π‘‡)(π‘₯ +β„Ž 𝑦) ∈ (nullβ€˜π‘‡) ∧ βˆ€π‘₯ ∈ β„‚ βˆ€π‘¦ ∈ (nullβ€˜π‘‡)(π‘₯ Β·β„Ž 𝑦) ∈ (nullβ€˜π‘‡))
47 issh3 30210 . . 3 ((nullβ€˜π‘‡) βŠ† β„‹ β†’ ((nullβ€˜π‘‡) ∈ Sβ„‹ ↔ (0β„Ž ∈ (nullβ€˜π‘‡) ∧ (βˆ€π‘₯ ∈ (nullβ€˜π‘‡)βˆ€π‘¦ ∈ (nullβ€˜π‘‡)(π‘₯ +β„Ž 𝑦) ∈ (nullβ€˜π‘‡) ∧ βˆ€π‘₯ ∈ β„‚ βˆ€π‘¦ ∈ (nullβ€˜π‘‡)(π‘₯ Β·β„Ž 𝑦) ∈ (nullβ€˜π‘‡)))))
4813, 47ax-mp 5 . 2 ((nullβ€˜π‘‡) ∈ Sβ„‹ ↔ (0β„Ž ∈ (nullβ€˜π‘‡) ∧ (βˆ€π‘₯ ∈ (nullβ€˜π‘‡)βˆ€π‘¦ ∈ (nullβ€˜π‘‡)(π‘₯ +β„Ž 𝑦) ∈ (nullβ€˜π‘‡) ∧ βˆ€π‘₯ ∈ β„‚ βˆ€π‘¦ ∈ (nullβ€˜π‘‡)(π‘₯ Β·β„Ž 𝑦) ∈ (nullβ€˜π‘‡))))
497, 46, 48mpbir2an 710 1 (nullβ€˜π‘‡) ∈ Sβ„‹
Colors of variables: wff setvar class
Syntax hints:   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107  βˆ€wral 3061   βŠ† wss 3914  {csn 4590  β—‘ccnv 5636  dom cdm 5637   β€œ cima 5640  βŸΆwf 6496  β€˜cfv 6500  (class class class)co 7361  β„‚cc 11057  0cc0 11059   + caddc 11062   Β· cmul 11064   β„‹chba 29910   +β„Ž cva 29911   Β·β„Ž csm 29912  0β„Žc0v 29915   Sβ„‹ csh 29919  nullcnl 29943  LinFnclf 29945
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5260  ax-nul 5267  ax-pow 5324  ax-pr 5388  ax-un 7676  ax-cnex 11115  ax-resscn 11116  ax-1cn 11117  ax-icn 11118  ax-addcl 11119  ax-addrcl 11120  ax-mulcl 11121  ax-mulrcl 11122  ax-mulcom 11123  ax-addass 11124  ax-mulass 11125  ax-distr 11126  ax-i2m1 11127  ax-1ne0 11128  ax-1rid 11129  ax-rnegex 11130  ax-rrecex 11131  ax-cnre 11132  ax-pre-lttri 11133  ax-pre-lttrn 11134  ax-pre-ltadd 11135  ax-hilex 29990  ax-hfvadd 29991  ax-hv0cl 29994  ax-hvaddid 29995  ax-hfvmul 29996  ax-hvmulid 29997
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3353  df-rab 3407  df-v 3449  df-sbc 3744  df-csb 3860  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4287  df-if 4491  df-pw 4566  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4870  df-iun 4960  df-br 5110  df-opab 5172  df-mpt 5193  df-id 5535  df-po 5549  df-so 5550  df-xp 5643  df-rel 5644  df-cnv 5645  df-co 5646  df-dm 5647  df-rn 5648  df-res 5649  df-ima 5650  df-iota 6452  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-riota 7317  df-ov 7364  df-oprab 7365  df-mpo 7366  df-er 8654  df-map 8773  df-en 8890  df-dom 8891  df-sdom 8892  df-pnf 11199  df-mnf 11200  df-ltxr 11202  df-sub 11395  df-sh 30198  df-nlfn 30837  df-lnfn 30839
This theorem is referenced by:  nlelchi  31052
  Copyright terms: Public domain W3C validator