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

Theorem spanuni 27208
Description: The span of a union is the subspace sum of spans. (Contributed by NM, 2-Jun-2004.) (New usage is discouraged.)
Hypotheses
Ref Expression
spanun.1  |-  A  C_  ~H
spanun.2  |-  B  C_  ~H
Assertion
Ref Expression
spanuni  |-  ( span `  ( A  u.  B
) )  =  ( ( span `  A
)  +H  ( span `  B ) )

Proof of Theorem spanuni
Dummy variables  x  y  z  w are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 spanun.1 . . . . . . 7  |-  A  C_  ~H
2 spancl 27000 . . . . . . 7  |-  ( A 
C_  ~H  ->  ( span `  A )  e.  SH )
31, 2ax-mp 5 . . . . . 6  |-  ( span `  A )  e.  SH
4 spanun.2 . . . . . . 7  |-  B  C_  ~H
5 spancl 27000 . . . . . . 7  |-  ( B 
C_  ~H  ->  ( span `  B )  e.  SH )
64, 5ax-mp 5 . . . . . 6  |-  ( span `  B )  e.  SH
73, 6shscli 26981 . . . . 5  |-  ( (
span `  A )  +H  ( span `  B
) )  e.  SH
87shssii 26877 . . . 4  |-  ( (
span `  A )  +H  ( span `  B
) )  C_  ~H
9 spanss2 27009 . . . . . . 7  |-  ( A 
C_  ~H  ->  A  C_  ( span `  A )
)
101, 9ax-mp 5 . . . . . 6  |-  A  C_  ( span `  A )
11 spanss2 27009 . . . . . . 7  |-  ( B 
C_  ~H  ->  B  C_  ( span `  B )
)
124, 11ax-mp 5 . . . . . 6  |-  B  C_  ( span `  B )
13 unss12 3573 . . . . . 6  |-  ( ( A  C_  ( span `  A )  /\  B  C_  ( span `  B
) )  ->  ( A  u.  B )  C_  ( ( span `  A
)  u.  ( span `  B ) ) )
1410, 12, 13mp2an 683 . . . . 5  |-  ( A  u.  B )  C_  ( ( span `  A
)  u.  ( span `  B ) )
153, 6shunssi 27032 . . . . 5  |-  ( (
span `  A )  u.  ( span `  B
) )  C_  (
( span `  A )  +H  ( span `  B
) )
1614, 15sstri 3408 . . . 4  |-  ( A  u.  B )  C_  ( ( span `  A
)  +H  ( span `  B ) )
17 spanss 27012 . . . 4  |-  ( ( ( ( span `  A
)  +H  ( span `  B ) )  C_  ~H  /\  ( A  u.  B )  C_  (
( span `  A )  +H  ( span `  B
) ) )  -> 
( span `  ( A  u.  B ) )  C_  ( span `  ( ( span `  A )  +H  ( span `  B
) ) ) )
188, 16, 17mp2an 683 . . 3  |-  ( span `  ( A  u.  B
) )  C_  ( span `  ( ( span `  A )  +H  ( span `  B ) ) )
19 spanid 27011 . . . 4  |-  ( ( ( span `  A
)  +H  ( span `  B ) )  e.  SH  ->  ( span `  ( ( span `  A
)  +H  ( span `  B ) ) )  =  ( ( span `  A )  +H  ( span `  B ) ) )
207, 19ax-mp 5 . . 3  |-  ( span `  ( ( span `  A
)  +H  ( span `  B ) ) )  =  ( ( span `  A )  +H  ( span `  B ) )
2118, 20sseqtri 3431 . 2  |-  ( span `  ( A  u.  B
) )  C_  (
( span `  A )  +H  ( span `  B
) )
223, 6shseli 26980 . . . . 5  |-  ( x  e.  ( ( span `  A )  +H  ( span `  B ) )  <->  E. z  e.  ( span `  A ) E. w  e.  ( span `  B ) x  =  ( z  +h  w
) )
23 r2ex 2881 . . . . 5  |-  ( E. z  e.  ( span `  A ) E. w  e.  ( span `  B
) x  =  ( z  +h  w )  <->  E. z E. w ( ( z  e.  (
span `  A )  /\  w  e.  ( span `  B ) )  /\  x  =  ( z  +h  w ) ) )
2422, 23bitri 257 . . . 4  |-  ( x  e.  ( ( span `  A )  +H  ( span `  B ) )  <->  E. z E. w ( ( z  e.  (
span `  A )  /\  w  e.  ( span `  B ) )  /\  x  =  ( z  +h  w ) ) )
25 vex 3015 . . . . . . . . . . 11  |-  z  e. 
_V
2625elspani 27207 . . . . . . . . . 10  |-  ( A 
C_  ~H  ->  ( z  e.  ( span `  A
)  <->  A. y  e.  SH  ( A  C_  y  -> 
z  e.  y ) ) )
271, 26ax-mp 5 . . . . . . . . 9  |-  ( z  e.  ( span `  A
)  <->  A. y  e.  SH  ( A  C_  y  -> 
z  e.  y ) )
28 vex 3015 . . . . . . . . . . 11  |-  w  e. 
_V
2928elspani 27207 . . . . . . . . . 10  |-  ( B 
C_  ~H  ->  ( w  e.  ( span `  B
)  <->  A. y  e.  SH  ( B  C_  y  ->  w  e.  y )
) )
304, 29ax-mp 5 . . . . . . . . 9  |-  ( w  e.  ( span `  B
)  <->  A. y  e.  SH  ( B  C_  y  ->  w  e.  y )
)
3127, 30anbi12i 708 . . . . . . . 8  |-  ( ( z  e.  ( span `  A )  /\  w  e.  ( span `  B
) )  <->  ( A. y  e.  SH  ( A  C_  y  ->  z  e.  y )  /\  A. y  e.  SH  ( B  C_  y  ->  w  e.  y ) ) )
32 r19.26 2884 . . . . . . . 8  |-  ( A. y  e.  SH  (
( A  C_  y  ->  z  e.  y )  /\  ( B  C_  y  ->  w  e.  y ) )  <->  ( A. y  e.  SH  ( A  C_  y  ->  z  e.  y )  /\  A. y  e.  SH  ( B  C_  y  ->  w  e.  y ) ) )
3331, 32bitr4i 260 . . . . . . 7  |-  ( ( z  e.  ( span `  A )  /\  w  e.  ( span `  B
) )  <->  A. y  e.  SH  ( ( A 
C_  y  ->  z  e.  y )  /\  ( B  C_  y  ->  w  e.  y ) ) )
34 r19.27v 2890 . . . . . . 7  |-  ( ( A. y  e.  SH  ( ( A  C_  y  ->  z  e.  y )  /\  ( B 
C_  y  ->  w  e.  y ) )  /\  x  =  ( z  +h  w ) )  ->  A. y  e.  SH  ( ( ( A 
C_  y  ->  z  e.  y )  /\  ( B  C_  y  ->  w  e.  y ) )  /\  x  =  ( z  +h  w ) ) )
3533, 34sylanb 479 . . . . . 6  |-  ( ( ( z  e.  (
span `  A )  /\  w  e.  ( span `  B ) )  /\  x  =  ( z  +h  w ) )  ->  A. y  e.  SH  ( ( ( A  C_  y  ->  z  e.  y )  /\  ( B  C_  y  ->  w  e.  y )
)  /\  x  =  ( z  +h  w
) ) )
36 unss 3575 . . . . . . . . . . . 12  |-  ( ( A  C_  y  /\  B  C_  y )  <->  ( A  u.  B )  C_  y
)
37 prth 579 . . . . . . . . . . . 12  |-  ( ( ( A  C_  y  ->  z  e.  y )  /\  ( B  C_  y  ->  w  e.  y ) )  ->  (
( A  C_  y  /\  B  C_  y )  ->  ( z  e.  y  /\  w  e.  y ) ) )
3836, 37syl5bir 226 . . . . . . . . . . 11  |-  ( ( ( A  C_  y  ->  z  e.  y )  /\  ( B  C_  y  ->  w  e.  y ) )  ->  (
( A  u.  B
)  C_  y  ->  ( z  e.  y  /\  w  e.  y )
) )
39 shaddcl 26881 . . . . . . . . . . . 12  |-  ( ( y  e.  SH  /\  z  e.  y  /\  w  e.  y )  ->  ( z  +h  w
)  e.  y )
40393expib 1213 . . . . . . . . . . 11  |-  ( y  e.  SH  ->  (
( z  e.  y  /\  w  e.  y )  ->  ( z  +h  w )  e.  y ) )
4138, 40sylan9r 668 . . . . . . . . . 10  |-  ( ( y  e.  SH  /\  ( ( A  C_  y  ->  z  e.  y )  /\  ( B 
C_  y  ->  w  e.  y ) ) )  ->  ( ( A  u.  B )  C_  y  ->  ( z  +h  w )  e.  y ) )
42 eleq1 2517 . . . . . . . . . . 11  |-  ( x  =  ( z  +h  w )  ->  (
x  e.  y  <->  ( z  +h  w )  e.  y ) )
4342biimprd 231 . . . . . . . . . 10  |-  ( x  =  ( z  +h  w )  ->  (
( z  +h  w
)  e.  y  ->  x  e.  y )
)
4441, 43sylan9 667 . . . . . . . . 9  |-  ( ( ( y  e.  SH  /\  ( ( A  C_  y  ->  z  e.  y )  /\  ( B 
C_  y  ->  w  e.  y ) ) )  /\  x  =  ( z  +h  w ) )  ->  ( ( A  u.  B )  C_  y  ->  x  e.  y ) )
4544expl 628 . . . . . . . 8  |-  ( y  e.  SH  ->  (
( ( ( A 
C_  y  ->  z  e.  y )  /\  ( B  C_  y  ->  w  e.  y ) )  /\  x  =  ( z  +h  w ) )  -> 
( ( A  u.  B )  C_  y  ->  x  e.  y ) ) )
4645ralimia 2774 . . . . . . 7  |-  ( A. y  e.  SH  (
( ( A  C_  y  ->  z  e.  y )  /\  ( B 
C_  y  ->  w  e.  y ) )  /\  x  =  ( z  +h  w ) )  ->  A. y  e.  SH  ( ( A  u.  B )  C_  y  ->  x  e.  y ) )
471, 4unssi 3576 . . . . . . . 8  |-  ( A  u.  B )  C_  ~H
48 vex 3015 . . . . . . . . 9  |-  x  e. 
_V
4948elspani 27207 . . . . . . . 8  |-  ( ( A  u.  B ) 
C_  ~H  ->  ( x  e.  ( span `  ( A  u.  B )
)  <->  A. y  e.  SH  ( ( A  u.  B )  C_  y  ->  x  e.  y ) ) )
5047, 49ax-mp 5 . . . . . . 7  |-  ( x  e.  ( span `  ( A  u.  B )
)  <->  A. y  e.  SH  ( ( A  u.  B )  C_  y  ->  x  e.  y ) )
5146, 50sylibr 217 . . . . . 6  |-  ( A. y  e.  SH  (
( ( A  C_  y  ->  z  e.  y )  /\  ( B 
C_  y  ->  w  e.  y ) )  /\  x  =  ( z  +h  w ) )  ->  x  e.  ( span `  ( A  u.  B
) ) )
5235, 51syl 17 . . . . 5  |-  ( ( ( z  e.  (
span `  A )  /\  w  e.  ( span `  B ) )  /\  x  =  ( z  +h  w ) )  ->  x  e.  ( span `  ( A  u.  B ) ) )
5352exlimivv 1781 . . . 4  |-  ( E. z E. w ( ( z  e.  (
span `  A )  /\  w  e.  ( span `  B ) )  /\  x  =  ( z  +h  w ) )  ->  x  e.  ( span `  ( A  u.  B ) ) )
5424, 53sylbi 200 . . 3  |-  ( x  e.  ( ( span `  A )  +H  ( span `  B ) )  ->  x  e.  (
span `  ( A  u.  B ) ) )
5554ssriv 3403 . 2  |-  ( (
span `  A )  +H  ( span `  B
) )  C_  ( span `  ( A  u.  B ) )
5621, 55eqssi 3415 1  |-  ( span `  ( A  u.  B
) )  =  ( ( span `  A
)  +H  ( span `  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    /\ wa 375    = wceq 1447   E.wex 1666    e. wcel 1890   A.wral 2736   E.wrex 2737    u. cun 3369    C_ wss 3371   ` cfv 5560  (class class class)co 6275   ~Hchil 26583    +h cva 26584   SHcsh 26592    +H cph 26595   spancspn 26596
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1672  ax-4 1685  ax-5 1761  ax-6 1808  ax-7 1854  ax-8 1892  ax-9 1899  ax-10 1918  ax-11 1923  ax-12 1936  ax-13 2091  ax-ext 2431  ax-rep 4486  ax-sep 4496  ax-nul 4505  ax-pow 4553  ax-pr 4611  ax-un 6570  ax-cnex 9581  ax-resscn 9582  ax-1cn 9583  ax-icn 9584  ax-addcl 9585  ax-addrcl 9586  ax-mulcl 9587  ax-mulrcl 9588  ax-mulcom 9589  ax-addass 9590  ax-mulass 9591  ax-distr 9592  ax-i2m1 9593  ax-1ne0 9594  ax-1rid 9595  ax-rnegex 9596  ax-rrecex 9597  ax-cnre 9598  ax-pre-lttri 9599  ax-pre-lttrn 9600  ax-pre-ltadd 9601  ax-pre-mulgt0 9602  ax-pre-sup 9603  ax-addf 9604  ax-mulf 9605  ax-hilex 26663  ax-hfvadd 26664  ax-hvcom 26665  ax-hvass 26666  ax-hv0cl 26667  ax-hvaddid 26668  ax-hfvmul 26669  ax-hvmulid 26670  ax-hvmulass 26671  ax-hvdistr1 26672  ax-hvdistr2 26673  ax-hvmul0 26674  ax-hfi 26743  ax-his1 26746  ax-his2 26747  ax-his3 26748  ax-his4 26749
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 987  df-3an 988  df-tru 1450  df-ex 1667  df-nf 1671  df-sb 1801  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2623  df-nel 2624  df-ral 2741  df-rex 2742  df-reu 2743  df-rmo 2744  df-rab 2745  df-v 3014  df-sbc 3235  df-csb 3331  df-dif 3374  df-un 3376  df-in 3378  df-ss 3385  df-pss 3387  df-nul 3699  df-if 3849  df-pw 3920  df-sn 3936  df-pr 3938  df-tp 3940  df-op 3942  df-uni 4168  df-int 4204  df-iun 4249  df-br 4374  df-opab 4433  df-mpt 4434  df-tr 4469  df-eprel 4722  df-id 4726  df-po 4732  df-so 4733  df-fr 4770  df-we 4772  df-xp 4817  df-rel 4818  df-cnv 4819  df-co 4820  df-dm 4821  df-rn 4822  df-res 4823  df-ima 4824  df-pred 5358  df-ord 5404  df-on 5405  df-lim 5406  df-suc 5407  df-iota 5524  df-fun 5562  df-fn 5563  df-f 5564  df-f1 5565  df-fo 5566  df-f1o 5567  df-fv 5568  df-riota 6237  df-ov 6278  df-oprab 6279  df-mpt2 6280  df-om 6680  df-1st 6780  df-2nd 6781  df-wrecs 7014  df-recs 7076  df-rdg 7114  df-er 7349  df-map 7460  df-pm 7461  df-en 7556  df-dom 7557  df-sdom 7558  df-sup 7942  df-inf 7943  df-pnf 9663  df-mnf 9664  df-xr 9665  df-ltxr 9666  df-le 9667  df-sub 9848  df-neg 9849  df-div 10258  df-nn 10598  df-2 10656  df-3 10657  df-4 10658  df-n0 10859  df-z 10927  df-uz 11149  df-q 11254  df-rp 11292  df-xneg 11398  df-xadd 11399  df-xmul 11400  df-icc 11631  df-seq 12207  df-exp 12266  df-cj 13172  df-re 13173  df-im 13174  df-sqrt 13308  df-abs 13309  df-topgen 15352  df-psmet 18972  df-xmet 18973  df-met 18974  df-bl 18975  df-mopn 18976  df-top 19931  df-bases 19932  df-topon 19933  df-lm 20255  df-haus 20341  df-grpo 25930  df-gid 25931  df-ginv 25932  df-gdiv 25933  df-ablo 26021  df-vc 26176  df-nv 26222  df-va 26225  df-ba 26226  df-sm 26227  df-0v 26228  df-vs 26229  df-nmcv 26230  df-ims 26231  df-hnorm 26632  df-hvsub 26635  df-hlim 26636  df-sh 26871  df-ch 26885  df-ch0 26917  df-shs 26972  df-span 26973
This theorem is referenced by:  spanun  27209  spanunsni  27243  spansnji  27310
  Copyright terms: Public domain W3C validator