Metamath Proof Explorer

Theorem dochkrshp3

Description: Properties of the closure of the kernel of a functional. (Contributed by NM, 1-Jan-2015)

Ref Expression
Hypotheses dochkrshp3.h ⊢ H = LHyp ⁡ K
dochkrshp3.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
dochkrshp3.u ⊢ U = DVecH ⁡ K ⁡ W
dochkrshp3.v ⊢ V = Base U
dochkrshp3.f ⊢ F = LFnl ⁡ U
dochkrshp3.l ⊢ L = LKer ⁡ U
dochkrshp3.k ⊢ φ → K ∈ HL ∧ W ∈ H
dochkrshp3.g ⊢ φ → G ∈ F
Assertion dochkrshp3 ⊢ φ → ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G ≠ V ↔ ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G = L ⁡ G ∧ L ⁡ G ≠ V

Proof

Step Hyp Ref Expression
1 dochkrshp3.h ⊢ H = LHyp ⁡ K
2 dochkrshp3.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
3 dochkrshp3.u ⊢ U = DVecH ⁡ K ⁡ W
4 dochkrshp3.v ⊢ V = Base U
5 dochkrshp3.f ⊢ F = LFnl ⁡ U
6 dochkrshp3.l ⊢ L = LKer ⁡ U
7 dochkrshp3.k ⊢ φ → K ∈ HL ∧ W ∈ H
8 dochkrshp3.g ⊢ φ → G ∈ F
9 eqid ⊢ LSHyp ⁡ U = LSHyp ⁡ U
10 1 2 3 4 9 5 6 7 8 dochkrshp2 ⊢ φ → ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G ≠ V ↔ ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G = L ⁡ G ∧ L ⁡ G ∈ LSHyp ⁡ U
11 1 3 7 dvhlvec ⊢ φ → U ∈ LVec
12 4 9 5 6 11 8 lkrshp4 ⊢ φ → L ⁡ G ≠ V ↔ L ⁡ G ∈ LSHyp ⁡ U
13 12 anbi2d ⊢ φ → ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G = L ⁡ G ∧ L ⁡ G ≠ V ↔ ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G = L ⁡ G ∧ L ⁡ G ∈ LSHyp ⁡ U
14 10 13 bitr4d ⊢ φ → ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G ≠ V ↔ ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G = L ⁡ G ∧ L ⁡ G ≠ V