Metamath Proof Explorer


Theorem 4atexlemwb

Description: Lemma for 4atexlem7 . (Contributed by NM, 23-Nov-2012)

Ref Expression
Hypotheses 4thatlem.ph
|- ( ph <-> ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( S e. A /\ ( R e. A /\ -. R .<_ W /\ ( P .\/ R ) = ( Q .\/ R ) ) /\ ( T e. A /\ ( U .\/ T ) = ( V .\/ T ) ) ) /\ ( P =/= Q /\ -. S .<_ ( P .\/ Q ) ) ) )
4thatlemmwb.h
|- H = ( LHyp ` K )
Assertion 4atexlemwb
|- ( ph -> W e. ( Base ` K ) )

Proof

Step Hyp Ref Expression
1 4thatlem.ph
 |-  ( ph <-> ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( S e. A /\ ( R e. A /\ -. R .<_ W /\ ( P .\/ R ) = ( Q .\/ R ) ) /\ ( T e. A /\ ( U .\/ T ) = ( V .\/ T ) ) ) /\ ( P =/= Q /\ -. S .<_ ( P .\/ Q ) ) ) )
2 4thatlemmwb.h
 |-  H = ( LHyp ` K )
3 1 4atexlemw
 |-  ( ph -> W e. H )
4 eqid
 |-  ( Base ` K ) = ( Base ` K )
5 4 2 lhpbase
 |-  ( W e. H -> W e. ( Base ` K ) )
6 3 5 syl
 |-  ( ph -> W e. ( Base ` K ) )