Step |
Hyp |
Ref |
Expression |
1 |
|
spansnsh |
⊢ ( 𝐴 ∈ ℋ → ( span ‘ { 𝐴 } ) ∈ Sℋ ) |
2 |
|
spansnsh |
⊢ ( 𝐵 ∈ ℋ → ( span ‘ { 𝐵 } ) ∈ Sℋ ) |
3 |
|
shscl |
⊢ ( ( ( span ‘ { 𝐴 } ) ∈ Sℋ ∧ ( span ‘ { 𝐵 } ) ∈ Sℋ ) → ( ( span ‘ { 𝐴 } ) +ℋ ( span ‘ { 𝐵 } ) ) ∈ Sℋ ) |
4 |
1 2 3
|
syl2an |
⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( span ‘ { 𝐴 } ) +ℋ ( span ‘ { 𝐵 } ) ) ∈ Sℋ ) |
5 |
4
|
adantr |
⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ 𝑥 ∈ ( span ‘ { ( 𝐴 +ℎ 𝐵 ) } ) ) → ( ( span ‘ { 𝐴 } ) +ℋ ( span ‘ { 𝐵 } ) ) ∈ Sℋ ) |
6 |
1 2
|
anim12i |
⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( span ‘ { 𝐴 } ) ∈ Sℋ ∧ ( span ‘ { 𝐵 } ) ∈ Sℋ ) ) |
7 |
|
spansnid |
⊢ ( 𝐴 ∈ ℋ → 𝐴 ∈ ( span ‘ { 𝐴 } ) ) |
8 |
|
spansnid |
⊢ ( 𝐵 ∈ ℋ → 𝐵 ∈ ( span ‘ { 𝐵 } ) ) |
9 |
7 8
|
anim12i |
⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 ∈ ( span ‘ { 𝐴 } ) ∧ 𝐵 ∈ ( span ‘ { 𝐵 } ) ) ) |
10 |
|
shsva |
⊢ ( ( ( span ‘ { 𝐴 } ) ∈ Sℋ ∧ ( span ‘ { 𝐵 } ) ∈ Sℋ ) → ( ( 𝐴 ∈ ( span ‘ { 𝐴 } ) ∧ 𝐵 ∈ ( span ‘ { 𝐵 } ) ) → ( 𝐴 +ℎ 𝐵 ) ∈ ( ( span ‘ { 𝐴 } ) +ℋ ( span ‘ { 𝐵 } ) ) ) ) |
11 |
6 9 10
|
sylc |
⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 +ℎ 𝐵 ) ∈ ( ( span ‘ { 𝐴 } ) +ℋ ( span ‘ { 𝐵 } ) ) ) |
12 |
11
|
adantr |
⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ 𝑥 ∈ ( span ‘ { ( 𝐴 +ℎ 𝐵 ) } ) ) → ( 𝐴 +ℎ 𝐵 ) ∈ ( ( span ‘ { 𝐴 } ) +ℋ ( span ‘ { 𝐵 } ) ) ) |
13 |
|
simpr |
⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ 𝑥 ∈ ( span ‘ { ( 𝐴 +ℎ 𝐵 ) } ) ) → 𝑥 ∈ ( span ‘ { ( 𝐴 +ℎ 𝐵 ) } ) ) |
14 |
|
elspansn3 |
⊢ ( ( ( ( span ‘ { 𝐴 } ) +ℋ ( span ‘ { 𝐵 } ) ) ∈ Sℋ ∧ ( 𝐴 +ℎ 𝐵 ) ∈ ( ( span ‘ { 𝐴 } ) +ℋ ( span ‘ { 𝐵 } ) ) ∧ 𝑥 ∈ ( span ‘ { ( 𝐴 +ℎ 𝐵 ) } ) ) → 𝑥 ∈ ( ( span ‘ { 𝐴 } ) +ℋ ( span ‘ { 𝐵 } ) ) ) |
15 |
5 12 13 14
|
syl3anc |
⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ 𝑥 ∈ ( span ‘ { ( 𝐴 +ℎ 𝐵 ) } ) ) → 𝑥 ∈ ( ( span ‘ { 𝐴 } ) +ℋ ( span ‘ { 𝐵 } ) ) ) |
16 |
15
|
ex |
⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝑥 ∈ ( span ‘ { ( 𝐴 +ℎ 𝐵 ) } ) → 𝑥 ∈ ( ( span ‘ { 𝐴 } ) +ℋ ( span ‘ { 𝐵 } ) ) ) ) |
17 |
16
|
ssrdv |
⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( span ‘ { ( 𝐴 +ℎ 𝐵 ) } ) ⊆ ( ( span ‘ { 𝐴 } ) +ℋ ( span ‘ { 𝐵 } ) ) ) |
18 |
|
df-pr |
⊢ { 𝐴 , 𝐵 } = ( { 𝐴 } ∪ { 𝐵 } ) |
19 |
18
|
fveq2i |
⊢ ( span ‘ { 𝐴 , 𝐵 } ) = ( span ‘ ( { 𝐴 } ∪ { 𝐵 } ) ) |
20 |
|
snssi |
⊢ ( 𝐴 ∈ ℋ → { 𝐴 } ⊆ ℋ ) |
21 |
|
snssi |
⊢ ( 𝐵 ∈ ℋ → { 𝐵 } ⊆ ℋ ) |
22 |
|
spanun |
⊢ ( ( { 𝐴 } ⊆ ℋ ∧ { 𝐵 } ⊆ ℋ ) → ( span ‘ ( { 𝐴 } ∪ { 𝐵 } ) ) = ( ( span ‘ { 𝐴 } ) +ℋ ( span ‘ { 𝐵 } ) ) ) |
23 |
20 21 22
|
syl2an |
⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( span ‘ ( { 𝐴 } ∪ { 𝐵 } ) ) = ( ( span ‘ { 𝐴 } ) +ℋ ( span ‘ { 𝐵 } ) ) ) |
24 |
19 23
|
eqtr2id |
⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( span ‘ { 𝐴 } ) +ℋ ( span ‘ { 𝐵 } ) ) = ( span ‘ { 𝐴 , 𝐵 } ) ) |
25 |
17 24
|
sseqtrd |
⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( span ‘ { ( 𝐴 +ℎ 𝐵 ) } ) ⊆ ( span ‘ { 𝐴 , 𝐵 } ) ) |