Metamath Proof Explorer

Theorem lcfl5

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

Ref Expression
Hypotheses lcfl5.h ⊢ H = LHyp ⁡ K
lcfl5.i ⊢ I = DIsoH ⁡ K ⁡ W
lcfl5.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
lcfl5.u ⊢ U = DVecH ⁡ K ⁡ W
lcfl5.f ⊢ F = LFnl ⁡ U
lcfl5.l ⊢ L = LKer ⁡ U
lcfl5.c ⊢ C = f ∈ F | ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ f = L ⁡ f
lcfl5.k ⊢ φ → K ∈ HL ∧ W ∈ H
lcfl5.g ⊢ φ → G ∈ F
Assertion lcfl5 ⊢ φ → G ∈ C ↔ L ⁡ G ∈ ran ⁡ I

Proof

Step Hyp Ref Expression
1 lcfl5.h ⊢ H = LHyp ⁡ K
2 lcfl5.i ⊢ I = DIsoH ⁡ K ⁡ W
3 lcfl5.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
4 lcfl5.u ⊢ U = DVecH ⁡ K ⁡ W
5 lcfl5.f ⊢ F = LFnl ⁡ U
6 lcfl5.l ⊢ L = LKer ⁡ U
7 lcfl5.c ⊢ C = f ∈ F | ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ f = L ⁡ f
8 lcfl5.k ⊢ φ → K ∈ HL ∧ W ∈ H
9 lcfl5.g ⊢ φ → G ∈ F
10 7 9 lcfl1 ⊢ φ → G ∈ C ↔ ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G = L ⁡ G
11 eqid ⊢ Base U = Base U
12 1 4 8 dvhlmod ⊢ φ → U ∈ LMod
13 11 5 6 12 9 lkrssv ⊢ φ → L ⁡ G ⊆ Base U
14 1 2 4 11 3 8 13 dochoccl ⊢ φ → L ⁡ G ∈ ran ⁡ I ↔ ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G = L ⁡ G
15 10 14 bitr4d ⊢ φ → G ∈ C ↔ L ⁡ G ∈ ran ⁡ I