dochkrsat

Description: The orthocomplement of a kernel is an atom iff it is nonzero. (Contributed by NM, 1-Nov-2014)

	Ref	Expression
Hypotheses	dochkrsat.h	$⊢ H = LHyp (K)$
	dochkrsat.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
	dochkrsat.u	$⊢ U = DVecH (K) (W)$
	dochkrsat.a	$⊢ A = LSAtoms (U)$
	dochkrsat.f	$⊢ F = LFnl (U)$
	dochkrsat.l	$⊢ L = LKer (U)$
	dochkrsat.z	$⊢ \underset{˙}{0} = 0_{U}$
	dochkrsat.k	$⊢ φ \to (K \in HL \land W \in H)$
	dochkrsat.g	$⊢ φ \to G \in F$
Assertion	dochkrsat	$⊢ φ \to (\underset{˙}{⊥} (L (G)) \neq \{\underset{˙}{0}\} \leftrightarrow \underset{˙}{⊥} (L (G)) \in A)$

Step	Hyp	Ref	Expression
1		dochkrsat.h	$⊢ H = LHyp (K)$
2		dochkrsat.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
3		dochkrsat.u	$⊢ U = DVecH (K) (W)$
4		dochkrsat.a	$⊢ A = LSAtoms (U)$
5		dochkrsat.f	$⊢ F = LFnl (U)$
6		dochkrsat.l	$⊢ L = LKer (U)$
7		dochkrsat.z	$⊢ \underset{˙}{0} = 0_{U}$
8		dochkrsat.k	$⊢ φ \to (K \in HL \land W \in H)$
9		dochkrsat.g	$⊢ φ \to G \in F$
10		eqid	$⊢ {Base}_{U} = {Base}_{U}$
11		eqid	$⊢ LSHyp (U) = LSHyp (U)$
12	1 2 3 10 11 5 6 8 9	dochkrshp	$⊢ φ \to (\underset{˙}{⊥} (\underset{˙}{⊥} (L (G))) \neq {Base}_{U} \leftrightarrow \underset{˙}{⊥} (\underset{˙}{⊥} (L (G))) \in LSHyp (U))$
13	1 3 8	dvhlmod	$⊢ φ \to U \in LMod$
14	10 5 6 13 9	lkrssv	$⊢ φ \to L (G) \subseteq {Base}_{U}$
15	1 2 3 10 7 8 14	dochn0nv	$⊢ φ \to (\underset{˙}{⊥} (L (G)) \neq \{\underset{˙}{0}\} \leftrightarrow \underset{˙}{⊥} (\underset{˙}{⊥} (L (G))) \neq {Base}_{U})$
16		eqid	$⊢ LSubSp (U) = LSubSp (U)$
17	1 3 10 16 2	dochlss	$⊢ ((K \in HL \land W \in H) \land L (G) \subseteq {Base}_{U}) \to \underset{˙}{⊥} (L (G)) \in LSubSp (U)$
18	8 14 17	syl2anc	$⊢ φ \to \underset{˙}{⊥} (L (G)) \in LSubSp (U)$
19	1 2 3 16 4 11 8 18	dochsatshpb	$⊢ φ \to (\underset{˙}{⊥} (L (G)) \in A \leftrightarrow \underset{˙}{⊥} (\underset{˙}{⊥} (L (G))) \in LSHyp (U))$
20	12 15 19	3bitr4d	$⊢ φ \to (\underset{˙}{⊥} (L (G)) \neq \{\underset{˙}{0}\} \leftrightarrow \underset{˙}{⊥} (L (G)) \in A)$

Metamath Proof Explorer