dochsnkr2cl

Description: The X determining functional G belongs to the atom formed by the orthocomplement of the kernel. (Contributed by NM, 4-Jan-2015)

	Ref	Expression
Hypotheses	dochsnkr2.h	$⊢ H = LHyp (K)$
	dochsnkr2.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
	dochsnkr2.u	$⊢ U = DVecH (K) (W)$
	dochsnkr2.v	$⊢ V = {Base}_{U}$
	dochsnkr2.z	$⊢ \underset{˙}{0} = 0_{U}$
	dochsnkr2.a	$⊢ \underset{˙}{+} = +_{U}$
	dochsnkr2.t	$⊢ \underset{˙}{\cdot} = \cdot_{U}$
	dochsnkr2.l	$⊢ L = LKer (U)$
	dochsnkr2.d	$⊢ D = Scalar (U)$
	dochsnkr2.r	$⊢ R = {Base}_{D}$
	dochsnkr2.g	$⊢ G = (v \in V ⟼ (ι k \in R \| \exists w \in \underset{˙}{⊥} (\{X\}) v = w \underset{˙}{+} (k \underset{˙}{\cdot} X)))$
	dochsnkr2.k	$⊢ φ \to (K \in HL \land W \in H)$
	dochsnkr2.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
Assertion	dochsnkr2cl	$⊢ φ \to X \in (\underset{˙}{⊥} (L (G)) ∖ \{\underset{˙}{0}\})$

Proof

Step	Hyp	Ref	Expression
1		dochsnkr2.h	$⊢ H = LHyp (K)$
2		dochsnkr2.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
3		dochsnkr2.u	$⊢ U = DVecH (K) (W)$
4		dochsnkr2.v	$⊢ V = {Base}_{U}$
5		dochsnkr2.z	$⊢ \underset{˙}{0} = 0_{U}$
6		dochsnkr2.a	$⊢ \underset{˙}{+} = +_{U}$
7		dochsnkr2.t	$⊢ \underset{˙}{\cdot} = \cdot_{U}$
8		dochsnkr2.l	$⊢ L = LKer (U)$
9		dochsnkr2.d	$⊢ D = Scalar (U)$
10		dochsnkr2.r	$⊢ R = {Base}_{D}$
11		dochsnkr2.g	$⊢ G = (v \in V ⟼ (ι k \in R \| \exists w \in \underset{˙}{⊥} (\{X\}) v = w \underset{˙}{+} (k \underset{˙}{\cdot} X)))$
12		dochsnkr2.k	$⊢ φ \to (K \in HL \land W \in H)$
13		dochsnkr2.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
14	1 3 12	dvhlmod	$⊢ φ \to U \in LMod$
15	13	eldifad	$⊢ φ \to X \in V$
16		eqid	$⊢ LSpan (U) = LSpan (U)$
17	4 16	lspsnid	$⊢ (U \in LMod \land X \in V) \to X \in LSpan (U) (\{X\})$
18	14 15 17	syl2anc	$⊢ φ \to X \in LSpan (U) (\{X\})$
19	1 2 3 4 5 6 7 8 9 10 11 12 13	dochsnkr2	$⊢ φ \to L (G) = \underset{˙}{⊥} (\{X\})$
20	15	snssd	$⊢ φ \to \{X\} \subseteq V$
21	1 3 2 4 16 12 20	dochocsp	$⊢ φ \to \underset{˙}{⊥} (LSpan (U) (\{X\})) = \underset{˙}{⊥} (\{X\})$
22	19 21	eqtr4d	$⊢ φ \to L (G) = \underset{˙}{⊥} (LSpan (U) (\{X\}))$
23	22	fveq2d	$⊢ φ \to \underset{˙}{⊥} (L (G)) = \underset{˙}{⊥} (\underset{˙}{⊥} (LSpan (U) (\{X\})))$
24		eqid	$⊢ DIsoH (K) (W) = DIsoH (K) (W)$
25	1 3 4 16 24	dihlsprn	$⊢ ((K \in HL \land W \in H) \land X \in V) \to LSpan (U) (\{X\}) \in ran DIsoH (K) (W)$
26	12 15 25	syl2anc	$⊢ φ \to LSpan (U) (\{X\}) \in ran DIsoH (K) (W)$
27	1 24 2	dochoc	$⊢ ((K \in HL \land W \in H) \land LSpan (U) (\{X\}) \in ran DIsoH (K) (W)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (LSpan (U) (\{X\}))) = LSpan (U) (\{X\})$
28	12 26 27	syl2anc	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (LSpan (U) (\{X\}))) = LSpan (U) (\{X\})$
29	23 28	eqtr2d	$⊢ φ \to LSpan (U) (\{X\}) = \underset{˙}{⊥} (L (G))$
30	18 29	eleqtrd	$⊢ φ \to X \in \underset{˙}{⊥} (L (G))$
31		eldifsni	$⊢ X \in (V ∖ \{\underset{˙}{0}\}) \to X \neq \underset{˙}{0}$
32	13 31	syl	$⊢ φ \to X \neq \underset{˙}{0}$
33		eldifsn	$⊢ X \in (\underset{˙}{⊥} (L (G)) ∖ \{\underset{˙}{0}\}) \leftrightarrow (X \in \underset{˙}{⊥} (L (G)) \land X \neq \underset{˙}{0})$
34	30 32 33	sylanbrc	$⊢ φ \to X \in (\underset{˙}{⊥} (L (G)) ∖ \{\underset{˙}{0}\})$

Metamath Proof Explorer

Theorem dochsnkr2cl

Proof