Metamath Proof Explorer

Theorem lcfl8a

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

Ref Expression
Hypotheses lcfl8a.h ⊢H=LHyp⁡K
lcfl8a.o ⊢⊥˙=ocH⁡K⁡W
lcfl8a.u ⊢U=DVecH⁡K⁡W
lcfl8a.v ⊢V=BaseU
lcfl8a.f ⊢F=LFnl⁡U
lcfl8a.l ⊢L=LKer⁡U
lcfl8a.k ⊢φ→K∈HL∧W∈H
lcfl8a.g ⊢φ→G∈F
Assertion lcfl8a ⊢φ→⊥˙⁡⊥˙⁡L⁡G=L⁡G↔∃x∈VL⁡G=⊥˙⁡x

Proof

Step Hyp Ref Expression
1 lcfl8a.h ⊢H=LHyp⁡K
2 lcfl8a.o ⊢⊥˙=ocH⁡K⁡W
3 lcfl8a.u ⊢U=DVecH⁡K⁡W
4 lcfl8a.v ⊢V=BaseU
5 lcfl8a.f ⊢F=LFnl⁡U
6 lcfl8a.l ⊢L=LKer⁡U
7 lcfl8a.k ⊢φ→K∈HL∧W∈H
8 lcfl8a.g ⊢φ→G∈F
9 eqid ⊢f∈F|⊥˙⁡⊥˙⁡L⁡f=L⁡f=f∈F|⊥˙⁡⊥˙⁡L⁡f=L⁡f
10 9 8 lcfl1 ⊢φ→G∈f∈F|⊥˙⁡⊥˙⁡L⁡f=L⁡f↔⊥˙⁡⊥˙⁡L⁡G=L⁡G
11 1 2 3 4 5 6 9 7 8 lcfl8 ⊢φ→G∈f∈F|⊥˙⁡⊥˙⁡L⁡f=L⁡f↔∃x∈VL⁡G=⊥˙⁡x
12 10 11 bitr3d ⊢φ→⊥˙⁡⊥˙⁡L⁡G=L⁡G↔∃x∈VL⁡G=⊥˙⁡x