Theorem lcfl1lem

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

	Ref	Expression
Hypothesis	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\}$$
Assertion	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)$$

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		fveq2	$$⊢f=G\to L\left(f\right)=L\left(G\right)$$
3	2	fveq2d	$$⊢f=G\to \underset{\dot{}}{\perp }\left(L\left(f\right)\right)=\underset{\dot{}}{\perp }\left(L\left(G\right)\right)$$
4	3	fveq2d	$$⊢f=G\to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(f\right)\right)\right)=\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(G\right)\right)\right)$$
5	4 2	eqeq12d	$$⊢f=G\to \left(\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(f\right)\right)\right)=L\left(f\right)\leftrightarrow \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(G\right)\right)\right)=L\left(G\right)\right)$$
6	5 1	elrab2	$$⊢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)$$