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 ∧ 𝑋𝑃𝑌𝑃 ) → ( 𝑋 𝑌𝑋 = 𝑌 ) )