Metamath Proof Explorer

Theorem lplnnlelln

Description: A lattice plane is not less than or equal to a lattice line. (Contributed by NM, 14-Jul-2012)

Ref Expression
Hypotheses lplnnlelln.l 
|- .<_ = ( le ` K )
lplnnlelln.n 
|- N = ( LLines ` K )
lplnnlelln.p 
|- P = ( LPlanes ` K )
Assertion lplnnlelln 
|- ( ( K e. HL /\ X e. P /\ Y e. N ) -> -. X .<_ Y )

Proof

Step Hyp Ref Expression
1 lplnnlelln.l 
 |-  .<_ = ( le ` K )
2 lplnnlelln.n 
 |-  N = ( LLines ` K )
3 lplnnlelln.p 
 |-  P = ( LPlanes ` K )
4 simp3 
 |-  ( ( K e. HL /\ X e. P /\ Y e. N ) -> Y e. N )
5 eqid 
 |-  ( Base ` K ) = ( Base ` K )
6 eqid 
 |-  ( join ` K ) = ( join ` K )
7 eqid 
 |-  ( Atoms ` K ) = ( Atoms ` K )
8 5 6 7 2 islln2 
 |-  ( K e. HL -> ( Y e. N <-> ( Y e. ( Base ` K ) /\ E. q e. ( Atoms ` K ) E. r e. ( Atoms ` K ) ( q =/= r /\ Y = ( q ( join ` K ) r ) ) ) ) )
9 8 3ad2ant1 
 |-  ( ( K e. HL /\ X e. P /\ Y e. N ) -> ( Y e. N <-> ( Y e. ( Base ` K ) /\ E. q e. ( Atoms ` K ) E. r e. ( Atoms ` K ) ( q =/= r /\ Y = ( q ( join ` K ) r ) ) ) ) )
10 4 9 mpbid 
 |-  ( ( K e. HL /\ X e. P /\ Y e. N ) -> ( Y e. ( Base ` K ) /\ E. q e. ( Atoms ` K ) E. r e. ( Atoms ` K ) ( q =/= r /\ Y = ( q ( join ` K ) r ) ) ) )
11 simp11 
 |-  ( ( ( K e. HL /\ X e. P /\ Y e. N ) /\ ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( q =/= r /\ Y = ( q ( join ` K ) r ) ) ) -> K e. HL )
12 simp12 
 |-  ( ( ( K e. HL /\ X e. P /\ Y e. N ) /\ ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( q =/= r /\ Y = ( q ( join ` K ) r ) ) ) -> X e. P )
13 simp2l 
 |-  ( ( ( K e. HL /\ X e. P /\ Y e. N ) /\ ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( q =/= r /\ Y = ( q ( join ` K ) r ) ) ) -> q e. ( Atoms ` K ) )
14 simp2r 
 |-  ( ( ( K e. HL /\ X e. P /\ Y e. N ) /\ ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( q =/= r /\ Y = ( q ( join ` K ) r ) ) ) -> r e. ( Atoms ` K ) )
15 1 6 7 3 lplnnle2at 
 |-  ( ( K e. HL /\ ( X e. P /\ q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) ) -> -. X .<_ ( q ( join ` K ) r ) )
16 11 12 13 14 15 syl13anc 
 |-  ( ( ( K e. HL /\ X e. P /\ Y e. N ) /\ ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( q =/= r /\ Y = ( q ( join ` K ) r ) ) ) -> -. X .<_ ( q ( join ` K ) r ) )
17 simp3r 
 |-  ( ( ( K e. HL /\ X e. P /\ Y e. N ) /\ ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( q =/= r /\ Y = ( q ( join ` K ) r ) ) ) -> Y = ( q ( join ` K ) r ) )
18 17 breq2d 
 |-  ( ( ( K e. HL /\ X e. P /\ Y e. N ) /\ ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( q =/= r /\ Y = ( q ( join ` K ) r ) ) ) -> ( X .<_ Y <-> X .<_ ( q ( join ` K ) r ) ) )
19 16 18 mtbird 
 |-  ( ( ( K e. HL /\ X e. P /\ Y e. N ) /\ ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( q =/= r /\ Y = ( q ( join ` K ) r ) ) ) -> -. X .<_ Y )
20 19 3exp 
 |-  ( ( K e. HL /\ X e. P /\ Y e. N ) -> ( ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) -> ( ( q =/= r /\ Y = ( q ( join ` K ) r ) ) -> -. X .<_ Y ) ) )
21 20 rexlimdvv 
 |-  ( ( K e. HL /\ X e. P /\ Y e. N ) -> ( E. q e. ( Atoms ` K ) E. r e. ( Atoms ` K ) ( q =/= r /\ Y = ( q ( join ` K ) r ) ) -> -. X .<_ Y ) )
22 21 adantld 
 |-  ( ( K e. HL /\ X e. P /\ Y e. N ) -> ( ( Y e. ( Base ` K ) /\ E. q e. ( Atoms ` K ) E. r e. ( Atoms ` K ) ( q =/= r /\ Y = ( q ( join ` K ) r ) ) ) -> -. X .<_ Y ) )
23 10 22 mpd 
 |-  ( ( K e. HL /\ X e. P /\ Y e. N ) -> -. X .<_ Y )