dochnel2

Description: A nonzero member of a subspace doesn't belong to the orthocomplement of the subspace. (Contributed by NM, 28-Feb-2015)

Step	Hyp	Ref	Expression
1		dochnoncon.h	$⊢ H = LHyp (K)$
2		dochnoncon.u	$⊢ U = DVecH (K) (W)$
3		dochnoncon.s	$⊢ S = LSubSp (U)$
4		dochnoncon.z	$⊢ \underset{˙}{0} = 0_{U}$
5		dochnoncon.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
6		dochnel2.k	$⊢ φ \to (K \in HL \land W \in H)$
7		dochnel2.t	$⊢ φ \to T \in S$
8		dochnel2.x	$⊢ φ \to X \in (T ∖ \{\underset{˙}{0}\})$
9	8	eldifbd	$⊢ φ \to \neg X \in \{\underset{˙}{0}\}$
10	8	eldifad	$⊢ φ \to X \in T$
11		elin	$⊢ X \in (T \cap \underset{˙}{⊥} (T)) \leftrightarrow (X \in T \land X \in \underset{˙}{⊥} (T))$
12	1 2 3 4 5	dochnoncon	$⊢ ((K \in HL \land W \in H) \land T \in S) \to T \cap \underset{˙}{⊥} (T) = \{\underset{˙}{0}\}$
13	6 7 12	syl2anc	$⊢ φ \to T \cap \underset{˙}{⊥} (T) = \{\underset{˙}{0}\}$
14	13	eleq2d	$⊢ φ \to (X \in (T \cap \underset{˙}{⊥} (T)) \leftrightarrow X \in \{\underset{˙}{0}\})$
15	11 14	bitr3id	$⊢ φ \to ((X \in T \land X \in \underset{˙}{⊥} (T)) \leftrightarrow X \in \{\underset{˙}{0}\})$
16	15	biimpd	$⊢ φ \to ((X \in T \land X \in \underset{˙}{⊥} (T)) \to X \in \{\underset{˙}{0}\})$
17	10 16	mpand	$⊢ φ \to (X \in \underset{˙}{⊥} (T) \to X \in \{\underset{˙}{0}\})$
18	9 17	mtod	$⊢ φ \to \neg X \in \underset{˙}{⊥} (T)$

Metamath Proof Explorer