Metamath Proof Explorer

Theorem lncmp

Description: If two lines are comparable, they are equal. (Contributed by NM, 30-Apr-2012)

Ref Expression
Hypotheses lncmp.b 
|- B = ( Base ` K )
lncmp.l 
|- .<_ = ( le ` K )
lncmp.n 
|- N = ( Lines ` K )
lncmp.m 
|- M = ( pmap ` K )
Assertion lncmp 
|- ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) -> ( X .<_ Y <-> X = Y ) )

Proof

Step Hyp Ref Expression
1 lncmp.b 
 |-  B = ( Base ` K )
2 lncmp.l 
 |-  .<_ = ( le ` K )
3 lncmp.n 
 |-  N = ( Lines ` K )
4 lncmp.m 
 |-  M = ( pmap ` K )
5 simplrl 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) /\ X .<_ Y ) -> ( M ` X ) e. N )
6 simpll1 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) /\ X .<_ Y ) -> K e. HL )
7 simpll2 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) /\ X .<_ Y ) -> X e. B )
8 eqid 
 |-  ( join ` K ) = ( join ` K )
9 eqid 
 |-  ( Atoms ` K ) = ( Atoms ` K )
10 1 8 9 3 4 isline3 
 |-  ( ( K e. HL /\ X e. B ) -> ( ( M ` X ) e. N <-> E. p e. ( Atoms ` K ) E. q e. ( Atoms ` K ) ( p =/= q /\ X = ( p ( join ` K ) q ) ) ) )
11 6 7 10 syl2anc 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) /\ X .<_ Y ) -> ( ( M ` X ) e. N <-> E. p e. ( Atoms ` K ) E. q e. ( Atoms ` K ) ( p =/= q /\ X = ( p ( join ` K ) q ) ) ) )
12 5 11 mpbid 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) /\ X .<_ Y ) -> E. p e. ( Atoms ` K ) E. q e. ( Atoms ` K ) ( p =/= q /\ X = ( p ( join ` K ) q ) ) )
13 simp3rr 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) /\ X .<_ Y /\ ( ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) ) ) -> X = ( p ( join ` K ) q ) )
14 simp1l1 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) /\ X .<_ Y /\ ( ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) ) ) -> K e. HL )
15 simp1l3 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) /\ X .<_ Y /\ ( ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) ) ) -> Y e. B )
16 simp1rr 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) /\ X .<_ Y /\ ( ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) ) ) -> ( M ` Y ) e. N )
17 simp3ll 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) /\ X .<_ Y /\ ( ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) ) ) -> p e. ( Atoms ` K ) )
18 simp3lr 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) /\ X .<_ Y /\ ( ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) ) ) -> q e. ( Atoms ` K ) )
19 simp3rl 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) /\ X .<_ Y /\ ( ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) ) ) -> p =/= q )
20 14 hllatd 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) /\ X .<_ Y /\ ( ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) ) ) -> K e. Lat )
21 1 9 atbase 
 |-  ( p e. ( Atoms ` K ) -> p e. B )
22 17 21 syl 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) /\ X .<_ Y /\ ( ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) ) ) -> p e. B )
23 simp1l2 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) /\ X .<_ Y /\ ( ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) ) ) -> X e. B )
24 2 8 9 hlatlej1 
 |-  ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) -> p .<_ ( p ( join ` K ) q ) )
25 14 17 18 24 syl3anc 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) /\ X .<_ Y /\ ( ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) ) ) -> p .<_ ( p ( join ` K ) q ) )
26 25 13 breqtrrd 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) /\ X .<_ Y /\ ( ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) ) ) -> p .<_ X )
27 simp2 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) /\ X .<_ Y /\ ( ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) ) ) -> X .<_ Y )
28 1 2 20 22 23 15 26 27 lattrd 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) /\ X .<_ Y /\ ( ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) ) ) -> p .<_ Y )
29 1 9 atbase 
 |-  ( q e. ( Atoms ` K ) -> q e. B )
30 18 29 syl 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) /\ X .<_ Y /\ ( ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) ) ) -> q e. B )
31 2 8 9 hlatlej2 
 |-  ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) -> q .<_ ( p ( join ` K ) q ) )
32 14 17 18 31 syl3anc 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) /\ X .<_ Y /\ ( ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) ) ) -> q .<_ ( p ( join ` K ) q ) )
33 32 13 breqtrrd 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) /\ X .<_ Y /\ ( ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) ) ) -> q .<_ X )
34 1 2 20 30 23 15 33 27 lattrd 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) /\ X .<_ Y /\ ( ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) ) ) -> q .<_ Y )
35 1 2 8 9 3 4 lneq2at 
 |-  ( ( ( K e. HL /\ Y e. B /\ ( M ` Y ) e. N ) /\ ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) /\ p =/= q ) /\ ( p .<_ Y /\ q .<_ Y ) ) -> Y = ( p ( join ` K ) q ) )
36 14 15 16 17 18 19 28 34 35 syl332anc 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) /\ X .<_ Y /\ ( ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) ) ) -> Y = ( p ( join ` K ) q ) )
37 13 36 eqtr4d 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) /\ X .<_ Y /\ ( ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) ) ) -> X = Y )
38 37 3expia 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) /\ X .<_ Y ) -> ( ( ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) ) -> X = Y ) )
39 38 expd 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) /\ X .<_ Y ) -> ( ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) -> ( ( p =/= q /\ X = ( p ( join ` K ) q ) ) -> X = Y ) ) )
40 39 rexlimdvv 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) /\ X .<_ Y ) -> ( E. p e. ( Atoms ` K ) E. q e. ( Atoms ` K ) ( p =/= q /\ X = ( p ( join ` K ) q ) ) -> X = Y ) )
41 12 40 mpd 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) /\ X .<_ Y ) -> X = Y )
42 41 ex 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) -> ( X .<_ Y -> X = Y ) )
43 simpl1 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) -> K e. HL )
44 43 hllatd 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) -> K e. Lat )
45 simpl2 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) -> X e. B )
46 1 2 latref 
 |-  ( ( K e. Lat /\ X e. B ) -> X .<_ X )
47 44 45 46 syl2anc 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) -> X .<_ X )
48 breq2 
 |-  ( X = Y -> ( X .<_ X <-> X .<_ Y ) )
49 47 48 syl5ibcom 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) -> ( X = Y -> X .<_ Y ) )
50 42 49 impbid 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) -> ( X .<_ Y <-> X = Y ) )