lshpkrcl

Description: The set G defined by hyperplane U is a linear functional. (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.f	$⊢ F = LFnl (W)$
Assertion	lshpkrcl	$⊢ φ \to G \in F$

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.f	$⊢ F = LFnl (W)$
15	6	adantr	$⊢ (φ \land a \in V) \to W \in LVec$
16	7	adantr	$⊢ (φ \land a \in V) \to U \in H$
17	8	adantr	$⊢ (φ \land a \in V) \to Z \in V$
18		simpr	$⊢ (φ \land a \in V) \to a \in V$
19	9	adantr	$⊢ (φ \land a \in V) \to U \underset{˙}{\oplus} N (\{Z\}) = V$
20	1 2 3 4 5 15 16 17 18 19 10 11 12	lshpsmreu	$⊢ (φ \land a \in V) \to \exists! k \in K \exists y \in U a = y \underset{˙}{+} (k \underset{˙}{\cdot} Z)$
21		riotacl	$⊢ \exists! k \in K \exists y \in U a = y \underset{˙}{+} (k \underset{˙}{\cdot} Z) \to (ι k \in K \| \exists y \in U a = y \underset{˙}{+} (k \underset{˙}{\cdot} Z)) \in K$
22	20 21	syl	$⊢ (φ \land a \in V) \to (ι k \in K \| \exists y \in U a = y \underset{˙}{+} (k \underset{˙}{\cdot} Z)) \in K$
23		eqeq1	$⊢ x = a \to (x = y \underset{˙}{+} (k \underset{˙}{\cdot} Z) \leftrightarrow a = y \underset{˙}{+} (k \underset{˙}{\cdot} Z))$
24	23	rexbidv	$⊢ x = a \to (\exists y \in U x = y \underset{˙}{+} (k \underset{˙}{\cdot} Z) \leftrightarrow \exists y \in U a = y \underset{˙}{+} (k \underset{˙}{\cdot} Z))$
25	24	riotabidv	$⊢ x = a \to (ι k \in K \| \exists y \in U x = y \underset{˙}{+} (k \underset{˙}{\cdot} Z)) = (ι k \in K \| \exists y \in U a = y \underset{˙}{+} (k \underset{˙}{\cdot} Z))$
26	25	cbvmptv	$⊢ (x \in V ⟼ (ι k \in K \| \exists y \in U x = y \underset{˙}{+} (k \underset{˙}{\cdot} Z))) = (a \in V ⟼ (ι k \in K \| \exists y \in U a = y \underset{˙}{+} (k \underset{˙}{\cdot} Z)))$
27	13 26	eqtri	$⊢ G = (a \in V ⟼ (ι k \in K \| \exists y \in U a = y \underset{˙}{+} (k \underset{˙}{\cdot} Z)))$
28	22 27	fmptd	$⊢ φ \to G : V ⟶ K$
29		eqid	$⊢ 0_{D} = 0_{D}$
30	1 2 3 4 5 6 7 8 8 9 10 11 12 29 13	lshpkrlem6	$⊢ (φ \land (l \in K \land u \in V \land v \in V)) \to G ((l \underset{˙}{\cdot} u) \underset{˙}{+} v) = (l \cdot_{D} G (u)) +_{D} G (v)$
31	30	ralrimivvva	$⊢ φ \to \forall l \in K \forall u \in V \forall v \in V G ((l \underset{˙}{\cdot} u) \underset{˙}{+} v) = (l \cdot_{D} G (u)) +_{D} G (v)$
32		eqid	$⊢ +_{D} = +_{D}$
33		eqid	$⊢ \cdot_{D} = \cdot_{D}$
34	1 2 10 12 11 32 33 14	islfl	$⊢ W \in LVec \to (G \in F \leftrightarrow (G : V ⟶ K \land \forall l \in K \forall u \in V \forall v \in V G ((l \underset{˙}{\cdot} u) \underset{˙}{+} v) = (l \cdot_{D} G (u)) +_{D} G (v)))$
35	6 34	syl	$⊢ φ \to (G \in F \leftrightarrow (G : V ⟶ K \land \forall l \in K \forall u \in V \forall v \in V G ((l \underset{˙}{\cdot} u) \underset{˙}{+} v) = (l \cdot_{D} G (u)) +_{D} G (v)))$
36	28 31 35	mpbir2and	$⊢ φ \to G \in F$

Metamath Proof Explorer

Theorem lshpkrcl

Proof