Theorem lclkrslem1

Description: The set of functionals having closed kernels and majorizing the orthocomplement of a given subspace Q is closed under scalar product. (Contributed by NM, 27-Jan-2015)

	Ref	Expression
Hypotheses	lclkrslem1.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	lclkrslem1.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
	lclkrslem1.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	lclkrslem1.s	$$⊢S=\mathrm{LSubSp}\left(U\right)$$
	lclkrslem1.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
	lclkrslem1.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
	lclkrslem1.d	$$⊢D=\mathrm{LDual}\left(U\right)$$
	lclkrslem1.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
	lclkrslem1.b	$$⊢B={\mathrm{Base}}_R$$
	lclkrslem1.t	$$⊢\underset{\dot{}}{·}={\cdot }_D$$
	lclkrslem1.c	$$⊢C=\left\{f\in F|\left(\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(f\right)\right)\right)=L\left(f\right)\wedge \underset{\dot{}}{\perp }\left(L\left(f\right)\right)\subseteq Q\right)\right\}$$
	lclkrslem1.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	lclkrslem1.q	$$⊢\phi \to Q\in S$$
	lclkrslem1.g	$$⊢\phi \to G\in C$$
	lclkrslem1.x	$$⊢\phi \to X\in B$$
Assertion	lclkrslem1	$$⊢\phi \to X\underset{\dot{}}{·}G\in C$$

Proof

Step	Hyp	Ref	Expression
1		lclkrslem1.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		lclkrslem1.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
3		lclkrslem1.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
4		lclkrslem1.s	$$⊢S=\mathrm{LSubSp}\left(U\right)$$
5		lclkrslem1.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
6		lclkrslem1.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
7		lclkrslem1.d	$$⊢D=\mathrm{LDual}\left(U\right)$$
8		lclkrslem1.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
9		lclkrslem1.b	$$⊢B={\mathrm{Base}}_R$$
10		lclkrslem1.t	$$⊢\underset{\dot{}}{·}={\cdot }_D$$
11		lclkrslem1.c	$$⊢C=\left\{f\in F|\left(\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(f\right)\right)\right)=L\left(f\right)\wedge \underset{\dot{}}{\perp }\left(L\left(f\right)\right)\subseteq Q\right)\right\}$$
12		lclkrslem1.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
13		lclkrslem1.q	$$⊢\phi \to Q\in S$$
14		lclkrslem1.g	$$⊢\phi \to G\in C$$
15		lclkrslem1.x	$$⊢\phi \to X\in B$$
16		eqid	$$⊢\left\{f\in F|\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(f\right)\right)\right)=L\left(f\right)\right\}=\left\{f\in F|\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(f\right)\right)\right)=L\left(f\right)\right\}$$
17	11 16	lcfls1c	$$⊢G\in C\leftrightarrow \left(G\in \left\{f\in F|\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(f\right)\right)\right)=L\left(f\right)\right\}\wedge \underset{\dot{}}{\perp }\left(L\left(G\right)\right)\subseteq Q\right)$$
18	17	simplbi	$$⊢G\in C\to G\in \left\{f\in F|\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(f\right)\right)\right)=L\left(f\right)\right\}$$
19	14 18	syl	$$⊢\phi \to G\in \left\{f\in F|\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(f\right)\right)\right)=L\left(f\right)\right\}$$
20	1 2 3 5 6 7 8 9 10 16 12 15 19	lclkrlem1	$$⊢\phi \to X\underset{\dot{}}{·}G\in \left\{f\in F|\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(f\right)\right)\right)=L\left(f\right)\right\}$$
21		eqid	$$⊢{\mathrm{Base}}_U={\mathrm{Base}}_U$$
22	1 3 12	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
23	11	lcfls1lem	$$⊢G\in C\leftrightarrow \left(G\in F\wedge \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(G\right)\right)\right)=L\left(G\right)\wedge \underset{\dot{}}{\perp }\left(L\left(G\right)\right)\subseteq Q\right)$$
24	14 23	sylib	$$⊢\phi \to \left(G\in F\wedge \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(G\right)\right)\right)=L\left(G\right)\wedge \underset{\dot{}}{\perp }\left(L\left(G\right)\right)\subseteq Q\right)$$
25	24	simp1d	$$⊢\phi \to G\in F$$
26	5 8 9 7 10 22 15 25	ldualvscl	$$⊢\phi \to X\underset{\dot{}}{·}G\in F$$
27	21 5 6 22 26	lkrssv	$$⊢\phi \to L\left(X\underset{\dot{}}{·}G\right)\subseteq {\mathrm{Base}}_U$$
28	1 3 12	dvhlvec	$$⊢\phi \to U\in \mathrm{LVec}$$
29	8 9 5 6 7 10 28 25 15	lkrss	$$⊢\phi \to L\left(G\right)\subseteq L\left(X\underset{\dot{}}{·}G\right)$$
30	1 3 21 2	dochss	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge L\left(X\underset{\dot{}}{·}G\right)\subseteq {\mathrm{Base}}_U\wedge L\left(G\right)\subseteq L\left(X\underset{\dot{}}{·}G\right)\right)\to \underset{\dot{}}{\perp }\left(L\left(X\underset{\dot{}}{·}G\right)\right)\subseteq \underset{\dot{}}{\perp }\left(L\left(G\right)\right)$$
31	12 27 29 30	syl3anc	$$⊢\phi \to \underset{\dot{}}{\perp }\left(L\left(X\underset{\dot{}}{·}G\right)\right)\subseteq \underset{\dot{}}{\perp }\left(L\left(G\right)\right)$$
32	24	simp3d	$$⊢\phi \to \underset{\dot{}}{\perp }\left(L\left(G\right)\right)\subseteq Q$$
33	31 32	sstrd	$$⊢\phi \to \underset{\dot{}}{\perp }\left(L\left(X\underset{\dot{}}{·}G\right)\right)\subseteq Q$$
34	11 16	lcfls1c	$$⊢X\underset{\dot{}}{·}G\in C\leftrightarrow \left(X\underset{\dot{}}{·}G\in \left\{f\in F|\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(f\right)\right)\right)=L\left(f\right)\right\}\wedge \underset{\dot{}}{\perp }\left(L\left(X\underset{\dot{}}{·}G\right)\right)\subseteq Q\right)$$
35	20 33 34	sylanbrc	$$⊢\phi \to X\underset{\dot{}}{·}G\in C$$