Theorem lcfl3

Description: Property of a functional with a closed kernel. (Contributed by NM, 1-Jan-2015)

	Ref	Expression
Hypotheses	lcfl3.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	lcfl3.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
	lcfl3.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	lcfl3.v	$$⊢V={\mathrm{Base}}_U$$
	lcfl3.a	$$⊢A=\mathrm{LSAtoms}\left(U\right)$$
	lcfl3.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
	lcfl3.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
	lcfl3.c	$$⊢C=\left\{f\in F|\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(f\right)\right)\right)=L\left(f\right)\right\}$$
	lcfl3.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	lcfl3.g	$$⊢\phi \to G\in F$$
Assertion	lcfl3	$$⊢\phi \to \left(G\in C\leftrightarrow \left(\underset{\dot{}}{\perp }\left(L\left(G\right)\right)\in A\vee L\left(G\right)=V\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		lcfl3.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		lcfl3.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
3		lcfl3.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
4		lcfl3.v	$$⊢V={\mathrm{Base}}_U$$
5		lcfl3.a	$$⊢A=\mathrm{LSAtoms}\left(U\right)$$
6		lcfl3.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
7		lcfl3.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
8		lcfl3.c	$$⊢C=\left\{f\in F|\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(f\right)\right)\right)=L\left(f\right)\right\}$$
9		lcfl3.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
10		lcfl3.g	$$⊢\phi \to G\in F$$
11	1 2 3 4 6 7 8 9 10	lcfl2	$$⊢\phi \to \left(G\in C\leftrightarrow \left(\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(G\right)\right)\right)\ne V\vee L\left(G\right)=V\right)\right)$$
12	1 2 3 4 5 6 7 9 10	dochkrsat2	$$⊢\phi \to \left(\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(G\right)\right)\right)\ne V\leftrightarrow \underset{\dot{}}{\perp }\left(L\left(G\right)\right)\in A\right)$$
13	12	orbi1d	$$⊢\phi \to \left(\left(\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(G\right)\right)\right)\ne V\vee L\left(G\right)=V\right)\leftrightarrow \left(\underset{\dot{}}{\perp }\left(L\left(G\right)\right)\in A\vee L\left(G\right)=V\right)\right)$$
14	11 13	bitrd	$$⊢\phi \to \left(G\in C\leftrightarrow \left(\underset{\dot{}}{\perp }\left(L\left(G\right)\right)\in A\vee L\left(G\right)=V\right)\right)$$