Metamath Proof Explorer

Theorem spanuni

Description: The span of a union is the subspace sum of spans. (Contributed by NM, 2-Jun-2004) (New usage is discouraged.)

Ref Expression
Hypotheses spanun.1 
|- A C_ ~H
spanun.2 
|- B C_ ~H
Assertion spanuni 
|- ( span ` ( A u. B ) ) = ( ( span ` A ) +H ( span ` B ) )

Proof

Step Hyp Ref Expression
1 spanun.1 
 |-  A C_ ~H
2 spanun.2 
 |-  B C_ ~H
3 spancl 
 |-  ( A C_ ~H -> ( span ` A ) e. SH )
4 1 3 ax-mp 
 |-  ( span ` A ) e. SH
5 spancl 
 |-  ( B C_ ~H -> ( span ` B ) e. SH )
6 2 5 ax-mp 
 |-  ( span ` B ) e. SH
7 4 6 shscli 
 |-  ( ( span ` A ) +H ( span ` B ) ) e. SH
8 7 shssii 
 |-  ( ( span ` A ) +H ( span ` B ) ) C_ ~H
9 spanss2 
 |-  ( A C_ ~H -> A C_ ( span ` A ) )
10 1 9 ax-mp 
 |-  A C_ ( span ` A )
11 spanss2 
 |-  ( B C_ ~H -> B C_ ( span ` B ) )
12 2 11 ax-mp 
 |-  B C_ ( span ` B )
13 unss12 
 |-  ( ( A C_ ( span ` A ) /\ B C_ ( span ` B ) ) -> ( A u. B ) C_ ( ( span ` A ) u. ( span ` B ) ) )
14 10 12 13 mp2an 
 |-  ( A u. B ) C_ ( ( span ` A ) u. ( span ` B ) )
15 4 6 shunssi 
 |-  ( ( span ` A ) u. ( span ` B ) ) C_ ( ( span ` A ) +H ( span ` B ) )
16 14 15 sstri 
 |-  ( A u. B ) C_ ( ( span ` A ) +H ( span ` B ) )
17 spanss 
 |-  ( ( ( ( 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 ) ) ) )
18 8 16 17 mp2an 
 |-  ( span ` ( A u. B ) ) C_ ( span ` ( ( span ` A ) +H ( span ` B ) ) )
19 spanid 
 |-  ( ( ( span ` A ) +H ( span ` B ) ) e. SH -> ( span ` ( ( span ` A ) +H ( span ` B ) ) ) = ( ( span ` A ) +H ( span ` B ) ) )
20 7 19 ax-mp 
 |-  ( span ` ( ( span ` A ) +H ( span ` B ) ) ) = ( ( span ` A ) +H ( span ` B ) )
21 18 20 sseqtri 
 |-  ( span ` ( A u. B ) ) C_ ( ( span ` A ) +H ( span ` B ) )
22 4 6 shseli 
 |-  ( x e. ( ( span ` A ) +H ( span ` B ) ) <-> E. z e. ( span ` A ) E. w e. ( span ` B ) x = ( z +h w ) )
23 r2ex 
 |-  ( 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 ) ) )
24 22 23 bitri 
 |-  ( 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 
 |-  z e. _V
26 25 elspani 
 |-  ( A C_ ~H -> ( z e. ( span ` A ) <-> A. y e. SH ( A C_ y -> z e. y ) ) )
27 1 26 ax-mp 
 |-  ( z e. ( span ` A ) <-> A. y e. SH ( A C_ y -> z e. y ) )
28 vex 
 |-  w e. _V
29 28 elspani 
 |-  ( B C_ ~H -> ( w e. ( span ` B ) <-> A. y e. SH ( B C_ y -> w e. y ) ) )
30 2 29 ax-mp 
 |-  ( w e. ( span ` B ) <-> A. y e. SH ( B C_ y -> w e. y ) )
31 27 30 anbi12i 
 |-  ( ( 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 
 |-  ( 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 ) ) )
33 31 32 bitr4i 
 |-  ( ( 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 
 |-  ( ( 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 ) ) )
35 33 34 sylanb 
 |-  ( ( ( 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 
 |-  ( ( A C_ y /\ B C_ y ) <-> ( A u. B ) C_ y )
37 anim12 
 |-  ( ( ( A C_ y -> z e. y ) /\ ( B C_ y -> w e. y ) ) -> ( ( A C_ y /\ B C_ y ) -> ( z e. y /\ w e. y ) ) )
38 36 37 biimtrrid 
 |-  ( ( ( 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 
 |-  ( ( y e. SH /\ z e. y /\ w e. y ) -> ( z +h w ) e. y )
40 39 3expib 
 |-  ( y e. SH -> ( ( z e. y /\ w e. y ) -> ( z +h w ) e. y ) )
41 38 40 sylan9r 
 |-  ( ( 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 
 |-  ( x = ( z +h w ) -> ( x e. y <-> ( z +h w ) e. y ) )
43 42 biimprd 
 |-  ( x = ( z +h w ) -> ( ( z +h w ) e. y -> x e. y ) )
44 41 43 sylan9 
 |-  ( ( ( 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 ) )
45 44 expl 
 |-  ( 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 ) ) )
46 45 ralimia 
 |-  ( 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 ) )
47 1 2 unssi 
 |-  ( A u. B ) C_ ~H
48 vex 
 |-  x e. _V
49 48 elspani 
 |-  ( ( A u. B ) C_ ~H -> ( x e. ( span ` ( A u. B ) ) <-> A. y e. SH ( ( A u. B ) C_ y -> x e. y ) ) )
50 47 49 ax-mp 
 |-  ( x e. ( span ` ( A u. B ) ) <-> A. y e. SH ( ( A u. B ) C_ y -> x e. y ) )
51 46 50 sylibr 
 |-  ( 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 ) ) )
52 35 51 syl 
 |-  ( ( ( z e. ( span ` A ) /\ w e. ( span ` B ) ) /\ x = ( z +h w ) ) -> x e. ( span ` ( A u. B ) ) )
53 52 exlimivv 
 |-  ( E. z E. w ( ( z e. ( span ` A ) /\ w e. ( span ` B ) ) /\ x = ( z +h w ) ) -> x e. ( span ` ( A u. B ) ) )
54 24 53 sylbi 
 |-  ( x e. ( ( span ` A ) +H ( span ` B ) ) -> x e. ( span ` ( A u. B ) ) )
55 54 ssriv 
 |-  ( ( span ` A ) +H ( span ` B ) ) C_ ( span ` ( A u. B ) )
56 21 55 eqssi 
 |-  ( span ` ( A u. B ) ) = ( ( span ` A ) +H ( span ` B ) )