lclkrs

Description: The set of functionals having closed kernels and majorizing the orthocomplement of a given subspace R is a subspace of the dual space. TODO: This proof repeats large parts of the lclkr proof. Do we achieve overall shortening by breaking them out as subtheorems? Or make lclkr a special case of this? (Contributed by NM, 29-Jan-2015)

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

Proof

Step	Hyp	Ref	Expression
1		lclkrs.h	$⊢ H = LHyp (K)$
2		lclkrs.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
3		lclkrs.u	$⊢ U = DVecH (K) (W)$
4		lclkrs.s	$⊢ S = LSubSp (U)$
5		lclkrs.f	$⊢ F = LFnl (U)$
6		lclkrs.l	$⊢ L = LKer (U)$
7		lclkrs.d	$⊢ D = LDual (U)$
8		lclkrs.t	$⊢ T = LSubSp (D)$
9		lclkrs.c	$⊢ C = \{f \in F \| (\underset{˙}{⊥} (\underset{˙}{⊥} (L (f))) = L (f) \land \underset{˙}{⊥} (L (f)) \subseteq R)\}$
10		lclkrs.k	$⊢ φ \to (K \in HL \land W \in H)$
11		lclkrs.r	$⊢ φ \to R \in S$
12		ssrab2	$⊢ \{f \in F \| (\underset{˙}{⊥} (\underset{˙}{⊥} (L (f))) = L (f) \land \underset{˙}{⊥} (L (f)) \subseteq R)\} \subseteq F$
13	12	a1i	$⊢ φ \to \{f \in F \| (\underset{˙}{⊥} (\underset{˙}{⊥} (L (f))) = L (f) \land \underset{˙}{⊥} (L (f)) \subseteq R)\} \subseteq F$
14	9	a1i	$⊢ φ \to C = \{f \in F \| (\underset{˙}{⊥} (\underset{˙}{⊥} (L (f))) = L (f) \land \underset{˙}{⊥} (L (f)) \subseteq R)\}$
15		eqid	$⊢ {Base}_{D} = {Base}_{D}$
16	1 3 10	dvhlmod	$⊢ φ \to U \in LMod$
17	5 7 15 16	ldualvbase	$⊢ φ \to {Base}_{D} = F$
18	13 14 17	3sstr4d	$⊢ φ \to C \subseteq {Base}_{D}$
19		eqid	$⊢ Scalar (U) = Scalar (U)$
20		eqid	$⊢ 0_{Scalar (U)} = 0_{Scalar (U)}$
21		eqid	$⊢ {Base}_{U} = {Base}_{U}$
22	19 20 21 5	lfl0f	$⊢ U \in LMod \to {Base}_{U} \times \{0_{Scalar (U)}\} \in F$
23	16 22	syl	$⊢ φ \to {Base}_{U} \times \{0_{Scalar (U)}\} \in F$
24	1 3 2 21 10	dochoc1	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} ({Base}_{U})) = {Base}_{U}$
25		eqidd	$⊢ φ \to {Base}_{U} \times \{0_{Scalar (U)}\} = {Base}_{U} \times \{0_{Scalar (U)}\}$
26	19 20 21 5 6	lkr0f	$⊢ (U \in LMod \land {Base}_{U} \times \{0_{Scalar (U)}\} \in F) \to (L ({Base}_{U} \times \{0_{Scalar (U)}\}) = {Base}_{U} \leftrightarrow {Base}_{U} \times \{0_{Scalar (U)}\} = {Base}_{U} \times \{0_{Scalar (U)}\})$
27	16 23 26	syl2anc	$⊢ φ \to (L ({Base}_{U} \times \{0_{Scalar (U)}\}) = {Base}_{U} \leftrightarrow {Base}_{U} \times \{0_{Scalar (U)}\} = {Base}_{U} \times \{0_{Scalar (U)}\})$
28	25 27	mpbird	$⊢ φ \to L ({Base}_{U} \times \{0_{Scalar (U)}\}) = {Base}_{U}$
29	28	fveq2d	$⊢ φ \to \underset{˙}{⊥} (L ({Base}_{U} \times \{0_{Scalar (U)}\})) = \underset{˙}{⊥} ({Base}_{U})$
30	29	fveq2d	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (L ({Base}_{U} \times \{0_{Scalar (U)}\}))) = \underset{˙}{⊥} (\underset{˙}{⊥} ({Base}_{U}))$
31	24 30 28	3eqtr4d	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (L ({Base}_{U} \times \{0_{Scalar (U)}\}))) = L ({Base}_{U} \times \{0_{Scalar (U)}\})$
32		eqid	$⊢ 0_{U} = 0_{U}$
33	1 3 2 21 32	doch1	$⊢ (K \in HL \land W \in H) \to \underset{˙}{⊥} ({Base}_{U}) = \{0_{U}\}$
34	10 33	syl	$⊢ φ \to \underset{˙}{⊥} ({Base}_{U}) = \{0_{U}\}$
35	29 34	eqtrd	$⊢ φ \to \underset{˙}{⊥} (L ({Base}_{U} \times \{0_{Scalar (U)}\})) = \{0_{U}\}$
36	32 4	lss0ss	$⊢ (U \in LMod \land R \in S) \to \{0_{U}\} \subseteq R$
37	16 11 36	syl2anc	$⊢ φ \to \{0_{U}\} \subseteq R$
38	35 37	eqsstrd	$⊢ φ \to \underset{˙}{⊥} (L ({Base}_{U} \times \{0_{Scalar (U)}\})) \subseteq R$
39	9	lcfls1lem	$⊢ {Base}_{U} \times \{0_{Scalar (U)}\} \in C \leftrightarrow ({Base}_{U} \times \{0_{Scalar (U)}\} \in F \land \underset{˙}{⊥} (\underset{˙}{⊥} (L ({Base}_{U} \times \{0_{Scalar (U)}\}))) = L ({Base}_{U} \times \{0_{Scalar (U)}\}) \land \underset{˙}{⊥} (L ({Base}_{U} \times \{0_{Scalar (U)}\})) \subseteq R)$
40	23 31 38 39	syl3anbrc	$⊢ φ \to {Base}_{U} \times \{0_{Scalar (U)}\} \in C$
41	40	ne0d	$⊢ φ \to C \neq \emptyset$
42		eqid	$⊢ {Base}_{Scalar (U)} = {Base}_{Scalar (U)}$
43		eqid	$⊢ \cdot_{D} = \cdot_{D}$
44	10	adantr	$⊢ (φ \land (x \in {Base}_{Scalar (D)} \land a \in C \land b \in C)) \to (K \in HL \land W \in H)$
45	11	adantr	$⊢ (φ \land (x \in {Base}_{Scalar (D)} \land a \in C \land b \in C)) \to R \in S$
46		simpr3	$⊢ (φ \land (x \in {Base}_{Scalar (D)} \land a \in C \land b \in C)) \to b \in C$
47		eqid	$⊢ +_{D} = +_{D}$
48		simpr2	$⊢ (φ \land (x \in {Base}_{Scalar (D)} \land a \in C \land b \in C)) \to a \in C$
49		simpr1	$⊢ (φ \land (x \in {Base}_{Scalar (D)} \land a \in C \land b \in C)) \to x \in {Base}_{Scalar (D)}$
50		eqid	$⊢ Scalar (D) = Scalar (D)$
51		eqid	$⊢ {Base}_{Scalar (D)} = {Base}_{Scalar (D)}$
52	19 42 7 50 51 16	ldualsbase	$⊢ φ \to {Base}_{Scalar (D)} = {Base}_{Scalar (U)}$
53	52	adantr	$⊢ (φ \land (x \in {Base}_{Scalar (D)} \land a \in C \land b \in C)) \to {Base}_{Scalar (D)} = {Base}_{Scalar (U)}$
54	49 53	eleqtrd	$⊢ (φ \land (x \in {Base}_{Scalar (D)} \land a \in C \land b \in C)) \to x \in {Base}_{Scalar (U)}$
55	1 2 3 4 5 6 7 19 42 43 9 44 45 48 54	lclkrslem1	$⊢ (φ \land (x \in {Base}_{Scalar (D)} \land a \in C \land b \in C)) \to x \cdot_{D} a \in C$
56	1 2 3 4 5 6 7 19 42 43 9 44 45 46 47 55	lclkrslem2	$⊢ (φ \land (x \in {Base}_{Scalar (D)} \land a \in C \land b \in C)) \to (x \cdot_{D} a) +_{D} b \in C$
57	56	ralrimivvva	$⊢ φ \to \forall x \in {Base}_{Scalar (D)} \forall a \in C \forall b \in C (x \cdot_{D} a) +_{D} b \in C$
58	50 51 15 47 43 8	islss	$⊢ C \in T \leftrightarrow (C \subseteq {Base}_{D} \land C \neq \emptyset \land \forall x \in {Base}_{Scalar (D)} \forall a \in C \forall b \in C (x \cdot_{D} a) +_{D} b \in C)$
59	18 41 57 58	syl3anbrc	$⊢ φ \to C \in T$

Metamath Proof Explorer

Theorem lclkrs

Proof