lcfrvalsnN

Description: Reconstruction from the dual space span of a singleton. (Contributed by NM, 19-Feb-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	lcfrvalsn.h	$⊢ H = LHyp (K)$
	lcfrvalsn.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
	lcfrvalsn.u	$⊢ U = DVecH (K) (W)$
	lcfrvalsn.f	$⊢ F = LFnl (U)$
	lcfrvalsn.l	$⊢ L = LKer (U)$
	lcfrvalsn.d	$⊢ D = LDual (U)$
	lcfrvalsn.n	$⊢ N = LSpan (D)$
	lcfrvalsn.k	$⊢ φ \to (K \in HL \land W \in H)$
	lcfrvalsn.g	$⊢ φ \to G \in F$
	lcfrvalsn.q	$⊢ Q = ⋃_{f \in R} \underset{˙}{⊥} (L (f))$
	lcfrvalsn.r	$⊢ R = N (\{G\})$
Assertion	lcfrvalsnN	$⊢ φ \to Q = \underset{˙}{⊥} (L (G))$

Proof

Step	Hyp	Ref	Expression
1		lcfrvalsn.h	$⊢ H = LHyp (K)$
2		lcfrvalsn.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
3		lcfrvalsn.u	$⊢ U = DVecH (K) (W)$
4		lcfrvalsn.f	$⊢ F = LFnl (U)$
5		lcfrvalsn.l	$⊢ L = LKer (U)$
6		lcfrvalsn.d	$⊢ D = LDual (U)$
7		lcfrvalsn.n	$⊢ N = LSpan (D)$
8		lcfrvalsn.k	$⊢ φ \to (K \in HL \land W \in H)$
9		lcfrvalsn.g	$⊢ φ \to G \in F$
10		lcfrvalsn.q	$⊢ Q = ⋃_{f \in R} \underset{˙}{⊥} (L (f))$
11		lcfrvalsn.r	$⊢ R = N (\{G\})$
12		eliun	$⊢ x \in ⋃_{f \in R} \underset{˙}{⊥} (L (f)) \leftrightarrow \exists f \in R x \in \underset{˙}{⊥} (L (f))$
13	11	eleq2i	$⊢ f \in R \leftrightarrow f \in N (\{G\})$
14	8	adantr	$⊢ (φ \land f \in N (\{G\})) \to (K \in HL \land W \in H)$
15		eqid	$⊢ {Base}_{U} = {Base}_{U}$
16	1 3 8	dvhlmod	$⊢ φ \to U \in LMod$
17	16	adantr	$⊢ (φ \land f \in N (\{G\})) \to U \in LMod$
18	6 16	lduallmod	$⊢ φ \to D \in LMod$
19		eqid	$⊢ {Base}_{D} = {Base}_{D}$
20	4 6 19 16 9	ldualelvbase	$⊢ φ \to G \in {Base}_{D}$
21		eqid	$⊢ LSubSp (D) = LSubSp (D)$
22	19 21 7	lspsncl	$⊢ (D \in LMod \land G \in {Base}_{D}) \to N (\{G\}) \in LSubSp (D)$
23	18 20 22	syl2anc	$⊢ φ \to N (\{G\}) \in LSubSp (D)$
24	19 21	lssel	$⊢ (N (\{G\}) \in LSubSp (D) \land f \in N (\{G\})) \to f \in {Base}_{D}$
25	23 24	sylan	$⊢ (φ \land f \in N (\{G\})) \to f \in {Base}_{D}$
26	4 6 19 16	ldualvbase	$⊢ φ \to {Base}_{D} = F$
27	26	adantr	$⊢ (φ \land f \in N (\{G\})) \to {Base}_{D} = F$
28	25 27	eleqtrd	$⊢ (φ \land f \in N (\{G\})) \to f \in F$
29	15 4 5 17 28	lkrssv	$⊢ (φ \land f \in N (\{G\})) \to L (f) \subseteq {Base}_{U}$
30		eqid	$⊢ Scalar (D) = Scalar (D)$
31		eqid	$⊢ {Base}_{Scalar (D)} = {Base}_{Scalar (D)}$
32		eqid	$⊢ \cdot_{D} = \cdot_{D}$
33	30 31 19 32 7	lspsnel	$⊢ (D \in LMod \land G \in {Base}_{D}) \to (f \in N (\{G\}) \leftrightarrow \exists k \in {Base}_{Scalar (D)} f = k \cdot_{D} G)$
34	18 20 33	syl2anc	$⊢ φ \to (f \in N (\{G\}) \leftrightarrow \exists k \in {Base}_{Scalar (D)} f = k \cdot_{D} G)$
35		eqid	$⊢ Scalar (U) = Scalar (U)$
36		eqid	$⊢ {Base}_{Scalar (U)} = {Base}_{Scalar (U)}$
37	35 36 6 30 31 16	ldualsbase	$⊢ φ \to {Base}_{Scalar (D)} = {Base}_{Scalar (U)}$
38	37	rexeqdv	$⊢ φ \to (\exists k \in {Base}_{Scalar (D)} f = k \cdot_{D} G \leftrightarrow \exists k \in {Base}_{Scalar (U)} f = k \cdot_{D} G)$
39	34 38	bitrd	$⊢ φ \to (f \in N (\{G\}) \leftrightarrow \exists k \in {Base}_{Scalar (U)} f = k \cdot_{D} G)$
40	39	biimpa	$⊢ (φ \land f \in N (\{G\})) \to \exists k \in {Base}_{Scalar (U)} f = k \cdot_{D} G$
41	1 3 8	dvhlvec	$⊢ φ \to U \in LVec$
42	41	adantr	$⊢ (φ \land f \in N (\{G\})) \to U \in LVec$
43	9	adantr	$⊢ (φ \land f \in N (\{G\})) \to G \in F$
44	35 36 4 5 6 32 42 43 28	lkrss2N	$⊢ (φ \land f \in N (\{G\})) \to (L (G) \subseteq L (f) \leftrightarrow \exists k \in {Base}_{Scalar (U)} f = k \cdot_{D} G)$
45	40 44	mpbird	$⊢ (φ \land f \in N (\{G\})) \to L (G) \subseteq L (f)$
46	1 3 15 2	dochss	$⊢ ((K \in HL \land W \in H) \land L (f) \subseteq {Base}_{U} \land L (G) \subseteq L (f)) \to \underset{˙}{⊥} (L (f)) \subseteq \underset{˙}{⊥} (L (G))$
47	14 29 45 46	syl3anc	$⊢ (φ \land f \in N (\{G\})) \to \underset{˙}{⊥} (L (f)) \subseteq \underset{˙}{⊥} (L (G))$
48	47	sseld	$⊢ (φ \land f \in N (\{G\})) \to (x \in \underset{˙}{⊥} (L (f)) \to x \in \underset{˙}{⊥} (L (G)))$
49	48	ex	$⊢ φ \to (f \in N (\{G\}) \to (x \in \underset{˙}{⊥} (L (f)) \to x \in \underset{˙}{⊥} (L (G))))$
50	13 49	syl5bi	$⊢ φ \to (f \in R \to (x \in \underset{˙}{⊥} (L (f)) \to x \in \underset{˙}{⊥} (L (G))))$
51	50	rexlimdv	$⊢ φ \to (\exists f \in R x \in \underset{˙}{⊥} (L (f)) \to x \in \underset{˙}{⊥} (L (G)))$
52	19 7	lspsnid	$⊢ (D \in LMod \land G \in {Base}_{D}) \to G \in N (\{G\})$
53	18 20 52	syl2anc	$⊢ φ \to G \in N (\{G\})$
54	53 11	eleqtrrdi	$⊢ φ \to G \in R$
55		2fveq3	$⊢ f = G \to \underset{˙}{⊥} (L (f)) = \underset{˙}{⊥} (L (G))$
56	55	eleq2d	$⊢ f = G \to (x \in \underset{˙}{⊥} (L (f)) \leftrightarrow x \in \underset{˙}{⊥} (L (G)))$
57	56	rspcev	$⊢ (G \in R \land x \in \underset{˙}{⊥} (L (G))) \to \exists f \in R x \in \underset{˙}{⊥} (L (f))$
58	54 57	sylan	$⊢ (φ \land x \in \underset{˙}{⊥} (L (G))) \to \exists f \in R x \in \underset{˙}{⊥} (L (f))$
59	58	ex	$⊢ φ \to (x \in \underset{˙}{⊥} (L (G)) \to \exists f \in R x \in \underset{˙}{⊥} (L (f)))$
60	51 59	impbid	$⊢ φ \to (\exists f \in R x \in \underset{˙}{⊥} (L (f)) \leftrightarrow x \in \underset{˙}{⊥} (L (G)))$
61	12 60	syl5bb	$⊢ φ \to (x \in ⋃_{f \in R} \underset{˙}{⊥} (L (f)) \leftrightarrow x \in \underset{˙}{⊥} (L (G)))$
62	61	eqrdv	$⊢ φ \to ⋃_{f \in R} \underset{˙}{⊥} (L (f)) = \underset{˙}{⊥} (L (G))$
63	10 62	syl5eq	$⊢ φ \to Q = \underset{˙}{⊥} (L (G))$

Metamath Proof Explorer

Theorem lcfrvalsnN

Proof