# 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}={\mathrm{Base}}_{{K}}$
lhpmcvr2.l
lhpmcvr2.j
lhpmcvr2.m
lhpmcvr2.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
lhpmcvr2.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
Assertion lhpmcvr3

### Proof

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