Metamath Proof Explorer

Theorem spanun

Description: The span of a union is the subspace sum of spans. (Contributed by NM, 9-Jun-2006) (New usage is discouraged.)

Ref Expression
Assertion spanun ⊢ A ⊆ ℋ ∧ B ⊆ ℋ → span ⁡ A ∪ B = span ⁡ A + ℋ span ⁡ B

Proof

Step Hyp Ref Expression
1 uneq1 ⊢ A = if A ⊆ ℋ A ℋ → A ∪ B = if A ⊆ ℋ A ℋ ∪ B
2 1 fveq2d ⊢ A = if A ⊆ ℋ A ℋ → span ⁡ A ∪ B = span ⁡ if A ⊆ ℋ A ℋ ∪ B
3 fveq2 ⊢ A = if A ⊆ ℋ A ℋ → span ⁡ A = span ⁡ if A ⊆ ℋ A ℋ
4 3 oveq1d ⊢ A = if A ⊆ ℋ A ℋ → span ⁡ A + ℋ span ⁡ B = span ⁡ if A ⊆ ℋ A ℋ + ℋ span ⁡ B
5 2 4 eqeq12d ⊢ A = if A ⊆ ℋ A ℋ → span ⁡ A ∪ B = span ⁡ A + ℋ span ⁡ B ↔ span ⁡ if A ⊆ ℋ A ℋ ∪ B = span ⁡ if A ⊆ ℋ A ℋ + ℋ span ⁡ B
6 uneq2 ⊢ B = if B ⊆ ℋ B ℋ → if A ⊆ ℋ A ℋ ∪ B = if A ⊆ ℋ A ℋ ∪ if B ⊆ ℋ B ℋ
7 6 fveq2d ⊢ B = if B ⊆ ℋ B ℋ → span ⁡ if A ⊆ ℋ A ℋ ∪ B = span ⁡ if A ⊆ ℋ A ℋ ∪ if B ⊆ ℋ B ℋ
8 fveq2 ⊢ B = if B ⊆ ℋ B ℋ → span ⁡ B = span ⁡ if B ⊆ ℋ B ℋ
9 8 oveq2d ⊢ B = if B ⊆ ℋ B ℋ → span ⁡ if A ⊆ ℋ A ℋ + ℋ span ⁡ B = span ⁡ if A ⊆ ℋ A ℋ + ℋ span ⁡ if B ⊆ ℋ B ℋ
10 7 9 eqeq12d ⊢ B = if B ⊆ ℋ B ℋ → span ⁡ if A ⊆ ℋ A ℋ ∪ B = span ⁡ if A ⊆ ℋ A ℋ + ℋ span ⁡ B ↔ span ⁡ if A ⊆ ℋ A ℋ ∪ if B ⊆ ℋ B ℋ = span ⁡ if A ⊆ ℋ A ℋ + ℋ span ⁡ if B ⊆ ℋ B ℋ
11 sseq1 ⊢ A = if A ⊆ ℋ A ℋ → A ⊆ ℋ ↔ if A ⊆ ℋ A ℋ ⊆ ℋ
12 sseq1 ⊢ ℋ = if A ⊆ ℋ A ℋ → ℋ ⊆ ℋ ↔ if A ⊆ ℋ A ℋ ⊆ ℋ
13 ssid ⊢ ℋ ⊆ ℋ
14 11 12 13 elimhyp ⊢ if A ⊆ ℋ A ℋ ⊆ ℋ
15 sseq1 ⊢ B = if B ⊆ ℋ B ℋ → B ⊆ ℋ ↔ if B ⊆ ℋ B ℋ ⊆ ℋ
16 sseq1 ⊢ ℋ = if B ⊆ ℋ B ℋ → ℋ ⊆ ℋ ↔ if B ⊆ ℋ B ℋ ⊆ ℋ
17 15 16 13 elimhyp ⊢ if B ⊆ ℋ B ℋ ⊆ ℋ
18 14 17 spanuni ⊢ span ⁡ if A ⊆ ℋ A ℋ ∪ if B ⊆ ℋ B ℋ = span ⁡ if A ⊆ ℋ A ℋ + ℋ span ⁡ if B ⊆ ℋ B ℋ
19 5 10 18 dedth2h ⊢ A ⊆ ℋ ∧ B ⊆ ℋ → span ⁡ A ∪ B = span ⁡ A + ℋ span ⁡ B