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

Theorem imaelshi 31349
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 6070 . . . 4 (๐‘‡ โ€œ ๐ด) โŠ† ran ๐‘‡
2 rnelsh.1 . . . . . 6 ๐‘‡ โˆˆ LinOp
32lnopfi 31260 . . . . 5 ๐‘‡: โ„‹โŸถ โ„‹
4 frn 6724 . . . . 5 (๐‘‡: โ„‹โŸถ โ„‹ โ†’ ran ๐‘‡ โŠ† โ„‹)
53, 4ax-mp 5 . . . 4 ran ๐‘‡ โŠ† โ„‹
61, 5sstri 3991 . . 3 (๐‘‡ โ€œ ๐ด) โŠ† โ„‹
72lnop0i 31261 . . . 4 (๐‘‡โ€˜0โ„Ž) = 0โ„Ž
8 imaelsh.2 . . . . . 6 ๐ด โˆˆ Sโ„‹
9 sh0 30507 . . . . . 6 (๐ด โˆˆ Sโ„‹ โ†’ 0โ„Ž โˆˆ ๐ด)
108, 9ax-mp 5 . . . . 5 0โ„Ž โˆˆ ๐ด
11 ffun 6720 . . . . . . 7 (๐‘‡: โ„‹โŸถ โ„‹ โ†’ Fun ๐‘‡)
123, 11ax-mp 5 . . . . . 6 Fun ๐‘‡
138shssii 30504 . . . . . . 7 ๐ด โŠ† โ„‹
143fdmi 6729 . . . . . . 7 dom ๐‘‡ = โ„‹
1513, 14sseqtrri 4019 . . . . . 6 ๐ด โŠ† dom ๐‘‡
16 funfvima2 7235 . . . . . 6 ((Fun ๐‘‡ โˆง ๐ด โŠ† dom ๐‘‡) โ†’ (0โ„Ž โˆˆ ๐ด โ†’ (๐‘‡โ€˜0โ„Ž) โˆˆ (๐‘‡ โ€œ ๐ด)))
1712, 15, 16mp2an 690 . . . . 5 (0โ„Ž โˆˆ ๐ด โ†’ (๐‘‡โ€˜0โ„Ž) โˆˆ (๐‘‡ โ€œ ๐ด))
1810, 17ax-mp 5 . . . 4 (๐‘‡โ€˜0โ„Ž) โˆˆ (๐‘‡ โ€œ ๐ด)
197, 18eqeltrri 2830 . . 3 0โ„Ž โˆˆ (๐‘‡ โ€œ ๐ด)
206, 19pm3.2i 471 . 2 ((๐‘‡ โ€œ ๐ด) โŠ† โ„‹ โˆง 0โ„Ž โˆˆ (๐‘‡ โ€œ ๐ด))
21 ffn 6717 . . . . . 6 (๐‘‡: โ„‹โŸถ โ„‹ โ†’ ๐‘‡ Fn โ„‹)
223, 21ax-mp 5 . . . . 5 ๐‘‡ Fn โ„‹
23 oveq1 7418 . . . . . . . 8 (๐‘ข = (๐‘‡โ€˜๐‘ฅ) โ†’ (๐‘ข +โ„Ž ๐‘ฃ) = ((๐‘‡โ€˜๐‘ฅ) +โ„Ž ๐‘ฃ))
2423eleq1d 2818 . . . . . . 7 (๐‘ข = (๐‘‡โ€˜๐‘ฅ) โ†’ ((๐‘ข +โ„Ž ๐‘ฃ) โˆˆ (๐‘‡ โ€œ ๐ด) โ†” ((๐‘‡โ€˜๐‘ฅ) +โ„Ž ๐‘ฃ) โˆˆ (๐‘‡ โ€œ ๐ด)))
2524ralbidv 3177 . . . . . 6 (๐‘ข = (๐‘‡โ€˜๐‘ฅ) โ†’ (โˆ€๐‘ฃ โˆˆ (๐‘‡ โ€œ ๐ด)(๐‘ข +โ„Ž ๐‘ฃ) โˆˆ (๐‘‡ โ€œ ๐ด) โ†” โˆ€๐‘ฃ โˆˆ (๐‘‡ โ€œ ๐ด)((๐‘‡โ€˜๐‘ฅ) +โ„Ž ๐‘ฃ) โˆˆ (๐‘‡ โ€œ ๐ด)))
2625ralima 7242 . . . . 5 ((๐‘‡ Fn โ„‹ โˆง ๐ด โŠ† โ„‹) โ†’ (โˆ€๐‘ข โˆˆ (๐‘‡ โ€œ ๐ด)โˆ€๐‘ฃ โˆˆ (๐‘‡ โ€œ ๐ด)(๐‘ข +โ„Ž ๐‘ฃ) โˆˆ (๐‘‡ โ€œ ๐ด) โ†” โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฃ โˆˆ (๐‘‡ โ€œ ๐ด)((๐‘‡โ€˜๐‘ฅ) +โ„Ž ๐‘ฃ) โˆˆ (๐‘‡ โ€œ ๐ด)))
2722, 13, 26mp2an 690 . . . 4 (โˆ€๐‘ข โˆˆ (๐‘‡ โ€œ ๐ด)โˆ€๐‘ฃ โˆˆ (๐‘‡ โ€œ ๐ด)(๐‘ข +โ„Ž ๐‘ฃ) โˆˆ (๐‘‡ โ€œ ๐ด) โ†” โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฃ โˆˆ (๐‘‡ โ€œ ๐ด)((๐‘‡โ€˜๐‘ฅ) +โ„Ž ๐‘ฃ) โˆˆ (๐‘‡ โ€œ ๐ด))
288sheli 30505 . . . . . . . 8 (๐‘ฅ โˆˆ ๐ด โ†’ ๐‘ฅ โˆˆ โ„‹)
298sheli 30505 . . . . . . . 8 (๐‘ฆ โˆˆ ๐ด โ†’ ๐‘ฆ โˆˆ โ„‹)
302lnopaddi 31262 . . . . . . . 8 ((๐‘ฅ โˆˆ โ„‹ โˆง ๐‘ฆ โˆˆ โ„‹) โ†’ (๐‘‡โ€˜(๐‘ฅ +โ„Ž ๐‘ฆ)) = ((๐‘‡โ€˜๐‘ฅ) +โ„Ž (๐‘‡โ€˜๐‘ฆ)))
3128, 29, 30syl2an 596 . . . . . . 7 ((๐‘ฅ โˆˆ ๐ด โˆง ๐‘ฆ โˆˆ ๐ด) โ†’ (๐‘‡โ€˜(๐‘ฅ +โ„Ž ๐‘ฆ)) = ((๐‘‡โ€˜๐‘ฅ) +โ„Ž (๐‘‡โ€˜๐‘ฆ)))
32 shaddcl 30508 . . . . . . . . 9 ((๐ด โˆˆ Sโ„‹ โˆง ๐‘ฅ โˆˆ ๐ด โˆง ๐‘ฆ โˆˆ ๐ด) โ†’ (๐‘ฅ +โ„Ž ๐‘ฆ) โˆˆ ๐ด)
338, 32mp3an1 1448 . . . . . . . 8 ((๐‘ฅ โˆˆ ๐ด โˆง ๐‘ฆ โˆˆ ๐ด) โ†’ (๐‘ฅ +โ„Ž ๐‘ฆ) โˆˆ ๐ด)
34 funfvima2 7235 . . . . . . . . 9 ((Fun ๐‘‡ โˆง ๐ด โŠ† dom ๐‘‡) โ†’ ((๐‘ฅ +โ„Ž ๐‘ฆ) โˆˆ ๐ด โ†’ (๐‘‡โ€˜(๐‘ฅ +โ„Ž ๐‘ฆ)) โˆˆ (๐‘‡ โ€œ ๐ด)))
3512, 15, 34mp2an 690 . . . . . . . 8 ((๐‘ฅ +โ„Ž ๐‘ฆ) โˆˆ ๐ด โ†’ (๐‘‡โ€˜(๐‘ฅ +โ„Ž ๐‘ฆ)) โˆˆ (๐‘‡ โ€œ ๐ด))
3633, 35syl 17 . . . . . . 7 ((๐‘ฅ โˆˆ ๐ด โˆง ๐‘ฆ โˆˆ ๐ด) โ†’ (๐‘‡โ€˜(๐‘ฅ +โ„Ž ๐‘ฆ)) โˆˆ (๐‘‡ โ€œ ๐ด))
3731, 36eqeltrrd 2834 . . . . . 6 ((๐‘ฅ โˆˆ ๐ด โˆง ๐‘ฆ โˆˆ ๐ด) โ†’ ((๐‘‡โ€˜๐‘ฅ) +โ„Ž (๐‘‡โ€˜๐‘ฆ)) โˆˆ (๐‘‡ โ€œ ๐ด))
3837ralrimiva 3146 . . . . 5 (๐‘ฅ โˆˆ ๐ด โ†’ โˆ€๐‘ฆ โˆˆ ๐ด ((๐‘‡โ€˜๐‘ฅ) +โ„Ž (๐‘‡โ€˜๐‘ฆ)) โˆˆ (๐‘‡ โ€œ ๐ด))
39 oveq2 7419 . . . . . . . 8 (๐‘ฃ = (๐‘‡โ€˜๐‘ฆ) โ†’ ((๐‘‡โ€˜๐‘ฅ) +โ„Ž ๐‘ฃ) = ((๐‘‡โ€˜๐‘ฅ) +โ„Ž (๐‘‡โ€˜๐‘ฆ)))
4039eleq1d 2818 . . . . . . 7 (๐‘ฃ = (๐‘‡โ€˜๐‘ฆ) โ†’ (((๐‘‡โ€˜๐‘ฅ) +โ„Ž ๐‘ฃ) โˆˆ (๐‘‡ โ€œ ๐ด) โ†” ((๐‘‡โ€˜๐‘ฅ) +โ„Ž (๐‘‡โ€˜๐‘ฆ)) โˆˆ (๐‘‡ โ€œ ๐ด)))
4140ralima 7242 . . . . . 6 ((๐‘‡ Fn โ„‹ โˆง ๐ด โŠ† โ„‹) โ†’ (โˆ€๐‘ฃ โˆˆ (๐‘‡ โ€œ ๐ด)((๐‘‡โ€˜๐‘ฅ) +โ„Ž ๐‘ฃ) โˆˆ (๐‘‡ โ€œ ๐ด) โ†” โˆ€๐‘ฆ โˆˆ ๐ด ((๐‘‡โ€˜๐‘ฅ) +โ„Ž (๐‘‡โ€˜๐‘ฆ)) โˆˆ (๐‘‡ โ€œ ๐ด)))
4222, 13, 41mp2an 690 . . . . 5 (โˆ€๐‘ฃ โˆˆ (๐‘‡ โ€œ ๐ด)((๐‘‡โ€˜๐‘ฅ) +โ„Ž ๐‘ฃ) โˆˆ (๐‘‡ โ€œ ๐ด) โ†” โˆ€๐‘ฆ โˆˆ ๐ด ((๐‘‡โ€˜๐‘ฅ) +โ„Ž (๐‘‡โ€˜๐‘ฆ)) โˆˆ (๐‘‡ โ€œ ๐ด))
4338, 42sylibr 233 . . . 4 (๐‘ฅ โˆˆ ๐ด โ†’ โˆ€๐‘ฃ โˆˆ (๐‘‡ โ€œ ๐ด)((๐‘‡โ€˜๐‘ฅ) +โ„Ž ๐‘ฃ) โˆˆ (๐‘‡ โ€œ ๐ด))
4427, 43mprgbir 3068 . . 3 โˆ€๐‘ข โˆˆ (๐‘‡ โ€œ ๐ด)โˆ€๐‘ฃ โˆˆ (๐‘‡ โ€œ ๐ด)(๐‘ข +โ„Ž ๐‘ฃ) โˆˆ (๐‘‡ โ€œ ๐ด)
452lnopmuli 31263 . . . . . . . 8 ((๐‘ข โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹) โ†’ (๐‘‡โ€˜(๐‘ข ยทโ„Ž ๐‘ฆ)) = (๐‘ข ยทโ„Ž (๐‘‡โ€˜๐‘ฆ)))
4629, 45sylan2 593 . . . . . . 7 ((๐‘ข โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ ๐ด) โ†’ (๐‘‡โ€˜(๐‘ข ยทโ„Ž ๐‘ฆ)) = (๐‘ข ยทโ„Ž (๐‘‡โ€˜๐‘ฆ)))
47 shmulcl 30509 . . . . . . . . 9 ((๐ด โˆˆ Sโ„‹ โˆง ๐‘ข โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ ๐ด) โ†’ (๐‘ข ยทโ„Ž ๐‘ฆ) โˆˆ ๐ด)
488, 47mp3an1 1448 . . . . . . . 8 ((๐‘ข โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ ๐ด) โ†’ (๐‘ข ยทโ„Ž ๐‘ฆ) โˆˆ ๐ด)
49 funfvima2 7235 . . . . . . . . 9 ((Fun ๐‘‡ โˆง ๐ด โŠ† dom ๐‘‡) โ†’ ((๐‘ข ยทโ„Ž ๐‘ฆ) โˆˆ ๐ด โ†’ (๐‘‡โ€˜(๐‘ข ยทโ„Ž ๐‘ฆ)) โˆˆ (๐‘‡ โ€œ ๐ด)))
5012, 15, 49mp2an 690 . . . . . . . 8 ((๐‘ข ยทโ„Ž ๐‘ฆ) โˆˆ ๐ด โ†’ (๐‘‡โ€˜(๐‘ข ยทโ„Ž ๐‘ฆ)) โˆˆ (๐‘‡ โ€œ ๐ด))
5148, 50syl 17 . . . . . . 7 ((๐‘ข โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ ๐ด) โ†’ (๐‘‡โ€˜(๐‘ข ยทโ„Ž ๐‘ฆ)) โˆˆ (๐‘‡ โ€œ ๐ด))
5246, 51eqeltrrd 2834 . . . . . 6 ((๐‘ข โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ ๐ด) โ†’ (๐‘ข ยทโ„Ž (๐‘‡โ€˜๐‘ฆ)) โˆˆ (๐‘‡ โ€œ ๐ด))
5352ralrimiva 3146 . . . . 5 (๐‘ข โˆˆ โ„‚ โ†’ โˆ€๐‘ฆ โˆˆ ๐ด (๐‘ข ยทโ„Ž (๐‘‡โ€˜๐‘ฆ)) โˆˆ (๐‘‡ โ€œ ๐ด))
54 oveq2 7419 . . . . . . . 8 (๐‘ฃ = (๐‘‡โ€˜๐‘ฆ) โ†’ (๐‘ข ยทโ„Ž ๐‘ฃ) = (๐‘ข ยทโ„Ž (๐‘‡โ€˜๐‘ฆ)))
5554eleq1d 2818 . . . . . . 7 (๐‘ฃ = (๐‘‡โ€˜๐‘ฆ) โ†’ ((๐‘ข ยทโ„Ž ๐‘ฃ) โˆˆ (๐‘‡ โ€œ ๐ด) โ†” (๐‘ข ยทโ„Ž (๐‘‡โ€˜๐‘ฆ)) โˆˆ (๐‘‡ โ€œ ๐ด)))
5655ralima 7242 . . . . . 6 ((๐‘‡ Fn โ„‹ โˆง ๐ด โŠ† โ„‹) โ†’ (โˆ€๐‘ฃ โˆˆ (๐‘‡ โ€œ ๐ด)(๐‘ข ยทโ„Ž ๐‘ฃ) โˆˆ (๐‘‡ โ€œ ๐ด) โ†” โˆ€๐‘ฆ โˆˆ ๐ด (๐‘ข ยทโ„Ž (๐‘‡โ€˜๐‘ฆ)) โˆˆ (๐‘‡ โ€œ ๐ด)))
5722, 13, 56mp2an 690 . . . . 5 (โˆ€๐‘ฃ โˆˆ (๐‘‡ โ€œ ๐ด)(๐‘ข ยทโ„Ž ๐‘ฃ) โˆˆ (๐‘‡ โ€œ ๐ด) โ†” โˆ€๐‘ฆ โˆˆ ๐ด (๐‘ข ยทโ„Ž (๐‘‡โ€˜๐‘ฆ)) โˆˆ (๐‘‡ โ€œ ๐ด))
5853, 57sylibr 233 . . . 4 (๐‘ข โˆˆ โ„‚ โ†’ โˆ€๐‘ฃ โˆˆ (๐‘‡ โ€œ ๐ด)(๐‘ข ยทโ„Ž ๐‘ฃ) โˆˆ (๐‘‡ โ€œ ๐ด))
5958rgen 3063 . . 3 โˆ€๐‘ข โˆˆ โ„‚ โˆ€๐‘ฃ โˆˆ (๐‘‡ โ€œ ๐ด)(๐‘ข ยทโ„Ž ๐‘ฃ) โˆˆ (๐‘‡ โ€œ ๐ด)
6044, 59pm3.2i 471 . 2 (โˆ€๐‘ข โˆˆ (๐‘‡ โ€œ ๐ด)โˆ€๐‘ฃ โˆˆ (๐‘‡ โ€œ ๐ด)(๐‘ข +โ„Ž ๐‘ฃ) โˆˆ (๐‘‡ โ€œ ๐ด) โˆง โˆ€๐‘ข โˆˆ โ„‚ โˆ€๐‘ฃ โˆˆ (๐‘‡ โ€œ ๐ด)(๐‘ข ยทโ„Ž ๐‘ฃ) โˆˆ (๐‘‡ โ€œ ๐ด))
61 issh2 30500 . 2 ((๐‘‡ โ€œ ๐ด) โˆˆ Sโ„‹ โ†” (((๐‘‡ โ€œ ๐ด) โŠ† โ„‹ โˆง 0โ„Ž โˆˆ (๐‘‡ โ€œ ๐ด)) โˆง (โˆ€๐‘ข โˆˆ (๐‘‡ โ€œ ๐ด)โˆ€๐‘ฃ โˆˆ (๐‘‡ โ€œ ๐ด)(๐‘ข +โ„Ž ๐‘ฃ) โˆˆ (๐‘‡ โ€œ ๐ด) โˆง โˆ€๐‘ข โˆˆ โ„‚ โˆ€๐‘ฃ โˆˆ (๐‘‡ โ€œ ๐ด)(๐‘ข ยทโ„Ž ๐‘ฃ) โˆˆ (๐‘‡ โ€œ ๐ด))))
6220, 60, 61mpbir2an 709 1 (๐‘‡ โ€œ ๐ด) โˆˆ Sโ„‹
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 396   = wceq 1541   โˆˆ wcel 2106  โˆ€wral 3061   โŠ† wss 3948  dom cdm 5676  ran crn 5677   โ€œ cima 5679  Fun wfun 6537   Fn wfn 6538  โŸถwf 6539  โ€˜cfv 6543  (class class class)co 7411  โ„‚cc 11110   โ„‹chba 30210   +โ„Ž cva 30211   ยทโ„Ž csm 30212  0โ„Žc0v 30215   Sโ„‹ csh 30219  LinOpclo 30238
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-hilex 30290  ax-hfvadd 30291  ax-hvass 30293  ax-hv0cl 30294  ax-hvaddid 30295  ax-hfvmul 30296  ax-hvmulid 30297  ax-hvdistr2 30300  ax-hvmul0 30301
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-po 5588  df-so 5589  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-er 8705  df-map 8824  df-en 8942  df-dom 8943  df-sdom 8944  df-pnf 11252  df-mnf 11253  df-ltxr 11255  df-sub 11448  df-neg 11449  df-hvsub 30262  df-sh 30498  df-lnop 31132
This theorem is referenced by:  rnelshi  31350
  Copyright terms: Public domain W3C validator