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 syl5bir
 |-  ( ( ( 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 ) )