Metamath Proof Explorer

Theorem cvrat3

Description: A condition implying that a certain lattice element is an atom. Part of Lemma 3.2.20 of PtakPulmannova p. 68. ( atcvat3i analog.) (Contributed by NM, 30-Nov-2011)

Ref Expression
Hypotheses cvrat3.b 
|- B = ( Base ` K )
cvrat3.l 
|- .<_ = ( le ` K )
cvrat3.j 
|- .\/ = ( join ` K )
cvrat3.m 
|- ./\ = ( meet ` K )
cvrat3.a 
|- A = ( Atoms ` K )
Assertion cvrat3 
|- ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> ( ( P =/= Q /\ -. Q .<_ X /\ P .<_ ( X .\/ Q ) ) -> ( X ./\ ( P .\/ Q ) ) e. A ) )

Proof

Step Hyp Ref Expression
1 cvrat3.b 
 |-  B = ( Base ` K )
2 cvrat3.l 
 |-  .<_ = ( le ` K )
3 cvrat3.j 
 |-  .\/ = ( join ` K )
4 cvrat3.m 
 |-  ./\ = ( meet ` K )
5 cvrat3.a 
 |-  A = ( Atoms ` K )
6 eqid 
 |-  (
7 1 2 3 6 5 cvr1 
 |-  ( ( K e. HL /\ X e. B /\ Q e. A ) -> ( -. Q .<_ X <-> X (
8 7 3adant3r2 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> ( -. Q .<_ X <-> X (
9 8 biimpa 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) /\ -. Q .<_ X ) -> X (
10 9 adantrr 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) /\ ( -. Q .<_ X /\ P .<_ ( X .\/ Q ) ) ) -> X (
11 hllat 
 |-  ( K e. HL -> K e. Lat )
12 11 adantr 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> K e. Lat )
13 simpr2 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> P e. A )
14 1 5 atbase 
 |-  ( P e. A -> P e. B )
15 13 14 syl 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> P e. B )
16 simpr3 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> Q e. A )
17 1 5 atbase 
 |-  ( Q e. A -> Q e. B )
18 16 17 syl 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> Q e. B )
19 1 3 latjcom 
 |-  ( ( K e. Lat /\ P e. B /\ Q e. B ) -> ( P .\/ Q ) = ( Q .\/ P ) )
20 12 15 18 19 syl3anc 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> ( P .\/ Q ) = ( Q .\/ P ) )
21 20 oveq2d 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> ( X .\/ ( P .\/ Q ) ) = ( X .\/ ( Q .\/ P ) ) )
22 simpr1 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> X e. B )
23 1 3 latjass 
 |-  ( ( K e. Lat /\ ( X e. B /\ Q e. B /\ P e. B ) ) -> ( ( X .\/ Q ) .\/ P ) = ( X .\/ ( Q .\/ P ) ) )
24 12 22 18 15 23 syl13anc 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> ( ( X .\/ Q ) .\/ P ) = ( X .\/ ( Q .\/ P ) ) )
25 21 24 eqtr4d 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> ( X .\/ ( P .\/ Q ) ) = ( ( X .\/ Q ) .\/ P ) )
26 25 adantr 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) /\ P .<_ ( X .\/ Q ) ) -> ( X .\/ ( P .\/ Q ) ) = ( ( X .\/ Q ) .\/ P ) )
27 1 3 latjcl 
 |-  ( ( K e. Lat /\ X e. B /\ Q e. B ) -> ( X .\/ Q ) e. B )
28 12 22 18 27 syl3anc 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> ( X .\/ Q ) e. B )
29 1 2 3 latjlej2 
 |-  ( ( K e. Lat /\ ( P e. B /\ ( X .\/ Q ) e. B /\ ( X .\/ Q ) e. B ) ) -> ( P .<_ ( X .\/ Q ) -> ( ( X .\/ Q ) .\/ P ) .<_ ( ( X .\/ Q ) .\/ ( X .\/ Q ) ) ) )
