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