Metamath Proof Explorer


Theorem cdlemg2cN

Description: Any translation belongs to the set of functions constructed for cdleme . TODO: Fix comment. (Contributed by NM, 22-Apr-2013) (New usage is discouraged.)

Ref Expression
Hypotheses cdlemg2.b B=BaseK
cdlemg2.l ˙=K
cdlemg2.j ˙=joinK
cdlemg2.m ˙=meetK
cdlemg2.a A=AtomsK
cdlemg2.h H=LHypK
cdlemg2.t T=LTrnKW
cdlemg2.u U=P˙Q˙W
cdlemg2.d D=t˙U˙Q˙P˙t˙W
cdlemg2.e E=P˙Q˙D˙s˙t˙W
cdlemg2.g G=xBifPQ¬x˙WιzB|sA¬s˙Ws˙x˙W=xz=ifs˙P˙QιyB|tA¬t˙W¬t˙P˙Qy=Es/tD˙x˙Wx
Assertion cdlemg2cN KHLWHPA¬P˙WQA¬Q˙WFP=QFTF=G

Proof

Step Hyp Ref Expression
1 cdlemg2.b B=BaseK
2 cdlemg2.l ˙=K
3 cdlemg2.j ˙=joinK
4 cdlemg2.m ˙=meetK
5 cdlemg2.a A=AtomsK
6 cdlemg2.h H=LHypK
7 cdlemg2.t T=LTrnKW
8 cdlemg2.u U=P˙Q˙W
9 cdlemg2.d D=t˙U˙Q˙P˙t˙W
10 cdlemg2.e E=P˙Q˙D˙s˙t˙W
11 cdlemg2.g G=xBifPQ¬x˙WιzB|sA¬s˙Ws˙x˙W=xz=ifs˙P˙QιyB|tA¬t˙W¬t˙P˙Qy=Es/tD˙x˙Wx
12 2 5 6 7 cdlemg1cN KHLWHPA¬P˙WQA¬Q˙WFP=QFTF=ιfT|fP=Q
13 eqid ιfT|fP=Q=ιfT|fP=Q
14 1 2 3 4 5 6 8 9 10 11 7 13 cdlemg1b2 KHLWHPA¬P˙WQA¬Q˙WιfT|fP=Q=G
15 14 adantr KHLWHPA¬P˙WQA¬Q˙WFP=QιfT|fP=Q=G
16 15 eqeq2d KHLWHPA¬P˙WQA¬Q˙WFP=QF=ιfT|fP=QF=G
17 12 16 bitrd KHLWHPA¬P˙WQA¬Q˙WFP=QFTF=G