Step |
Hyp |
Ref |
Expression |
1 |
|
spansnsh |
|- ( A e. ~H -> ( span ` { A } ) e. SH ) |
2 |
|
spansnsh |
|- ( B e. ~H -> ( span ` { B } ) e. SH ) |
3 |
|
shscl |
|- ( ( ( span ` { A } ) e. SH /\ ( span ` { B } ) e. SH ) -> ( ( span ` { A } ) +H ( span ` { B } ) ) e. SH ) |
4 |
1 2 3
|
syl2an |
|- ( ( A e. ~H /\ B e. ~H ) -> ( ( span ` { A } ) +H ( span ` { B } ) ) e. SH ) |
5 |
4
|
adantr |
|- ( ( ( A e. ~H /\ B e. ~H ) /\ x e. ( span ` { ( A +h B ) } ) ) -> ( ( span ` { A } ) +H ( span ` { B } ) ) e. SH ) |
6 |
1 2
|
anim12i |
|- ( ( A e. ~H /\ B e. ~H ) -> ( ( span ` { A } ) e. SH /\ ( span ` { B } ) e. SH ) ) |
7 |
|
spansnid |
|- ( A e. ~H -> A e. ( span ` { A } ) ) |
8 |
|
spansnid |
|- ( B e. ~H -> B e. ( span ` { B } ) ) |
9 |
7 8
|
anim12i |
|- ( ( A e. ~H /\ B e. ~H ) -> ( A e. ( span ` { A } ) /\ B e. ( span ` { B } ) ) ) |
10 |
|
shsva |
|- ( ( ( span ` { A } ) e. SH /\ ( span ` { B } ) e. SH ) -> ( ( A e. ( span ` { A } ) /\ B e. ( span ` { B } ) ) -> ( A +h B ) e. ( ( span ` { A } ) +H ( span ` { B } ) ) ) ) |
11 |
6 9 10
|
sylc |
|- ( ( A e. ~H /\ B e. ~H ) -> ( A +h B ) e. ( ( span ` { A } ) +H ( span ` { B } ) ) ) |
12 |
11
|
adantr |
|- ( ( ( A e. ~H /\ B e. ~H ) /\ x e. ( span ` { ( A +h B ) } ) ) -> ( A +h B ) e. ( ( span ` { A } ) +H ( span ` { B } ) ) ) |
13 |
|
simpr |
|- ( ( ( A e. ~H /\ B e. ~H ) /\ x e. ( span ` { ( A +h B ) } ) ) -> x e. ( span ` { ( A +h B ) } ) ) |
14 |
|
elspansn3 |
|- ( ( ( ( span ` { A } ) +H ( span ` { B } ) ) e. SH /\ ( A +h B ) e. ( ( span ` { A } ) +H ( span ` { B } ) ) /\ x e. ( span ` { ( A +h B ) } ) ) -> x e. ( ( span ` { A } ) +H ( span ` { B } ) ) ) |
15 |
5 12 13 14
|
syl3anc |
|- ( ( ( A e. ~H /\ B e. ~H ) /\ x e. ( span ` { ( A +h B ) } ) ) -> x e. ( ( span ` { A } ) +H ( span ` { B } ) ) ) |
16 |
15
|
ex |
|- ( ( A e. ~H /\ B e. ~H ) -> ( x e. ( span ` { ( A +h B ) } ) -> x e. ( ( span ` { A } ) +H ( span ` { B } ) ) ) ) |
17 |
16
|
ssrdv |
|- ( ( A e. ~H /\ B e. ~H ) -> ( span ` { ( A +h B ) } ) C_ ( ( span ` { A } ) +H ( span ` { B } ) ) ) |
18 |
|
df-pr |
|- { A , B } = ( { A } u. { B } ) |
19 |
18
|
fveq2i |
|- ( span ` { A , B } ) = ( span ` ( { A } u. { B } ) ) |
20 |
|
snssi |
|- ( A e. ~H -> { A } C_ ~H ) |
21 |
|
snssi |
|- ( B e. ~H -> { B } C_ ~H ) |
22 |
|
spanun |
|- ( ( { A } C_ ~H /\ { B } C_ ~H ) -> ( span ` ( { A } u. { B } ) ) = ( ( span ` { A } ) +H ( span ` { B } ) ) ) |
23 |
20 21 22
|
syl2an |
|- ( ( A e. ~H /\ B e. ~H ) -> ( span ` ( { A } u. { B } ) ) = ( ( span ` { A } ) +H ( span ` { B } ) ) ) |
24 |
19 23
|
eqtr2id |
|- ( ( A e. ~H /\ B e. ~H ) -> ( ( span ` { A } ) +H ( span ` { B } ) ) = ( span ` { A , B } ) ) |
25 |
17 24
|
sseqtrd |
|- ( ( A e. ~H /\ B e. ~H ) -> ( span ` { ( A +h B ) } ) C_ ( span ` { A , B } ) ) |