30 12 15 28 28 29 syl13anc 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> ( P .<_ ( X .\/ Q ) -> ( ( X .\/ Q ) .\/ P ) .<_ ( ( X .\/ Q ) .\/ ( X .\/ Q ) ) ) )
31 30 imp 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) /\ P .<_ ( X .\/ Q ) ) -> ( ( X .\/ Q ) .\/ P ) .<_ ( ( X .\/ Q ) .\/ ( X .\/ Q ) ) )
32 26 31 eqbrtrd 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) /\ P .<_ ( X .\/ Q ) ) -> ( X .\/ ( P .\/ Q ) ) .<_ ( ( X .\/ Q ) .\/ ( X .\/ Q ) ) )
33 1 3 latjidm 
 |-  ( ( K e. Lat /\ ( X .\/ Q ) e. B ) -> ( ( X .\/ Q ) .\/ ( X .\/ Q ) ) = ( X .\/ Q ) )
34 12 28 33 syl2anc 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> ( ( X .\/ Q ) .\/ ( X .\/ Q ) ) = ( X .\/ Q ) )
35 34 adantr 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) /\ P .<_ ( X .\/ Q ) ) -> ( ( X .\/ Q ) .\/ ( X .\/ Q ) ) = ( X .\/ Q ) )
36 32 35 breqtrd 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) /\ P .<_ ( X .\/ Q ) ) -> ( X .\/ ( P .\/ Q ) ) .<_ ( X .\/ Q ) )
37 simpl 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> K e. HL )
38 2 3 5 hlatlej2 
 |-  ( ( K e. HL /\ P e. A /\ Q e. A ) -> Q .<_ ( P .\/ Q ) )
39 37 13 16 38 syl3anc 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> Q .<_ ( P .\/ Q ) )
40 1 3 latjcl 
 |-  ( ( K e. Lat /\ P e. B /\ Q e. B ) -> ( P .\/ Q ) e. B )
41 12 15 18 40 syl3anc 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> ( P .\/ Q ) e. B )
42 1 2 3 latjlej2 
 |-  ( ( K e. Lat /\ ( Q e. B /\ ( P .\/ Q ) e. B /\ X e. B ) ) -> ( Q .<_ ( P .\/ Q ) -> ( X .\/ Q ) .<_ ( X .\/ ( P .\/ Q ) ) ) )
43 12 18 41 22 42 syl13anc 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> ( Q .<_ ( P .\/ Q ) -> ( X .\/ Q ) .<_ ( X .\/ ( P .\/ Q ) ) ) )
44 39 43 mpd 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> ( X .\/ Q ) .<_ ( X .\/ ( P .\/ Q ) ) )
45 44 adantr 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) /\ P .<_ ( X .\/ Q ) ) -> ( X .\/ Q ) .<_ ( X .\/ ( P .\/ Q ) ) )
46 1 3 latjcl 
 |-  ( ( K e. Lat /\ X e. B /\ ( P .\/ Q ) e. B ) -> ( X .\/ ( P .\/ Q ) ) e. B )
47 12 22 41 46 syl3anc 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> ( X .\/ ( P .\/ Q ) ) e. B )
48 1 2 latasymb 
 |-  ( ( K e. Lat /\ ( X .\/ ( P .\/ Q ) ) e. B /\ ( X .\/ Q ) e. B ) -> ( ( ( X .\/ ( P .\/ Q ) ) .<_ ( X .\/ Q ) /\ ( X .\/ Q ) .<_ ( X .\/ ( P .\/ Q ) ) ) <-> ( X .\/ ( P .\/ Q ) ) = ( X .\/ Q ) ) )
