dochsnkr2

Description: Kernel of the explicit functional G determined by a nonzero vector X . Compare the more general lshpkr . (Contributed by NM, 27-Oct-2014)

	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	dochsnkr2	$⊢ φ \to L (G) = \underset{˙}{⊥} (\{X\})$

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		eqid	$⊢ LSpan (U) = LSpan (U)$
15		eqid	$⊢ LSSum (U) = LSSum (U)$
16		eqid	$⊢ LSHyp (U) = LSHyp (U)$
17	1 3 12	dvhlvec	$⊢ φ \to U \in LVec$
18	1 2 3 4 5 16 12 13	dochsnshp	$⊢ φ \to \underset{˙}{⊥} (\{X\}) \in LSHyp (U)$
19	13	eldifad	$⊢ φ \to X \in V$
20	1 2 3 4 5 14 15 12 13	dochexmidat	$⊢ φ \to \underset{˙}{⊥} (\{X\}) LSSum (U) LSpan (U) (\{X\}) = V$
21	4 6 14 15 16 17 18 19 20 9 10 7 11 8	lshpkr	$⊢ φ \to L (G) = \underset{˙}{⊥} (\{X\})$

Metamath Proof Explorer

Theorem dochsnkr2

Proof