Metamath Proof Explorer

Theorem spanuni

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

Ref Expression
Hypotheses spanun.1 ⊢ 𝐴 ⊆ ℋ
spanun.2 ⊢ 𝐵 ⊆ ℋ
Assertion spanuni ( span ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( span ‘ 𝐴 ) +ℋ ( span ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 spanun.1 ⊢ 𝐴 ⊆ ℋ
2 spanun.2 ⊢ 𝐵 ⊆ ℋ
3 spancl ⊢ ( 𝐴 ⊆ ℋ → ( span ‘ 𝐴 ) ∈ Sℋ )
4 1 3 ax-mp ⊢ ( span ‘ 𝐴 ) ∈ Sℋ
5 spancl ⊢ ( 𝐵 ⊆ ℋ → ( span ‘ 𝐵 ) ∈ Sℋ )
6 2 5 ax-mp ⊢ ( span ‘ 𝐵 ) ∈ Sℋ
7 4 6 shscli ⊢ ( ( span ‘ 𝐴 ) +ℋ ( span ‘ 𝐵 ) ) ∈ Sℋ
8 7 shssii ⊢ ( ( span ‘ 𝐴 ) +ℋ ( span ‘ 𝐵 ) ) ⊆ ℋ
9 spanss2 ⊢ ( 𝐴 ⊆ ℋ → 𝐴 ⊆ ( span ‘ 𝐴 ) )
10 1 9 ax-mp ⊢ 𝐴 ⊆ ( span ‘ 𝐴 )
11 spanss2 ⊢ ( 𝐵 ⊆ ℋ → 𝐵 ⊆ ( span ‘ 𝐵 ) )
12 2 11 ax-mp ⊢ 𝐵 ⊆ ( span ‘ 𝐵 )
13 unss12 ⊢ ( ( 𝐴 ⊆ ( span ‘ 𝐴 ) ∧ 𝐵 ⊆ ( span ‘ 𝐵 ) ) → ( 𝐴 ∪ 𝐵 ) ⊆ ( ( span ‘ 𝐴 ) ∪ ( span ‘ 𝐵 ) ) )
14 10 12 13 mp2an ⊢ ( 𝐴 ∪ 𝐵 ) ⊆ ( ( span ‘ 𝐴 ) ∪ ( span ‘ 𝐵 ) )
15 4 6 shunssi ⊢ ( ( span ‘ 𝐴 ) ∪ ( span ‘ 𝐵 ) ) ⊆ ( ( span ‘ 𝐴 ) +ℋ ( span ‘ 𝐵 ) )
16 14 15 sstri ⊢ ( 𝐴 ∪ 𝐵 ) ⊆ ( ( span ‘ 𝐴 ) +ℋ ( span ‘ 𝐵 ) )
17 spanss ⊢ ( ( ( ( span ‘ 𝐴 ) +ℋ ( span ‘ 𝐵 ) ) ⊆ ℋ ∧ ( 𝐴 ∪ 𝐵 ) ⊆ ( ( span ‘ 𝐴 ) +ℋ ( span ‘ 𝐵 ) ) ) → ( span ‘ ( 𝐴 ∪ 𝐵 ) ) ⊆ ( span ‘ ( ( span ‘ 𝐴 ) +ℋ ( span ‘ 𝐵 ) ) ) )
18 8 16 17 mp2an ⊢ ( span ‘ ( 𝐴 ∪ 𝐵 ) ) ⊆ ( span ‘ ( ( span ‘ 𝐴 ) +ℋ ( span ‘ 𝐵 ) ) )
19 spanid ⊢ ( ( ( span ‘ 𝐴 ) +ℋ ( span ‘ 𝐵 ) ) ∈ Sℋ → ( span ‘ ( ( span ‘ 𝐴 ) +ℋ ( span ‘ 𝐵 ) ) ) = ( ( span ‘ 𝐴 ) +ℋ ( span ‘ 𝐵 ) ) )
20 7 19 ax-mp ⊢ ( span ‘ ( ( span ‘ 𝐴 ) +ℋ ( span ‘ 𝐵 ) ) ) = ( ( span ‘ 𝐴 ) +ℋ ( span ‘ 𝐵 ) )
21 18 20 sseqtri ⊢ ( span ‘ ( 𝐴 ∪ 𝐵 ) ) ⊆ ( ( span ‘ 𝐴 ) +ℋ ( span ‘ 𝐵 ) )
22 4 6 shseli ⊢ ( 𝑥 ∈ ( ( span ‘ 𝐴 ) +ℋ ( span ‘ 𝐵 ) ) ↔ ∃ 𝑧 ∈ ( span ‘ 𝐴 ) ∃ 𝑤 ∈ ( span ‘ 𝐵 ) 𝑥 = ( 𝑧 +ℎ 𝑤 ) )
23 r2ex ⊢ ( ∃ 𝑧 ∈ ( span ‘ 𝐴 ) ∃ 𝑤 ∈ ( span ‘ 𝐵 ) 𝑥 = ( 𝑧 +ℎ 𝑤 ) ↔ ∃ 𝑧 ∃ 𝑤 ( ( 𝑧 ∈ ( span ‘ 𝐴 ) ∧ 𝑤 ∈ ( span ‘ 𝐵 ) ) ∧ 𝑥 = ( 𝑧 +ℎ 𝑤 ) ) )
24 22 23 bitri ⊢ ( 𝑥 ∈ ( ( span ‘ 𝐴 ) +ℋ ( span ‘ 𝐵 ) ) ↔ ∃ 𝑧 ∃ 𝑤 ( ( 𝑧 ∈ ( span ‘ 𝐴 ) ∧ 𝑤 ∈ ( span ‘ 𝐵 ) ) ∧ 𝑥 = ( 𝑧 +ℎ 𝑤 ) ) )
25 vex ⊢ 𝑧 ∈ V
26 25 elspani ⊢ ( 𝐴 ⊆ ℋ → ( 𝑧 ∈ ( span ‘ 𝐴 ) ↔ ∀ 𝑦 ∈ Sℋ ( 𝐴 ⊆ 𝑦 → 𝑧 ∈ 𝑦 ) ) )
27 1 26 ax-mp ⊢ ( 𝑧 ∈ ( span ‘ 𝐴 ) ↔ ∀ 𝑦 ∈ Sℋ ( 𝐴 ⊆ 𝑦 → 𝑧 ∈ 𝑦 ) )
28 vex ⊢ 𝑤 ∈ V
29 28 elspani ⊢ ( 𝐵 ⊆ ℋ → ( 𝑤 ∈ ( span ‘ 𝐵 ) ↔ ∀ 𝑦 ∈ Sℋ ( 𝐵 ⊆ 𝑦 → 𝑤 ∈ 𝑦 ) ) )
30 2 29 ax-mp ⊢ ( 𝑤 ∈ ( span ‘ 𝐵 ) ↔ ∀ 𝑦 ∈ Sℋ ( 𝐵 ⊆ 𝑦 → 𝑤 ∈ 𝑦 ) )
31 27 30 anbi12i ⊢ ( ( 𝑧 ∈ ( span ‘ 𝐴 ) ∧ 𝑤 ∈ ( span ‘ 𝐵 ) ) ↔ ( ∀ 𝑦 ∈ Sℋ ( 𝐴 ⊆ 𝑦 → 𝑧 ∈ 𝑦 ) ∧ ∀ 𝑦 ∈ Sℋ ( 𝐵 ⊆ 𝑦 → 𝑤 ∈ 𝑦 ) ) )
32 r19.26 ⊢ ( ∀ 𝑦 ∈ Sℋ ( ( 𝐴 ⊆ 𝑦 → 𝑧 ∈ 𝑦 ) ∧ ( 𝐵 ⊆ 𝑦 → 𝑤 ∈ 𝑦 ) ) ↔ ( ∀ 𝑦 ∈ Sℋ ( 𝐴 ⊆ 𝑦 → 𝑧 ∈ 𝑦 ) ∧ ∀ 𝑦 ∈ Sℋ ( 𝐵 ⊆ 𝑦 → 𝑤 ∈ 𝑦 ) ) )
33 31 32 bitr4i ⊢ ( ( 𝑧 ∈ ( span ‘ 𝐴 ) ∧ 𝑤 ∈ ( span ‘ 𝐵 ) ) ↔ ∀ 𝑦 ∈ Sℋ ( ( 𝐴 ⊆ 𝑦 → 𝑧 ∈ 𝑦 ) ∧ ( 𝐵 ⊆ 𝑦 → 𝑤 ∈ 𝑦 ) ) )
34 r19.27v ⊢ ( ( ∀ 𝑦 ∈ Sℋ ( ( 𝐴 ⊆ 𝑦 → 𝑧 ∈ 𝑦 ) ∧ ( 𝐵 ⊆ 𝑦 → 𝑤 ∈ 𝑦 ) ) ∧ 𝑥 = ( 𝑧 +ℎ 𝑤 ) ) → ∀ 𝑦 ∈ Sℋ ( ( ( 𝐴 ⊆ 𝑦 → 𝑧 ∈ 𝑦 ) ∧ ( 𝐵 ⊆ 𝑦 → 𝑤 ∈ 𝑦 ) ) ∧ 𝑥 = ( 𝑧 +ℎ 𝑤 ) ) )
35 33 34 sylanb ⊢ ( ( ( 𝑧 ∈ ( span ‘ 𝐴 ) ∧ 𝑤 ∈ ( span ‘ 𝐵 ) ) ∧ 𝑥 = ( 𝑧 +ℎ 𝑤 ) ) → ∀ 𝑦 ∈ Sℋ ( ( ( 𝐴 ⊆ 𝑦 → 𝑧 ∈ 𝑦 ) ∧ ( 𝐵 ⊆ 𝑦 → 𝑤 ∈ 𝑦 ) ) ∧ 𝑥 = ( 𝑧 +ℎ 𝑤 ) ) )
36 unss ⊢ ( ( 𝐴 ⊆ 𝑦 ∧ 𝐵 ⊆ 𝑦 ) ↔ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑦 )
37 anim12 ⊢ ( ( ( 𝐴 ⊆ 𝑦 → 𝑧 ∈ 𝑦 ) ∧ ( 𝐵 ⊆ 𝑦 → 𝑤 ∈ 𝑦 ) ) → ( ( 𝐴 ⊆ 𝑦 ∧ 𝐵 ⊆ 𝑦 ) → ( 𝑧 ∈ 𝑦 ∧ 𝑤 ∈ 𝑦 ) ) )
38 36 37 syl5bir ⊢ ( ( ( 𝐴 ⊆ 𝑦 → 𝑧 ∈ 𝑦 ) ∧ ( 𝐵 ⊆ 𝑦 → 𝑤 ∈ 𝑦 ) ) → ( ( 𝐴 ∪ 𝐵 ) ⊆ 𝑦 → ( 𝑧 ∈ 𝑦 ∧ 𝑤 ∈ 𝑦 ) ) )
39 shaddcl ⊢ ( ( 𝑦 ∈ Sℋ ∧ 𝑧 ∈ 𝑦 ∧ 𝑤 ∈ 𝑦 ) → ( 𝑧 +ℎ 𝑤 ) ∈ 𝑦 )
40 39 3expib ⊢ ( 𝑦 ∈ Sℋ → ( ( 𝑧 ∈ 𝑦 ∧ 𝑤 ∈ 𝑦 ) → ( 𝑧 +ℎ 𝑤 ) ∈ 𝑦 ) )
41 38 40 sylan9r ⊢ ( ( 𝑦 ∈ Sℋ ∧ ( ( 𝐴 ⊆ 𝑦 → 𝑧 ∈ 𝑦 ) ∧ ( 𝐵 ⊆ 𝑦 → 𝑤 ∈ 𝑦 ) ) ) → ( ( 𝐴 ∪ 𝐵 ) ⊆ 𝑦 → ( 𝑧 +ℎ 𝑤 ) ∈ 𝑦 ) )
42 eleq1 ⊢ ( 𝑥 = ( 𝑧 +ℎ 𝑤 ) → ( 𝑥 ∈ 𝑦 ↔ ( 𝑧 +ℎ 𝑤 ) ∈ 𝑦 ) )
43 42 biimprd ⊢ ( 𝑥 = ( 𝑧 +ℎ 𝑤 ) → ( ( 𝑧 +ℎ 𝑤 ) ∈ 𝑦 → 𝑥 ∈ 𝑦 ) )
44 41 43 sylan9 ⊢ ( ( ( 𝑦 ∈ Sℋ ∧ ( ( 𝐴 ⊆ 𝑦 → 𝑧 ∈ 𝑦 ) ∧ ( 𝐵 ⊆ 𝑦 → 𝑤 ∈ 𝑦 ) ) ) ∧ 𝑥 = ( 𝑧 +ℎ 𝑤 ) ) → ( ( 𝐴 ∪ 𝐵 ) ⊆ 𝑦 → 𝑥 ∈ 𝑦 ) )
45 44 expl ⊢ ( 𝑦 ∈ Sℋ → ( ( ( ( 𝐴 ⊆ 𝑦 → 𝑧 ∈ 𝑦 ) ∧ ( 𝐵 ⊆ 𝑦 → 𝑤 ∈ 𝑦 ) ) ∧ 𝑥 = ( 𝑧 +ℎ 𝑤 ) ) → ( ( 𝐴 ∪ 𝐵 ) ⊆ 𝑦 → 𝑥 ∈ 𝑦 ) ) )
46 45 ralimia ⊢ ( ∀ 𝑦 ∈ Sℋ ( ( ( 𝐴 ⊆ 𝑦 → 𝑧 ∈ 𝑦 ) ∧ ( 𝐵 ⊆ 𝑦 → 𝑤 ∈ 𝑦 ) ) ∧ 𝑥 = ( 𝑧 +ℎ 𝑤 ) ) → ∀ 𝑦 ∈ Sℋ ( ( 𝐴 ∪ 𝐵 ) ⊆ 𝑦 → 𝑥 ∈ 𝑦 ) )
47 1 2 unssi ⊢ ( 𝐴 ∪ 𝐵 ) ⊆ ℋ
48 vex ⊢ 𝑥 ∈ V
49 48 elspani ⊢ ( ( 𝐴 ∪ 𝐵 ) ⊆ ℋ → ( 𝑥 ∈ ( span ‘ ( 𝐴 ∪ 𝐵 ) ) ↔ ∀ 𝑦 ∈ Sℋ ( ( 𝐴 ∪ 𝐵 ) ⊆ 𝑦 → 𝑥 ∈ 𝑦 ) ) )
50 47 49 ax-mp ⊢ ( 𝑥 ∈ ( span ‘ ( 𝐴 ∪ 𝐵 ) ) ↔ ∀ 𝑦 ∈ Sℋ ( ( 𝐴 ∪ 𝐵 ) ⊆ 𝑦 → 𝑥 ∈ 𝑦 ) )
51 46 50 sylibr ⊢ ( ∀ 𝑦 ∈ Sℋ ( ( ( 𝐴 ⊆ 𝑦 → 𝑧 ∈ 𝑦 ) ∧ ( 𝐵 ⊆ 𝑦 → 𝑤 ∈ 𝑦 ) ) ∧ 𝑥 = ( 𝑧 +ℎ 𝑤 ) ) → 𝑥 ∈ ( span ‘ ( 𝐴 ∪ 𝐵 ) ) )
52 35 51 syl ⊢ ( ( ( 𝑧 ∈ ( span ‘ 𝐴 ) ∧ 𝑤 ∈ ( span ‘ 𝐵 ) ) ∧ 𝑥 = ( 𝑧 +ℎ 𝑤 ) ) → 𝑥 ∈ ( span ‘ ( 𝐴 ∪ 𝐵 ) ) )
53 52 exlimivv ⊢ ( ∃ 𝑧 ∃ 𝑤 ( ( 𝑧 ∈ ( span ‘ 𝐴 ) ∧ 𝑤 ∈ ( span ‘ 𝐵 ) ) ∧ 𝑥 = ( 𝑧 +ℎ 𝑤 ) ) → 𝑥 ∈ ( span ‘ ( 𝐴 ∪ 𝐵 ) ) )
54 24 53 sylbi ⊢ ( 𝑥 ∈ ( ( span ‘ 𝐴 ) +ℋ ( span ‘ 𝐵 ) ) → 𝑥 ∈ ( span ‘ ( 𝐴 ∪ 𝐵 ) ) )
55 54 ssriv ⊢ ( ( span ‘ 𝐴 ) +ℋ ( span ‘ 𝐵 ) ) ⊆ ( span ‘ ( 𝐴 ∪ 𝐵 ) )
56 21 55 eqssi ⊢ ( span ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( span ‘ 𝐴 ) +ℋ ( span ‘ 𝐵 ) )