lcfr

Description: Reconstruction of a subspace from a dual subspace of functionals with closed kernels. Our proof was suggested by Mario Carneiro, 20-Feb-2015. (Contributed by NM, 5-Mar-2015)

	Ref	Expression
Hypotheses	lcfr.h	$⊢ H = LHyp (K)$
	lcfr.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
	lcfr.u	$⊢ U = DVecH (K) (W)$
	lcfr.s	$⊢ S = LSubSp (U)$
	lcfr.f	$⊢ F = LFnl (U)$
	lcfr.l	$⊢ L = LKer (U)$
	lcfr.d	$⊢ D = LDual (U)$
	lcfr.t	$⊢ T = LSubSp (D)$
	lcfr.c	$⊢ C = \{f \in F \| \underset{˙}{⊥} (\underset{˙}{⊥} (L (f))) = L (f)\}$
	lcfr.q	$⊢ Q = ⋃_{g \in R} \underset{˙}{⊥} (L (g))$
	lcfr.k	$⊢ φ \to (K \in HL \land W \in H)$
	lcfr.r	$⊢ φ \to R \in T$
	lcfr.rs	$⊢ φ \to R \subseteq C$
Assertion	lcfr	$⊢ φ \to Q \in S$

Proof

Step	Hyp	Ref	Expression
1		lcfr.h	$⊢ H = LHyp (K)$
2		lcfr.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
3		lcfr.u	$⊢ U = DVecH (K) (W)$
4		lcfr.s	$⊢ S = LSubSp (U)$
5		lcfr.f	$⊢ F = LFnl (U)$
6		lcfr.l	$⊢ L = LKer (U)$
7		lcfr.d	$⊢ D = LDual (U)$
8		lcfr.t	$⊢ T = LSubSp (D)$
9		lcfr.c	$⊢ C = \{f \in F \| \underset{˙}{⊥} (\underset{˙}{⊥} (L (f))) = L (f)\}$
10		lcfr.q	$⊢ Q = ⋃_{g \in R} \underset{˙}{⊥} (L (g))$
11		lcfr.k	$⊢ φ \to (K \in HL \land W \in H)$
12		lcfr.r	$⊢ φ \to R \in T$
13		lcfr.rs	$⊢ φ \to R \subseteq C$
14		2fveq3	$⊢ g = h \to \underset{˙}{⊥} (L (g)) = \underset{˙}{⊥} (L (h))$
15	14	cbviunv	$⊢ ⋃_{g \in R} \underset{˙}{⊥} (L (g)) = ⋃_{h \in R} \underset{˙}{⊥} (L (h))$
16	10 15	eqtri	$⊢ Q = ⋃_{h \in R} \underset{˙}{⊥} (L (h))$
17	11	adantr	$⊢ (φ \land h \in R) \to (K \in HL \land W \in H)$
18		eqid	$⊢ {Base}_{U} = {Base}_{U}$
19	1 3 11	dvhlmod	$⊢ φ \to U \in LMod$
20	19	adantr	$⊢ (φ \land h \in R) \to U \in LMod$
21		eqid	$⊢ {Base}_{D} = {Base}_{D}$
22	21 8	lssss	$⊢ R \in T \to R \subseteq {Base}_{D}$
23	12 22	syl	$⊢ φ \to R \subseteq {Base}_{D}$
24	5 7 21 19	ldualvbase	$⊢ φ \to {Base}_{D} = F$
25	23 24	sseqtrd	$⊢ φ \to R \subseteq F$
26	25	sselda	$⊢ (φ \land h \in R) \to h \in F$
27	18 5 6 20 26	lkrssv	$⊢ (φ \land h \in R) \to L (h) \subseteq {Base}_{U}$
28	1 3 18 2	dochssv	$⊢ ((K \in HL \land W \in H) \land L (h) \subseteq {Base}_{U}) \to \underset{˙}{⊥} (L (h)) \subseteq {Base}_{U}$
29	17 27 28	syl2anc	$⊢ (φ \land h \in R) \to \underset{˙}{⊥} (L (h)) \subseteq {Base}_{U}$
30	29	ralrimiva	$⊢ φ \to \forall h \in R \underset{˙}{⊥} (L (h)) \subseteq {Base}_{U}$
31		iunss	$⊢ ⋃_{h \in R} \underset{˙}{⊥} (L (h)) \subseteq {Base}_{U} \leftrightarrow \forall h \in R \underset{˙}{⊥} (L (h)) \subseteq {Base}_{U}$
32	30 31	sylibr	$⊢ φ \to ⋃_{h \in R} \underset{˙}{⊥} (L (h)) \subseteq {Base}_{U}$
33	16 32	eqsstrid	$⊢ φ \to Q \subseteq {Base}_{U}$
34	16	a1i	$⊢ φ \to Q = ⋃_{h \in R} \underset{˙}{⊥} (L (h))$
35	7 19	lduallmod	$⊢ φ \to D \in LMod$
36		eqid	$⊢ 0_{D} = 0_{D}$
37	36 8	lss0cl	$⊢ (D \in LMod \land R \in T) \to 0_{D} \in R$
38	35 12 37	syl2anc	$⊢ φ \to 0_{D} \in R$
39	5 7 36 19	ldual0vcl	$⊢ φ \to 0_{D} \in F$
40	18 5 6 19 39	lkrssv	$⊢ φ \to L (0_{D}) \subseteq {Base}_{U}$
41	1 3 18 4 2	dochlss	$⊢ ((K \in HL \land W \in H) \land L (0_{D}) \subseteq {Base}_{U}) \to \underset{˙}{⊥} (L (0_{D})) \in S$
42	11 40 41	syl2anc	$⊢ φ \to \underset{˙}{⊥} (L (0_{D})) \in S$
43		eqid	$⊢ 0_{U} = 0_{U}$
44	43 4	lss0cl	$⊢ (U \in LMod \land \underset{˙}{⊥} (L (0_{D})) \in S) \to 0_{U} \in \underset{˙}{⊥} (L (0_{D}))$
45	19 42 44	syl2anc	$⊢ φ \to 0_{U} \in \underset{˙}{⊥} (L (0_{D}))$
46		2fveq3	$⊢ h = 0_{D} \to \underset{˙}{⊥} (L (h)) = \underset{˙}{⊥} (L (0_{D}))$
47	46	eleq2d	$⊢ h = 0_{D} \to (0_{U} \in \underset{˙}{⊥} (L (h)) \leftrightarrow 0_{U} \in \underset{˙}{⊥} (L (0_{D})))$
48	47	rspcev	$⊢ (0_{D} \in R \land 0_{U} \in \underset{˙}{⊥} (L (0_{D}))) \to \exists h \in R 0_{U} \in \underset{˙}{⊥} (L (h))$
49	38 45 48	syl2anc	$⊢ φ \to \exists h \in R 0_{U} \in \underset{˙}{⊥} (L (h))$
50		eliun	$⊢ 0_{U} \in ⋃_{h \in R} \underset{˙}{⊥} (L (h)) \leftrightarrow \exists h \in R 0_{U} \in \underset{˙}{⊥} (L (h))$
51	49 50	sylibr	$⊢ φ \to 0_{U} \in ⋃_{h \in R} \underset{˙}{⊥} (L (h))$
52	51	ne0d	$⊢ φ \to ⋃_{h \in R} \underset{˙}{⊥} (L (h)) \neq \emptyset$
53	34 52	eqnetrd	$⊢ φ \to Q \neq \emptyset$
54		eqid	$⊢ +_{U} = +_{U}$
55		rabeq	$⊢ F = LFnl (U) \to \{f \in F \| \underset{˙}{⊥} (\underset{˙}{⊥} (L (f))) = L (f)\} = \{f \in LFnl (U) \| \underset{˙}{⊥} (\underset{˙}{⊥} (L (f))) = L (f)\}$
56	5 55	ax-mp	$⊢ \{f \in F \| \underset{˙}{⊥} (\underset{˙}{⊥} (L (f))) = L (f)\} = \{f \in LFnl (U) \| \underset{˙}{⊥} (\underset{˙}{⊥} (L (f))) = L (f)\}$
57	9 56	eqtri	$⊢ C = \{f \in LFnl (U) \| \underset{˙}{⊥} (\underset{˙}{⊥} (L (f))) = L (f)\}$
58	11	adantr	$⊢ (φ \land (x \in {Base}_{Scalar (U)} \land a \in Q \land b \in Q)) \to (K \in HL \land W \in H)$
59	12	adantr	$⊢ (φ \land (x \in {Base}_{Scalar (U)} \land a \in Q \land b \in Q)) \to R \in T$
60	13	adantr	$⊢ (φ \land (x \in {Base}_{Scalar (U)} \land a \in Q \land b \in Q)) \to R \subseteq C$
61		simpr2	$⊢ (φ \land (x \in {Base}_{Scalar (U)} \land a \in Q \land b \in Q)) \to a \in Q$
62		eqid	$⊢ Scalar (U) = Scalar (U)$
63		eqid	$⊢ {Base}_{Scalar (U)} = {Base}_{Scalar (U)}$
64		eqid	$⊢ \cdot_{U} = \cdot_{U}$
65		simpr1	$⊢ (φ \land (x \in {Base}_{Scalar (U)} \land a \in Q \land b \in Q)) \to x \in {Base}_{Scalar (U)}$
66	1 2 3 18 5 6 7 8 58 59 16 61 62 63 64 65	lcfrlem5	$⊢ (φ \land (x \in {Base}_{Scalar (U)} \land a \in Q \land b \in Q)) \to x \cdot_{U} a \in Q$
67		simpr3	$⊢ (φ \land (x \in {Base}_{Scalar (U)} \land a \in Q \land b \in Q)) \to b \in Q$
68	1 2 3 54 5 6 7 8 57 16 58 59 60 66 67	lcfrlem42	$⊢ (φ \land (x \in {Base}_{Scalar (U)} \land a \in Q \land b \in Q)) \to (x \cdot_{U} a) +_{U} b \in Q$
69	68	ralrimivvva	$⊢ φ \to \forall x \in {Base}_{Scalar (U)} \forall a \in Q \forall b \in Q (x \cdot_{U} a) +_{U} b \in Q$
70	62 63 18 54 64 4	islss	$⊢ Q \in S \leftrightarrow (Q \subseteq {Base}_{U} \land Q \neq \emptyset \land \forall x \in {Base}_{Scalar (U)} \forall a \in Q \forall b \in Q (x \cdot_{U} a) +_{U} b \in Q)$
71	33 53 69 70	syl3anbrc	$⊢ φ \to Q \in S$

Metamath Proof Explorer

Theorem lcfr

Proof