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 ) ) |
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 ) ) |