This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( ph -> ( K e. HL /\ W e. H ) )
dochkrshp2.g 
|- ( ph -> G e. F )
Assertion dochkrshp2 
|- ( ph -> ( ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) =/= V <-> ( ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) /\ ( L ` G ) e. 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 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
9 dochkrshp2.g 
 |-  ( ph -> G e. F )
10 1 2 3 4 5 6 7 8 9 dochkrshp 
 |-  ( ph -> ( ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) =/= V <-> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) e. Y ) )
11 1 2 3 6 5 7 8 9 dochlkr 
 |-  ( ph -> ( ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) e. Y <-> ( ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) /\ ( L ` G ) e. Y ) ) )
12 10 11 bitrd 
 |-  ( ph -> ( ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) =/= V <-> ( ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) /\ ( L ` G ) e. Y ) ) )