h1da

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

		Ref	Expression
	Assertion	h1da	$⊢ (A \in ℋ \land A \neq 0_{ℎ}) \to ⊥ (⊥ (\{A\})) \in HAtoms$

Step	Hyp	Ref	Expression
1		snssi	$⊢ A \in ℋ \to \{A\} \subseteq ℋ$
2		occl	$⊢ \{A\} \subseteq ℋ \to ⊥ (\{A\}) \in C_{ℋ}$
3		choccl	$⊢ ⊥ (\{A\}) \in C_{ℋ} \to ⊥ (⊥ (\{A\})) \in C_{ℋ}$
4	1 2 3	3syl	$⊢ A \in ℋ \to ⊥ (⊥ (\{A\})) \in C_{ℋ}$
5	4	adantr	$⊢ (A \in ℋ \land A \neq 0_{ℎ}) \to ⊥ (⊥ (\{A\})) \in C_{ℋ}$
6		h1dn0	$⊢ (A \in ℋ \land A \neq 0_{ℎ}) \to ⊥ (⊥ (\{A\})) \neq 0_{ℋ}$
7		h1datom	$⊢ (x \in C_{ℋ} \land A \in ℋ) \to (x \subseteq ⊥ (⊥ (\{A\})) \to (x = ⊥ (⊥ (\{A\})) \lor x = 0_{ℋ}))$
8	7	expcom	$⊢ A \in ℋ \to (x \in C_{ℋ} \to (x \subseteq ⊥ (⊥ (\{A\})) \to (x = ⊥ (⊥ (\{A\})) \lor x = 0_{ℋ})))$
9	8	ralrimiv	$⊢ A \in ℋ \to \forall x \in C_{ℋ} (x \subseteq ⊥ (⊥ (\{A\})) \to (x = ⊥ (⊥ (\{A\})) \lor x = 0_{ℋ}))$
10	9	adantr	$⊢ (A \in ℋ \land A \neq 0_{ℎ}) \to \forall x \in C_{ℋ} (x \subseteq ⊥ (⊥ (\{A\})) \to (x = ⊥ (⊥ (\{A\})) \lor x = 0_{ℋ}))$
11	6 10	jca	$⊢ (A \in ℋ \land A \neq 0_{ℎ}) \to (⊥ (⊥ (\{A\})) \neq 0_{ℋ} \land \forall x \in C_{ℋ} (x \subseteq ⊥ (⊥ (\{A\})) \to (x = ⊥ (⊥ (\{A\})) \lor x = 0_{ℋ})))$
12		elat2	$⊢ ⊥ (⊥ (\{A\})) \in HAtoms \leftrightarrow (⊥ (⊥ (\{A\})) \in C_{ℋ} \land (⊥ (⊥ (\{A\})) \neq 0_{ℋ} \land \forall x \in C_{ℋ} (x \subseteq ⊥ (⊥ (\{A\})) \to (x = ⊥ (⊥ (\{A\})) \lor x = 0_{ℋ}))))$
13	5 11 12	sylanbrc	$⊢ (A \in ℋ \land A \neq 0_{ℎ}) \to ⊥ (⊥ (\{A\})) \in HAtoms$

Metamath Proof Explorer