49 12 47 28 48 syl3anc 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> ( ( ( X .\/ ( P .\/ Q ) ) .<_ ( X .\/ Q ) /\ ( X .\/ Q ) .<_ ( X .\/ ( P .\/ Q ) ) ) <-> ( X .\/ ( P .\/ Q ) ) = ( X .\/ Q ) ) )
50 49 adantr 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) /\ P .<_ ( X .\/ Q ) ) -> ( ( ( X .\/ ( P .\/ Q ) ) .<_ ( X .\/ Q ) /\ ( X .\/ Q ) .<_ ( X .\/ ( P .\/ Q ) ) ) <-> ( X .\/ ( P .\/ Q ) ) = ( X .\/ Q ) ) )
51 36 45 50 mpbi2and 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) /\ P .<_ ( X .\/ Q ) ) -> ( X .\/ ( P .\/ Q ) ) = ( X .\/ Q ) )
52 51 breq2d 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) /\ P .<_ ( X .\/ Q ) ) -> ( X (  X (
53 52 adantrl 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) /\ ( -. Q .<_ X /\ P .<_ ( X .\/ Q ) ) ) -> ( X (  X (
54 10 53 mpbird 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) /\ ( -. Q .<_ X /\ P .<_ ( X .\/ Q ) ) ) -> X (
55 54 ex 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> ( ( -. Q .<_ X /\ P .<_ ( X .\/ Q ) ) -> X (
56 1 3 4 6 cvrexch 
 |-  ( ( K e. HL /\ X e. B /\ ( P .\/ Q ) e. B ) -> ( ( X ./\ ( P .\/ Q ) ) (  X (
57 37 22 41 56 syl3anc 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> ( ( X ./\ ( P .\/ Q ) ) (  X (
58 55 57 sylibrd 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> ( ( -. Q .<_ X /\ P .<_ ( X .\/ Q ) ) -> ( X ./\ ( P .\/ Q ) ) (
59 58 adantr 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) /\ P =/= Q ) -> ( ( -. Q .<_ X /\ P .<_ ( X .\/ Q ) ) -> ( X ./\ ( P .\/ Q ) ) (
60 1 4 latmcl 
 |-  ( ( K e. Lat /\ X e. B /\ ( P .\/ Q ) e. B ) -> ( X ./\ ( P .\/ Q ) ) e. B )
61 12 22 41 60 syl3anc 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> ( X ./\ ( P .\/ Q ) ) e. B )
62 1 3 6 5 cvrat2 
 |-  ( ( K e. HL /\ ( ( X ./\ ( P .\/ Q ) ) e. B /\ P e. A /\ Q e. A ) /\ ( P =/= Q /\ ( X ./\ ( P .\/ Q ) ) (  ( X ./\ ( P .\/ Q ) ) e. A )
63 62 3expia 
 |-  ( ( K e. HL /\ ( ( X ./\ ( P .\/ Q ) ) e. B /\ P e. A /\ Q e. A ) ) -> ( ( P =/= Q /\ ( X ./\ ( P .\/ Q ) ) (  ( X ./\ ( P .\/ Q ) ) e. A ) )
64 37 61 13 16 63 syl13anc 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> ( ( P =/= Q /\ ( X ./\ ( P .\/ Q ) ) (  ( X ./\ ( P .\/ Q ) ) e. A ) )
65 64 expdimp 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) /\ P =/= Q ) -> ( ( X ./\ ( P .\/ Q ) ) (  ( X ./\ ( P .\/ Q ) ) e. A ) )
66 59 65 syld 
 |-  ( ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) /\ P =/= Q ) -> ( ( -. Q .<_ X /\ P .<_ ( X .\/ Q ) ) -> ( X ./\ ( P .\/ Q ) ) e. A ) )
67 66 exp4b 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> ( P =/= Q -> ( -. Q .<_ X -> ( P .<_ ( X .\/ Q ) -> ( X ./\ ( P .\/ Q ) ) e. A ) ) ) )
68 67 3impd 
 |-  ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> ( ( P =/= Q /\ -. Q .<_ X /\ P .<_ ( X .\/ Q ) ) -> ( X ./\ ( P .\/ Q ) ) e. A ) )