Metamath Proof Explorer

Theorem lvolex3N

Description: There is an atom outside of a lattice plane i.e. a 3-dimensional lattice volume exists. (Contributed by NM, 28-Jul-2012) (New usage is discouraged.)

Ref Expression
Hypotheses lvolex3.l 
|- .<_ = ( le ` K )
lvolex3.a 
|- A = ( Atoms ` K )
lvolex3.p 
|- P = ( LPlanes ` K )
Assertion lvolex3N 
|- ( ( K e. HL /\ X e. P ) -> E. q e. A -. q .<_ X )

Proof

Step Hyp Ref Expression
1 lvolex3.l 
 |-  .<_ = ( le ` K )
2 lvolex3.a 
 |-  A = ( Atoms ` K )
3 lvolex3.p 
 |-  P = ( LPlanes ` K )
4 eqid 
 |-  ( Base ` K ) = ( Base ` K )
5 eqid 
 |-  ( join ` K ) = ( join ` K )
6 4 1 5 2 3 islpln2 
 |-  ( K e. HL -> ( X e. P <-> ( X e. ( Base ` K ) /\ E. r e. A E. s e. A E. t e. A ( r =/= s /\ -. t .<_ ( r ( join ` K ) s ) /\ X = ( ( r ( join ` K ) s ) ( join ` K ) t ) ) ) ) )
7 simp1l 
 |-  ( ( ( K e. HL /\ ( r e. A /\ s e. A ) ) /\ t e. A /\ ( r =/= s /\ -. t .<_ ( r ( join ` K ) s ) /\ X = ( ( r ( join ` K ) s ) ( join ` K ) t ) ) ) -> K e. HL )
8 simp1rl 
 |-  ( ( ( K e. HL /\ ( r e. A /\ s e. A ) ) /\ t e. A /\ ( r =/= s /\ -. t .<_ ( r ( join ` K ) s ) /\ X = ( ( r ( join ` K ) s ) ( join ` K ) t ) ) ) -> r e. A )
9 simp1rr 
 |-  ( ( ( K e. HL /\ ( r e. A /\ s e. A ) ) /\ t e. A /\ ( r =/= s /\ -. t .<_ ( r ( join ` K ) s ) /\ X = ( ( r ( join ` K ) s ) ( join ` K ) t ) ) ) -> s e. A )
10 simp2 
 |-  ( ( ( K e. HL /\ ( r e. A /\ s e. A ) ) /\ t e. A /\ ( r =/= s /\ -. t .<_ ( r ( join ` K ) s ) /\ X = ( ( r ( join ` K ) s ) ( join ` K ) t ) ) ) -> t e. A )
11 5 1 2 3dim3 
 |-  ( ( K e. HL /\ ( r e. A /\ s e. A /\ t e. A ) ) -> E. q e. A -. q .<_ ( ( r ( join ` K ) s ) ( join ` K ) t ) )
12 7 8 9 10 11 syl13anc 
 |-  ( ( ( K e. HL /\ ( r e. A /\ s e. A ) ) /\ t e. A /\ ( r =/= s /\ -. t .<_ ( r ( join ` K ) s ) /\ X = ( ( r ( join ` K ) s ) ( join ` K ) t ) ) ) -> E. q e. A -. q .<_ ( ( r ( join ` K ) s ) ( join ` K ) t ) )
13 simp33 
 |-  ( ( ( K e. HL /\ ( r e. A /\ s e. A ) ) /\ t e. A /\ ( r =/= s /\ -. t .<_ ( r ( join ` K ) s ) /\ X = ( ( r ( join ` K ) s ) ( join ` K ) t ) ) ) -> X = ( ( r ( join ` K ) s ) ( join ` K ) t ) )
14 breq2 
 |-  ( X = ( ( r ( join ` K ) s ) ( join ` K ) t ) -> ( q .<_ X <-> q .<_ ( ( r ( join ` K ) s ) ( join ` K ) t ) ) )
15 14 notbid 
 |-  ( X = ( ( r ( join ` K ) s ) ( join ` K ) t ) -> ( -. q .<_ X <-> -. q .<_ ( ( r ( join ` K ) s ) ( join ` K ) t ) ) )
16 15 rexbidv 
 |-  ( X = ( ( r ( join ` K ) s ) ( join ` K ) t ) -> ( E. q e. A -. q .<_ X <-> E. q e. A -. q .<_ ( ( r ( join ` K ) s ) ( join ` K ) t ) ) )
17 13 16 syl 
 |-  ( ( ( K e. HL /\ ( r e. A /\ s e. A ) ) /\ t e. A /\ ( r =/= s /\ -. t .<_ ( r ( join ` K ) s ) /\ X = ( ( r ( join ` K ) s ) ( join ` K ) t ) ) ) -> ( E. q e. A -. q .<_ X <-> E. q e. A -. q .<_ ( ( r ( join ` K ) s ) ( join ` K ) t ) ) )
18 12 17 mpbird 
 |-  ( ( ( K e. HL /\ ( r e. A /\ s e. A ) ) /\ t e. A /\ ( r =/= s /\ -. t .<_ ( r ( join ` K ) s ) /\ X = ( ( r ( join ` K ) s ) ( join ` K ) t ) ) ) -> E. q e. A -. q .<_ X )
19 18 rexlimdv3a 
 |-  ( ( K e. HL /\ ( r e. A /\ s e. A ) ) -> ( E. t e. A ( r =/= s /\ -. t .<_ ( r ( join ` K ) s ) /\ X = ( ( r ( join ` K ) s ) ( join ` K ) t ) ) -> E. q e. A -. q .<_ X ) )
20 19 rexlimdvva 
 |-  ( K e. HL -> ( E. r e. A E. s e. A E. t e. A ( r =/= s /\ -. t .<_ ( r ( join ` K ) s ) /\ X = ( ( r ( join ` K ) s ) ( join ` K ) t ) ) -> E. q e. A -. q .<_ X ) )
21 20 adantld 
 |-  ( K e. HL -> ( ( X e. ( Base ` K ) /\ E. r e. A E. s e. A E. t e. A ( r =/= s /\ -. t .<_ ( r ( join ` K ) s ) /\ X = ( ( r ( join ` K ) s ) ( join ` K ) t ) ) ) -> E. q e. A -. q .<_ X ) )
22 6 21 sylbid 
 |-  ( K e. HL -> ( X e. P -> E. q e. A -. q .<_ X ) )
23 22 imp 
 |-  ( ( K e. HL /\ X e. P ) -> E. q e. A -. q .<_ X )