Metamath Proof Explorer


Theorem cdleme50ex

Description: Part of Lemma E in Crawley p. 113. TODO: fix comment. (Contributed by NM, 11-Apr-2013)

Ref Expression
Hypotheses cdleme.l ˙=K
cdleme.a A=AtomsK
cdleme.h H=LHypK
cdleme.t T=LTrnKW
Assertion cdleme50ex KHLWHPA¬P˙WQA¬Q˙WfTfP=Q

Proof

Step Hyp Ref Expression
1 cdleme.l ˙=K
2 cdleme.a A=AtomsK
3 cdleme.h H=LHypK
4 cdleme.t T=LTrnKW
5 eqid BaseK=BaseK
6 eqid joinK=joinK
7 eqid meetK=meetK
8 eqid PjoinKQmeetKW=PjoinKQmeetKW
9 eqid tjoinKPjoinKQmeetKWmeetKQjoinKPjoinKtmeetKW=tjoinKPjoinKQmeetKWmeetKQjoinKPjoinKtmeetKW
10 eqid PjoinKQmeetKtjoinKPjoinKQmeetKWmeetKQjoinKPjoinKtmeetKWjoinKsjoinKtmeetKW=PjoinKQmeetKtjoinKPjoinKQmeetKWmeetKQjoinKPjoinKtmeetKWjoinKsjoinKtmeetKW
11 eqid xBaseKifPQ¬x˙WιzBaseK|sA¬s˙WsjoinKxmeetKW=xz=ifs˙PjoinKQιyBaseK|tA¬t˙W¬t˙PjoinKQy=PjoinKQmeetKtjoinKPjoinKQmeetKWmeetKQjoinKPjoinKtmeetKWjoinKsjoinKtmeetKWs/ttjoinKPjoinKQmeetKWmeetKQjoinKPjoinKtmeetKWjoinKxmeetKWx=xBaseKifPQ¬x˙WιzBaseK|sA¬s˙WsjoinKxmeetKW=xz=ifs˙PjoinKQιyBaseK|tA¬t˙W¬t˙PjoinKQy=PjoinKQmeetKtjoinKPjoinKQmeetKWmeetKQjoinKPjoinKtmeetKWjoinKsjoinKtmeetKWs/ttjoinKPjoinKQmeetKWmeetKQjoinKPjoinKtmeetKWjoinKxmeetKWx
12 5 1 6 7 2 3 8 9 10 11 4 cdleme50ltrn KHLWHPA¬P˙WQA¬Q˙WxBaseKifPQ¬x˙WιzBaseK|sA¬s˙WsjoinKxmeetKW=xz=ifs˙PjoinKQιyBaseK|tA¬t˙W¬t˙PjoinKQy=PjoinKQmeetKtjoinKPjoinKQmeetKWmeetKQjoinKPjoinKtmeetKWjoinKsjoinKtmeetKWs/ttjoinKPjoinKQmeetKWmeetKQjoinKPjoinKtmeetKWjoinKxmeetKWxT
13 5 1 6 7 2 3 8 9 10 11 cdleme17d KHLWHPA¬P˙WQA¬Q˙WxBaseKifPQ¬x˙WιzBaseK|sA¬s˙WsjoinKxmeetKW=xz=ifs˙PjoinKQιyBaseK|tA¬t˙W¬t˙PjoinKQy=PjoinKQmeetKtjoinKPjoinKQmeetKWmeetKQjoinKPjoinKtmeetKWjoinKsjoinKtmeetKWs/ttjoinKPjoinKQmeetKWmeetKQjoinKPjoinKtmeetKWjoinKxmeetKWxP=Q
14 fveq1 f=xBaseKifPQ¬x˙WιzBaseK|sA¬s˙WsjoinKxmeetKW=xz=ifs˙PjoinKQιyBaseK|tA¬t˙W¬t˙PjoinKQy=PjoinKQmeetKtjoinKPjoinKQmeetKWmeetKQjoinKPjoinKtmeetKWjoinKsjoinKtmeetKWs/ttjoinKPjoinKQmeetKWmeetKQjoinKPjoinKtmeetKWjoinKxmeetKWxfP=xBaseKifPQ¬x˙WιzBaseK|sA¬s˙WsjoinKxmeetKW=xz=ifs˙PjoinKQιyBaseK|tA¬t˙W¬t˙PjoinKQy=PjoinKQmeetKtjoinKPjoinKQmeetKWmeetKQjoinKPjoinKtmeetKWjoinKsjoinKtmeetKWs/ttjoinKPjoinKQmeetKWmeetKQjoinKPjoinKtmeetKWjoinKxmeetKWxP
15 14 eqeq1d f=xBaseKifPQ¬x˙WιzBaseK|sA¬s˙WsjoinKxmeetKW=xz=ifs˙PjoinKQιyBaseK|tA¬t˙W¬t˙PjoinKQy=PjoinKQmeetKtjoinKPjoinKQmeetKWmeetKQjoinKPjoinKtmeetKWjoinKsjoinKtmeetKWs/ttjoinKPjoinKQmeetKWmeetKQjoinKPjoinKtmeetKWjoinKxmeetKWxfP=QxBaseKifPQ¬x˙WιzBaseK|sA¬s˙WsjoinKxmeetKW=xz=ifs˙PjoinKQιyBaseK|tA¬t˙W¬t˙PjoinKQy=PjoinKQmeetKtjoinKPjoinKQmeetKWmeetKQjoinKPjoinKtmeetKWjoinKsjoinKtmeetKWs/ttjoinKPjoinKQmeetKWmeetKQjoinKPjoinKtmeetKWjoinKxmeetKWxP=Q
16 15 rspcev xBaseKifPQ¬x˙WιzBaseK|sA¬s˙WsjoinKxmeetKW=xz=ifs˙PjoinKQιyBaseK|tA¬t˙W¬t˙PjoinKQy=PjoinKQmeetKtjoinKPjoinKQmeetKWmeetKQjoinKPjoinKtmeetKWjoinKsjoinKtmeetKWs/ttjoinKPjoinKQmeetKWmeetKQjoinKPjoinKtmeetKWjoinKxmeetKWxTxBaseKifPQ¬x˙WιzBaseK|sA¬s˙WsjoinKxmeetKW=xz=ifs˙PjoinKQιyBaseK|tA¬t˙W¬t˙PjoinKQy=PjoinKQmeetKtjoinKPjoinKQmeetKWmeetKQjoinKPjoinKtmeetKWjoinKsjoinKtmeetKWs/ttjoinKPjoinKQmeetKWmeetKQjoinKPjoinKtmeetKWjoinKxmeetKWxP=QfTfP=Q
17 12 13 16 syl2anc KHLWHPA¬P˙WQA¬Q˙WfTfP=Q