Metamath Proof Explorer


Theorem atltcvr

Description: An equivalence of less-than ordering and covers relation. (Contributed by NM, 7-Feb-2012)

Ref Expression
Hypotheses atltcvr.s < = ( lt ‘ 𝐾 )
atltcvr.j = ( join ‘ 𝐾 )
atltcvr.a 𝐴 = ( Atoms ‘ 𝐾 )
atltcvr.c 𝐶 = ( ⋖ ‘ 𝐾 )
Assertion atltcvr ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) → ( 𝑃 < ( 𝑄 𝑅 ) ↔ 𝑃 𝐶 ( 𝑄 𝑅 ) ) )

Proof

Step Hyp Ref Expression
1 atltcvr.s < = ( lt ‘ 𝐾 )
2 atltcvr.j = ( join ‘ 𝐾 )
3 atltcvr.a 𝐴 = ( Atoms ‘ 𝐾 )
4 atltcvr.c 𝐶 = ( ⋖ ‘ 𝐾 )
5 oveq1 ( 𝑄 = 𝑅 → ( 𝑄 𝑅 ) = ( 𝑅 𝑅 ) )
6 simpr3 ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) → 𝑅𝐴 )
7 2 3 hlatjidm ( ( 𝐾 ∈ HL ∧ 𝑅𝐴 ) → ( 𝑅 𝑅 ) = 𝑅 )
8 6 7 syldan ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) → ( 𝑅 𝑅 ) = 𝑅 )
9 5 8 sylan9eqr ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ 𝑄 = 𝑅 ) → ( 𝑄 𝑅 ) = 𝑅 )
10 9 breq2d ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ 𝑄 = 𝑅 ) → ( 𝑃 < ( 𝑄 𝑅 ) ↔ 𝑃 < 𝑅 ) )
11 hlatl ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
12 11 adantr ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) → 𝐾 ∈ AtLat )
13 simpr1 ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) → 𝑃𝐴 )
14 1 3 atnlt ( ( 𝐾 ∈ AtLat ∧ 𝑃𝐴𝑅𝐴 ) → ¬ 𝑃 < 𝑅 )
15 12 13 6 14 syl3anc ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) → ¬ 𝑃 < 𝑅 )
16 15 pm2.21d ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) → ( 𝑃 < 𝑅𝑃 𝐶 ( 𝑄 𝑅 ) ) )
17 16 adantr ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ 𝑄 = 𝑅 ) → ( 𝑃 < 𝑅𝑃 𝐶 ( 𝑄 𝑅 ) ) )
18 10 17 sylbid ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ 𝑄 = 𝑅 ) → ( 𝑃 < ( 𝑄 𝑅 ) → 𝑃 𝐶 ( 𝑄 𝑅 ) ) )
19 simpl ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) → 𝐾 ∈ HL )
20 hllat ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
21 20 adantr ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) → 𝐾 ∈ Lat )
22 simpr2 ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) → 𝑄𝐴 )
23 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
24 23 3 atbase ( 𝑄𝐴𝑄 ∈ ( Base ‘ 𝐾 ) )
25 22 24 syl ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) → 𝑄 ∈ ( Base ‘ 𝐾 ) )
26 23 3 atbase ( 𝑅𝐴𝑅 ∈ ( Base ‘ 𝐾 ) )
27 6 26 syl ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) → 𝑅 ∈ ( Base ‘ 𝐾 ) )
28 23 2 latjcl ( ( 𝐾 ∈ Lat ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ 𝑅 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑄 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
29 21 25 27 28 syl3anc ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) → ( 𝑄 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
30 eqid ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
31 30 1 pltle ( ( 𝐾 ∈ HL ∧ 𝑃𝐴 ∧ ( 𝑄 𝑅 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝑃 < ( 𝑄 𝑅 ) → 𝑃 ( le ‘ 𝐾 ) ( 𝑄 𝑅 ) ) )
32 19 13 29 31 syl3anc ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) → ( 𝑃 < ( 𝑄 𝑅 ) → 𝑃 ( le ‘ 𝐾 ) ( 𝑄 𝑅 ) ) )
33 32 adantr ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ 𝑄𝑅 ) → ( 𝑃 < ( 𝑄 𝑅 ) → 𝑃 ( le ‘ 𝐾 ) ( 𝑄 𝑅 ) ) )
34 simpll ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ ( 𝑄𝑅𝑃 ( le ‘ 𝐾 ) ( 𝑄 𝑅 ) ) ) → 𝐾 ∈ HL )
35 simplr ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ ( 𝑄𝑅𝑃 ( le ‘ 𝐾 ) ( 𝑄 𝑅 ) ) ) → ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) )
36 simpr ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ ( 𝑄𝑅𝑃 ( le ‘ 𝐾 ) ( 𝑄 𝑅 ) ) ) → ( 𝑄𝑅𝑃 ( le ‘ 𝐾 ) ( 𝑄 𝑅 ) ) )
37 34 35 36 3jca ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ ( 𝑄𝑅𝑃 ( le ‘ 𝐾 ) ( 𝑄 𝑅 ) ) ) → ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑄𝑅𝑃 ( le ‘ 𝐾 ) ( 𝑄 𝑅 ) ) ) )
38 37 anassrs ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ 𝑄𝑅 ) ∧ 𝑃 ( le ‘ 𝐾 ) ( 𝑄 𝑅 ) ) → ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑄𝑅𝑃 ( le ‘ 𝐾 ) ( 𝑄 𝑅 ) ) ) )
39 30 2 4 3 atcvrj2 ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑄𝑅𝑃 ( le ‘ 𝐾 ) ( 𝑄 𝑅 ) ) ) → 𝑃 𝐶 ( 𝑄 𝑅 ) )
40 38 39 syl ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ 𝑄𝑅 ) ∧ 𝑃 ( le ‘ 𝐾 ) ( 𝑄 𝑅 ) ) → 𝑃 𝐶 ( 𝑄 𝑅 ) )
41 40 ex ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ 𝑄𝑅 ) → ( 𝑃 ( le ‘ 𝐾 ) ( 𝑄 𝑅 ) → 𝑃 𝐶 ( 𝑄 𝑅 ) ) )
42 33 41 syld ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ 𝑄𝑅 ) → ( 𝑃 < ( 𝑄 𝑅 ) → 𝑃 𝐶 ( 𝑄 𝑅 ) ) )
43 18 42 pm2.61dane ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) → ( 𝑃 < ( 𝑄 𝑅 ) → 𝑃 𝐶 ( 𝑄 𝑅 ) ) )
44 23 3 atbase ( 𝑃𝐴𝑃 ∈ ( Base ‘ 𝐾 ) )
45 13 44 syl ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
46 23 1 4 cvrlt ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑄 𝑅 ) ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑃 𝐶 ( 𝑄 𝑅 ) ) → 𝑃 < ( 𝑄 𝑅 ) )
47 46 ex ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑄 𝑅 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝑃 𝐶 ( 𝑄 𝑅 ) → 𝑃 < ( 𝑄 𝑅 ) ) )
48 19 45 29 47 syl3anc ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) → ( 𝑃 𝐶 ( 𝑄 𝑅 ) → 𝑃 < ( 𝑄 𝑅 ) ) )
49 43 48 impbid ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) → ( 𝑃 < ( 𝑄 𝑅 ) ↔ 𝑃 𝐶 ( 𝑄 𝑅 ) ) )