lfl1dim

Description: Equivalent expressions for a 1-dim subspace (ray) of functionals. (Contributed by NM, 24-Oct-2014)

	Ref	Expression
Hypotheses	lfl1dim.v	$⊢ V = {Base}_{W}$
	lfl1dim.d	$⊢ D = Scalar (W)$
	lfl1dim.f	$⊢ F = LFnl (W)$
	lfl1dim.l	$⊢ L = LKer (W)$
	lfl1dim.k	$⊢ K = {Base}_{D}$
	lfl1dim.t	$⊢ \underset{˙}{\cdot} = \cdot_{D}$
	lfl1dim.w	$⊢ φ \to W \in LVec$
	lfl1dim.g	$⊢ φ \to G \in F$
Assertion	lfl1dim	$⊢ φ \to \{g \in F \| L (G) \subseteq L (g)\} = \{g \| \exists k \in K g = G {\underset{˙}{\cdot}}_{f} (V \times \{k\})\}$

Proof

Step	Hyp	Ref	Expression
1		lfl1dim.v	$⊢ V = {Base}_{W}$
2		lfl1dim.d	$⊢ D = Scalar (W)$
3		lfl1dim.f	$⊢ F = LFnl (W)$
4		lfl1dim.l	$⊢ L = LKer (W)$
5		lfl1dim.k	$⊢ K = {Base}_{D}$
6		lfl1dim.t	$⊢ \underset{˙}{\cdot} = \cdot_{D}$
7		lfl1dim.w	$⊢ φ \to W \in LVec$
8		lfl1dim.g	$⊢ φ \to G \in F$
9		df-rab	$⊢ \{g \in F \| L (G) \subseteq L (g)\} = \{g \| (g \in F \land L (G) \subseteq L (g))\}$
10		lveclmod	$⊢ W \in LVec \to W \in LMod$
11	7 10	syl	$⊢ φ \to W \in LMod$
12		eqid	$⊢ 0_{D} = 0_{D}$
13	2 5 12	lmod0cl	$⊢ W \in LMod \to 0_{D} \in K$
14	11 13	syl	$⊢ φ \to 0_{D} \in K$
15	14	ad2antrr	$⊢ ((φ \land g \in F) \land g = V \times \{0_{D}\}) \to 0_{D} \in K$
16		simpr	$⊢ ((φ \land g \in F) \land g = V \times \{0_{D}\}) \to g = V \times \{0_{D}\}$
17	11	ad2antrr	$⊢ ((φ \land g \in F) \land g = V \times \{0_{D}\}) \to W \in LMod$
18	8	ad2antrr	$⊢ ((φ \land g \in F) \land g = V \times \{0_{D}\}) \to G \in F$
19	1 2 3 5 6 12 17 18	lfl0sc	$⊢ ((φ \land g \in F) \land g = V \times \{0_{D}\}) \to G {\underset{˙}{\cdot}}_{f} (V \times \{0_{D}\}) = V \times \{0_{D}\}$
20	16 19	eqtr4d	$⊢ ((φ \land g \in F) \land g = V \times \{0_{D}\}) \to g = G {\underset{˙}{\cdot}}_{f} (V \times \{0_{D}\})$
21		sneq	$⊢ k = 0_{D} \to \{k\} = \{0_{D}\}$
22	21	xpeq2d	$⊢ k = 0_{D} \to V \times \{k\} = V \times \{0_{D}\}$
23	22	oveq2d	$⊢ k = 0_{D} \to G {\underset{˙}{\cdot}}_{f} (V \times \{k\}) = G {\underset{˙}{\cdot}}_{f} (V \times \{0_{D}\})$
24	23	rspceeqv	$⊢ (0_{D} \in K \land g = G {\underset{˙}{\cdot}}_{f} (V \times \{0_{D}\})) \to \exists k \in K g = G {\underset{˙}{\cdot}}_{f} (V \times \{k\})$
25	15 20 24	syl2anc	$⊢ ((φ \land g \in F) \land g = V \times \{0_{D}\}) \to \exists k \in K g = G {\underset{˙}{\cdot}}_{f} (V \times \{k\})$
26	25	a1d	$⊢ ((φ \land g \in F) \land g = V \times \{0_{D}\}) \to (L (G) \subseteq L (g) \to \exists k \in K g = G {\underset{˙}{\cdot}}_{f} (V \times \{k\}))$
27	14	ad3antrrr	$⊢ (((φ \land g \in F) \land G = V \times \{0_{D}\}) \land L (G) \subseteq L (g)) \to 0_{D} \in K$
28	11	ad3antrrr	$⊢ (((φ \land g \in F) \land G = V \times \{0_{D}\}) \land L (G) \subseteq L (g)) \to W \in LMod$
29		simpllr	$⊢ (((φ \land g \in F) \land G = V \times \{0_{D}\}) \land L (G) \subseteq L (g)) \to g \in F$
30	1 3 4 28 29	lkrssv	$⊢ (((φ \land g \in F) \land G = V \times \{0_{D}\}) \land L (G) \subseteq L (g)) \to L (g) \subseteq V$
31	11	adantr	$⊢ (φ \land g \in F) \to W \in LMod$
32	8	adantr	$⊢ (φ \land g \in F) \to G \in F$
33	2 12 1 3 4	lkr0f	$⊢ (W \in LMod \land G \in F) \to (L (G) = V \leftrightarrow G = V \times \{0_{D}\})$
34	31 32 33	syl2anc	$⊢ (φ \land g \in F) \to (L (G) = V \leftrightarrow G = V \times \{0_{D}\})$
35	34	biimpar	$⊢ ((φ \land g \in F) \land G = V \times \{0_{D}\}) \to L (G) = V$
36	35	sseq1d	$⊢ ((φ \land g \in F) \land G = V \times \{0_{D}\}) \to (L (G) \subseteq L (g) \leftrightarrow V \subseteq L (g))$
37	36	biimpa	$⊢ (((φ \land g \in F) \land G = V \times \{0_{D}\}) \land L (G) \subseteq L (g)) \to V \subseteq L (g)$
38	30 37	eqssd	$⊢ (((φ \land g \in F) \land G = V \times \{0_{D}\}) \land L (G) \subseteq L (g)) \to L (g) = V$
39	2 12 1 3 4	lkr0f	$⊢ (W \in LMod \land g \in F) \to (L (g) = V \leftrightarrow g = V \times \{0_{D}\})$
40	28 29 39	syl2anc	$⊢ (((φ \land g \in F) \land G = V \times \{0_{D}\}) \land L (G) \subseteq L (g)) \to (L (g) = V \leftrightarrow g = V \times \{0_{D}\})$
41	38 40	mpbid	$⊢ (((φ \land g \in F) \land G = V \times \{0_{D}\}) \land L (G) \subseteq L (g)) \to g = V \times \{0_{D}\}$
42	8	ad3antrrr	$⊢ (((φ \land g \in F) \land G = V \times \{0_{D}\}) \land L (G) \subseteq L (g)) \to G \in F$
43	1 2 3 5 6 12 28 42	lfl0sc	$⊢ (((φ \land g \in F) \land G = V \times \{0_{D}\}) \land L (G) \subseteq L (g)) \to G {\underset{˙}{\cdot}}_{f} (V \times \{0_{D}\}) = V \times \{0_{D}\}$
44	41 43	eqtr4d	$⊢ (((φ \land g \in F) \land G = V \times \{0_{D}\}) \land L (G) \subseteq L (g)) \to g = G {\underset{˙}{\cdot}}_{f} (V \times \{0_{D}\})$
45	27 44 24	syl2anc	$⊢ (((φ \land g \in F) \land G = V \times \{0_{D}\}) \land L (G) \subseteq L (g)) \to \exists k \in K g = G {\underset{˙}{\cdot}}_{f} (V \times \{k\})$
46	45	ex	$⊢ ((φ \land g \in F) \land G = V \times \{0_{D}\}) \to (L (G) \subseteq L (g) \to \exists k \in K g = G {\underset{˙}{\cdot}}_{f} (V \times \{k\}))$
47		eqid	$⊢ LSHyp (W) = LSHyp (W)$
48	7	ad2antrr	$⊢ ((φ \land g \in F) \land (g \neq V \times \{0_{D}\} \land G \neq V \times \{0_{D}\})) \to W \in LVec$
49	8	ad2antrr	$⊢ ((φ \land g \in F) \land (g \neq V \times \{0_{D}\} \land G \neq V \times \{0_{D}\})) \to G \in F$
50		simprr	$⊢ ((φ \land g \in F) \land (g \neq V \times \{0_{D}\} \land G \neq V \times \{0_{D}\})) \to G \neq V \times \{0_{D}\}$
51	1 2 12 47 3 4	lkrshp	$⊢ (W \in LVec \land G \in F \land G \neq V \times \{0_{D}\}) \to L (G) \in LSHyp (W)$
52	48 49 50 51	syl3anc	$⊢ ((φ \land g \in F) \land (g \neq V \times \{0_{D}\} \land G \neq V \times \{0_{D}\})) \to L (G) \in LSHyp (W)$
53		simplr	$⊢ ((φ \land g \in F) \land (g \neq V \times \{0_{D}\} \land G \neq V \times \{0_{D}\})) \to g \in F$
54		simprl	$⊢ ((φ \land g \in F) \land (g \neq V \times \{0_{D}\} \land G \neq V \times \{0_{D}\})) \to g \neq V \times \{0_{D}\}$
55	1 2 12 47 3 4	lkrshp	$⊢ (W \in LVec \land g \in F \land g \neq V \times \{0_{D}\}) \to L (g) \in LSHyp (W)$
56	48 53 54 55	syl3anc	$⊢ ((φ \land g \in F) \land (g \neq V \times \{0_{D}\} \land G \neq V \times \{0_{D}\})) \to L (g) \in LSHyp (W)$
57	47 48 52 56	lshpcmp	$⊢ ((φ \land g \in F) \land (g \neq V \times \{0_{D}\} \land G \neq V \times \{0_{D}\})) \to (L (G) \subseteq L (g) \leftrightarrow L (G) = L (g))$
58	7	ad3antrrr	$⊢ (((φ \land g \in F) \land (g \neq V \times \{0_{D}\} \land G \neq V \times \{0_{D}\})) \land L (G) = L (g)) \to W \in LVec$
59	8	ad3antrrr	$⊢ (((φ \land g \in F) \land (g \neq V \times \{0_{D}\} \land G \neq V \times \{0_{D}\})) \land L (G) = L (g)) \to G \in F$
60		simpllr	$⊢ (((φ \land g \in F) \land (g \neq V \times \{0_{D}\} \land G \neq V \times \{0_{D}\})) \land L (G) = L (g)) \to g \in F$
61		simpr	$⊢ (((φ \land g \in F) \land (g \neq V \times \{0_{D}\} \land G \neq V \times \{0_{D}\})) \land L (G) = L (g)) \to L (G) = L (g)$
62	2 5 6 1 3 4	eqlkr2	$⊢ (W \in LVec \land (G \in F \land g \in F) \land L (G) = L (g)) \to \exists k \in K g = G {\underset{˙}{\cdot}}_{f} (V \times \{k\})$
63	58 59 60 61 62	syl121anc	$⊢ (((φ \land g \in F) \land (g \neq V \times \{0_{D}\} \land G \neq V \times \{0_{D}\})) \land L (G) = L (g)) \to \exists k \in K g = G {\underset{˙}{\cdot}}_{f} (V \times \{k\})$
64	63	ex	$⊢ ((φ \land g \in F) \land (g \neq V \times \{0_{D}\} \land G \neq V \times \{0_{D}\})) \to (L (G) = L (g) \to \exists k \in K g = G {\underset{˙}{\cdot}}_{f} (V \times \{k\}))$
65	57 64	sylbid	$⊢ ((φ \land g \in F) \land (g \neq V \times \{0_{D}\} \land G \neq V \times \{0_{D}\})) \to (L (G) \subseteq L (g) \to \exists k \in K g = G {\underset{˙}{\cdot}}_{f} (V \times \{k\}))$
66	26 46 65	pm2.61da2ne	$⊢ (φ \land g \in F) \to (L (G) \subseteq L (g) \to \exists k \in K g = G {\underset{˙}{\cdot}}_{f} (V \times \{k\}))$
67	7	ad2antrr	$⊢ ((φ \land g \in F) \land k \in K) \to W \in LVec$
68	8	ad2antrr	$⊢ ((φ \land g \in F) \land k \in K) \to G \in F$
69		simpr	$⊢ ((φ \land g \in F) \land k \in K) \to k \in K$
70	1 2 5 6 3 4 67 68 69	lkrscss	$⊢ ((φ \land g \in F) \land k \in K) \to L (G) \subseteq L (G {\underset{˙}{\cdot}}_{f} (V \times \{k\}))$
71	70	ex	$⊢ (φ \land g \in F) \to (k \in K \to L (G) \subseteq L (G {\underset{˙}{\cdot}}_{f} (V \times \{k\})))$
72		fveq2	$⊢ g = G {\underset{˙}{\cdot}}_{f} (V \times \{k\}) \to L (g) = L (G {\underset{˙}{\cdot}}_{f} (V \times \{k\}))$
73	72	sseq2d	$⊢ g = G {\underset{˙}{\cdot}}_{f} (V \times \{k\}) \to (L (G) \subseteq L (g) \leftrightarrow L (G) \subseteq L (G {\underset{˙}{\cdot}}_{f} (V \times \{k\})))$
74	73	biimprcd	$⊢ L (G) \subseteq L (G {\underset{˙}{\cdot}}_{f} (V \times \{k\})) \to (g = G {\underset{˙}{\cdot}}_{f} (V \times \{k\}) \to L (G) \subseteq L (g))$
75	71 74	syl6	$⊢ (φ \land g \in F) \to (k \in K \to (g = G {\underset{˙}{\cdot}}_{f} (V \times \{k\}) \to L (G) \subseteq L (g)))$
76	75	rexlimdv	$⊢ (φ \land g \in F) \to (\exists k \in K g = G {\underset{˙}{\cdot}}_{f} (V \times \{k\}) \to L (G) \subseteq L (g))$
77	66 76	impbid	$⊢ (φ \land g \in F) \to (L (G) \subseteq L (g) \leftrightarrow \exists k \in K g = G {\underset{˙}{\cdot}}_{f} (V \times \{k\}))$
78	77	pm5.32da	$⊢ φ \to ((g \in F \land L (G) \subseteq L (g)) \leftrightarrow (g \in F \land \exists k \in K g = G {\underset{˙}{\cdot}}_{f} (V \times \{k\})))$
79	11	adantr	$⊢ (φ \land k \in K) \to W \in LMod$
80	8	adantr	$⊢ (φ \land k \in K) \to G \in F$
81		simpr	$⊢ (φ \land k \in K) \to k \in K$
82	1 2 5 6 3 79 80 81	lflvscl	$⊢ (φ \land k \in K) \to G {\underset{˙}{\cdot}}_{f} (V \times \{k\}) \in F$
83		eleq1a	$⊢ G {\underset{˙}{\cdot}}_{f} (V \times \{k\}) \in F \to (g = G {\underset{˙}{\cdot}}_{f} (V \times \{k\}) \to g \in F)$
84	82 83	syl	$⊢ (φ \land k \in K) \to (g = G {\underset{˙}{\cdot}}_{f} (V \times \{k\}) \to g \in F)$
85	84	pm4.71rd	$⊢ (φ \land k \in K) \to (g = G {\underset{˙}{\cdot}}_{f} (V \times \{k\}) \leftrightarrow (g \in F \land g = G {\underset{˙}{\cdot}}_{f} (V \times \{k\})))$
86	85	rexbidva	$⊢ φ \to (\exists k \in K g = G {\underset{˙}{\cdot}}_{f} (V \times \{k\}) \leftrightarrow \exists k \in K (g \in F \land g = G {\underset{˙}{\cdot}}_{f} (V \times \{k\})))$
87		r19.42v	$⊢ \exists k \in K (g \in F \land g = G {\underset{˙}{\cdot}}_{f} (V \times \{k\})) \leftrightarrow (g \in F \land \exists k \in K g = G {\underset{˙}{\cdot}}_{f} (V \times \{k\}))$
88	86 87	bitr2di	$⊢ φ \to ((g \in F \land \exists k \in K g = G {\underset{˙}{\cdot}}_{f} (V \times \{k\})) \leftrightarrow \exists k \in K g = G {\underset{˙}{\cdot}}_{f} (V \times \{k\}))$
89	78 88	bitrd	$⊢ φ \to ((g \in F \land L (G) \subseteq L (g)) \leftrightarrow \exists k \in K g = G {\underset{˙}{\cdot}}_{f} (V \times \{k\}))$
90	89	abbidv	$⊢ φ \to \{g \| (g \in F \land L (G) \subseteq L (g))\} = \{g \| \exists k \in K g = G {\underset{˙}{\cdot}}_{f} (V \times \{k\})\}$
91	9 90	syl5eq	$⊢ φ \to \{g \in F \| L (G) \subseteq L (g)\} = \{g \| \exists k \in K g = G {\underset{˙}{\cdot}}_{f} (V \times \{k\})\}$

Metamath Proof Explorer

Theorem lfl1dim

Proof