lcfl5

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

	Ref	Expression
Hypotheses	lcfl5.h	$⊢ H = LHyp (K)$
	lcfl5.i	$⊢ I = DIsoH (K) (W)$
	lcfl5.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
	lcfl5.u	$⊢ U = DVecH (K) (W)$
	lcfl5.f	$⊢ F = LFnl (U)$
	lcfl5.l	$⊢ L = LKer (U)$
	lcfl5.c	$⊢ C = \{f \in F \| \underset{˙}{⊥} (\underset{˙}{⊥} (L (f))) = L (f)\}$
	lcfl5.k	$⊢ φ \to (K \in HL \land W \in H)$
	lcfl5.g	$⊢ φ \to G \in F$
Assertion	lcfl5	$⊢ φ \to (G \in C \leftrightarrow L (G) \in ran I)$

Step	Hyp	Ref	Expression
1		lcfl5.h	$⊢ H = LHyp (K)$
2		lcfl5.i	$⊢ I = DIsoH (K) (W)$
3		lcfl5.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
4		lcfl5.u	$⊢ U = DVecH (K) (W)$
5		lcfl5.f	$⊢ F = LFnl (U)$
6		lcfl5.l	$⊢ L = LKer (U)$
7		lcfl5.c	$⊢ C = \{f \in F \| \underset{˙}{⊥} (\underset{˙}{⊥} (L (f))) = L (f)\}$
8		lcfl5.k	$⊢ φ \to (K \in HL \land W \in H)$
9		lcfl5.g	$⊢ φ \to G \in F$
10	7 9	lcfl1	$⊢ φ \to (G \in C \leftrightarrow \underset{˙}{⊥} (\underset{˙}{⊥} (L (G))) = L (G))$
11		eqid	$⊢ {Base}_{U} = {Base}_{U}$
12	1 4 8	dvhlmod	$⊢ φ \to U \in LMod$
13	11 5 6 12 9	lkrssv	$⊢ φ \to L (G) \subseteq {Base}_{U}$
14	1 2 4 11 3 8 13	dochoccl	$⊢ φ \to (L (G) \in ran I \leftrightarrow \underset{˙}{⊥} (\underset{˙}{⊥} (L (G))) = L (G))$
15	10 14	bitr4d	$⊢ φ \to (G \in C \leftrightarrow L (G) \in ran I)$

Metamath Proof Explorer