Theorem lcfl1

Description: Property of a functional with a closed kernel. (Contributed by NM, 31-Dec-2014)

	Ref	Expression
Hypotheses	lcfl1.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\}$$
	lcfl1.g	$$⊢\phi \to G\in F$$
Assertion	lcfl1	$$⊢\phi \to \left(G\in C\leftrightarrow \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(G\right)\right)\right)=L\left(G\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		lcfl1.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\}$$
2		lcfl1.g	$$⊢\phi \to G\in F$$
3	1	lcfl1lem	$$⊢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)\right)$$
4	2	biantrurd	$$⊢\phi \to \left(\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(G\right)\right)\right)=L\left(G\right)\leftrightarrow \left(G\in F\wedge \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(G\right)\right)\right)=L\left(G\right)\right)\right)$$
5	3 4	bitr4id	$$⊢\phi \to \left(G\in C\leftrightarrow \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(G\right)\right)\right)=L\left(G\right)\right)$$