Theorem lcfls1N

Description: Property of a functional with a closed kernel. (Contributed by NM, 27-Jan-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	lcfls1.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\}$$
	lcfls1.g	$$⊢\phi \to G\in F$$
Assertion	lcfls1N	$$⊢\phi \to \left(G\in C\leftrightarrow \left(\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)\right)$$

Proof

Step	Hyp	Ref	Expression
1		lcfls1.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\}$$
2		lcfls1.g	$$⊢\phi \to G\in F$$
3	1	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)$$
4		3anass	$$⊢\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)\leftrightarrow \left(G\in F\wedge \left(\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)\right)$$
5	3 4	bitri	$$⊢G\in C\leftrightarrow \left(G\in F\wedge \left(\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)\right)$$
6	2	biantrurd	$$⊢\phi \to \left(\left(\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)\leftrightarrow \left(G\in F\wedge \left(\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)\right)\right)$$
7	5 6	bitr4id	$$⊢\phi \to \left(G\in C\leftrightarrow \left(\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)\right)$$