Metamath Proof Explorer

Theorem lhpmcvr3

Description: Specialization of lhpmcvr2 . TODO: Use this to simplify many uses of ( P .\/ ( X ./\ W ) ) = X to become P .<_ X . (Contributed by NM, 6-Apr-2014)

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

Proof

Step Hyp Ref Expression
1 lhpmcvr2.b 
 |-  B = ( Base ` K )
2 lhpmcvr2.l 
 |-  .<_ = ( le ` K )
3 lhpmcvr2.j 
 |-  .\/ = ( join ` K )
4 lhpmcvr2.m 
 |-  ./\ = ( meet ` K )
5 lhpmcvr2.a 
 |-  A = ( Atoms ` K )
6 lhpmcvr2.h 
 |-  H = ( LHyp ` K )
7 simpl1l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) /\ P .<_ X ) -> K e. HL )
8 simpl3l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) /\ P .<_ X ) -> P e. A )
9 simpl2l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) /\ P .<_ X ) -> X e. B )
10 simpl1r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) /\ P .<_ X ) -> W e. H )
11 1 6 lhpbase 
 |-  ( W e. H -> W e. B )
12 10 11 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) /\ P .<_ X ) -> W e. B )
13 simpr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) /\ P .<_ X ) -> P .<_ X )
14 1 2 3 4 5 atmod3i1 
 |-  ( ( K e. HL /\ ( P e. A /\ X e. B /\ W e. B ) /\ P .<_ X ) -> ( P .\/ ( X ./\ W ) ) = ( X ./\ ( P .\/ W ) ) )
15 7 8 9 12 13 14 syl131anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) /\ P .<_ X ) -> ( P .\/ ( X ./\ W ) ) = ( X ./\ ( P .\/ W ) ) )
16 simpl1 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) /\ P .<_ X ) -> ( K e. HL /\ W e. H ) )
17 simpl3 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) /\ P .<_ X ) -> ( P e. A /\ -. P .<_ W ) )
18 eqid 
 |-  ( 1. ` K ) = ( 1. ` K )
19 2 3 18 5 6 lhpjat2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( P .\/ W ) = ( 1. ` K ) )
20 16 17 19 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) /\ P .<_ X ) -> ( P .\/ W ) = ( 1. ` K ) )
21 20 oveq2d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) /\ P .<_ X ) -> ( X ./\ ( P .\/ W ) ) = ( X ./\ ( 1. ` K ) ) )
22 hlol 
 |-  ( K e. HL -> K e. OL )
23 7 22 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) /\ P .<_ X ) -> K e. OL )
24 1 4 18 olm11 
 |-  ( ( K e. OL /\ X e. B ) -> ( X ./\ ( 1. ` K ) ) = X )
25 23 9 24 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) /\ P .<_ X ) -> ( X ./\ ( 1. ` K ) ) = X )
26 15 21 25 3eqtrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) /\ P .<_ X ) -> ( P .\/ ( X ./\ W ) ) = X )
27 simpl1l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( P .\/ ( X ./\ W ) ) = X ) -> K e. HL )
28 27 hllatd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( P .\/ ( X ./\ W ) ) = X ) -> K e. Lat )
29 simpl3l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( P .\/ ( X ./\ W ) ) = X ) -> P e. A )
30 1 5 atbase 
 |-  ( P e. A -> P e. B )
31 29 30 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( P .\/ ( X ./\ W ) ) = X ) -> P e. B )
32 simpl2l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( P .\/ ( X ./\ W ) ) = X ) -> X e. B )
33 simpl1r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( P .\/ ( X ./\ W ) ) = X ) -> W e. H )
34 33 11 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( P .\/ ( X ./\ W ) ) = X ) -> W e. B )
35 1 4 latmcl 
 |-  ( ( K e. Lat /\ X e. B /\ W e. B ) -> ( X ./\ W ) e. B )
36 28 32 34 35 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( P .\/ ( X ./\ W ) ) = X ) -> ( X ./\ W ) e. B )
37 1 2 3 latlej1 
 |-  ( ( K e. Lat /\ P e. B /\ ( X ./\ W ) e. B ) -> P .<_ ( P .\/ ( X ./\ W ) ) )
38 28 31 36 37 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( P .\/ ( X ./\ W ) ) = X ) -> P .<_ ( P .\/ ( X ./\ W ) ) )
39 simpr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( P .\/ ( X ./\ W ) ) = X ) -> ( P .\/ ( X ./\ W ) ) = X )
40 38 39 breqtrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( P .\/ ( X ./\ W ) ) = X ) -> P .<_ X )
41 26 40 impbida 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( P .<_ X <-> ( P .\/ ( X ./\ W ) ) = X ) )