| Step | Hyp | Ref
| Expression |
| 1 | | spanun.1 |
. . . . . . 7
⊢ 𝐴 ⊆
ℋ |
| 2 | | spancl 31355 |
. . . . . . 7
⊢ (𝐴 ⊆ ℋ →
(span‘𝐴) ∈
Sℋ ) |
| 3 | 1, 2 | ax-mp 5 |
. . . . . 6
⊢
(span‘𝐴)
∈ Sℋ |
| 4 | | spanun.2 |
. . . . . . 7
⊢ 𝐵 ⊆
ℋ |
| 5 | | spancl 31355 |
. . . . . . 7
⊢ (𝐵 ⊆ ℋ →
(span‘𝐵) ∈
Sℋ ) |
| 6 | 4, 5 | ax-mp 5 |
. . . . . 6
⊢
(span‘𝐵)
∈ Sℋ |
| 7 | 3, 6 | shscli 31336 |
. . . . 5
⊢
((span‘𝐴)
+ℋ (span‘𝐵)) ∈
Sℋ |
| 8 | 7 | shssii 31232 |
. . . 4
⊢
((span‘𝐴)
+ℋ (span‘𝐵)) ⊆ ℋ |
| 9 | | spanss2 31364 |
. . . . . . 7
⊢ (𝐴 ⊆ ℋ → 𝐴 ⊆ (span‘𝐴)) |
| 10 | 1, 9 | ax-mp 5 |
. . . . . 6
⊢ 𝐴 ⊆ (span‘𝐴) |
| 11 | | spanss2 31364 |
. . . . . . 7
⊢ (𝐵 ⊆ ℋ → 𝐵 ⊆ (span‘𝐵)) |
| 12 | 4, 11 | ax-mp 5 |
. . . . . 6
⊢ 𝐵 ⊆ (span‘𝐵) |
| 13 | | unss12 4188 |
. . . . . 6
⊢ ((𝐴 ⊆ (span‘𝐴) ∧ 𝐵 ⊆ (span‘𝐵)) → (𝐴 ∪ 𝐵) ⊆ ((span‘𝐴) ∪ (span‘𝐵))) |
| 14 | 10, 12, 13 | mp2an 692 |
. . . . 5
⊢ (𝐴 ∪ 𝐵) ⊆ ((span‘𝐴) ∪ (span‘𝐵)) |
| 15 | 3, 6 | shunssi 31387 |
. . . . 5
⊢
((span‘𝐴)
∪ (span‘𝐵))
⊆ ((span‘𝐴)
+ℋ (span‘𝐵)) |
| 16 | 14, 15 | sstri 3993 |
. . . 4
⊢ (𝐴 ∪ 𝐵) ⊆ ((span‘𝐴) +ℋ (span‘𝐵)) |
| 17 | | spanss 31367 |
. . . 4
⊢
((((span‘𝐴)
+ℋ (span‘𝐵)) ⊆ ℋ ∧ (𝐴 ∪ 𝐵) ⊆ ((span‘𝐴) +ℋ (span‘𝐵))) → (span‘(𝐴 ∪ 𝐵)) ⊆ (span‘((span‘𝐴) +ℋ
(span‘𝐵)))) |
| 18 | 8, 16, 17 | mp2an 692 |
. . 3
⊢
(span‘(𝐴 ∪
𝐵)) ⊆
(span‘((span‘𝐴)
+ℋ (span‘𝐵))) |
| 19 | | spanid 31366 |
. . . 4
⊢
(((span‘𝐴)
+ℋ (span‘𝐵)) ∈ Sℋ
→ (span‘((span‘𝐴) +ℋ (span‘𝐵))) = ((span‘𝐴) +ℋ
(span‘𝐵))) |
| 20 | 7, 19 | ax-mp 5 |
. . 3
⊢
(span‘((span‘𝐴) +ℋ (span‘𝐵))) = ((span‘𝐴) +ℋ
(span‘𝐵)) |
| 21 | 18, 20 | sseqtri 4032 |
. 2
⊢
(span‘(𝐴 ∪
𝐵)) ⊆
((span‘𝐴)
+ℋ (span‘𝐵)) |
| 22 | 3, 6 | shseli 31335 |
. . . . 5
⊢ (𝑥 ∈ ((span‘𝐴) +ℋ
(span‘𝐵)) ↔
∃𝑧 ∈
(span‘𝐴)∃𝑤 ∈ (span‘𝐵)𝑥 = (𝑧 +ℎ 𝑤)) |
| 23 | | r2ex 3196 |
. . . . 5
⊢
(∃𝑧 ∈
(span‘𝐴)∃𝑤 ∈ (span‘𝐵)𝑥 = (𝑧 +ℎ 𝑤) ↔ ∃𝑧∃𝑤((𝑧 ∈ (span‘𝐴) ∧ 𝑤 ∈ (span‘𝐵)) ∧ 𝑥 = (𝑧 +ℎ 𝑤))) |
| 24 | 22, 23 | bitri 275 |
. . . 4
⊢ (𝑥 ∈ ((span‘𝐴) +ℋ
(span‘𝐵)) ↔
∃𝑧∃𝑤((𝑧 ∈ (span‘𝐴) ∧ 𝑤 ∈ (span‘𝐵)) ∧ 𝑥 = (𝑧 +ℎ 𝑤))) |
| 25 | | vex 3484 |
. . . . . . . . . . 11
⊢ 𝑧 ∈ V |
| 26 | 25 | elspani 31562 |
. . . . . . . . . 10
⊢ (𝐴 ⊆ ℋ → (𝑧 ∈ (span‘𝐴) ↔ ∀𝑦 ∈
Sℋ (𝐴 ⊆ 𝑦 → 𝑧 ∈ 𝑦))) |
| 27 | 1, 26 | ax-mp 5 |
. . . . . . . . 9
⊢ (𝑧 ∈ (span‘𝐴) ↔ ∀𝑦 ∈
Sℋ (𝐴 ⊆ 𝑦 → 𝑧 ∈ 𝑦)) |
| 28 | | vex 3484 |
. . . . . . . . . . 11
⊢ 𝑤 ∈ V |
| 29 | 28 | elspani 31562 |
. . . . . . . . . 10
⊢ (𝐵 ⊆ ℋ → (𝑤 ∈ (span‘𝐵) ↔ ∀𝑦 ∈
Sℋ (𝐵 ⊆ 𝑦 → 𝑤 ∈ 𝑦))) |
| 30 | 4, 29 | ax-mp 5 |
. . . . . . . . 9
⊢ (𝑤 ∈ (span‘𝐵) ↔ ∀𝑦 ∈
Sℋ (𝐵 ⊆ 𝑦 → 𝑤 ∈ 𝑦)) |
| 31 | 27, 30 | anbi12i 628 |
. . . . . . . 8
⊢ ((𝑧 ∈ (span‘𝐴) ∧ 𝑤 ∈ (span‘𝐵)) ↔ (∀𝑦 ∈ Sℋ
(𝐴 ⊆ 𝑦 → 𝑧 ∈ 𝑦) ∧ ∀𝑦 ∈ Sℋ
(𝐵 ⊆ 𝑦 → 𝑤 ∈ 𝑦))) |
| 32 | | r19.26 3111 |
. . . . . . . 8
⊢
(∀𝑦 ∈
Sℋ ((𝐴 ⊆ 𝑦 → 𝑧 ∈ 𝑦) ∧ (𝐵 ⊆ 𝑦 → 𝑤 ∈ 𝑦)) ↔ (∀𝑦 ∈ Sℋ
(𝐴 ⊆ 𝑦 → 𝑧 ∈ 𝑦) ∧ ∀𝑦 ∈ Sℋ
(𝐵 ⊆ 𝑦 → 𝑤 ∈ 𝑦))) |
| 33 | 31, 32 | bitr4i 278 |
. . . . . . 7
⊢ ((𝑧 ∈ (span‘𝐴) ∧ 𝑤 ∈ (span‘𝐵)) ↔ ∀𝑦 ∈ Sℋ
((𝐴 ⊆ 𝑦 → 𝑧 ∈ 𝑦) ∧ (𝐵 ⊆ 𝑦 → 𝑤 ∈ 𝑦))) |
| 34 | | r19.27v 3188 |
. . . . . . 7
⊢
((∀𝑦 ∈
Sℋ ((𝐴 ⊆ 𝑦 → 𝑧 ∈ 𝑦) ∧ (𝐵 ⊆ 𝑦 → 𝑤 ∈ 𝑦)) ∧ 𝑥 = (𝑧 +ℎ 𝑤)) → ∀𝑦 ∈ Sℋ
(((𝐴 ⊆ 𝑦 → 𝑧 ∈ 𝑦) ∧ (𝐵 ⊆ 𝑦 → 𝑤 ∈ 𝑦)) ∧ 𝑥 = (𝑧 +ℎ 𝑤))) |
| 35 | 33, 34 | sylanb 581 |
. . . . . 6
⊢ (((𝑧 ∈ (span‘𝐴) ∧ 𝑤 ∈ (span‘𝐵)) ∧ 𝑥 = (𝑧 +ℎ 𝑤)) → ∀𝑦 ∈ Sℋ
(((𝐴 ⊆ 𝑦 → 𝑧 ∈ 𝑦) ∧ (𝐵 ⊆ 𝑦 → 𝑤 ∈ 𝑦)) ∧ 𝑥 = (𝑧 +ℎ 𝑤))) |
| 36 | | unss 4190 |
. . . . . . . . . . . 12
⊢ ((𝐴 ⊆ 𝑦 ∧ 𝐵 ⊆ 𝑦) ↔ (𝐴 ∪ 𝐵) ⊆ 𝑦) |
| 37 | | anim12 809 |
. . . . . . . . . . . 12
⊢ (((𝐴 ⊆ 𝑦 → 𝑧 ∈ 𝑦) ∧ (𝐵 ⊆ 𝑦 → 𝑤 ∈ 𝑦)) → ((𝐴 ⊆ 𝑦 ∧ 𝐵 ⊆ 𝑦) → (𝑧 ∈ 𝑦 ∧ 𝑤 ∈ 𝑦))) |
| 38 | 36, 37 | biimtrrid 243 |
. . . . . . . . . . 11
⊢ (((𝐴 ⊆ 𝑦 → 𝑧 ∈ 𝑦) ∧ (𝐵 ⊆ 𝑦 → 𝑤 ∈ 𝑦)) → ((𝐴 ∪ 𝐵) ⊆ 𝑦 → (𝑧 ∈ 𝑦 ∧ 𝑤 ∈ 𝑦))) |
| 39 | | shaddcl 31236 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈
Sℋ ∧ 𝑧 ∈ 𝑦 ∧ 𝑤 ∈ 𝑦) → (𝑧 +ℎ 𝑤) ∈ 𝑦) |
| 40 | 39 | 3expib 1123 |
. . . . . . . . . . 11
⊢ (𝑦 ∈
Sℋ → ((𝑧 ∈ 𝑦 ∧ 𝑤 ∈ 𝑦) → (𝑧 +ℎ 𝑤) ∈ 𝑦)) |
| 41 | 38, 40 | sylan9r 508 |
. . . . . . . . . 10
⊢ ((𝑦 ∈
Sℋ ∧ ((𝐴 ⊆ 𝑦 → 𝑧 ∈ 𝑦) ∧ (𝐵 ⊆ 𝑦 → 𝑤 ∈ 𝑦))) → ((𝐴 ∪ 𝐵) ⊆ 𝑦 → (𝑧 +ℎ 𝑤) ∈ 𝑦)) |
| 42 | | eleq1 2829 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑧 +ℎ 𝑤) → (𝑥 ∈ 𝑦 ↔ (𝑧 +ℎ 𝑤) ∈ 𝑦)) |
| 43 | 42 | biimprd 248 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑧 +ℎ 𝑤) → ((𝑧 +ℎ 𝑤) ∈ 𝑦 → 𝑥 ∈ 𝑦)) |
| 44 | 41, 43 | sylan9 507 |
. . . . . . . . 9
⊢ (((𝑦 ∈
Sℋ ∧ ((𝐴 ⊆ 𝑦 → 𝑧 ∈ 𝑦) ∧ (𝐵 ⊆ 𝑦 → 𝑤 ∈ 𝑦))) ∧ 𝑥 = (𝑧 +ℎ 𝑤)) → ((𝐴 ∪ 𝐵) ⊆ 𝑦 → 𝑥 ∈ 𝑦)) |
| 45 | 44 | expl 457 |
. . . . . . . 8
⊢ (𝑦 ∈
Sℋ → ((((𝐴 ⊆ 𝑦 → 𝑧 ∈ 𝑦) ∧ (𝐵 ⊆ 𝑦 → 𝑤 ∈ 𝑦)) ∧ 𝑥 = (𝑧 +ℎ 𝑤)) → ((𝐴 ∪ 𝐵) ⊆ 𝑦 → 𝑥 ∈ 𝑦))) |
| 46 | 45 | ralimia 3080 |
. . . . . . 7
⊢
(∀𝑦 ∈
Sℋ (((𝐴 ⊆ 𝑦 → 𝑧 ∈ 𝑦) ∧ (𝐵 ⊆ 𝑦 → 𝑤 ∈ 𝑦)) ∧ 𝑥 = (𝑧 +ℎ 𝑤)) → ∀𝑦 ∈ Sℋ
((𝐴 ∪ 𝐵) ⊆ 𝑦 → 𝑥 ∈ 𝑦)) |
| 47 | 1, 4 | unssi 4191 |
. . . . . . . 8
⊢ (𝐴 ∪ 𝐵) ⊆ ℋ |
| 48 | | vex 3484 |
. . . . . . . . 9
⊢ 𝑥 ∈ V |
| 49 | 48 | elspani 31562 |
. . . . . . . 8
⊢ ((𝐴 ∪ 𝐵) ⊆ ℋ → (𝑥 ∈ (span‘(𝐴 ∪ 𝐵)) ↔ ∀𝑦 ∈ Sℋ
((𝐴 ∪ 𝐵) ⊆ 𝑦 → 𝑥 ∈ 𝑦))) |
| 50 | 47, 49 | ax-mp 5 |
. . . . . . 7
⊢ (𝑥 ∈ (span‘(𝐴 ∪ 𝐵)) ↔ ∀𝑦 ∈ Sℋ
((𝐴 ∪ 𝐵) ⊆ 𝑦 → 𝑥 ∈ 𝑦)) |
| 51 | 46, 50 | sylibr 234 |
. . . . . 6
⊢
(∀𝑦 ∈
Sℋ (((𝐴 ⊆ 𝑦 → 𝑧 ∈ 𝑦) ∧ (𝐵 ⊆ 𝑦 → 𝑤 ∈ 𝑦)) ∧ 𝑥 = (𝑧 +ℎ 𝑤)) → 𝑥 ∈ (span‘(𝐴 ∪ 𝐵))) |
| 52 | 35, 51 | syl 17 |
. . . . 5
⊢ (((𝑧 ∈ (span‘𝐴) ∧ 𝑤 ∈ (span‘𝐵)) ∧ 𝑥 = (𝑧 +ℎ 𝑤)) → 𝑥 ∈ (span‘(𝐴 ∪ 𝐵))) |
| 53 | 52 | exlimivv 1932 |
. . . 4
⊢
(∃𝑧∃𝑤((𝑧 ∈ (span‘𝐴) ∧ 𝑤 ∈ (span‘𝐵)) ∧ 𝑥 = (𝑧 +ℎ 𝑤)) → 𝑥 ∈ (span‘(𝐴 ∪ 𝐵))) |
| 54 | 24, 53 | sylbi 217 |
. . 3
⊢ (𝑥 ∈ ((span‘𝐴) +ℋ
(span‘𝐵)) →
𝑥 ∈ (span‘(𝐴 ∪ 𝐵))) |
| 55 | 54 | ssriv 3987 |
. 2
⊢
((span‘𝐴)
+ℋ (span‘𝐵)) ⊆ (span‘(𝐴 ∪ 𝐵)) |
| 56 | 21, 55 | eqssi 4000 |
1
⊢
(span‘(𝐴 ∪
𝐵)) = ((span‘𝐴) +ℋ
(span‘𝐵)) |