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 ‘ 𝐵 ) )