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