Metamath Proof Explorer

Theorem atcvrj2b

Description: Condition for an atom to be covered by the join of two others. (Contributed by NM, 7-Feb-2012)

Ref Expression
Hypotheses atcvrj1x.l 
|- .<_ = ( le ` K )
atcvrj1x.j 
|- .\/ = ( join ` K )
atcvrj1x.c 
|- C = (
atcvrj1x.a 
|- A = ( Atoms ` K )
Assertion atcvrj2b 
|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> ( ( Q =/= R /\ P .<_ ( Q .\/ R ) ) <-> P C ( Q .\/ R ) ) )

Proof

Step Hyp Ref Expression
1 atcvrj1x.l 
 |-  .<_ = ( le ` K )
2 atcvrj1x.j 
 |-  .\/ = ( join ` K )
3 atcvrj1x.c 
 |-  C = (
4 atcvrj1x.a 
 |-  A = ( Atoms ` K )
5 simpl3l 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( Q =/= R /\ P .<_ ( Q .\/ R ) ) ) /\ P = R ) -> Q =/= R )
6 5 necomd 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( Q =/= R /\ P .<_ ( Q .\/ R ) ) ) /\ P = R ) -> R =/= Q )
7 simpl1 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( Q =/= R /\ P .<_ ( Q .\/ R ) ) ) /\ P = R ) -> K e. HL )
8 simpl23 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( Q =/= R /\ P .<_ ( Q .\/ R ) ) ) /\ P = R ) -> R e. A )
9 simpl22 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( Q =/= R /\ P .<_ ( Q .\/ R ) ) ) /\ P = R ) -> Q e. A )
10 2 3 4 atcvr2 
 |-  ( ( K e. HL /\ R e. A /\ Q e. A ) -> ( R =/= Q <-> R C ( Q .\/ R ) ) )
11 7 8 9 10 syl3anc 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( Q =/= R /\ P .<_ ( Q .\/ R ) ) ) /\ P = R ) -> ( R =/= Q <-> R C ( Q .\/ R ) ) )
12 6 11 mpbid 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( Q =/= R /\ P .<_ ( Q .\/ R ) ) ) /\ P = R ) -> R C ( Q .\/ R ) )
13 breq1 
 |-  ( P = R -> ( P C ( Q .\/ R ) <-> R C ( Q .\/ R ) ) )
14 13 adantl 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( Q =/= R /\ P .<_ ( Q .\/ R ) ) ) /\ P = R ) -> ( P C ( Q .\/ R ) <-> R C ( Q .\/ R ) ) )
15 12 14 mpbird 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( Q =/= R /\ P .<_ ( Q .\/ R ) ) ) /\ P = R ) -> P C ( Q .\/ R ) )
16 simpl1 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( Q =/= R /\ P .<_ ( Q .\/ R ) ) ) /\ P =/= R ) -> K e. HL )
17 simpl2 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( Q =/= R /\ P .<_ ( Q .\/ R ) ) ) /\ P =/= R ) -> ( P e. A /\ Q e. A /\ R e. A ) )
18 simpr 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( Q =/= R /\ P .<_ ( Q .\/ R ) ) ) /\ P =/= R ) -> P =/= R )
19 simpl3r 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( Q =/= R /\ P .<_ ( Q .\/ R ) ) ) /\ P =/= R ) -> P .<_ ( Q .\/ R ) )
20 1 2 3 4 atcvrj1 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= R /\ P .<_ ( Q .\/ R ) ) ) -> P C ( Q .\/ R ) )
21 16 17 18 19 20 syl112anc 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( Q =/= R /\ P .<_ ( Q .\/ R ) ) ) /\ P =/= R ) -> P C ( Q .\/ R ) )
22 15 21 pm2.61dane 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( Q =/= R /\ P .<_ ( Q .\/ R ) ) ) -> P C ( Q .\/ R ) )
23 22 3expia 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> ( ( Q =/= R /\ P .<_ ( Q .\/ R ) ) -> P C ( Q .\/ R ) ) )
24 hlatl 
 |-  ( K e. HL -> K e. AtLat )
