# 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 ) )`