chjatom

Description: The join of a closed subspace and an atom equals their subspace sum. Special case of remark in Kalmbach p. 65, stating that if A or B is finite-dimensional, then this equality holds. (Contributed by NM, 4-Jun-2004) (New usage is discouraged.)

		Ref	Expression
	Assertion	chjatom	$⊢ (A \in C_{ℋ} \land B \in HAtoms) \to A +_{ℋ} B = A \lor_{ℋ} B$

Proof

Step	Hyp	Ref	Expression
1		atom1d	$⊢ B \in HAtoms \leftrightarrow \exists x \in ℋ (x \neq 0_{ℎ} \land B = span (\{x\}))$
2		spansnj	$⊢ (A \in C_{ℋ} \land x \in ℋ) \to A +_{ℋ} span (\{x\}) = A \lor_{ℋ} span (\{x\})$
3		oveq2	$⊢ B = span (\{x\}) \to A +_{ℋ} B = A +_{ℋ} span (\{x\})$
4		oveq2	$⊢ B = span (\{x\}) \to A \lor_{ℋ} B = A \lor_{ℋ} span (\{x\})$
5	3 4	eqeq12d	$⊢ B = span (\{x\}) \to (A +_{ℋ} B = A \lor_{ℋ} B \leftrightarrow A +_{ℋ} span (\{x\}) = A \lor_{ℋ} span (\{x\}))$
6	2 5	imbitrrid	$⊢ B = span (\{x\}) \to ((A \in C_{ℋ} \land x \in ℋ) \to A +_{ℋ} B = A \lor_{ℋ} B)$
7	6	expd	$⊢ B = span (\{x\}) \to (A \in C_{ℋ} \to (x \in ℋ \to A +_{ℋ} B = A \lor_{ℋ} B))$
8	7	adantl	$⊢ (x \neq 0_{ℎ} \land B = span (\{x\})) \to (A \in C_{ℋ} \to (x \in ℋ \to A +_{ℋ} B = A \lor_{ℋ} B))$
9	8	com3l	$⊢ A \in C_{ℋ} \to (x \in ℋ \to ((x \neq 0_{ℎ} \land B = span (\{x\})) \to A +_{ℋ} B = A \lor_{ℋ} B))$
10	9	rexlimdv	$⊢ A \in C_{ℋ} \to (\exists x \in ℋ (x \neq 0_{ℎ} \land B = span (\{x\})) \to A +_{ℋ} B = A \lor_{ℋ} B)$
11	1 10	biimtrid	$⊢ A \in C_{ℋ} \to (B \in HAtoms \to A +_{ℋ} B = A \lor_{ℋ} B)$
12	11	imp	$⊢ (A \in C_{ℋ} \land B \in HAtoms) \to A +_{ℋ} B = A \lor_{ℋ} B$

Metamath Proof Explorer

Theorem chjatom

Proof