25 24 ad2antrr 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ P C ( Q .\/ R ) ) -> K e. AtLat )
26 simplr1 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ P C ( Q .\/ R ) ) -> P e. A )
27 eqid 
 |-  ( 0. ` K ) = ( 0. ` K )
28 27 4 atn0 
 |-  ( ( K e. AtLat /\ P e. A ) -> P =/= ( 0. ` K ) )
29 25 26 28 syl2anc 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ P C ( Q .\/ R ) ) -> P =/= ( 0. ` K ) )
30 simpll 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ P C ( Q .\/ R ) ) -> K e. HL )
31 eqid 
 |-  ( Base ` K ) = ( Base ` K )
32 31 4 atbase 
 |-  ( P e. A -> P e. ( Base ` K ) )
33 26 32 syl 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ P C ( Q .\/ R ) ) -> P e. ( Base ` K ) )
34 simplr2 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ P C ( Q .\/ R ) ) -> Q e. A )
35 simplr3 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ P C ( Q .\/ R ) ) -> R e. A )
36 simpr 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ P C ( Q .\/ R ) ) -> P C ( Q .\/ R ) )
37 31 2 27 3 4 atcvrj0 
 |-  ( ( K e. HL /\ ( P e. ( Base ` K ) /\ Q e. A /\ R e. A ) /\ P C ( Q .\/ R ) ) -> ( P = ( 0. ` K ) <-> Q = R ) )
38 30 33 34 35 36 37 syl131anc 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ P C ( Q .\/ R ) ) -> ( P = ( 0. ` K ) <-> Q = R ) )
39 38 necon3bid 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ P C ( Q .\/ R ) ) -> ( P =/= ( 0. ` K ) <-> Q =/= R ) )
40 29 39 mpbid 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ P C ( Q .\/ R ) ) -> Q =/= R )
41 hllat 
 |-  ( K e. HL -> K e. Lat )
42 41 ad2antrr 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ P C ( Q .\/ R ) ) -> K e. Lat )
43 31 4 atbase 
 |-  ( Q e. A -> Q e. ( Base ` K ) )
44 34 43 syl 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ P C ( Q .\/ R ) ) -> Q e. ( Base ` K ) )
45 31 4 atbase 
 |-  ( R e. A -> R e. ( Base ` K ) )
46 35 45 syl 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ P C ( Q .\/ R ) ) -> R e. ( Base ` K ) )
47 31 2 latjcl 
 |-  ( ( K e. Lat /\ Q e. ( Base ` K ) /\ R e. ( Base ` K ) ) -> ( Q .\/ R ) e. ( Base ` K ) )
48 42 44 46 47 syl3anc 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ P C ( Q .\/ R ) ) -> ( Q .\/ R ) e. ( Base ` K ) )
49 30 33 48 3jca 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ P C ( Q .\/ R ) ) -> ( K e. HL /\ P e. ( Base ` K ) /\ ( Q .\/ R ) e. ( Base ` K ) ) )
50 31 1 3 cvrle 
 |-  ( ( ( K e. HL /\ P e. ( Base ` K ) /\ ( Q .\/ R ) e. ( Base ` K ) ) /\ P C ( Q .\/ R ) ) -> P .<_ ( Q .\/ R ) )
51 49 50 sylancom 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ P C ( Q .\/ R ) ) -> P .<_ ( Q .\/ R ) )
52 40 51 jca 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ P C ( Q .\/ R ) ) -> ( Q =/= R /\ P .<_ ( Q .\/ R ) ) )
53 52 ex 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> ( P C ( Q .\/ R ) -> ( Q =/= R /\ P .<_ ( Q .\/ R ) ) ) )
54 23 53 impbid 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> ( ( Q =/= R /\ P .<_ ( Q .\/ R ) ) <-> P C ( Q .\/ R ) ) )