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 ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) → ( 𝑋 ≤ 𝑌 ↔ 𝑋 = 𝑌 ) )