Metamath Proof Explorer


Theorem cdleme02N

Description: Part of proof of Lemma E in Crawley p. 113. (Contributed by NM, 9-Nov-2012) (New usage is discouraged.)

Ref Expression
Hypotheses cdleme0.l ˙=K
cdleme0.j ˙=joinK
cdleme0.m ˙=meetK
cdleme0.a A=AtomsK
cdleme0.h H=LHypK
cdleme0.u U=P˙Q˙W
Assertion cdleme02N KHLWHPA¬P˙WQA¬Q˙WPQP˙U=Q˙UU˙W

Proof

Step Hyp Ref Expression
1 cdleme0.l ˙=K
2 cdleme0.j ˙=joinK
3 cdleme0.m ˙=meetK
4 cdleme0.a A=AtomsK
5 cdleme0.h H=LHypK
6 cdleme0.u U=P˙Q˙W
7 1 2 3 4 5 6 cdleme01N KHLWHPA¬P˙WQA¬Q˙WPQUPUQU˙P˙QU˙W
8 simp1l KHLWHPA¬P˙WQA¬Q˙WPQKHL
9 hlcvl KHLKCvLat
10 8 9 syl KHLWHPA¬P˙WQA¬Q˙WPQKCvLat
11 simp2ll KHLWHPA¬P˙WQA¬Q˙WPQPA
12 simp2rl KHLWHPA¬P˙WQA¬Q˙WPQQA
13 simp1 KHLWHPA¬P˙WQA¬Q˙WPQKHLWH
14 simp2l KHLWHPA¬P˙WQA¬Q˙WPQPA¬P˙W
15 simp3 KHLWHPA¬P˙WQA¬Q˙WPQPQ
16 1 2 3 4 5 6 lhpat2 KHLWHPA¬P˙WQAPQUA
17 13 14 12 15 16 syl112anc KHLWHPA¬P˙WQA¬Q˙WPQUA
18 4 1 2 cvlsupr2 KCvLatPAQAUAPQP˙U=Q˙UUPUQU˙P˙Q
19 10 11 12 17 15 18 syl131anc KHLWHPA¬P˙WQA¬Q˙WPQP˙U=Q˙UUPUQU˙P˙Q
20 19 anbi1d KHLWHPA¬P˙WQA¬Q˙WPQP˙U=Q˙UU˙WUPUQU˙P˙QU˙W
21 7 20 mpbird KHLWHPA¬P˙WQA¬Q˙WPQP˙U=Q˙UU˙W