Step |
Hyp |
Ref |
Expression |
1 |
|
spansnm0.1 |
⊢ 𝐴 ∈ ℋ |
2 |
|
spansnm0.2 |
⊢ 𝐵 ∈ ℋ |
3 |
2
|
spansnchi |
⊢ ( span ‘ { 𝐵 } ) ∈ Cℋ |
4 |
3
|
chshii |
⊢ ( span ‘ { 𝐵 } ) ∈ Sℋ |
5 |
|
elspansn5 |
⊢ ( ( span ‘ { 𝐵 } ) ∈ Sℋ → ( ( ( 𝐴 ∈ ℋ ∧ ¬ 𝐴 ∈ ( span ‘ { 𝐵 } ) ) ∧ ( 𝑥 ∈ ( span ‘ { 𝐴 } ) ∧ 𝑥 ∈ ( span ‘ { 𝐵 } ) ) ) → 𝑥 = 0ℎ ) ) |
6 |
4 5
|
ax-mp |
⊢ ( ( ( 𝐴 ∈ ℋ ∧ ¬ 𝐴 ∈ ( span ‘ { 𝐵 } ) ) ∧ ( 𝑥 ∈ ( span ‘ { 𝐴 } ) ∧ 𝑥 ∈ ( span ‘ { 𝐵 } ) ) ) → 𝑥 = 0ℎ ) |
7 |
1 6
|
mpanl1 |
⊢ ( ( ¬ 𝐴 ∈ ( span ‘ { 𝐵 } ) ∧ ( 𝑥 ∈ ( span ‘ { 𝐴 } ) ∧ 𝑥 ∈ ( span ‘ { 𝐵 } ) ) ) → 𝑥 = 0ℎ ) |
8 |
7
|
ex |
⊢ ( ¬ 𝐴 ∈ ( span ‘ { 𝐵 } ) → ( ( 𝑥 ∈ ( span ‘ { 𝐴 } ) ∧ 𝑥 ∈ ( span ‘ { 𝐵 } ) ) → 𝑥 = 0ℎ ) ) |
9 |
|
elin |
⊢ ( 𝑥 ∈ ( ( span ‘ { 𝐴 } ) ∩ ( span ‘ { 𝐵 } ) ) ↔ ( 𝑥 ∈ ( span ‘ { 𝐴 } ) ∧ 𝑥 ∈ ( span ‘ { 𝐵 } ) ) ) |
10 |
|
elch0 |
⊢ ( 𝑥 ∈ 0ℋ ↔ 𝑥 = 0ℎ ) |
11 |
8 9 10
|
3imtr4g |
⊢ ( ¬ 𝐴 ∈ ( span ‘ { 𝐵 } ) → ( 𝑥 ∈ ( ( span ‘ { 𝐴 } ) ∩ ( span ‘ { 𝐵 } ) ) → 𝑥 ∈ 0ℋ ) ) |
12 |
11
|
ssrdv |
⊢ ( ¬ 𝐴 ∈ ( span ‘ { 𝐵 } ) → ( ( span ‘ { 𝐴 } ) ∩ ( span ‘ { 𝐵 } ) ) ⊆ 0ℋ ) |
13 |
1
|
spansnchi |
⊢ ( span ‘ { 𝐴 } ) ∈ Cℋ |
14 |
13 3
|
chincli |
⊢ ( ( span ‘ { 𝐴 } ) ∩ ( span ‘ { 𝐵 } ) ) ∈ Cℋ |
15 |
14
|
chle0i |
⊢ ( ( ( span ‘ { 𝐴 } ) ∩ ( span ‘ { 𝐵 } ) ) ⊆ 0ℋ ↔ ( ( span ‘ { 𝐴 } ) ∩ ( span ‘ { 𝐵 } ) ) = 0ℋ ) |
16 |
12 15
|
sylib |
⊢ ( ¬ 𝐴 ∈ ( span ‘ { 𝐵 } ) → ( ( span ‘ { 𝐴 } ) ∩ ( span ‘ { 𝐵 } ) ) = 0ℋ ) |