Metamath Proof Explorer

Theorem hlrelat5N

Description: An atomistic lattice with 0 is relatively atomic, using the definition in Remark 2 of Kalmbach p. 149. (Contributed by NM, 21-Oct-2011) (New usage is discouraged.)

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 hlrelat5N 
|- ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) -> E. p e. A ( X .< ( X .\/ p ) /\ p .<_ Y ) )

Proof

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 hllat 
 |-  ( K e. HL -> K e. Lat )
9 id 
 |-  ( X e. B -> X e. B )
10 1 5 atbase 
 |-  ( p e. A -> p e. B )
11 ovexd 
 |-  ( p e. B -> ( X .\/ p ) e. _V )
12 2 3 pltval 
 |-  ( ( K e. Lat /\ X e. B /\ ( X .\/ p ) e. _V ) -> ( X .< ( X .\/ p ) <-> ( X .<_ ( X .\/ p ) /\ X =/= ( X .\/ p ) ) ) )
13 11 12 syl3an3 
 |-  ( ( K e. Lat /\ X e. B /\ p e. B ) -> ( X .< ( X .\/ p ) <-> ( X .<_ ( X .\/ p ) /\ X =/= ( X .\/ p ) ) ) )
14 1 2 4 latlej1 
 |-  ( ( K e. Lat /\ X e. B /\ p e. B ) -> X .<_ ( X .\/ p ) )
15 14 biantrurd 
 |-  ( ( K e. Lat /\ X e. B /\ p e. B ) -> ( X =/= ( X .\/ p ) <-> ( X .<_ ( X .\/ p ) /\ X =/= ( X .\/ p ) ) ) )
16 13 15 bitr4d 
 |-  ( ( K e. Lat /\ X e. B /\ p e. B ) -> ( X .< ( X .\/ p ) <-> X =/= ( X .\/ p ) ) )
17 1 2 4 latleeqj1 
 |-  ( ( K e. Lat /\ p e. B /\ X e. B ) -> ( p .<_ X <-> ( p .\/ X ) = X ) )
18 17 3com23 
 |-  ( ( K e. Lat /\ X e. B /\ p e. B ) -> ( p .<_ X <-> ( p .\/ X ) = X ) )
19 1 4 latjcom 
 |-  ( ( K e. Lat /\ X e. B /\ p e. B ) -> ( X .\/ p ) = ( p .\/ X ) )
20 19 eqeq1d 
 |-  ( ( K e. Lat /\ X e. B /\ p e. B ) -> ( ( X .\/ p ) = X <-> ( p .\/ X ) = X ) )
21 18 20 bitr4d 
 |-  ( ( K e. Lat /\ X e. B /\ p e. B ) -> ( p .<_ X <-> ( X .\/ p ) = X ) )
22 21 notbid 
 |-  ( ( K e. Lat /\ X e. B /\ p e. B ) -> ( -. p .<_ X <-> -. ( X .\/ p ) = X ) )
23 nesym 
 |-  ( X =/= ( X .\/ p ) <-> -. ( X .\/ p ) = X )
24 22 23 bitr4di 
 |-  ( ( K e. Lat /\ X e. B /\ p e. B ) -> ( -. p .<_ X <-> X =/= ( X .\/ p ) ) )
25 16 24 bitr4d 
 |-  ( ( K e. Lat /\ X e. B /\ p e. B ) -> ( X .< ( X .\/ p ) <-> -. p .<_ X ) )
26 8 9 10 25 syl3an 
 |-  ( ( K e. HL /\ X e. B /\ p e. A ) -> ( X .< ( X .\/ p ) <-> -. p .<_ X ) )
27 26 3expa 
 |-  ( ( ( K e. HL /\ X e. B ) /\ p e. A ) -> ( X .< ( X .\/ p ) <-> -. p .<_ X ) )
28 27 anbi1d 
 |-  ( ( ( K e. HL /\ X e. B ) /\ p e. A ) -> ( ( X .< ( X .\/ p ) /\ p .<_ Y ) <-> ( -. p .<_ X /\ p .<_ Y ) ) )
29 28 rexbidva 
 |-  ( ( K e. HL /\ X e. B ) -> ( E. p e. A ( X .< ( X .\/ p ) /\ p .<_ Y ) <-> E. p e. A ( -. p .<_ X /\ p .<_ Y ) ) )
30 29 3adant3 
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( E. p e. A ( X .< ( X .\/ p ) /\ p .<_ Y ) <-> E. p e. A ( -. p .<_ X /\ p .<_ Y ) ) )
31 30 adantr 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) -> ( E. p e. A ( X .< ( X .\/ p ) /\ p .<_ Y ) <-> E. p e. A ( -. p .<_ X /\ p .<_ Y ) ) )
32 7 31 mpbird 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) -> E. p e. A ( X .< ( X .\/ p ) /\ p .<_ Y ) )