Metamath Proof Explorer


Theorem pexmidlem4N

Description: Lemma for pexmidN . (Contributed by NM, 2-Feb-2012) (New usage is discouraged.)

Ref Expression
Hypotheses pexmidlem.l ˙ = K
pexmidlem.j ˙ = join K
pexmidlem.a A = Atoms K
pexmidlem.p + ˙ = + 𝑃 K
pexmidlem.o ˙ = 𝑃 K
pexmidlem.m M = X + ˙ p
Assertion pexmidlem4N K HL X A p A X q ˙ X M p X + ˙ ˙ X

Proof

Step Hyp Ref Expression
1 pexmidlem.l ˙ = K
2 pexmidlem.j ˙ = join K
3 pexmidlem.a A = Atoms K
4 pexmidlem.p + ˙ = + 𝑃 K
5 pexmidlem.o ˙ = 𝑃 K
6 pexmidlem.m M = X + ˙ p
7 simpl1 K HL X A p A X q ˙ X M K HL
8 7 hllatd K HL X A p A X q ˙ X M K Lat
9 simpl2 K HL X A p A X q ˙ X M X A
10 simpl3 K HL X A p A X q ˙ X M p A
11 simprl K HL X A p A X q ˙ X M X
12 inss2 ˙ X M M
13 12 sseli q ˙ X M q M
14 13 6 eleqtrdi q ˙ X M q X + ˙ p
15 14 ad2antll K HL X A p A X q ˙ X M q X + ˙ p
16 1 2 3 4 elpaddatiN K Lat X A p A X q X + ˙ p r X q ˙ r ˙ p
17 8 9 10 11 15 16 syl32anc K HL X A p A X q ˙ X M r X q ˙ r ˙ p
18 simp1 K HL X A p A X q ˙ X M r X q ˙ r ˙ p K HL X A p A
19 simp3l K HL X A p A X q ˙ X M r X q ˙ r ˙ p r X
20 inss1 ˙ X M ˙ X
21 simp2r K HL X A p A X q ˙ X M r X q ˙ r ˙ p q ˙ X M
22 20 21 sseldi K HL X A p A X q ˙ X M r X q ˙ r ˙ p q ˙ X
23 simp3r K HL X A p A X q ˙ X M r X q ˙ r ˙ p q ˙ r ˙ p
24 1 2 3 4 5 6 pexmidlem3N K HL X A p A r X q ˙ X q ˙ r ˙ p p X + ˙ ˙ X
25 18 19 22 23 24 syl121anc K HL X A p A X q ˙ X M r X q ˙ r ˙ p p X + ˙ ˙ X
26 25 3expia K HL X A p A X q ˙ X M r X q ˙ r ˙ p p X + ˙ ˙ X
27 26 expd K HL X A p A X q ˙ X M r X q ˙ r ˙ p p X + ˙ ˙ X
28 27 rexlimdv K HL X A p A X q ˙ X M r X q ˙ r ˙ p p X + ˙ ˙ X
29 17 28 mpd K HL X A p A X q ˙ X M p X + ˙ ˙ X