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

Metamath Proof Explorer

Theorem lplncmp

Description: If two lattice planes are comparable, they are equal. (Contributed by NM, 24-Jun-2012)

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

Proof

Step Hyp Ref Expression
1 lplncmp.l 
 |-  .<_ = ( le ` K )
2 lplncmp.p 
 |-  P = ( LPlanes ` K )
3 simp2 
 |-  ( ( K e. HL /\ X e. P /\ Y e. P ) -> X e. P )
4 simp1 
 |-  ( ( K e. HL /\ X e. P /\ Y e. P ) -> K e. HL )
5 eqid 
 |-  ( Base ` K ) = ( Base ` K )
6 5 2 lplnbase 
 |-  ( X e. P -> X e. ( Base ` K ) )
7 6 3ad2ant2 
 |-  ( ( K e. HL /\ X e. P /\ Y e. P ) -> X e. ( Base ` K ) )
8 eqid 
 |-  (
9 eqid 
 |-  ( LLines ` K ) = ( LLines ` K )
10 5 8 9 2 islpln4 
 |-  ( ( K e. HL /\ X e. ( Base ` K ) ) -> ( X e. P <-> E. z e. ( LLines ` K ) z (
11 4 7 10 syl2anc 
 |-  ( ( K e. HL /\ X e. P /\ Y e. P ) -> ( X e. P <-> E. z e. ( LLines ` K ) z (
12 3 11 mpbid 
 |-  ( ( K e. HL /\ X e. P /\ Y e. P ) -> E. z e. ( LLines ` K ) z (
13 simpr3 
 |-  ( ( ( K e. HL /\ X e. P /\ Y e. P ) /\ ( z e. ( LLines ` K ) /\ z (  X .<_ Y )
14 hlpos 
 |-  ( K e. HL -> K e. Poset )
15 14 3ad2ant1 
 |-  ( ( K e. HL /\ X e. P /\ Y e. P ) -> K e. Poset )
16 15 adantr 
 |-  ( ( ( K e. HL /\ X e. P /\ Y e. P ) /\ ( z e. ( LLines ` K ) /\ z (  K e. Poset )
17 7 adantr 
 |-  ( ( ( K e. HL /\ X e. P /\ Y e. P ) /\ ( z e. ( LLines ` K ) /\ z (  X e. ( Base ` K ) )
18 simpl3 
 |-  ( ( ( K e. HL /\ X e. P /\ Y e. P ) /\ ( z e. ( LLines ` K ) /\ z (  Y e. P )
19 5 2 lplnbase 
 |-  ( Y e. P -> Y e. ( Base ` K ) )
20 18 19 syl 
 |-  ( ( ( K e. HL /\ X e. P /\ Y e. P ) /\ ( z e. ( LLines ` K ) /\ z (  Y e. ( Base ` K ) )
21 simpr1 
 |-  ( ( ( K e. HL /\ X e. P /\ Y e. P ) /\ ( z e. ( LLines ` K ) /\ z (  z e. ( LLines ` K ) )
22 5 9 llnbase 
 |-  ( z e. ( LLines ` K ) -> z e. ( Base ` K ) )
23 21 22 syl 
 |-  ( ( ( K e. HL /\ X e. P /\ Y e. P ) /\ ( z e. ( LLines ` K ) /\ z (  z e. ( Base ` K ) )
24 simpr2 
 |-  ( ( ( K e. HL /\ X e. P /\ Y e. P ) /\ ( z e. ( LLines ` K ) /\ z (  z (
25 simpl1 
 |-  ( ( ( K e. HL /\ X e. P /\ Y e. P ) /\ ( z e. ( LLines ` K ) /\ z (  K e. HL )
26 5 1 8 cvrle 
 |-  ( ( ( K e. HL /\ z e. ( Base ` K ) /\ X e. ( Base ` K ) ) /\ z (  z .<_ X )
27 25 23 17 24 26 syl31anc 
 |-  ( ( ( K e. HL /\ X e. P /\ Y e. P ) /\ ( z e. ( LLines ` K ) /\ z (  z .<_ X )
28 5 1 postr 
 |-  ( ( K e. Poset /\ ( z e. ( Base ` K ) /\ X e. ( Base ` K ) /\ Y e. ( Base ` K ) ) ) -> ( ( z .<_ X /\ X .<_ Y ) -> z .<_ Y ) )
29 16 23 17 20 28 syl13anc 
 |-  ( ( ( K e. HL /\ X e. P /\ Y e. P ) /\ ( z e. ( LLines ` K ) /\ z (  ( ( z .<_ X /\ X .<_ Y ) -> z .<_ Y ) )
30 27 13 29 mp2and 
 |-  ( ( ( K e. HL /\ X e. P /\ Y e. P ) /\ ( z e. ( LLines ` K ) /\ z (  z .<_ Y )
31 1 8 9 2 llncvrlpln2 
 |-  ( ( ( K e. HL /\ z e. ( LLines ` K ) /\ Y e. P ) /\ z .<_ Y ) -> z (
32 25 21 18 30 31 syl31anc 
 |-  ( ( ( K e. HL /\ X e. P /\ Y e. P ) /\ ( z e. ( LLines ` K ) /\ z (  z (
33 5 1 8 cvrcmp 
 |-  ( ( K e. Poset /\ ( X e. ( Base ` K ) /\ Y e. ( Base ` K ) /\ z e. ( Base ` K ) ) /\ ( z (  ( X .<_ Y <-> X = Y ) )
34 16 17 20 23 24 32 33 syl132anc 
 |-  ( ( ( K e. HL /\ X e. P /\ Y e. P ) /\ ( z e. ( LLines ` K ) /\ z (  ( X .<_ Y <-> X = Y ) )
35 13 34 mpbid 
 |-  ( ( ( K e. HL /\ X e. P /\ Y e. P ) /\ ( z e. ( LLines ` K ) /\ z (  X = Y )
36 35 3exp2 
 |-  ( ( K e. HL /\ X e. P /\ Y e. P ) -> ( z e. ( LLines ` K ) -> ( z (  ( X .<_ Y -> X = Y ) ) ) )
37 36 rexlimdv 
 |-  ( ( K e. HL /\ X e. P /\ Y e. P ) -> ( E. z e. ( LLines ` K ) z (  ( X .<_ Y -> X = Y ) ) )
38 12 37 mpd 
 |-  ( ( K e. HL /\ X e. P /\ Y e. P ) -> ( X .<_ Y -> X = Y ) )
39 5 1 posref 
 |-  ( ( K e. Poset /\ X e. ( Base ` K ) ) -> X .<_ X )
40 15 7 39 syl2anc 
 |-  ( ( K e. HL /\ X e. P /\ Y e. P ) -> X .<_ X )
41 breq2 
 |-  ( X = Y -> ( X .<_ X <-> X .<_ Y ) )
42 40 41 syl5ibcom 
 |-  ( ( K e. HL /\ X e. P /\ Y e. P ) -> ( X = Y -> X .<_ Y ) )
43 38 42 impbid 
 |-  ( ( K e. HL /\ X e. P /\ Y e. P ) -> ( X .<_ Y <-> X = Y ) )