Step |
Hyp |
Ref |
Expression |
1 |
|
atom1d |
⊢ ( 𝐵 ∈ HAtoms ↔ ∃ 𝑥 ∈ ℋ ( 𝑥 ≠ 0ℎ ∧ 𝐵 = ( span ‘ { 𝑥 } ) ) ) |
2 |
|
spansncv2 |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝑥 ∈ ℋ ) → ( ¬ ( span ‘ { 𝑥 } ) ⊆ 𝐴 → 𝐴 ⋖ℋ ( 𝐴 ∨ℋ ( span ‘ { 𝑥 } ) ) ) ) |
3 |
|
sseq1 |
⊢ ( 𝐵 = ( span ‘ { 𝑥 } ) → ( 𝐵 ⊆ 𝐴 ↔ ( span ‘ { 𝑥 } ) ⊆ 𝐴 ) ) |
4 |
3
|
notbid |
⊢ ( 𝐵 = ( span ‘ { 𝑥 } ) → ( ¬ 𝐵 ⊆ 𝐴 ↔ ¬ ( span ‘ { 𝑥 } ) ⊆ 𝐴 ) ) |
5 |
|
oveq2 |
⊢ ( 𝐵 = ( span ‘ { 𝑥 } ) → ( 𝐴 ∨ℋ 𝐵 ) = ( 𝐴 ∨ℋ ( span ‘ { 𝑥 } ) ) ) |
6 |
5
|
breq2d |
⊢ ( 𝐵 = ( span ‘ { 𝑥 } ) → ( 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) ↔ 𝐴 ⋖ℋ ( 𝐴 ∨ℋ ( span ‘ { 𝑥 } ) ) ) ) |
7 |
4 6
|
imbi12d |
⊢ ( 𝐵 = ( span ‘ { 𝑥 } ) → ( ( ¬ 𝐵 ⊆ 𝐴 → 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) ) ↔ ( ¬ ( span ‘ { 𝑥 } ) ⊆ 𝐴 → 𝐴 ⋖ℋ ( 𝐴 ∨ℋ ( span ‘ { 𝑥 } ) ) ) ) ) |
8 |
2 7
|
syl5ibrcom |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝑥 ∈ ℋ ) → ( 𝐵 = ( span ‘ { 𝑥 } ) → ( ¬ 𝐵 ⊆ 𝐴 → 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) |
9 |
8
|
adantld |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝑥 ∈ ℋ ) → ( ( 𝑥 ≠ 0ℎ ∧ 𝐵 = ( span ‘ { 𝑥 } ) ) → ( ¬ 𝐵 ⊆ 𝐴 → 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) |
10 |
9
|
rexlimdva |
⊢ ( 𝐴 ∈ Cℋ → ( ∃ 𝑥 ∈ ℋ ( 𝑥 ≠ 0ℎ ∧ 𝐵 = ( span ‘ { 𝑥 } ) ) → ( ¬ 𝐵 ⊆ 𝐴 → 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) |
11 |
10
|
imp |
⊢ ( ( 𝐴 ∈ Cℋ ∧ ∃ 𝑥 ∈ ℋ ( 𝑥 ≠ 0ℎ ∧ 𝐵 = ( span ‘ { 𝑥 } ) ) ) → ( ¬ 𝐵 ⊆ 𝐴 → 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) ) ) |
12 |
1 11
|
sylan2b |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ) → ( ¬ 𝐵 ⊆ 𝐴 → 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) ) ) |
13 |
|
atelch |
⊢ ( 𝐵 ∈ HAtoms → 𝐵 ∈ Cℋ ) |
14 |
|
chjcl |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 ∨ℋ 𝐵 ) ∈ Cℋ ) |
15 |
|
cvpss |
⊢ ( ( 𝐴 ∈ Cℋ ∧ ( 𝐴 ∨ℋ 𝐵 ) ∈ Cℋ ) → ( 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) → 𝐴 ⊊ ( 𝐴 ∨ℋ 𝐵 ) ) ) |
16 |
14 15
|
syldan |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) → 𝐴 ⊊ ( 𝐴 ∨ℋ 𝐵 ) ) ) |
17 |
|
chnle |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ¬ 𝐵 ⊆ 𝐴 ↔ 𝐴 ⊊ ( 𝐴 ∨ℋ 𝐵 ) ) ) |
18 |
16 17
|
sylibrd |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) → ¬ 𝐵 ⊆ 𝐴 ) ) |
19 |
13 18
|
sylan2 |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ) → ( 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) → ¬ 𝐵 ⊆ 𝐴 ) ) |
20 |
12 19
|
impbid |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ) → ( ¬ 𝐵 ⊆ 𝐴 ↔ 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) ) ) |