This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem hl2at

Description: A Hilbert lattice has at least 2 atoms. (Contributed by NM, 5-Dec-2011)

Ref Expression
Hypothesis hl2atom.a 
|- A = ( Atoms ` K )
Assertion hl2at 
|- ( K e. HL -> E. p e. A E. q e. A p =/= q )

Proof

Step Hyp Ref Expression
1 hl2atom.a 
 |-  A = ( Atoms ` K )
2 eqid 
 |-  ( Base ` K ) = ( Base ` K )
3 eqid 
 |-  ( lt ` K ) = ( lt ` K )
4 eqid 
 |-  ( 0. ` K ) = ( 0. ` K )
5 eqid 
 |-  ( 1. ` K ) = ( 1. ` K )
6 2 3 4 5 hlhgt2 
 |-  ( K e. HL -> E. x e. ( Base ` K ) ( ( 0. ` K ) ( lt ` K ) x /\ x ( lt ` K ) ( 1. ` K ) ) )
7 simpl 
 |-  ( ( K e. HL /\ x e. ( Base ` K ) ) -> K e. HL )
8 hlop 
 |-  ( K e. HL -> K e. OP )
9 8 adantr 
 |-  ( ( K e. HL /\ x e. ( Base ` K ) ) -> K e. OP )
10 2 4 op0cl 
 |-  ( K e. OP -> ( 0. ` K ) e. ( Base ` K ) )
11 9 10 syl 
 |-  ( ( K e. HL /\ x e. ( Base ` K ) ) -> ( 0. ` K ) e. ( Base ` K ) )
12 simpr 
 |-  ( ( K e. HL /\ x e. ( Base ` K ) ) -> x e. ( Base ` K ) )
13 eqid 
 |-  ( le ` K ) = ( le ` K )
14 2 13 3 1 hlrelat1 
 |-  ( ( K e. HL /\ ( 0. ` K ) e. ( Base ` K ) /\ x e. ( Base ` K ) ) -> ( ( 0. ` K ) ( lt ` K ) x -> E. p e. A ( -. p ( le ` K ) ( 0. ` K ) /\ p ( le ` K ) x ) ) )
15 7 11 12 14 syl3anc 
 |-  ( ( K e. HL /\ x e. ( Base ` K ) ) -> ( ( 0. ` K ) ( lt ` K ) x -> E. p e. A ( -. p ( le ` K ) ( 0. ` K ) /\ p ( le ` K ) x ) ) )
16 2 5 op1cl 
 |-  ( K e. OP -> ( 1. ` K ) e. ( Base ` K ) )
17 9 16 syl 
 |-  ( ( K e. HL /\ x e. ( Base ` K ) ) -> ( 1. ` K ) e. ( Base ` K ) )
18 2 13 3 1 hlrelat1 
 |-  ( ( K e. HL /\ x e. ( Base ` K ) /\ ( 1. ` K ) e. ( Base ` K ) ) -> ( x ( lt ` K ) ( 1. ` K ) -> E. q e. A ( -. q ( le ` K ) x /\ q ( le ` K ) ( 1. ` K ) ) ) )
19 17 18 mpd3an3 
 |-  ( ( K e. HL /\ x e. ( Base ` K ) ) -> ( x ( lt ` K ) ( 1. ` K ) -> E. q e. A ( -. q ( le ` K ) x /\ q ( le ` K ) ( 1. ` K ) ) ) )
20 15 19 anim12d 
 |-  ( ( K e. HL /\ x e. ( Base ` K ) ) -> ( ( ( 0. ` K ) ( lt ` K ) x /\ x ( lt ` K ) ( 1. ` K ) ) -> ( E. p e. A ( -. p ( le ` K ) ( 0. ` K ) /\ p ( le ` K ) x ) /\ E. q e. A ( -. q ( le ` K ) x /\ q ( le ` K ) ( 1. ` K ) ) ) ) )
21 reeanv 
 |-  ( E. p e. A E. q e. A ( ( -. p ( le ` K ) ( 0. ` K ) /\ p ( le ` K ) x ) /\ ( -. q ( le ` K ) x /\ q ( le ` K ) ( 1. ` K ) ) ) <-> ( E. p e. A ( -. p ( le ` K ) ( 0. ` K ) /\ p ( le ` K ) x ) /\ E. q e. A ( -. q ( le ` K ) x /\ q ( le ` K ) ( 1. ` K ) ) ) )
22 nbrne2 
 |-  ( ( p ( le ` K ) x /\ -. q ( le ` K ) x ) -> p =/= q )
23 22 ad2ant2lr 
 |-  ( ( ( -. p ( le ` K ) ( 0. ` K ) /\ p ( le ` K ) x ) /\ ( -. q ( le ` K ) x /\ q ( le ` K ) ( 1. ` K ) ) ) -> p =/= q )
24 23 reximi 
 |-  ( E. q e. A ( ( -. p ( le ` K ) ( 0. ` K ) /\ p ( le ` K ) x ) /\ ( -. q ( le ` K ) x /\ q ( le ` K ) ( 1. ` K ) ) ) -> E. q e. A p =/= q )
25 24 reximi 
 |-  ( E. p e. A E. q e. A ( ( -. p ( le ` K ) ( 0. ` K ) /\ p ( le ` K ) x ) /\ ( -. q ( le ` K ) x /\ q ( le ` K ) ( 1. ` K ) ) ) -> E. p e. A E. q e. A p =/= q )
26 21 25 sylbir 
 |-  ( ( E. p e. A ( -. p ( le ` K ) ( 0. ` K ) /\ p ( le ` K ) x ) /\ E. q e. A ( -. q ( le ` K ) x /\ q ( le ` K ) ( 1. ` K ) ) ) -> E. p e. A E. q e. A p =/= q )
27 20 26 syl6 
 |-  ( ( K e. HL /\ x e. ( Base ` K ) ) -> ( ( ( 0. ` K ) ( lt ` K ) x /\ x ( lt ` K ) ( 1. ` K ) ) -> E. p e. A E. q e. A p =/= q ) )
28 27 rexlimdva 
 |-  ( K e. HL -> ( E. x e. ( Base ` K ) ( ( 0. ` K ) ( lt ` K ) x /\ x ( lt ` K ) ( 1. ` K ) ) -> E. p e. A E. q e. A p =/= q ) )
29 6 28 mpd 
 |-  ( K e. HL -> E. p e. A E. q e. A p =/= q )