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 = Base U
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 ∈ V L ⁡ 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 = Base U
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 ∈ V L ⁡ G = ⊥ ˙ ⁡ x
12 10 11 bitr3d ⊢ φ → ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G = L ⁡ G ↔ ∃ x ∈ V L ⁡ G = ⊥ ˙ ⁡ x