Metamath Proof Explorer

Theorem ocnel

Description: A nonzero vector in the complement of a subspace does not belong to the subspace. (Contributed by NM, 10-Apr-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	ocnel	$⊢ (H \in S_{ℋ} \land A \in ⊥ (H) \land A \neq 0_{ℎ}) \to \neg A \in H$

Proof

Step	Hyp	Ref	Expression
1		elin	$⊢ A \in (H \cap ⊥ (H)) \leftrightarrow (A \in H \land A \in ⊥ (H))$
2		ocin	$⊢ H \in S_{ℋ} \to H \cap ⊥ (H) = 0_{ℋ}$
3	2	eleq2d	$⊢ H \in S_{ℋ} \to (A \in (H \cap ⊥ (H)) \leftrightarrow A \in 0_{ℋ})$
4	3	biimpd	$⊢ H \in S_{ℋ} \to (A \in (H \cap ⊥ (H)) \to A \in 0_{ℋ})$
5	1 4	biimtrrid	$⊢ H \in S_{ℋ} \to ((A \in H \land A \in ⊥ (H)) \to A \in 0_{ℋ})$
6	5	expcomd	$⊢ H \in S_{ℋ} \to (A \in ⊥ (H) \to (A \in H \to A \in 0_{ℋ}))$
7	6	imp	$⊢ (H \in S_{ℋ} \land A \in ⊥ (H)) \to (A \in H \to A \in 0_{ℋ})$
8		elch0	$⊢ A \in 0_{ℋ} \leftrightarrow A = 0_{ℎ}$
9	7 8	imbitrdi	$⊢ (H \in S_{ℋ} \land A \in ⊥ (H)) \to (A \in H \to A = 0_{ℎ})$
10	9	necon3ad	$⊢ (H \in S_{ℋ} \land A \in ⊥ (H)) \to (A \neq 0_{ℎ} \to \neg A \in H)$
11	10	3impia	$⊢ (H \in S_{ℋ} \land A \in ⊥ (H) \land A \neq 0_{ℎ}) \to \neg A \in H$