Metamath Proof Explorer


Theorem llncmp

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

Ref Expression
Hypotheses llncmp.l = ( le ‘ 𝐾 )
llncmp.n 𝑁 = ( LLines ‘ 𝐾 )
Assertion llncmp ( ( 𝐾 ∈ HL ∧ 𝑋𝑁𝑌𝑁 ) → ( 𝑋 𝑌𝑋 = 𝑌 ) )

Proof

Step Hyp Ref Expression
1 llncmp.l = ( le ‘ 𝐾 )
2 llncmp.n 𝑁 = ( LLines ‘ 𝐾 )
3 simp2 ( ( 𝐾 ∈ HL ∧ 𝑋𝑁𝑌𝑁 ) → 𝑋𝑁 )
4 simp1 ( ( 𝐾 ∈ HL ∧ 𝑋𝑁𝑌𝑁 ) → 𝐾 ∈ HL )
5 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
6 5 2 llnbase ( 𝑋𝑁𝑋 ∈ ( Base ‘ 𝐾 ) )
7 6 3ad2ant2 ( ( 𝐾 ∈ HL ∧ 𝑋𝑁𝑌𝑁 ) → 𝑋 ∈ ( Base ‘ 𝐾 ) )
8 eqid ( ⋖ ‘ 𝐾 ) = ( ⋖ ‘ 𝐾 )
9 eqid ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
10 5 8 9 2 islln4 ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑋𝑁 ↔ ∃ 𝑝 ∈ ( Atoms ‘ 𝐾 ) 𝑝 ( ⋖ ‘ 𝐾 ) 𝑋 ) )
11 4 7 10 syl2anc ( ( 𝐾 ∈ HL ∧ 𝑋𝑁𝑌𝑁 ) → ( 𝑋𝑁 ↔ ∃ 𝑝 ∈ ( Atoms ‘ 𝐾 ) 𝑝 ( ⋖ ‘ 𝐾 ) 𝑋 ) )
12 3 11 mpbid ( ( 𝐾 ∈ HL ∧ 𝑋𝑁𝑌𝑁 ) → ∃ 𝑝 ∈ ( Atoms ‘ 𝐾 ) 𝑝 ( ⋖ ‘ 𝐾 ) 𝑋 )
13 simpr3 ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑁𝑌𝑁 ) ∧ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ( ⋖ ‘ 𝐾 ) 𝑋𝑋 𝑌 ) ) → 𝑋 𝑌 )
14 hlpos ( 𝐾 ∈ HL → 𝐾 ∈ Poset )
15 14 3ad2ant1 ( ( 𝐾 ∈ HL ∧ 𝑋𝑁𝑌𝑁 ) → 𝐾 ∈ Poset )
16 15 adantr ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑁𝑌𝑁 ) ∧ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ( ⋖ ‘ 𝐾 ) 𝑋𝑋 𝑌 ) ) → 𝐾 ∈ Poset )
17 7 adantr ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑁𝑌𝑁 ) ∧ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ( ⋖ ‘ 𝐾 ) 𝑋𝑋 𝑌 ) ) → 𝑋 ∈ ( Base ‘ 𝐾 ) )
18 simpl3 ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑁𝑌𝑁 ) ∧ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ( ⋖ ‘ 𝐾 ) 𝑋𝑋 𝑌 ) ) → 𝑌𝑁 )
19 5 2 llnbase ( 𝑌𝑁𝑌 ∈ ( Base ‘ 𝐾 ) )
20 18 19 syl ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑁𝑌𝑁 ) ∧ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ( ⋖ ‘ 𝐾 ) 𝑋𝑋 𝑌 ) ) → 𝑌 ∈ ( Base ‘ 𝐾 ) )
21 simpr1 ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑁𝑌𝑁 ) ∧ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ( ⋖ ‘ 𝐾 ) 𝑋𝑋 𝑌 ) ) → 𝑝 ∈ ( Atoms ‘ 𝐾 ) )
22 5 9 atbase ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) → 𝑝 ∈ ( Base ‘ 𝐾 ) )
23 21 22 syl ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑁𝑌𝑁 ) ∧ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ( ⋖ ‘ 𝐾 ) 𝑋𝑋 𝑌 ) ) → 𝑝 ∈ ( Base ‘ 𝐾 ) )
24 simpr2 ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑁𝑌𝑁 ) ∧ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ( ⋖ ‘ 𝐾 ) 𝑋𝑋 𝑌 ) ) → 𝑝 ( ⋖ ‘ 𝐾 ) 𝑋 )
25 simpl1 ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑁𝑌𝑁 ) ∧ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ( ⋖ ‘ 𝐾 ) 𝑋𝑋 𝑌 ) ) → 𝐾 ∈ HL )
26 5 1 8 cvrle ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Base ‘ 𝐾 ) ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑝 ( ⋖ ‘ 𝐾 ) 𝑋 ) → 𝑝 𝑋 )
27 25 23 17 24 26 syl31anc ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑁𝑌𝑁 ) ∧ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ( ⋖ ‘ 𝐾 ) 𝑋𝑋 𝑌 ) ) → 𝑝 𝑋 )
28 5 1 postr ( ( 𝐾 ∈ Poset ∧ ( 𝑝 ∈ ( Base ‘ 𝐾 ) ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ 𝑌 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑝 𝑋𝑋 𝑌 ) → 𝑝 𝑌 ) )
29 16 23 17 20 28 syl13anc ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑁𝑌𝑁 ) ∧ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ( ⋖ ‘ 𝐾 ) 𝑋𝑋 𝑌 ) ) → ( ( 𝑝 𝑋𝑋 𝑌 ) → 𝑝 𝑌 ) )
30 27 13 29 mp2and ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑁𝑌𝑁 ) ∧ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ( ⋖ ‘ 𝐾 ) 𝑋𝑋 𝑌 ) ) → 𝑝 𝑌 )
31 1 8 9 2 atcvrlln2 ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌𝑁 ) ∧ 𝑝 𝑌 ) → 𝑝 ( ⋖ ‘ 𝐾 ) 𝑌 )
32 25 21 18 30 31 syl31anc ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑁𝑌𝑁 ) ∧ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ( ⋖ ‘ 𝐾 ) 𝑋𝑋 𝑌 ) ) → 𝑝 ( ⋖ ‘ 𝐾 ) 𝑌 )
33 5 1 8 cvrcmp ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ 𝑌 ∈ ( Base ‘ 𝐾 ) ∧ 𝑝 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑝 ( ⋖ ‘ 𝐾 ) 𝑋𝑝 ( ⋖ ‘ 𝐾 ) 𝑌 ) ) → ( 𝑋 𝑌𝑋 = 𝑌 ) )
34 16 17 20 23 24 32 33 syl132anc ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑁𝑌𝑁 ) ∧ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ( ⋖ ‘ 𝐾 ) 𝑋𝑋 𝑌 ) ) → ( 𝑋 𝑌𝑋 = 𝑌 ) )
35 13 34 mpbid ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑁𝑌𝑁 ) ∧ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ( ⋖ ‘ 𝐾 ) 𝑋𝑋 𝑌 ) ) → 𝑋 = 𝑌 )
36 35 3exp2 ( ( 𝐾 ∈ HL ∧ 𝑋𝑁𝑌𝑁 ) → ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) → ( 𝑝 ( ⋖ ‘ 𝐾 ) 𝑋 → ( 𝑋 𝑌𝑋 = 𝑌 ) ) ) )
37 36 rexlimdv ( ( 𝐾 ∈ HL ∧ 𝑋𝑁𝑌𝑁 ) → ( ∃ 𝑝 ∈ ( Atoms ‘ 𝐾 ) 𝑝 ( ⋖ ‘ 𝐾 ) 𝑋 → ( 𝑋 𝑌𝑋 = 𝑌 ) ) )
38 12 37 mpd ( ( 𝐾 ∈ HL ∧ 𝑋𝑁𝑌𝑁 ) → ( 𝑋 𝑌𝑋 = 𝑌 ) )
39 5 1 posref ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ) → 𝑋 𝑋 )
40 15 7 39 syl2anc ( ( 𝐾 ∈ HL ∧ 𝑋𝑁𝑌𝑁 ) → 𝑋 𝑋 )
41 breq2 ( 𝑋 = 𝑌 → ( 𝑋 𝑋𝑋 𝑌 ) )
42 40 41 syl5ibcom ( ( 𝐾 ∈ HL ∧ 𝑋𝑁𝑌𝑁 ) → ( 𝑋 = 𝑌𝑋 𝑌 ) )
43 38 42 impbid ( ( 𝐾 ∈ HL ∧ 𝑋𝑁𝑌𝑁 ) → ( 𝑋 𝑌𝑋 = 𝑌 ) )