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 = Base U
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 = Base U
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