Metamath Proof Explorer

Theorem h1da

Description: A 1-dimensional subspace is an atom. (Contributed by NM, 22-Jul-2001) (New usage is discouraged.)

Ref Expression
Assertion h1da ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → ⊥ ⁡ ⊥ ⁡ A ∈ HAtoms

Proof

Step Hyp Ref Expression
1 snssi ⊢ A ∈ ℋ → A ⊆ ℋ
2 occl ⊢ A ⊆ ℋ → ⊥ ⁡ A ∈ C ℋ
3 choccl ⊢ ⊥ ⁡ A ∈ C ℋ → ⊥ ⁡ ⊥ ⁡ A ∈ C ℋ
4 1 2 3 3syl ⊢ A ∈ ℋ → ⊥ ⁡ ⊥ ⁡ A ∈ C ℋ
5 4 adantr ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → ⊥ ⁡ ⊥ ⁡ A ∈ C ℋ
6 h1dn0 ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → ⊥ ⁡ ⊥ ⁡ A ≠ 0 ℋ
7 h1datom ⊢ x ∈ C ℋ ∧ A ∈ ℋ → x ⊆ ⊥ ⁡ ⊥ ⁡ A → x = ⊥ ⁡ ⊥ ⁡ A ∨ x = 0 ℋ
8 7 expcom ⊢ A ∈ ℋ → x ∈ C ℋ → x ⊆ ⊥ ⁡ ⊥ ⁡ A → x = ⊥ ⁡ ⊥ ⁡ A ∨ x = 0 ℋ
9 8 ralrimiv ⊢ A ∈ ℋ → ∀ x ∈ C ℋ x ⊆ ⊥ ⁡ ⊥ ⁡ A → x = ⊥ ⁡ ⊥ ⁡ A ∨ x = 0 ℋ
10 9 adantr ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → ∀ x ∈ C ℋ x ⊆ ⊥ ⁡ ⊥ ⁡ A → x = ⊥ ⁡ ⊥ ⁡ A ∨ x = 0 ℋ
11 6 10 jca ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → ⊥ ⁡ ⊥ ⁡ A ≠ 0 ℋ ∧ ∀ x ∈ C ℋ x ⊆ ⊥ ⁡ ⊥ ⁡ A → x = ⊥ ⁡ ⊥ ⁡ A ∨ x = 0 ℋ
12 elat2 ⊢ ⊥ ⁡ ⊥ ⁡ A ∈ HAtoms ↔ ⊥ ⁡ ⊥ ⁡ A ∈ C ℋ ∧ ⊥ ⁡ ⊥ ⁡ A ≠ 0 ℋ ∧ ∀ x ∈ C ℋ x ⊆ ⊥ ⁡ ⊥ ⁡ A → x = ⊥ ⁡ ⊥ ⁡ A ∨ x = 0 ℋ
13 5 11 12 sylanbrc ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → ⊥ ⁡ ⊥ ⁡ A ∈ HAtoms