Metamath Proof Explorer


Theorem cdlemg1ci2

Description: Any function of the form of the function constructed for cdleme is a translation. TODO: Fix comment. (Contributed by NM, 18-Apr-2013)

Ref Expression
Hypotheses cdlemg1c.l ˙=K
cdlemg1c.a A=AtomsK
cdlemg1c.h H=LHypK
cdlemg1c.t T=LTrnKW
Assertion cdlemg1ci2 KHLWHPA¬P˙WQA¬Q˙WF=ιfT|fP=QFT

Proof

Step Hyp Ref Expression
1 cdlemg1c.l ˙=K
2 cdlemg1c.a A=AtomsK
3 cdlemg1c.h H=LHypK
4 cdlemg1c.t T=LTrnKW
5 simpr KHLWHPA¬P˙WQA¬Q˙WF=ιfT|fP=QF=ιfT|fP=Q
6 eqid ιfT|fP=Q=ιfT|fP=Q
7 1 2 3 4 6 ltrniotacl KHLWHPA¬P˙WQA¬Q˙WιfT|fP=QT
8 7 adantr KHLWHPA¬P˙WQA¬Q˙WF=ιfT|fP=QιfT|fP=QT
9 5 8 eqeltrd KHLWHPA¬P˙WQA¬Q˙WF=ιfT|fP=QFT