Metamath Proof Explorer


Theorem lhpmcvr6N

Description: Specialization of lhpmcvr2 . (Contributed by NM, 6-Apr-2014) (New usage is discouraged.)

Ref Expression
Hypotheses lhpmcvr2.b B = Base K
lhpmcvr2.l ˙ = K
lhpmcvr2.j ˙ = join K
lhpmcvr2.m ˙ = meet K
lhpmcvr2.a A = Atoms K
lhpmcvr2.h H = LHyp K
Assertion lhpmcvr6N K HL W H X B ¬ X ˙ W Y B X ˙ Y ˙ W p A ¬ p ˙ W ¬ p ˙ Y p ˙ X

Proof

Step Hyp Ref Expression
1 lhpmcvr2.b B = Base K
2 lhpmcvr2.l ˙ = K
3 lhpmcvr2.j ˙ = join K
4 lhpmcvr2.m ˙ = meet K
5 lhpmcvr2.a A = Atoms K
6 lhpmcvr2.h H = LHyp K
7 1 2 3 4 5 6 lhpmcvr5N K HL W H X B ¬ X ˙ W Y B X ˙ Y ˙ W p A ¬ p ˙ W ¬ p ˙ Y p ˙ X ˙ W = X
8 simp31 K HL W H X B ¬ X ˙ W Y B X ˙ Y ˙ W p A ¬ p ˙ W ¬ p ˙ Y p ˙ X ˙ W = X ¬ p ˙ W
9 simp32 K HL W H X B ¬ X ˙ W Y B X ˙ Y ˙ W p A ¬ p ˙ W ¬ p ˙ Y p ˙ X ˙ W = X ¬ p ˙ Y
10 simp11l K HL W H X B ¬ X ˙ W Y B X ˙ Y ˙ W p A ¬ p ˙ W ¬ p ˙ Y p ˙ X ˙ W = X K HL
11 10 hllatd K HL W H X B ¬ X ˙ W Y B X ˙ Y ˙ W p A ¬ p ˙ W ¬ p ˙ Y p ˙ X ˙ W = X K Lat
12 1 5 atbase p A p B
13 12 3ad2ant2 K HL W H X B ¬ X ˙ W Y B X ˙ Y ˙ W p A ¬ p ˙ W ¬ p ˙ Y p ˙ X ˙ W = X p B
14 simp12l K HL W H X B ¬ X ˙ W Y B X ˙ Y ˙ W p A ¬ p ˙ W ¬ p ˙ Y p ˙ X ˙ W = X X B
15 simp11r K HL W H X B ¬ X ˙ W Y B X ˙ Y ˙ W p A ¬ p ˙ W ¬ p ˙ Y p ˙ X ˙ W = X W H
16 1 6 lhpbase W H W B
17 15 16 syl K HL W H X B ¬ X ˙ W Y B X ˙ Y ˙ W p A ¬ p ˙ W ¬ p ˙ Y p ˙ X ˙ W = X W B
18 1 4 latmcl K Lat X B W B X ˙ W B
19 11 14 17 18 syl3anc K HL W H X B ¬ X ˙ W Y B X ˙ Y ˙ W p A ¬ p ˙ W ¬ p ˙ Y p ˙ X ˙ W = X X ˙ W B
20 1 2 3 latlej1 K Lat p B X ˙ W B p ˙ p ˙ X ˙ W
21 11 13 19 20 syl3anc K HL W H X B ¬ X ˙ W Y B X ˙ Y ˙ W p A ¬ p ˙ W ¬ p ˙ Y p ˙ X ˙ W = X p ˙ p ˙ X ˙ W
22 simp33 K HL W H X B ¬ X ˙ W Y B X ˙ Y ˙ W p A ¬ p ˙ W ¬ p ˙ Y p ˙ X ˙ W = X p ˙ X ˙ W = X
23 21 22 breqtrd K HL W H X B ¬ X ˙ W Y B X ˙ Y ˙ W p A ¬ p ˙ W ¬ p ˙ Y p ˙ X ˙ W = X p ˙ X
24 8 9 23 3jca K HL W H X B ¬ X ˙ W Y B X ˙ Y ˙ W p A ¬ p ˙ W ¬ p ˙ Y p ˙ X ˙ W = X ¬ p ˙ W ¬ p ˙ Y p ˙ X
25 24 3expia K HL W H X B ¬ X ˙ W Y B X ˙ Y ˙ W p A ¬ p ˙ W ¬ p ˙ Y p ˙ X ˙ W = X ¬ p ˙ W ¬ p ˙ Y p ˙ X
26 25 reximdva K HL W H X B ¬ X ˙ W Y B X ˙ Y ˙ W p A ¬ p ˙ W ¬ p ˙ Y p ˙ X ˙ W = X p A ¬ p ˙ W ¬ p ˙ Y p ˙ X
27 7 26 mpd K HL W H X B ¬ X ˙ W Y B X ˙ Y ˙ W p A ¬ p ˙ W ¬ p ˙ Y p ˙ X