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 ` K )
atltcvr.j 
|- .\/ = ( join ` K )
atltcvr.a 
|- A = ( Atoms ` K )
atltcvr.c 
|- C = (
Assertion atltcvr 
|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> ( P .< ( Q .\/ R ) <-> P C ( Q .\/ R ) ) )

Proof

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