Step |
Hyp |
Ref |
Expression |
1 |
|
elin |
⊢ ( 𝐴 ∈ ( 𝐻 ∩ ( ⊥ ‘ 𝐻 ) ) ↔ ( 𝐴 ∈ 𝐻 ∧ 𝐴 ∈ ( ⊥ ‘ 𝐻 ) ) ) |
2 |
|
ocin |
⊢ ( 𝐻 ∈ Sℋ → ( 𝐻 ∩ ( ⊥ ‘ 𝐻 ) ) = 0ℋ ) |
3 |
2
|
eleq2d |
⊢ ( 𝐻 ∈ Sℋ → ( 𝐴 ∈ ( 𝐻 ∩ ( ⊥ ‘ 𝐻 ) ) ↔ 𝐴 ∈ 0ℋ ) ) |
4 |
3
|
biimpd |
⊢ ( 𝐻 ∈ Sℋ → ( 𝐴 ∈ ( 𝐻 ∩ ( ⊥ ‘ 𝐻 ) ) → 𝐴 ∈ 0ℋ ) ) |
5 |
1 4
|
syl5bir |
⊢ ( 𝐻 ∈ Sℋ → ( ( 𝐴 ∈ 𝐻 ∧ 𝐴 ∈ ( ⊥ ‘ 𝐻 ) ) → 𝐴 ∈ 0ℋ ) ) |
6 |
5
|
expcomd |
⊢ ( 𝐻 ∈ Sℋ → ( 𝐴 ∈ ( ⊥ ‘ 𝐻 ) → ( 𝐴 ∈ 𝐻 → 𝐴 ∈ 0ℋ ) ) ) |
7 |
6
|
imp |
⊢ ( ( 𝐻 ∈ Sℋ ∧ 𝐴 ∈ ( ⊥ ‘ 𝐻 ) ) → ( 𝐴 ∈ 𝐻 → 𝐴 ∈ 0ℋ ) ) |
8 |
|
elch0 |
⊢ ( 𝐴 ∈ 0ℋ ↔ 𝐴 = 0ℎ ) |
9 |
7 8
|
syl6ib |
⊢ ( ( 𝐻 ∈ Sℋ ∧ 𝐴 ∈ ( ⊥ ‘ 𝐻 ) ) → ( 𝐴 ∈ 𝐻 → 𝐴 = 0ℎ ) ) |
10 |
9
|
necon3ad |
⊢ ( ( 𝐻 ∈ Sℋ ∧ 𝐴 ∈ ( ⊥ ‘ 𝐻 ) ) → ( 𝐴 ≠ 0ℎ → ¬ 𝐴 ∈ 𝐻 ) ) |
11 |
10
|
3impia |
⊢ ( ( 𝐻 ∈ Sℋ ∧ 𝐴 ∈ ( ⊥ ‘ 𝐻 ) ∧ 𝐴 ≠ 0ℎ ) → ¬ 𝐴 ∈ 𝐻 ) |