Step |
Hyp |
Ref |
Expression |
1 |
|
atom1d |
⊢ ( 𝐵 ∈ HAtoms ↔ ∃ 𝑥 ∈ ℋ ( 𝑥 ≠ 0ℎ ∧ 𝐵 = ( span ‘ { 𝑥 } ) ) ) |
2 |
|
spansnj |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝑥 ∈ ℋ ) → ( 𝐴 +ℋ ( span ‘ { 𝑥 } ) ) = ( 𝐴 ∨ℋ ( span ‘ { 𝑥 } ) ) ) |
3 |
|
oveq2 |
⊢ ( 𝐵 = ( span ‘ { 𝑥 } ) → ( 𝐴 +ℋ 𝐵 ) = ( 𝐴 +ℋ ( span ‘ { 𝑥 } ) ) ) |
4 |
|
oveq2 |
⊢ ( 𝐵 = ( span ‘ { 𝑥 } ) → ( 𝐴 ∨ℋ 𝐵 ) = ( 𝐴 ∨ℋ ( span ‘ { 𝑥 } ) ) ) |
5 |
3 4
|
eqeq12d |
⊢ ( 𝐵 = ( span ‘ { 𝑥 } ) → ( ( 𝐴 +ℋ 𝐵 ) = ( 𝐴 ∨ℋ 𝐵 ) ↔ ( 𝐴 +ℋ ( span ‘ { 𝑥 } ) ) = ( 𝐴 ∨ℋ ( span ‘ { 𝑥 } ) ) ) ) |
6 |
2 5
|
syl5ibr |
⊢ ( 𝐵 = ( span ‘ { 𝑥 } ) → ( ( 𝐴 ∈ Cℋ ∧ 𝑥 ∈ ℋ ) → ( 𝐴 +ℋ 𝐵 ) = ( 𝐴 ∨ℋ 𝐵 ) ) ) |
7 |
6
|
expd |
⊢ ( 𝐵 = ( span ‘ { 𝑥 } ) → ( 𝐴 ∈ Cℋ → ( 𝑥 ∈ ℋ → ( 𝐴 +ℋ 𝐵 ) = ( 𝐴 ∨ℋ 𝐵 ) ) ) ) |
8 |
7
|
adantl |
⊢ ( ( 𝑥 ≠ 0ℎ ∧ 𝐵 = ( span ‘ { 𝑥 } ) ) → ( 𝐴 ∈ Cℋ → ( 𝑥 ∈ ℋ → ( 𝐴 +ℋ 𝐵 ) = ( 𝐴 ∨ℋ 𝐵 ) ) ) ) |
9 |
8
|
com3l |
⊢ ( 𝐴 ∈ Cℋ → ( 𝑥 ∈ ℋ → ( ( 𝑥 ≠ 0ℎ ∧ 𝐵 = ( span ‘ { 𝑥 } ) ) → ( 𝐴 +ℋ 𝐵 ) = ( 𝐴 ∨ℋ 𝐵 ) ) ) ) |
10 |
9
|
rexlimdv |
⊢ ( 𝐴 ∈ Cℋ → ( ∃ 𝑥 ∈ ℋ ( 𝑥 ≠ 0ℎ ∧ 𝐵 = ( span ‘ { 𝑥 } ) ) → ( 𝐴 +ℋ 𝐵 ) = ( 𝐴 ∨ℋ 𝐵 ) ) ) |
11 |
1 10
|
syl5bi |
⊢ ( 𝐴 ∈ Cℋ → ( 𝐵 ∈ HAtoms → ( 𝐴 +ℋ 𝐵 ) = ( 𝐴 ∨ℋ 𝐵 ) ) ) |
12 |
11
|
imp |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ) → ( 𝐴 +ℋ 𝐵 ) = ( 𝐴 ∨ℋ 𝐵 ) ) |