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