Metamath Proof Explorer

Theorem dochkrshp2

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

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

Proof

Step Hyp Ref Expression
1 dochkrshp2.h ⊢ H = LHyp ⁡ K
2 dochkrshp2.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
3 dochkrshp2.u ⊢ U = DVecH ⁡ K ⁡ W
4 dochkrshp2.v ⊢ V = Base U
5 dochkrshp2.y ⊢ Y = LSHyp ⁡ U
6 dochkrshp2.f ⊢ F = LFnl ⁡ U
7 dochkrshp2.l ⊢ L = LKer ⁡ U
8 dochkrshp2.k ⊢ φ → K ∈ HL ∧ W ∈ H
9 dochkrshp2.g ⊢ φ → G ∈ F
10 1 2 3 4 5 6 7 8 9 dochkrshp ⊢ φ → ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G ≠ V ↔ ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G ∈ Y
11 1 2 3 6 5 7 8 9 dochlkr ⊢ φ → ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G ∈ Y ↔ ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G = L ⁡ G ∧ L ⁡ G ∈ Y
12 10 11 bitrd ⊢ φ → ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G ≠ V ↔ ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G = L ⁡ G ∧ L ⁡ G ∈ Y