Metamath Proof Explorer

Theorem lcfl2

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

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

Proof

Step Hyp Ref Expression
1 lcfl2.h ⊢H=LHyp⁡K
2 lcfl2.o ⊢⊥˙=ocH⁡K⁡W
3 lcfl2.u ⊢U=DVecH⁡K⁡W
4 lcfl2.v ⊢V=BaseU
5 lcfl2.f ⊢F=LFnl⁡U
6 lcfl2.l ⊢L=LKer⁡U
7 lcfl2.c ⊢C=f∈F|⊥˙⁡⊥˙⁡L⁡f=L⁡f
8 lcfl2.k ⊢φ→K∈HL∧W∈H
9 lcfl2.g ⊢φ→G∈F
10 7 9 lcfl1 ⊢φ→G∈C↔⊥˙⁡⊥˙⁡L⁡G=L⁡G
11 1 2 3 4 5 6 8 9 dochkrshp4 ⊢φ→⊥˙⁡⊥˙⁡L⁡G=L⁡G↔⊥˙⁡⊥˙⁡L⁡G≠V∨L⁡G=V
12 10 11 bitrd ⊢φ→G∈C↔⊥˙⁡⊥˙⁡L⁡G≠V∨L⁡G=V