HomeHome Hilbert Space Explorer < Previous   Next >
Related theorems
Unicode version
Theorem spanun 9382
Description: The span of a union is the subspace sum of spans.
Hypotheses
Ref Expression
spanun.1 |- A (_ H~
spanun.2 |- B (_ H~
Assertion
Ref Expression
spanun |- (span` (A u. B)) = ((span` A) +H (span` B))
Proof of Theorem spanun
StepHypRef Expression
1 spanun.1 . . . . . . 7 |- A (_ H~
2 spanclt 9219 . . . . . . 7 |- (A (_ H~ -> (span` A) e. SH)
31, 2ax-mp 7 . . . . . 6 |- (span` A) e. SH
4 spanun.2 . . . . . . 7 |- B (_ H~
5 spanclt 9219 . . . . . . 7 |- (B (_ H~ -> (span` B) e. SH)
64, 5ax-mp 7 . . . . . 6 |- (span` B) e. SH
73, 6shscl 9196 . . . . 5 |- ((span` A) +H (span` B)) e. SH
87shssi 9002 . . . 4 |- ((span` A) +H (span` B)) (_ H~
9 spanss2 9229 . . . . . . 7 |- (A (_ H~ -> A (_ (span` A))
101, 9ax-mp 7 . . . . . 6 |- A (_ (span` A)
11 spanss2 9229 . . . . . . 7 |- (B (_ H~ -> B (_ (span` B))
124, 11ax-mp 7 . . . . . 6 |- B (_ (span` B)
13 unss12 2192 . . . . . 6 |- ((A (_ (span` A) /\ B (_ (span` B)) -> (A u. B) (_ ((span` A) u. (span` B)))
1410, 12, 13mp2an 695 . . . . 5 |- (A u. B) (_ ((span` A) u. (span` B))
153, 6shunss 9252 . . . . 5 |- ((span` A) u. (span` B)) (_ ((span` A) +H (span` B))
1614, 15sstri 2063 . . . 4 |- (A u. B) (_ ((span` A) +H (span` B))
17 spanss 9233 . . . 4 |- ((((span` A) +H (span` B)) (_ H~ /\ (A u. B) (_ ((span` A) +H (span` B))) -> (span` (A u. B)) (_ (span` ((span` A) +H (span` B))))
188, 16, 17mp2an 695 . . 3 |- (span` (A u. B)) (_ (span` ((span` A) +H (span` B)))
19 spanid 9232 . . . 4 |- (((span` A) +H (span` B)) e. SH -> (span` ((span` A) +H (span` B))) = ((span` A) +H (span` B)))
207, 19ax-mp 7 . . 3 |- (span` ((span` A) +H (span` B))) = ((span` A) +H (span` B))
2118, 20sseqtr 2083 . 2 |- (span` (A u. B)) (_ ((span` A) +H (span` B))
223, 6shsel 9195 . . . . 5 |- (x e. ((span` A) +H (span` B)) <-> E.z e. (span` A)E.w e. (span` B)x = (z +h w))
23 r2ex 1683 . . . . 5 |- (E.z e. (span` A)E.w e. (span` B)x = (z +h w) <-> E.zE.w((z e. (span` A) /\ w e. (span` B)) /\ x = (z +h w)))
2422, 23bitr 173 . . . 4 |- (x e. ((span` A) +H (span` B)) <-> E.zE.w((z e. (span` A) /\ w e. (span` B)) /\ x = (z +h w)))
25 r19.27av 1746 . . . . . . 7 |- ((A.y e. SH ((A (_ y -> z e. y) /\ (B (_ y -> w e. y)) /\ x = (z +h w)) -> A.y e. SH (((A (_ y -> z e. y) /\ (B (_ y -> w e. y)) /\ x = (z +h w)))
26 visset 1804 . . . . . . . . . . 11 |- z e. V
2726elspan 9381 . . . . . . . . . 10 |- (A (_ H~ -> (z e. (span` A) <-> A.y e. SH (A (_ y -> z e. y)))
281, 27ax-mp 7 . . . . . . . . 9 |- (z e. (span` A) <-> A.y e. SH (A (_ y -> z e. y))
29 visset 1804 . . . . . . . . . . 11 |- w e. V
3029elspan 9381 . . . . . . . . . 10 |- (B (_ H~ -> (w e. (span` B) <-> A.y e. SH (B (_ y -> w e. y)))
314, 30ax-mp 7 . . . . . . . . 9 |- (w e. (span` B) <-> A.y e. SH (B (_ y -> w e. y))
3228, 31anbi12i 481 . . . . . . . 8 |- ((z e. (span` A) /\ w e. (span` B)) <-> (A.y e. SH (A (_ y -> z e. y) /\ A.y e. SH (B (_ y -> w e. y)))
33 r19.26 1742 . . . . . . . 8 |- (A.y e. SH ((A (_ y -> z e. y) /\ (B (_ y -> w e. y)) <-> (A.y e. SH (A (_ y -> z e. y) /\ A.y e. SH (B (_ y -> w e. y)))
3432, 33bitr4 176 . . . . . . 7 |- ((z e. (span` A) /\ w e. (span` B)) <-> A.y e. SH ((A (_ y -> z e. y) /\ (B (_ y -> w e. y)))
3525, 34sylanb 449 . . . . . 6 |- (((z e. (span` A) /\ w e. (span` B)) /\ x = (z +h w)) -> A.y e. SH (((A (_ y -> z e. y) /\ (B (_ y -> w e. y)) /\ x = (z +h w)))
36 prth 554 . . . . . . . . . . . . 13 |- (((A (_ y -> z e. y) /\ (B (_ y -> w e. y)) -> ((A (_ y /\ B (_ y) -> (z e. y /\ w e. y)))
37 unss 2194 . . . . . . . . . . . . 13 |- ((A (_ y /\ B (_ y) <-> (A u. B) (_ y)
3836, 37syl5ibr 207 . . . . . . . . . . . 12 |- (((A (_ y -> z e. y) /\ (B (_ y -> w e. y)) -> ((A u. B) (_ y -> (z e. y /\ w e. y)))
39 shaddcltOLD 9007 . . . . . . . . . . . 12 |- (y e. SH -> ((z e. y /\ w e. y) -> (z +h w) e. y))
4038, 39sylan9r 469 . . . . . . . . . . 11 |- ((y e. SH /\ ((A (_ y -> z e. y) /\ (B (_ y -> w e. y))) -> ((A u. B) (_ y -> (z +h w) e. y))
41 eleq1 1526 . . . . . . . . . . . 12 |- (x = (z +h w) -> (x e. y <-> (z +h w) e. y))
4241biimprd 154 . . . . . . . . . . 11 |- (x = (z +h w) -> ((z +h w) e. y -> x e. y))
4340, 42sylan9 468 . . . . . . . . . 10 |- (((y e. SH /\ ((A (_ y -> z e. y) /\ (B (_ y -> w e. y))) /\ x = (z +h w)) -> ((A u. B) (_ y -> x e. y))
4443exp42 383 . . . . . . . . 9 |- (y e. SH -> ((A (_ y -> z e. y) -> ((B (_ y -> w e. y) -> (x = (z +h w) -> ((A u. B) (_ y -> x e. y)))))
4544imp4c 366 . . . . . . . 8 |- (y e. SH -> ((((A (_ y -> z e. y) /\ (B (_ y -> w e. y)) /\ x = (z +h w)) -> ((A u. B) (_ y -> x e. y)))
4645r19.20i 1696 . . . . . . 7 |- (A.y e. SH (((A (_ y -> z e. y) /\ (B (_ y -> w e. y)) /\ x = (z +h w)) -> A.y e. SH ((A u. B) (_ y -> x e. y))
471, 4unssi 2195 . . . . . . . 8 |- (A u. B) (_ H~
48 visset 1804 . . . . . . . . 9 |- x e. V
4948elspan 9381 . . . . . . . 8 |- ((A u. B) (_ H~ -> (x e. (span` (A u. B)) <-> A.y e. SH ((A u. B) (_ y -> x e. y)))
5047, 49ax-mp 7 . . . . . . 7 |- (x e. (span` (A u. B)) <-> A.y e. SH ((A u. B) (_ y -> x e. y))
5146, 50sylibr 200 . . . . . 6 |- (A.y e. SH (((A (_ y -> z e. y) /\ (B (_ y -> w e. y)) /\ x = (z +h w)) -> x e. (span` (A u. B)))
5235, 51syl 10 . . . . 5 |- (((z e. (span` A) /\ w e. (span` B)) /\ x = (z +h w)) -> x e. (span` (A u. B)))
535219.23aivv 1291 . . . 4 |- (E.zE.w((z e. (span` A) /\ w e. (span` B)) /\ x = (z +h w)) -> x e. (span` (A u. B)))
5424, 53sylbi 199 . . 3 |- (x e. ((span` A) +H (span` B)) -> x e. (span` (A u. B)))
5554ssriv 2059 . 2 |- ((span` A) +H (span` B)) (_ (span` (A u. B))
5621, 55eqssi 2068 1 |- (span` (A u. B)) = ((span` A) +H (span` B))
Colors of variables: wff set class
Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   = wceq 953   e. wcel 955  E.wex 977  A.wral 1637  E.wrex 1638   u. cun 2035   (_ wss 2037  ` cfv 3172  (class class class)co 3948  H~chil 8727   +h cva 8728  SHcsh 8736   +H cph 8739  spancspn 8740
This theorem is referenced by:  spanunt 9383  spanunsn 9419  spansnj 9508
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-9 962  ax-10 963  ax-11 964  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-rep 2683  ax-sep 2693  ax-nul 2700  ax-pow 2732  ax-pr 2769  ax-un 2857  ax-inf2 4597  ax-hilex 8790  ax-hfvadd 8791  ax-hvcom 8792  ax-hvass 8793  ax-hv0cl 8794  ax-hvaddid 8795  ax-hfvmul 8796  ax-hvmulid 8797  ax-hvmulass 8798  ax-hvdistr1 8799  ax-hvdistr2 8800  ax-hvmul0 8801  ax-hfi 8867  ax-his1 8870  ax-his2 8871  ax-his3 8872  ax-his4 8873
This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 774  df-3an 775  df-ex 978  df-sb 1168  df-eu 1375  df-mo 1376  df-clab 1457  df-cleq 1462  df-clel 1465  df-ne 1579  df-nel 1580  df-ral 1641  df-rex 1642  df-reu 1643  df-rab 1644  df-v 1803  df-sbc 1932  df-csb 1992  df-dif 2039  df-un 2040  df-in 2041  df-ss 2043  df-pss 2045  df-nul 2271  df-if 2352  df-pw 2392  df-sn 2402  df-pr 2403  df-tp 2405  df-op 2406  df-uni 2494  df-int 2524  df-iun 2558  df-br 2610  df-opab 2657  df-tr 2671  df-eprel 2821  df-id 2824  df-po 2831  df-so 2841  df-fr 2907  df-we 2924  df-ord 2941  df-on 2942  df-lim 2943  df-suc 2944  df-om 3122  df-xp 3174  df-rel 3175  df-cnv 3176  df-co 3177  df-dm 3178  df-rn 3179  df-res 3180  df-ima 3181  df-fun 3182  df-fn 3183  df-f