Metamath Proof Explorer


Theorem lhpat

Description: Create an atom under a co-atom. Part of proof of Lemma B in Crawley p. 112. (Contributed by NM, 23-May-2012)

Ref Expression
Hypotheses lhpat.l ˙=K
lhpat.j ˙=joinK
lhpat.m ˙=meetK
lhpat.a A=AtomsK
lhpat.h H=LHypK
Assertion lhpat KHLWHPA¬P˙WQAPQP˙Q˙WA

Proof

Step Hyp Ref Expression
1 lhpat.l ˙=K
2 lhpat.j ˙=joinK
3 lhpat.m ˙=meetK
4 lhpat.a A=AtomsK
5 lhpat.h H=LHypK
6 simp1l KHLWHPA¬P˙WQAPQKHL
7 simp2l KHLWHPA¬P˙WQAPQPA
8 simp3l KHLWHPA¬P˙WQAPQQA
9 simp1r KHLWHPA¬P˙WQAPQWH
10 eqid BaseK=BaseK
11 10 5 lhpbase WHWBaseK
12 9 11 syl KHLWHPA¬P˙WQAPQWBaseK
13 simp3r KHLWHPA¬P˙WQAPQPQ
14 eqid 1.K=1.K
15 eqid K=K
16 14 15 5 lhp1cvr KHLWHWK1.K
17 16 3ad2ant1 KHLWHPA¬P˙WQAPQWK1.K
18 simp2r KHLWHPA¬P˙WQAPQ¬P˙W
19 10 1 2 3 14 15 4 1cvrat KHLPAQAWBaseKPQWK1.K¬P˙WP˙Q˙WA
20 6 7 8 12 13 17 18 19 syl133anc KHLWHPA¬P˙WQAPQP˙Q˙WA