Metamath Proof Explorer

Theorem lcfl4N

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

Ref Expression
Hypotheses lcfl4.h ⊢H=LHyp⁡K
lcfl4.o ⊢⊥˙=ocH⁡K⁡W
lcfl4.u ⊢U=DVecH⁡K⁡W
lcfl4.v ⊢V=BaseU
lcfl4.y ⊢Y=LSHyp⁡U
lcfl4.f ⊢F=LFnl⁡U
lcfl4.l ⊢L=LKer⁡U
lcfl4.c ⊢C=f∈F|⊥˙⁡⊥˙⁡L⁡f=L⁡f
lcfl4.k ⊢φ→K∈HL∧W∈H
lcfl4.g ⊢φ→G∈F
Assertion lcfl4N ⊢φ→G∈C↔⊥˙⁡⊥˙⁡L⁡G∈Y∨L⁡G=V

Proof

Step Hyp Ref Expression
1 lcfl4.h ⊢H=LHyp⁡K
2 lcfl4.o ⊢⊥˙=ocH⁡K⁡W
3 lcfl4.u ⊢U=DVecH⁡K⁡W
4 lcfl4.v ⊢V=BaseU
5 lcfl4.y ⊢Y=LSHyp⁡U
6 lcfl4.f ⊢F=LFnl⁡U
7 lcfl4.l ⊢L=LKer⁡U
8 lcfl4.c ⊢C=f∈F|⊥˙⁡⊥˙⁡L⁡f=L⁡f
9 lcfl4.k ⊢φ→K∈HL∧W∈H
10 lcfl4.g ⊢φ→G∈F
11 eqid ⊢LSAtoms⁡U=LSAtoms⁡U
12 1 2 3 4 11 6 7 8 9 10 lcfl3 ⊢φ→G∈C↔⊥˙⁡L⁡G∈LSAtoms⁡U∨L⁡G=V
13 eqid ⊢LSubSp⁡U=LSubSp⁡U
14 1 3 9 dvhlmod ⊢φ→U∈LMod
15 4 6 7 14 10 lkrssv ⊢φ→L⁡G⊆V
16 1 3 4 13 2 dochlss ⊢K∈HL∧W∈H∧L⁡G⊆V→⊥˙⁡L⁡G∈LSubSp⁡U
17 9 15 16 syl2anc ⊢φ→⊥˙⁡L⁡G∈LSubSp⁡U
18 1 2 3 13 11 5 9 17 dochsatshpb ⊢φ→⊥˙⁡L⁡G∈LSAtoms⁡U↔⊥˙⁡⊥˙⁡L⁡G∈Y
19 18 orbi1d ⊢φ→⊥˙⁡L⁡G∈LSAtoms⁡U∨L⁡G=V↔⊥˙⁡⊥˙⁡L⁡G∈Y∨L⁡G=V
20 12 19 bitrd ⊢φ→G∈C↔⊥˙⁡⊥˙⁡L⁡G∈Y∨L⁡G=V