Metamath Proof Explorer

Theorem lcfl3

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

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

Proof

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