This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Description: A Hilbert lattice is relatively atomic. Remark 2 of Kalmbach p. 149. ( chrelati analog.) (Contributed by NM, 4-Feb-2012)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | hlrelat5.b | |- B = ( Base ` K ) |
|
| hlrelat5.l | |- .<_ = ( le ` K ) |
||
| hlrelat5.s | |- .< = ( lt ` K ) |
||
| hlrelat5.j | |- .\/ = ( join ` K ) |
||
| hlrelat5.a | |- A = ( Atoms ` K ) |
||
| Assertion | hlrelat | |- ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) -> E. p e. A ( X .< ( X .\/ p ) /\ ( X .\/ p ) .<_ Y ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | hlrelat5.b | |- B = ( Base ` K ) |
|
| 2 | hlrelat5.l | |- .<_ = ( le ` K ) |
|
| 3 | hlrelat5.s | |- .< = ( lt ` K ) |
|
| 4 | hlrelat5.j | |- .\/ = ( join ` K ) |
|
| 5 | hlrelat5.a | |- A = ( Atoms ` K ) |
|
| 6 | 1 2 3 5 | hlrelat1 | |- ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( X .< Y -> E. p e. A ( -. p .<_ X /\ p .<_ Y ) ) ) |
| 7 | 6 | imp | |- ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) -> E. p e. A ( -. p .<_ X /\ p .<_ Y ) ) |
| 8 | simpll1 | |- ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) /\ p e. A ) -> K e. HL ) |
|
| 9 | 8 | hllatd | |- ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) /\ p e. A ) -> K e. Lat ) |
| 10 | simpll2 | |- ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) /\ p e. A ) -> X e. B ) |
|
| 11 | 1 5 | atbase | |- ( p e. A -> p e. B ) |
| 12 | 11 | adantl | |- ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) /\ p e. A ) -> p e. B ) |
| 13 | 1 2 3 4 | latnle | |- ( ( K e. Lat /\ X e. B /\ p e. B ) -> ( -. p .<_ X <-> X .< ( X .\/ p ) ) ) |
| 14 | 9 10 12 13 | syl3anc | |- ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) /\ p e. A ) -> ( -. p .<_ X <-> X .< ( X .\/ p ) ) ) |
| 15 | 2 3 | pltle | |- ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( X .< Y -> X .<_ Y ) ) |
| 16 | 15 | imp | |- ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) -> X .<_ Y ) |
| 17 | 16 | adantr | |- ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) /\ p e. A ) -> X .<_ Y ) |
| 18 | 17 | biantrurd | |- ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) /\ p e. A ) -> ( p .<_ Y <-> ( X .<_ Y /\ p .<_ Y ) ) ) |
| 19 | simpll3 | |- ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) /\ p e. A ) -> Y e. B ) |
|
| 20 | 1 2 4 | latjle12 | |- ( ( K e. Lat /\ ( X e. B /\ p e. B /\ Y e. B ) ) -> ( ( X .<_ Y /\ p .<_ Y ) <-> ( X .\/ p ) .<_ Y ) ) |
| 21 | 9 10 12 19 20 | syl13anc | |- ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) /\ p e. A ) -> ( ( X .<_ Y /\ p .<_ Y ) <-> ( X .\/ p ) .<_ Y ) ) |
| 22 | 18 21 | bitrd | |- ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) /\ p e. A ) -> ( p .<_ Y <-> ( X .\/ p ) .<_ Y ) ) |
| 23 | 14 22 | anbi12d | |- ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) /\ p e. A ) -> ( ( -. p .<_ X /\ p .<_ Y ) <-> ( X .< ( X .\/ p ) /\ ( X .\/ p ) .<_ Y ) ) ) |
| 24 | 23 | rexbidva | |- ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) -> ( E. p e. A ( -. p .<_ X /\ p .<_ Y ) <-> E. p e. A ( X .< ( X .\/ p ) /\ ( X .\/ p ) .<_ Y ) ) ) |
| 25 | 7 24 | mpbid | |- ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) -> E. p e. A ( X .< ( X .\/ p ) /\ ( X .\/ p ) .<_ Y ) ) |