lfl1dim2N

Description: Equivalent expressions for a 1-dim subspace (ray) of functionals. TODO: delete this if not useful; lfl1dim may be more compatible with lspsn . (Contributed by NM, 24-Oct-2014) (New usage is discouraged.)

	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	lfl1dim2N	$⊢ φ \to \{g \in F \| L (G) \subseteq L (g)\} = \{g \in F \| \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		lveclmod	$⊢ W \in LVec \to W \in LMod$
10	7 9	syl	$⊢ φ \to W \in LMod$
11		eqid	$⊢ 0_{D} = 0_{D}$
12	2 5 11	lmod0cl	$⊢ W \in LMod \to 0_{D} \in K$
13	10 12	syl	$⊢ φ \to 0_{D} \in K$
14	13	ad2antrr	$⊢ ((φ \land g \in F) \land g = V \times \{0_{D}\}) \to 0_{D} \in K$
15		simpr	$⊢ ((φ \land g \in F) \land g = V \times \{0_{D}\}) \to g = V \times \{0_{D}\}$
16	10	ad2antrr	$⊢ ((φ \land g \in F) \land g = V \times \{0_{D}\}) \to W \in LMod$
17	8	ad2antrr	$⊢ ((φ \land g \in F) \land g = V \times \{0_{D}\}) \to G \in F$
18	1 2 3 5 6 11 16 17	lfl0sc	$⊢ ((φ \land g \in F) \land g = V \times \{0_{D}\}) \to G {\underset{˙}{\cdot}}_{f} (V \times \{0_{D}\}) = V \times \{0_{D}\}$
19	15 18	eqtr4d	$⊢ ((φ \land g \in F) \land g = V \times \{0_{D}\}) \to g = G {\underset{˙}{\cdot}}_{f} (V \times \{0_{D}\})$
20		sneq	$⊢ k = 0_{D} \to \{k\} = \{0_{D}\}$
21	20	xpeq2d	$⊢ k = 0_{D} \to V \times \{k\} = V \times \{0_{D}\}$
22	21	oveq2d	$⊢ k = 0_{D} \to G {\underset{˙}{\cdot}}_{f} (V \times \{k\}) = G {\underset{˙}{\cdot}}_{f} (V \times \{0_{D}\})$
23	22	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\})$
24	14 19 23	syl2anc	$⊢ ((φ \land g \in F) \land g = V \times \{0_{D}\}) \to \exists k \in K g = G {\underset{˙}{\cdot}}_{f} (V \times \{k\})$
25	24	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\}))$
26	13	ad3antrrr	$⊢ (((φ \land g \in F) \land G = V \times \{0_{D}\}) \land L (G) \subseteq L (g)) \to 0_{D} \in K$
27	10	ad3antrrr	$⊢ (((φ \land g \in F) \land G = V \times \{0_{D}\}) \land L (G) \subseteq L (g)) \to W \in LMod$
28		simpllr	$⊢ (((φ \land g \in F) \land G = V \times \{0_{D}\}) \land L (G) \subseteq L (g)) \to g \in F$
29	1 3 4 27 28	lkrssv	$⊢ (((φ \land g \in F) \land G = V \times \{0_{D}\}) \land L (G) \subseteq L (g)) \to L (g) \subseteq V$
30	10	adantr	$⊢ (φ \land g \in F) \to W \in LMod$
31	8	adantr	$⊢ (φ \land g \in F) \to G \in F$
32	2 11 1 3 4	lkr0f	$⊢ (W \in LMod \land G \in F) \to (L (G) = V \leftrightarrow G = V \times \{0_{D}\})$
33	30 31 32	syl2anc	$⊢ (φ \land g \in F) \to (L (G) = V \leftrightarrow G = V \times \{0_{D}\})$
34	33	biimpar	$⊢ ((φ \land g \in F) \land G = V \times \{0_{D}\}) \to L (G) = V$
35	34	sseq1d	$⊢ ((φ \land g \in F) \land G = V \times \{0_{D}\}) \to (L (G) \subseteq L (g) \leftrightarrow V \subseteq L (g))$
36	35	biimpa	$⊢ (((φ \land g \in F) \land G = V \times \{0_{D}\}) \land L (G) \subseteq L (g)) \to V \subseteq L (g)$
37	29 36	eqssd	$⊢ (((φ \land g \in F) \land G = V \times \{0_{D}\}) \land L (G) \subseteq L (g)) \to L (g) = V$
38	2 11 1 3 4	lkr0f	$⊢ (W \in LMod \land g \in F) \to (L (g) = V \leftrightarrow g = V \times \{0_{D}\})$
39	27 28 38	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}\})$
40	37 39	mpbid	$⊢ (((φ \land g \in F) \land G = V \times \{0_{D}\}) \land L (G) \subseteq L (g)) \to g = V \times \{0_{D}\}$
41	8	ad3antrrr	$⊢ (((φ \land g \in F) \land G = V \times \{0_{D}\}) \land L (G) \subseteq L (g)) \to G \in F$
42	1 2 3 5 6 11 27 41	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}\}$
43	40 42	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}\})$
44	26 43 23	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\})$
45	44	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\}))$
46		eqid	$⊢ LSHyp (W) = LSHyp (W)$
47	7	ad2antrr	$⊢ ((φ \land g \in F) \land (g \neq V \times \{0_{D}\} \land G \neq V \times \{0_{D}\})) \to W \in LVec$
48	8	ad2antrr	$⊢ ((φ \land g \in F) \land (g \neq V \times \{0_{D}\} \land G \neq V \times \{0_{D}\})) \to G \in F$
49		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}\}$
50	1 2 11 46 3 4	lkrshp	$⊢ (W \in LVec \land G \in F \land G \neq V \times \{0_{D}\}) \to L (G) \in LSHyp (W)$
51	47 48 49 50	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)$
52		simplr	$⊢ ((φ \land g \in F) \land (g \neq V \times \{0_{D}\} \land G \neq V \times \{0_{D}\})) \to g \in F$
53		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}\}$
54	1 2 11 46 3 4	lkrshp	$⊢ (W \in LVec \land g \in F \land g \neq V \times \{0_{D}\}) \to L (g) \in LSHyp (W)$
55	47 52 53 54	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)$
56	46 47 51 55	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))$
57	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$
58	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$
59		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$
60		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)$
61	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\})$
62	57 58 59 60 61	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\})$
63	62	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\}))$
64	56 63	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\}))$
65	25 45 64	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\}))$
66	7	ad2antrr	$⊢ ((φ \land g \in F) \land k \in K) \to W \in LVec$
67	8	ad2antrr	$⊢ ((φ \land g \in F) \land k \in K) \to G \in F$
68		simpr	$⊢ ((φ \land g \in F) \land k \in K) \to k \in K$
69	1 2 5 6 3 4 66 67 68	lkrscss	$⊢ ((φ \land g \in F) \land k \in K) \to L (G) \subseteq L (G {\underset{˙}{\cdot}}_{f} (V \times \{k\}))$
70	69	ex	$⊢ (φ \land g \in F) \to (k \in K \to L (G) \subseteq L (G {\underset{˙}{\cdot}}_{f} (V \times \{k\})))$
71		fveq2	$⊢ g = G {\underset{˙}{\cdot}}_{f} (V \times \{k\}) \to L (g) = L (G {\underset{˙}{\cdot}}_{f} (V \times \{k\}))$
72	71	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\})))$
73	72	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))$
74	70 73	syl6	$⊢ (φ \land g \in F) \to (k \in K \to (g = G {\underset{˙}{\cdot}}_{f} (V \times \{k\}) \to L (G) \subseteq L (g)))$
75	74	rexlimdv	$⊢ (φ \land g \in F) \to (\exists k \in K g = G {\underset{˙}{\cdot}}_{f} (V \times \{k\}) \to L (G) \subseteq L (g))$
76	65 75	impbid	$⊢ (φ \land g \in F) \to (L (G) \subseteq L (g) \leftrightarrow \exists k \in K g = G {\underset{˙}{\cdot}}_{f} (V \times \{k\}))$
77	76	rabbidva	$⊢ φ \to \{g \in F \| L (G) \subseteq L (g)\} = \{g \in F \| \exists k \in K g = G {\underset{˙}{\cdot}}_{f} (V \times \{k\})\}$

Metamath Proof Explorer

Theorem lfl1dim2N

Proof