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 ‘ 𝐾 )
lplncmp.p ⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
Assertion lplncmp ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( 𝑋 ≤ 𝑌 ↔ 𝑋 = 𝑌 ) )

Proof

Step Hyp Ref Expression
1 lplncmp.l ⊢ ≤ = ( le ‘ 𝐾 )
2 lplncmp.p ⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
3 simp2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → 𝑋 ∈ 𝑃 )
4 simp1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → 𝐾 ∈ HL )
5 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
6 5 2 lplnbase ⊢ ( 𝑋 ∈ 𝑃 → 𝑋 ∈ ( Base ‘ 𝐾 ) )
7 6 3ad2ant2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → 𝑋 ∈ ( Base ‘ 𝐾 ) )
8 eqid ⊢ ( ⋖ ‘ 𝐾 ) = ( ⋖ ‘ 𝐾 )
9 eqid ⊢ ( LLines ‘ 𝐾 ) = ( LLines ‘ 𝐾 )
10 5 8 9 2 islpln4 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑋 ∈ 𝑃 ↔ ∃ 𝑧 ∈ ( LLines ‘ 𝐾 ) 𝑧 ( ⋖ ‘ 𝐾 ) 𝑋 ) )
11 4 7 10 syl2anc ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( 𝑋 ∈ 𝑃 ↔ ∃ 𝑧 ∈ ( LLines ‘ 𝐾 ) 𝑧 ( ⋖ ‘ 𝐾 ) 𝑋 ) )
12 3 11 mpbid ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ∃ 𝑧 ∈ ( LLines ‘ 𝐾 ) 𝑧 ( ⋖ ‘ 𝐾 ) 𝑋 )
13 simpr3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( LLines ‘ 𝐾 ) ∧ 𝑧 ( ⋖ ‘ 𝐾 ) 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → 𝑋 ≤ 𝑌 )
14 hlpos ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Poset )
15 14 3ad2ant1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → 𝐾 ∈ Poset )
16 15 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( LLines ‘ 𝐾 ) ∧ 𝑧 ( ⋖ ‘ 𝐾 ) 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → 𝐾 ∈ Poset )
17 7 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( LLines ‘ 𝐾 ) ∧ 𝑧 ( ⋖ ‘ 𝐾 ) 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → 𝑋 ∈ ( Base ‘ 𝐾 ) )
18 simpl3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( LLines ‘ 𝐾 ) ∧ 𝑧 ( ⋖ ‘ 𝐾 ) 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → 𝑌 ∈ 𝑃 )
19 5 2 lplnbase ⊢ ( 𝑌 ∈ 𝑃 → 𝑌 ∈ ( Base ‘ 𝐾 ) )
20 18 19 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( LLines ‘ 𝐾 ) ∧ 𝑧 ( ⋖ ‘ 𝐾 ) 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → 𝑌 ∈ ( Base ‘ 𝐾 ) )
21 simpr1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( LLines ‘ 𝐾 ) ∧ 𝑧 ( ⋖ ‘ 𝐾 ) 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → 𝑧 ∈ ( LLines ‘ 𝐾 ) )
22 5 9 llnbase ⊢ ( 𝑧 ∈ ( LLines ‘ 𝐾 ) → 𝑧 ∈ ( Base ‘ 𝐾 ) )
23 21 22 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( LLines ‘ 𝐾 ) ∧ 𝑧 ( ⋖ ‘ 𝐾 ) 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → 𝑧 ∈ ( Base ‘ 𝐾 ) )
24 simpr2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( LLines ‘ 𝐾 ) ∧ 𝑧 ( ⋖ ‘ 𝐾 ) 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → 𝑧 ( ⋖ ‘ 𝐾 ) 𝑋 )
25 simpl1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( LLines ‘ 𝐾 ) ∧ 𝑧 ( ⋖ ‘ 𝐾 ) 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → 𝐾 ∈ HL )
26 5 1 8 cvrle ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ( ⋖ ‘ 𝐾 ) 𝑋 ) → 𝑧 ≤ 𝑋 )
27 25 23 17 24 26 syl31anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( LLines ‘ 𝐾 ) ∧ 𝑧 ( ⋖ ‘ 𝐾 ) 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → 𝑧 ≤ 𝑋 )
28 5 1 postr ⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑧 ∈ ( Base ‘ 𝐾 ) ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ 𝑌 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑧 ≤ 𝑋 ∧ 𝑋 ≤ 𝑌 ) → 𝑧 ≤ 𝑌 ) )
29 16 23 17 20 28 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( LLines ‘ 𝐾 ) ∧ 𝑧 ( ⋖ ‘ 𝐾 ) 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → ( ( 𝑧 ≤ 𝑋 ∧ 𝑋 ≤ 𝑌 ) → 𝑧 ≤ 𝑌 ) )
30 27 13 29 mp2and ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( LLines ‘ 𝐾 ) ∧ 𝑧 ( ⋖ ‘ 𝐾 ) 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → 𝑧 ≤ 𝑌 )
31 1 8 9 2 llncvrlpln2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑧 ∈ ( LLines ‘ 𝐾 ) ∧ 𝑌 ∈ 𝑃 ) ∧ 𝑧 ≤ 𝑌 ) → 𝑧 ( ⋖ ‘ 𝐾 ) 𝑌 )
32 25 21 18 30 31 syl31anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( LLines ‘ 𝐾 ) ∧ 𝑧 ( ⋖ ‘ 𝐾 ) 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → 𝑧 ( ⋖ ‘ 𝐾 ) 𝑌 )
33 5 1 8 cvrcmp ⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ 𝑌 ∈ ( Base ‘ 𝐾 ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑧 ( ⋖ ‘ 𝐾 ) 𝑋 ∧ 𝑧 ( ⋖ ‘ 𝐾 ) 𝑌 ) ) → ( 𝑋 ≤ 𝑌 ↔ 𝑋 = 𝑌 ) )
34 16 17 20 23 24 32 33 syl132anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( LLines ‘ 𝐾 ) ∧ 𝑧 ( ⋖ ‘ 𝐾 ) 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → ( 𝑋 ≤ 𝑌 ↔ 𝑋 = 𝑌 ) )
35 13 34 mpbid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( LLines ‘ 𝐾 ) ∧ 𝑧 ( ⋖ ‘ 𝐾 ) 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) → 𝑋 = 𝑌 )
36 35 3exp2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( 𝑧 ∈ ( LLines ‘ 𝐾 ) → ( 𝑧 ( ⋖ ‘ 𝐾 ) 𝑋 → ( 𝑋 ≤ 𝑌 → 𝑋 = 𝑌 ) ) ) )
37 36 rexlimdv ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( ∃ 𝑧 ∈ ( LLines ‘ 𝐾 ) 𝑧 ( ⋖ ‘ 𝐾 ) 𝑋 → ( 𝑋 ≤ 𝑌 → 𝑋 = 𝑌 ) ) )
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 ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( 𝑋 ≤ 𝑌 ↔ 𝑋 = 𝑌 ) )