Metamath Proof Explorer

Theorem 1cvrjat

Description: An element covered by the lattice unit, when joined with an atom not under it, equals the lattice unit. (Contributed by NM, 30-Apr-2012)

Ref Expression
Hypotheses 1cvrjat.b 
|- B = ( Base ` K )
1cvrjat.l 
|- .<_ = ( le ` K )
1cvrjat.j 
|- .\/ = ( join ` K )
1cvrjat.u 
|- .1. = ( 1. ` K )
1cvrjat.c 
|- C = (
1cvrjat.a 
|- A = ( Atoms ` K )
Assertion 1cvrjat 
|- ( ( ( K e. HL /\ X e. B /\ P e. A ) /\ ( X C .1. /\ -. P .<_ X ) ) -> ( X .\/ P ) = .1. )

Proof

Step Hyp Ref Expression
1 1cvrjat.b 
 |-  B = ( Base ` K )
2 1cvrjat.l 
 |-  .<_ = ( le ` K )
3 1cvrjat.j 
 |-  .\/ = ( join ` K )
4 1cvrjat.u 
 |-  .1. = ( 1. ` K )
5 1cvrjat.c 
 |-  C = (
6 1cvrjat.a 
 |-  A = ( Atoms ` K )
7 simprr 
 |-  ( ( ( K e. HL /\ X e. B /\ P e. A ) /\ ( X C .1. /\ -. P .<_ X ) ) -> -. P .<_ X )
8 1 2 3 5 6 cvr1 
 |-  ( ( K e. HL /\ X e. B /\ P e. A ) -> ( -. P .<_ X <-> X C ( X .\/ P ) ) )
9 8 adantr 
 |-  ( ( ( K e. HL /\ X e. B /\ P e. A ) /\ ( X C .1. /\ -. P .<_ X ) ) -> ( -. P .<_ X <-> X C ( X .\/ P ) ) )
10 7 9 mpbid 
 |-  ( ( ( K e. HL /\ X e. B /\ P e. A ) /\ ( X C .1. /\ -. P .<_ X ) ) -> X C ( X .\/ P ) )
11 simpl1 
 |-  ( ( ( K e. HL /\ X e. B /\ P e. A ) /\ ( X C .1. /\ -. P .<_ X ) ) -> K e. HL )
12 hlop 
 |-  ( K e. HL -> K e. OP )
13 11 12 syl 
 |-  ( ( ( K e. HL /\ X e. B /\ P e. A ) /\ ( X C .1. /\ -. P .<_ X ) ) -> K e. OP )
14 simpl2 
 |-  ( ( ( K e. HL /\ X e. B /\ P e. A ) /\ ( X C .1. /\ -. P .<_ X ) ) -> X e. B )
15 11 hllatd 
 |-  ( ( ( K e. HL /\ X e. B /\ P e. A ) /\ ( X C .1. /\ -. P .<_ X ) ) -> K e. Lat )
16 simpl3 
 |-  ( ( ( K e. HL /\ X e. B /\ P e. A ) /\ ( X C .1. /\ -. P .<_ X ) ) -> P e. A )
17 1 6 atbase 
 |-  ( P e. A -> P e. B )
18 16 17 syl 
 |-  ( ( ( K e. HL /\ X e. B /\ P e. A ) /\ ( X C .1. /\ -. P .<_ X ) ) -> P e. B )
19 1 3 latjcl 
 |-  ( ( K e. Lat /\ X e. B /\ P e. B ) -> ( X .\/ P ) e. B )
20 15 14 18 19 syl3anc 
 |-  ( ( ( K e. HL /\ X e. B /\ P e. A ) /\ ( X C .1. /\ -. P .<_ X ) ) -> ( X .\/ P ) e. B )
21 eqid 
 |-  ( oc ` K ) = ( oc ` K )
22 1 21 5 cvrcon3b 
 |-  ( ( K e. OP /\ X e. B /\ ( X .\/ P ) e. B ) -> ( X C ( X .\/ P ) <-> ( ( oc ` K ) ` ( X .\/ P ) ) C ( ( oc ` K ) ` X ) ) )
23 13 14 20 22 syl3anc 
 |-  ( ( ( K e. HL /\ X e. B /\ P e. A ) /\ ( X C .1. /\ -. P .<_ X ) ) -> ( X C ( X .\/ P ) <-> ( ( oc ` K ) ` ( X .\/ P ) ) C ( ( oc ` K ) ` X ) ) )
24 10 23 mpbid 
 |-  ( ( ( K e. HL /\ X e. B /\ P e. A ) /\ ( X C .1. /\ -. P .<_ X ) ) -> ( ( oc ` K ) ` ( X .\/ P ) ) C ( ( oc ` K ) ` X ) )
25 hlatl 
 |-  ( K e. HL -> K e. AtLat )
26 11 25 syl 
 |-  ( ( ( K e. HL /\ X e. B /\ P e. A ) /\ ( X C .1. /\ -. P .<_ X ) ) -> K e. AtLat )
27 1 21 opoccl 
 |-  ( ( K e. OP /\ ( X .\/ P ) e. B ) -> ( ( oc ` K ) ` ( X .\/ P ) ) e. B )
28 13 20 27 syl2anc 
 |-  ( ( ( K e. HL /\ X e. B /\ P e. A ) /\ ( X C .1. /\ -. P .<_ X ) ) -> ( ( oc ` K ) ` ( X .\/ P ) ) e. B )
29 1 21 opoccl 
 |-  ( ( K e. OP /\ X e. B ) -> ( ( oc ` K ) ` X ) e. B )
30 13 14 29 syl2anc 
 |-  ( ( ( K e. HL /\ X e. B /\ P e. A ) /\ ( X C .1. /\ -. P .<_ X ) ) -> ( ( oc ` K ) ` X ) e. B )
31 eqid 
 |-  ( 0. ` K ) = ( 0. ` K )
32 31 4 21 opoc1 
 |-  ( K e. OP -> ( ( oc ` K ) ` .1. ) = ( 0. ` K ) )
33 11 12 32 3syl 
 |-  ( ( ( K e. HL /\ X e. B /\ P e. A ) /\ ( X C .1. /\ -. P .<_ X ) ) -> ( ( oc ` K ) ` .1. ) = ( 0. ` K ) )
34 simprl 
 |-  ( ( ( K e. HL /\ X e. B /\ P e. A ) /\ ( X C .1. /\ -. P .<_ X ) ) -> X C .1. )
35 1 4 op1cl 
 |-  ( K e. OP -> .1. e. B )
36 11 12 35 3syl 
 |-  ( ( ( K e. HL /\ X e. B /\ P e. A ) /\ ( X C .1. /\ -. P .<_ X ) ) -> .1. e. B )
37 1 21 5 cvrcon3b 
 |-  ( ( K e. OP /\ X e. B /\ .1. e. B ) -> ( X C .1. <-> ( ( oc ` K ) ` .1. ) C ( ( oc ` K ) ` X ) ) )
38 13 14 36 37 syl3anc 
 |-  ( ( ( K e. HL /\ X e. B /\ P e. A ) /\ ( X C .1. /\ -. P .<_ X ) ) -> ( X C .1. <-> ( ( oc ` K ) ` .1. ) C ( ( oc ` K ) ` X ) ) )
39 34 38 mpbid 
 |-  ( ( ( K e. HL /\ X e. B /\ P e. A ) /\ ( X C .1. /\ -. P .<_ X ) ) -> ( ( oc ` K ) ` .1. ) C ( ( oc ` K ) ` X ) )
40 33 39 eqbrtrrd 
 |-  ( ( ( K e. HL /\ X e. B /\ P e. A ) /\ ( X C .1. /\ -. P .<_ X ) ) -> ( 0. ` K ) C ( ( oc ` K ) ` X ) )
41 1 31 5 6 isat 
 |-  ( K e. HL -> ( ( ( oc ` K ) ` X ) e. A <-> ( ( ( oc ` K ) ` X ) e. B /\ ( 0. ` K ) C ( ( oc ` K ) ` X ) ) ) )
42 11 41 syl 
 |-  ( ( ( K e. HL /\ X e. B /\ P e. A ) /\ ( X C .1. /\ -. P .<_ X ) ) -> ( ( ( oc ` K ) ` X ) e. A <-> ( ( ( oc ` K ) ` X ) e. B /\ ( 0. ` K ) C ( ( oc ` K ) ` X ) ) ) )
43 30 40 42 mpbir2and 
 |-  ( ( ( K e. HL /\ X e. B /\ P e. A ) /\ ( X C .1. /\ -. P .<_ X ) ) -> ( ( oc ` K ) ` X ) e. A )
44 1 2 31 5 6 atcvreq0 
 |-  ( ( K e. AtLat /\ ( ( oc ` K ) ` ( X .\/ P ) ) e. B /\ ( ( oc ` K ) ` X ) e. A ) -> ( ( ( oc ` K ) ` ( X .\/ P ) ) C ( ( oc ` K ) ` X ) <-> ( ( oc ` K ) ` ( X .\/ P ) ) = ( 0. ` K ) ) )
45 26 28 43 44 syl3anc 
 |-  ( ( ( K e. HL /\ X e. B /\ P e. A ) /\ ( X C .1. /\ -. P .<_ X ) ) -> ( ( ( oc ` K ) ` ( X .\/ P ) ) C ( ( oc ` K ) ` X ) <-> ( ( oc ` K ) ` ( X .\/ P ) ) = ( 0. ` K ) ) )
46 24 45 mpbid 
 |-  ( ( ( K e. HL /\ X e. B /\ P e. A ) /\ ( X C .1. /\ -. P .<_ X ) ) -> ( ( oc ` K ) ` ( X .\/ P ) ) = ( 0. ` K ) )
47 46 fveq2d 
 |-  ( ( ( K e. HL /\ X e. B /\ P e. A ) /\ ( X C .1. /\ -. P .<_ X ) ) -> ( ( oc ` K ) ` ( ( oc ` K ) ` ( X .\/ P ) ) ) = ( ( oc ` K ) ` ( 0. ` K ) ) )
48 1 21 opococ 
 |-  ( ( K e. OP /\ ( X .\/ P ) e. B ) -> ( ( oc ` K ) ` ( ( oc ` K ) ` ( X .\/ P ) ) ) = ( X .\/ P ) )
49 13 20 48 syl2anc 
 |-  ( ( ( K e. HL /\ X e. B /\ P e. A ) /\ ( X C .1. /\ -. P .<_ X ) ) -> ( ( oc ` K ) ` ( ( oc ` K ) ` ( X .\/ P ) ) ) = ( X .\/ P ) )
50 31 4 21 opoc0 
 |-  ( K e. OP -> ( ( oc ` K ) ` ( 0. ` K ) ) = .1. )
51 11 12 50 3syl 
 |-  ( ( ( K e. HL /\ X e. B /\ P e. A ) /\ ( X C .1. /\ -. P .<_ X ) ) -> ( ( oc ` K ) ` ( 0. ` K ) ) = .1. )
52 47 49 51 3eqtr3d 
 |-  ( ( ( K e. HL /\ X e. B /\ P e. A ) /\ ( X C .1. /\ -. P .<_ X ) ) -> ( X .\/ P ) = .1. )