Metamath Proof Explorer


Theorem dochsnkrlem2

Description: Lemma for dochsnkr . (Contributed by NM, 1-Jan-2015)

Ref Expression
Hypotheses dochsnkr.h
|- H = ( LHyp ` K )
dochsnkr.o
|- ._|_ = ( ( ocH ` K ) ` W )
dochsnkr.u
|- U = ( ( DVecH ` K ) ` W )
dochsnkr.v
|- V = ( Base ` U )
dochsnkr.z
|- .0. = ( 0g ` U )
dochsnkr.f
|- F = ( LFnl ` U )
dochsnkr.l
|- L = ( LKer ` U )
dochsnkr.k
|- ( ph -> ( K e. HL /\ W e. H ) )
dochsnkr.g
|- ( ph -> G e. F )
dochsnkr.x
|- ( ph -> X e. ( ( ._|_ ` ( L ` G ) ) \ { .0. } ) )
dochsnkr.a
|- A = ( LSAtoms ` U )
Assertion dochsnkrlem2
|- ( ph -> ( ._|_ ` ( L ` G ) ) e. A )

Proof

Step Hyp Ref Expression
1 dochsnkr.h
 |-  H = ( LHyp ` K )
2 dochsnkr.o
 |-  ._|_ = ( ( ocH ` K ) ` W )
3 dochsnkr.u
 |-  U = ( ( DVecH ` K ) ` W )
4 dochsnkr.v
 |-  V = ( Base ` U )
5 dochsnkr.z
 |-  .0. = ( 0g ` U )
6 dochsnkr.f
 |-  F = ( LFnl ` U )
7 dochsnkr.l
 |-  L = ( LKer ` U )
8 dochsnkr.k
 |-  ( ph -> ( K e. HL /\ W e. H ) )
9 dochsnkr.g
 |-  ( ph -> G e. F )
10 dochsnkr.x
 |-  ( ph -> X e. ( ( ._|_ ` ( L ` G ) ) \ { .0. } ) )
11 dochsnkr.a
 |-  A = ( LSAtoms ` U )
12 1 2 3 4 5 6 7 8 9 10 dochsnkrlem1
 |-  ( ph -> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) =/= V )
13 1 2 3 4 11 6 7 8 9 dochkrsat2
 |-  ( ph -> ( ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) =/= V <-> ( ._|_ ` ( L ` G ) ) e. A ) )
14 12 13 mpbid
 |-  ( ph -> ( ._|_ ` ( L ` G ) ) e. A )