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

Theorem imaelshi 30799
Description: The image of a subspace under a linear operator is a subspace. (Contributed by Mario Carneiro, 19-May-2014.) (New usage is discouraged.)
Hypotheses
Ref Expression
rnelsh.1 ๐‘‡ โˆˆ LinOp
imaelsh.2 ๐ด โˆˆ Sโ„‹
Assertion
Ref Expression
imaelshi (๐‘‡ โ€œ ๐ด) โˆˆ Sโ„‹

Proof of Theorem imaelshi
Dummy variables ๐‘ฃ ๐‘ข ๐‘ฅ ๐‘ฆ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 imassrn 6021 . . . 4 (๐‘‡ โ€œ ๐ด) โŠ† ran ๐‘‡
2 rnelsh.1 . . . . . 6 ๐‘‡ โˆˆ LinOp
32lnopfi 30710 . . . . 5 ๐‘‡: โ„‹โŸถ โ„‹
4 frn 6671 . . . . 5 (๐‘‡: โ„‹โŸถ โ„‹ โ†’ ran ๐‘‡ โŠ† โ„‹)
53, 4ax-mp 5 . . . 4 ran ๐‘‡ โŠ† โ„‹
61, 5sstri 3952 . . 3 (๐‘‡ โ€œ ๐ด) โŠ† โ„‹
72lnop0i 30711 . . . 4 (๐‘‡โ€˜0โ„Ž) = 0โ„Ž
8 imaelsh.2 . . . . . 6 ๐ด โˆˆ Sโ„‹
9 sh0 29957 . . . . . 6 (๐ด โˆˆ Sโ„‹ โ†’ 0โ„Ž โˆˆ ๐ด)
108, 9ax-mp 5 . . . . 5 0โ„Ž โˆˆ ๐ด
11 ffun 6667 . . . . . . 7 (๐‘‡: โ„‹โŸถ โ„‹ โ†’ Fun ๐‘‡)
123, 11ax-mp 5 . . . . . 6 Fun ๐‘‡
138shssii 29954 . . . . . . 7 ๐ด โŠ† โ„‹
143fdmi 6676 . . . . . . 7 dom ๐‘‡ = โ„‹
1513, 14sseqtrri 3980 . . . . . 6 ๐ด โŠ† dom ๐‘‡
16 funfvima2 7176 . . . . . 6 ((Fun ๐‘‡ โˆง ๐ด โŠ† dom ๐‘‡) โ†’ (0โ„Ž โˆˆ ๐ด โ†’ (๐‘‡โ€˜0โ„Ž) โˆˆ (๐‘‡ โ€œ ๐ด)))
1712, 15, 16mp2an 691 . . . . 5 (0โ„Ž โˆˆ ๐ด โ†’ (๐‘‡โ€˜0โ„Ž) โˆˆ (๐‘‡ โ€œ ๐ด))
1810, 17ax-mp 5 . . . 4 (๐‘‡โ€˜0โ„Ž) โˆˆ (๐‘‡ โ€œ ๐ด)
197, 18eqeltrri 2836 . . 3 0โ„Ž โˆˆ (๐‘‡ โ€œ ๐ด)
206, 19pm3.2i 472 . 2 ((๐‘‡ โ€œ ๐ด) โŠ† โ„‹ โˆง 0โ„Ž โˆˆ (๐‘‡ โ€œ ๐ด))
21 ffn 6664 . . . . . 6 (๐‘‡: โ„‹โŸถ โ„‹ โ†’ ๐‘‡ Fn โ„‹)
223, 21ax-mp 5 . . . . 5 ๐‘‡ Fn โ„‹
23 oveq1 7357 . . . . . . . 8 (๐‘ข = (๐‘‡โ€˜๐‘ฅ) โ†’ (๐‘ข +โ„Ž ๐‘ฃ) = ((๐‘‡โ€˜๐‘ฅ) +โ„Ž ๐‘ฃ))
2423eleq1d 2823 . . . . . . 7 (๐‘ข = (๐‘‡โ€˜๐‘ฅ) โ†’ ((๐‘ข +โ„Ž ๐‘ฃ) โˆˆ (๐‘‡ โ€œ ๐ด) โ†” ((๐‘‡โ€˜๐‘ฅ) +โ„Ž ๐‘ฃ) โˆˆ (๐‘‡ โ€œ ๐ด)))
2524ralbidv 3173 . . . . . 6 (๐‘ข = (๐‘‡โ€˜๐‘ฅ) โ†’ (โˆ€๐‘ฃ โˆˆ (๐‘‡ โ€œ ๐ด)(๐‘ข +โ„Ž ๐‘ฃ) โˆˆ (๐‘‡ โ€œ ๐ด) โ†” โˆ€๐‘ฃ โˆˆ (๐‘‡ โ€œ ๐ด)((๐‘‡โ€˜๐‘ฅ) +โ„Ž ๐‘ฃ) โˆˆ (๐‘‡ โ€œ ๐ด)))
2625ralima 7183 . . . . 5 ((๐‘‡ Fn โ„‹ โˆง ๐ด โŠ† โ„‹) โ†’ (โˆ€๐‘ข โˆˆ (๐‘‡ โ€œ ๐ด)โˆ€๐‘ฃ โˆˆ (๐‘‡ โ€œ ๐ด)(๐‘ข +โ„Ž ๐‘ฃ) โˆˆ (๐‘‡ โ€œ ๐ด) โ†” โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฃ โˆˆ (๐‘‡ โ€œ ๐ด)((๐‘‡โ€˜๐‘ฅ) +โ„Ž ๐‘ฃ) โˆˆ (๐‘‡ โ€œ ๐ด)))
2722, 13, 26mp2an 691 . . . 4 (โˆ€๐‘ข โˆˆ (๐‘‡ โ€œ ๐ด)โˆ€๐‘ฃ โˆˆ (๐‘‡ โ€œ ๐ด)(๐‘ข +โ„Ž ๐‘ฃ) โˆˆ (๐‘‡ โ€œ ๐ด) โ†” โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฃ โˆˆ (๐‘‡ โ€œ ๐ด)((๐‘‡โ€˜๐‘ฅ) +โ„Ž ๐‘ฃ) โˆˆ (๐‘‡ โ€œ ๐ด))
288sheli 29955 . . . . . . . 8 (๐‘ฅ โˆˆ ๐ด โ†’ ๐‘ฅ โˆˆ โ„‹)
298sheli 29955 . . . . . . . 8 (๐‘ฆ โˆˆ ๐ด โ†’ ๐‘ฆ โˆˆ โ„‹)
302lnopaddi 30712 . . . . . . . 8 ((๐‘ฅ โˆˆ โ„‹ โˆง ๐‘ฆ โˆˆ โ„‹) โ†’ (๐‘‡โ€˜(๐‘ฅ +โ„Ž ๐‘ฆ)) = ((๐‘‡โ€˜๐‘ฅ) +โ„Ž (๐‘‡โ€˜๐‘ฆ)))
3128, 29, 30syl2an 597 . . . . . . 7 ((๐‘ฅ โˆˆ ๐ด โˆง ๐‘ฆ โˆˆ ๐ด) โ†’ (๐‘‡โ€˜(๐‘ฅ +โ„Ž ๐‘ฆ)) = ((๐‘‡โ€˜๐‘ฅ) +โ„Ž (๐‘‡โ€˜๐‘ฆ)))
32 shaddcl 29958 . . . . . . . . 9 ((๐ด โˆˆ Sโ„‹ โˆง ๐‘ฅ โˆˆ ๐ด โˆง ๐‘ฆ โˆˆ ๐ด) โ†’ (๐‘ฅ +โ„Ž ๐‘ฆ) โˆˆ ๐ด)
338, 32mp3an1 1449 . . . . . . . 8 ((๐‘ฅ โˆˆ ๐ด โˆง ๐‘ฆ โˆˆ ๐ด) โ†’ (๐‘ฅ +โ„Ž ๐‘ฆ) โˆˆ ๐ด)
34 funfvima2 7176 . . . . . . . . 9 ((Fun ๐‘‡ โˆง ๐ด โŠ† dom ๐‘‡) โ†’ ((๐‘ฅ +โ„Ž ๐‘ฆ) โˆˆ ๐ด โ†’ (๐‘‡โ€˜(๐‘ฅ +โ„Ž ๐‘ฆ)) โˆˆ (๐‘‡ โ€œ ๐ด)))
3512, 15, 34mp2an 691 . . . . . . . 8 ((๐‘ฅ +โ„Ž ๐‘ฆ) โˆˆ ๐ด โ†’ (๐‘‡โ€˜(๐‘ฅ +โ„Ž ๐‘ฆ)) โˆˆ (๐‘‡ โ€œ ๐ด))
3633, 35syl 17 . . . . . . 7 ((๐‘ฅ โˆˆ ๐ด โˆง ๐‘ฆ โˆˆ ๐ด) โ†’ (๐‘‡โ€˜(๐‘ฅ +โ„Ž ๐‘ฆ)) โˆˆ (๐‘‡ โ€œ ๐ด))
3731, 36eqeltrrd 2840 . . . . . 6 ((๐‘ฅ โˆˆ ๐ด โˆง ๐‘ฆ โˆˆ ๐ด) โ†’ ((๐‘‡โ€˜๐‘ฅ) +โ„Ž (๐‘‡โ€˜๐‘ฆ)) โˆˆ (๐‘‡ โ€œ ๐ด))
3837ralrimiva 3142 . . . . 5 (๐‘ฅ โˆˆ ๐ด โ†’ โˆ€๐‘ฆ โˆˆ ๐ด ((๐‘‡โ€˜๐‘ฅ) +โ„Ž (๐‘‡โ€˜๐‘ฆ)) โˆˆ (๐‘‡ โ€œ ๐ด))
39 oveq2 7358 . . . . . . . 8 (๐‘ฃ = (๐‘‡โ€˜๐‘ฆ) โ†’ ((๐‘‡โ€˜๐‘ฅ) +โ„Ž ๐‘ฃ) = ((๐‘‡โ€˜๐‘ฅ) +โ„Ž (๐‘‡โ€˜๐‘ฆ)))
4039eleq1d 2823 . . . . . . 7 (๐‘ฃ = (๐‘‡โ€˜๐‘ฆ) โ†’ (((๐‘‡โ€˜๐‘ฅ) +โ„Ž ๐‘ฃ) โˆˆ (๐‘‡ โ€œ ๐ด) โ†” ((๐‘‡โ€˜๐‘ฅ) +โ„Ž (๐‘‡โ€˜๐‘ฆ)) โˆˆ (๐‘‡ โ€œ ๐ด)))
4140ralima 7183 . . . . . 6 ((๐‘‡ Fn โ„‹ โˆง ๐ด โŠ† โ„‹) โ†’ (โˆ€๐‘ฃ โˆˆ (๐‘‡ โ€œ ๐ด)((๐‘‡โ€˜๐‘ฅ) +โ„Ž ๐‘ฃ) โˆˆ (๐‘‡ โ€œ ๐ด) โ†” โˆ€๐‘ฆ โˆˆ ๐ด ((๐‘‡โ€˜๐‘ฅ) +โ„Ž (๐‘‡โ€˜๐‘ฆ)) โˆˆ (๐‘‡ โ€œ ๐ด)))
4222, 13, 41mp2an 691 . . . . 5 (โˆ€๐‘ฃ โˆˆ (๐‘‡ โ€œ ๐ด)((๐‘‡โ€˜๐‘ฅ) +โ„Ž ๐‘ฃ) โˆˆ (๐‘‡ โ€œ ๐ด) โ†” โˆ€๐‘ฆ โˆˆ ๐ด ((๐‘‡โ€˜๐‘ฅ) +โ„Ž (๐‘‡โ€˜๐‘ฆ)) โˆˆ (๐‘‡ โ€œ ๐ด))
4338, 42sylibr 233 . . . 4 (๐‘ฅ โˆˆ ๐ด โ†’ โˆ€๐‘ฃ โˆˆ (๐‘‡ โ€œ ๐ด)((๐‘‡โ€˜๐‘ฅ) +โ„Ž ๐‘ฃ) โˆˆ (๐‘‡ โ€œ ๐ด))
4427, 43mprgbir 3070 . . 3 โˆ€๐‘ข โˆˆ (๐‘‡ โ€œ ๐ด)โˆ€๐‘ฃ โˆˆ (๐‘‡ โ€œ ๐ด)(๐‘ข +โ„Ž ๐‘ฃ) โˆˆ (๐‘‡ โ€œ ๐ด)
452lnopmuli 30713 . . . . . . . 8 ((๐‘ข โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹) โ†’ (๐‘‡โ€˜(๐‘ข ยทโ„Ž ๐‘ฆ)) = (๐‘ข ยทโ„Ž (๐‘‡โ€˜๐‘ฆ)))
4629, 45sylan2 594 . . . . . . 7 ((๐‘ข โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ ๐ด) โ†’ (๐‘‡โ€˜(๐‘ข ยทโ„Ž ๐‘ฆ)) = (๐‘ข ยทโ„Ž (๐‘‡โ€˜๐‘ฆ)))
47 shmulcl 29959 . . . . . . . . 9 ((๐ด โˆˆ Sโ„‹ โˆง ๐‘ข โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ ๐ด) โ†’ (๐‘ข ยทโ„Ž ๐‘ฆ) โˆˆ ๐ด)
488, 47mp3an1 1449 . . . . . . . 8 ((๐‘ข โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ ๐ด) โ†’ (๐‘ข ยทโ„Ž ๐‘ฆ) โˆˆ ๐ด)
49 funfvima2 7176 . . . . . . . . 9 ((Fun ๐‘‡ โˆง ๐ด โŠ† dom ๐‘‡) โ†’ ((๐‘ข ยทโ„Ž ๐‘ฆ) โˆˆ ๐ด โ†’ (๐‘‡โ€˜(๐‘ข ยทโ„Ž ๐‘ฆ)) โˆˆ (๐‘‡ โ€œ ๐ด)))
5012, 15, 49mp2an 691 . . . . . . . 8 ((๐‘ข ยทโ„Ž ๐‘ฆ) โˆˆ ๐ด โ†’ (๐‘‡โ€˜(๐‘ข ยทโ„Ž ๐‘ฆ)) โˆˆ (๐‘‡ โ€œ ๐ด))
5148, 50syl 17 . . . . . . 7 ((๐‘ข โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ ๐ด) โ†’ (๐‘‡โ€˜(๐‘ข ยทโ„Ž ๐‘ฆ)) โˆˆ (๐‘‡ โ€œ ๐ด))
5246, 51eqeltrrd 2840 . . . . . 6 ((๐‘ข โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ ๐ด) โ†’ (๐‘ข ยทโ„Ž (๐‘‡โ€˜๐‘ฆ)) โˆˆ (๐‘‡ โ€œ ๐ด))
5352ralrimiva 3142 . . . . 5 (๐‘ข โˆˆ โ„‚ โ†’ โˆ€๐‘ฆ โˆˆ ๐ด (๐‘ข ยทโ„Ž (๐‘‡โ€˜๐‘ฆ)) โˆˆ (๐‘‡ โ€œ ๐ด))
54 oveq2 7358 . . . . . . . 8 (๐‘ฃ = (๐‘‡โ€˜๐‘ฆ) โ†’ (๐‘ข ยทโ„Ž ๐‘ฃ) = (๐‘ข ยทโ„Ž (๐‘‡โ€˜๐‘ฆ)))
5554eleq1d 2823 . . . . . . 7 (๐‘ฃ = (๐‘‡โ€˜๐‘ฆ) โ†’ ((๐‘ข ยทโ„Ž ๐‘ฃ) โˆˆ (๐‘‡ โ€œ ๐ด) โ†” (๐‘ข ยทโ„Ž (๐‘‡โ€˜๐‘ฆ)) โˆˆ (๐‘‡ โ€œ ๐ด)))
5655ralima 7183 . . . . . 6 ((๐‘‡ Fn โ„‹ โˆง ๐ด โŠ† โ„‹) โ†’ (โˆ€๐‘ฃ โˆˆ (๐‘‡ โ€œ ๐ด)(๐‘ข ยทโ„Ž ๐‘ฃ) โˆˆ (๐‘‡ โ€œ ๐ด) โ†” โˆ€๐‘ฆ โˆˆ ๐ด (๐‘ข ยทโ„Ž (๐‘‡โ€˜๐‘ฆ)) โˆˆ (๐‘‡ โ€œ ๐ด)))
5722, 13, 56mp2an 691 . . . . 5 (โˆ€๐‘ฃ โˆˆ (๐‘‡ โ€œ ๐ด)(๐‘ข ยทโ„Ž ๐‘ฃ) โˆˆ (๐‘‡ โ€œ ๐ด) โ†” โˆ€๐‘ฆ โˆˆ ๐ด (๐‘ข ยทโ„Ž (๐‘‡โ€˜๐‘ฆ)) โˆˆ (๐‘‡ โ€œ ๐ด))
5853, 57sylibr 233 . . . 4 (๐‘ข โˆˆ โ„‚ โ†’ โˆ€๐‘ฃ โˆˆ (๐‘‡ โ€œ ๐ด)(๐‘ข ยทโ„Ž ๐‘ฃ) โˆˆ (๐‘‡ โ€œ ๐ด))
5958rgen 3065 . . 3 โˆ€๐‘ข โˆˆ โ„‚ โˆ€๐‘ฃ โˆˆ (๐‘‡ โ€œ ๐ด)(๐‘ข ยทโ„Ž ๐‘ฃ) โˆˆ (๐‘‡ โ€œ ๐ด)
6044, 59pm3.2i 472 . 2 (โˆ€๐‘ข โˆˆ (๐‘‡ โ€œ ๐ด)โˆ€๐‘ฃ โˆˆ (๐‘‡ โ€œ ๐ด)(๐‘ข +โ„Ž ๐‘ฃ) โˆˆ (๐‘‡ โ€œ ๐ด) โˆง โˆ€๐‘ข โˆˆ โ„‚ โˆ€๐‘ฃ โˆˆ (๐‘‡ โ€œ ๐ด)(๐‘ข ยทโ„Ž ๐‘ฃ) โˆˆ (๐‘‡ โ€œ ๐ด))
61 issh2 29950 . 2 ((๐‘‡ โ€œ ๐ด) โˆˆ Sโ„‹ โ†” (((๐‘‡ โ€œ ๐ด) โŠ† โ„‹ โˆง 0โ„Ž โˆˆ (๐‘‡ โ€œ ๐ด)) โˆง (โˆ€๐‘ข โˆˆ (๐‘‡ โ€œ ๐ด)โˆ€๐‘ฃ โˆˆ (๐‘‡ โ€œ ๐ด)(๐‘ข +โ„Ž ๐‘ฃ) โˆˆ (๐‘‡ โ€œ ๐ด) โˆง โˆ€๐‘ข โˆˆ โ„‚ โˆ€๐‘ฃ โˆˆ (๐‘‡ โ€œ ๐ด)(๐‘ข ยทโ„Ž ๐‘ฃ) โˆˆ (๐‘‡ โ€œ ๐ด))))
6220, 60, 61mpbir2an 710 1 (๐‘‡ โ€œ ๐ด) โˆˆ Sโ„‹
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 397   = wceq 1542   โˆˆ wcel 2107  โˆ€wral 3063   โŠ† wss 3909  dom cdm 5631  ran crn 5632   โ€œ cima 5634  Fun wfun 6486   Fn wfn 6487  โŸถwf 6488  โ€˜cfv 6492  (class class class)co 7350  โ„‚cc 10983   โ„‹chba 29660   +โ„Ž cva 29661   ยทโ„Ž csm 29662  0โ„Žc0v 29665   Sโ„‹ csh 29669  LinOpclo 29688
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 2709  ax-sep 5255  ax-nul 5262  ax-pow 5319  ax-pr 5383  ax-un 7663  ax-resscn 11042  ax-1cn 11043  ax-icn 11044  ax-addcl 11045  ax-addrcl 11046  ax-mulcl 11047  ax-mulrcl 11048  ax-mulcom 11049  ax-addass 11050  ax-mulass 11051  ax-distr 11052  ax-i2m1 11053  ax-1ne0 11054  ax-1rid 11055  ax-rnegex 11056  ax-rrecex 11057  ax-cnre 11058  ax-pre-lttri 11059  ax-pre-lttrn 11060  ax-pre-ltadd 11061  ax-hilex 29740  ax-hfvadd 29741  ax-hvass 29743  ax-hv0cl 29744  ax-hvaddid 29745  ax-hfvmul 29746  ax-hvmulid 29747  ax-hvdistr2 29750  ax-hvmul0 29751
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 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3064  df-rex 3073  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3739  df-csb 3855  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-nul 4282  df-if 4486  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4865  df-iun 4955  df-br 5105  df-opab 5167  df-mpt 5188  df-id 5529  df-po 5543  df-so 5544  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6444  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7306  df-ov 7353  df-oprab 7354  df-mpo 7355  df-er 8582  df-map 8701  df-en 8818  df-dom 8819  df-sdom 8820  df-pnf 11125  df-mnf 11126  df-ltxr 11128  df-sub 11321  df-neg 11322  df-hvsub 29712  df-sh 29948  df-lnop 30582
This theorem is referenced by:  rnelshi  30800
  Copyright terms: Public domain W3C validator