This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → ( ⊥ ‘ ( ⊥ ‘ { 𝐴 } ) ) ∈ HAtoms )

Proof

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