Metamath Proof Explorer


Theorem cdleme21at

Description: Part of proof of Lemma E in Crawley p. 115. (Contributed by NM, 29-Nov-2012)

Ref Expression
Hypotheses cdleme21.l ˙=K
cdleme21.j ˙=joinK
cdleme21.m ˙=meetK
cdleme21.a A=AtomsK
cdleme21.h H=LHypK
cdleme21.u U=P˙Q˙W
Assertion cdleme21at KHLWHPA¬P˙WQASAPQ¬S˙P˙QU˙S˙TzAP˙z=S˙zTz

Proof

Step Hyp Ref Expression
1 cdleme21.l ˙=K
2 cdleme21.j ˙=joinK
3 cdleme21.m ˙=meetK
4 cdleme21.a A=AtomsK
5 cdleme21.h H=LHypK
6 cdleme21.u U=P˙Q˙W
7 1 2 3 4 5 6 cdleme21c KHLWHPA¬P˙WQASAPQ¬S˙P˙QzAP˙z=S˙z¬U˙S˙z
8 7 3adant2r KHLWHPA¬P˙WQASAPQ¬S˙P˙QU˙S˙TzAP˙z=S˙z¬U˙S˙z
9 simp2r KHLWHPA¬P˙WQASAPQ¬S˙P˙QU˙S˙TzAP˙z=S˙zU˙S˙T
10 oveq2 T=zS˙T=S˙z
11 10 breq2d T=zU˙S˙TU˙S˙z
12 9 11 syl5ibcom KHLWHPA¬P˙WQASAPQ¬S˙P˙QU˙S˙TzAP˙z=S˙zT=zU˙S˙z
13 12 necon3bd KHLWHPA¬P˙WQASAPQ¬S˙P˙QU˙S˙TzAP˙z=S˙z¬U˙S˙zTz
14 8 13 mpd KHLWHPA¬P˙WQASAPQ¬S˙P˙QU˙S˙TzAP˙z=S˙zTz