lshpkr

Description: The kernel of functional G is the hyperplane defining it. (Contributed by NM, 17-Jul-2014)

	Ref	Expression
Hypotheses	lshpkr.v	$⊢ V = {Base}_{W}$
	lshpkr.a	$⊢ \underset{˙}{+} = +_{W}$
	lshpkr.n	$⊢ N = LSpan (W)$
	lshpkr.p	$⊢ \underset{˙}{\oplus} = LSSum (W)$
	lshpkr.h	$⊢ H = LSHyp (W)$
	lshpkr.w	$⊢ φ \to W \in LVec$
	lshpkr.u	$⊢ φ \to U \in H$
	lshpkr.z	$⊢ φ \to Z \in V$
	lshpkr.e	$⊢ φ \to U \underset{˙}{\oplus} N (\{Z\}) = V$
	lshpkr.d	$⊢ D = Scalar (W)$
	lshpkr.k	$⊢ K = {Base}_{D}$
	lshpkr.t	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	lshpkr.g	$⊢ G = (x \in V ⟼ (ι k \in K \| \exists y \in U x = y \underset{˙}{+} (k \underset{˙}{\cdot} Z)))$
	lshpkr.l	$⊢ L = LKer (W)$
Assertion	lshpkr	$⊢ φ \to L (G) = U$

Proof

Step	Hyp	Ref	Expression
1		lshpkr.v	$⊢ V = {Base}_{W}$
2		lshpkr.a	$⊢ \underset{˙}{+} = +_{W}$
3		lshpkr.n	$⊢ N = LSpan (W)$
4		lshpkr.p	$⊢ \underset{˙}{\oplus} = LSSum (W)$
5		lshpkr.h	$⊢ H = LSHyp (W)$
6		lshpkr.w	$⊢ φ \to W \in LVec$
7		lshpkr.u	$⊢ φ \to U \in H$
8		lshpkr.z	$⊢ φ \to Z \in V$
9		lshpkr.e	$⊢ φ \to U \underset{˙}{\oplus} N (\{Z\}) = V$
10		lshpkr.d	$⊢ D = Scalar (W)$
11		lshpkr.k	$⊢ K = {Base}_{D}$
12		lshpkr.t	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
13		lshpkr.g	$⊢ G = (x \in V ⟼ (ι k \in K \| \exists y \in U x = y \underset{˙}{+} (k \underset{˙}{\cdot} Z)))$
14		lshpkr.l	$⊢ L = LKer (W)$
15		eqid	$⊢ LFnl (W) = LFnl (W)$
16		lveclmod	$⊢ W \in LVec \to W \in LMod$
17	6 16	syl	$⊢ φ \to W \in LMod$
18	1 2 3 4 5 6 7 8 9 10 11 12 13 15	lshpkrcl	$⊢ φ \to G \in LFnl (W)$
19	1 15 14 17 18	lkrssv	$⊢ φ \to L (G) \subseteq V$
20	19	sseld	$⊢ φ \to (v \in L (G) \to v \in V)$
21		eqid	$⊢ LSubSp (W) = LSubSp (W)$
22	21 5 17 7	lshplss	$⊢ φ \to U \in LSubSp (W)$
23	1 21	lssel	$⊢ (U \in LSubSp (W) \land v \in U) \to v \in V$
24	22 23	sylan	$⊢ (φ \land v \in U) \to v \in V$
25	24	ex	$⊢ φ \to (v \in U \to v \in V)$
26		eqid	$⊢ 0_{D} = 0_{D}$
27	1 10 26 15 14	ellkr	$⊢ (W \in LVec \land G \in LFnl (W)) \to (v \in L (G) \leftrightarrow (v \in V \land G (v) = 0_{D}))$
28	6 18 27	syl2anc	$⊢ φ \to (v \in L (G) \leftrightarrow (v \in V \land G (v) = 0_{D}))$
29	28	baibd	$⊢ (φ \land v \in V) \to (v \in L (G) \leftrightarrow G (v) = 0_{D})$
30	6	adantr	$⊢ (φ \land v \in V) \to W \in LVec$
31	7	adantr	$⊢ (φ \land v \in V) \to U \in H$
32	8	adantr	$⊢ (φ \land v \in V) \to Z \in V$
33		simpr	$⊢ (φ \land v \in V) \to v \in V$
34	9	adantr	$⊢ (φ \land v \in V) \to U \underset{˙}{\oplus} N (\{Z\}) = V$
35	1 2 3 4 5 30 31 32 33 34 10 11 12 26 13	lshpkrlem1	$⊢ (φ \land v \in V) \to (v \in U \leftrightarrow G (v) = 0_{D})$
36	29 35	bitr4d	$⊢ (φ \land v \in V) \to (v \in L (G) \leftrightarrow v \in U)$
37	36	ex	$⊢ φ \to (v \in V \to (v \in L (G) \leftrightarrow v \in U))$
38	20 25 37	pm5.21ndd	$⊢ φ \to (v \in L (G) \leftrightarrow v \in U)$
39	38	eqrdv	$⊢ φ \to L (G) = U$

Metamath Proof Explorer

Theorem lshpkr

Proof