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 ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ( 𝑃 < ( 𝑄 ∨ 𝑅 ) ↔ 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) ) )