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