Metamath Proof Explorer


Theorem cdlemg4f

Description: TODO: FIX COMMENT. (Contributed by NM, 25-Apr-2013)

Ref Expression
Hypotheses cdlemg4.l ˙=K
cdlemg4.a A=AtomsK
cdlemg4.h H=LHypK
cdlemg4.t T=LTrnKW
cdlemg4.r R=trLKW
cdlemg4.j ˙=joinK
cdlemg4b.v V=RG
cdlemg4.m ˙=meetK
Assertion cdlemg4f KHLWHPA¬P˙WQA¬Q˙WFTGT¬Q˙P˙VFGP=PFGQ=Q˙V˙P˙P˙Q˙W

Proof

Step Hyp Ref Expression
1 cdlemg4.l ˙=K
2 cdlemg4.a A=AtomsK
3 cdlemg4.h H=LHypK
4 cdlemg4.t T=LTrnKW
5 cdlemg4.r R=trLKW
6 cdlemg4.j ˙=joinK
7 cdlemg4b.v V=RG
8 cdlemg4.m ˙=meetK
9 1 2 3 4 5 6 7 8 cdlemg4e KHLWHPA¬P˙WQA¬Q˙WFTGT¬Q˙P˙VFGP=PFGQ=GQ˙RF˙FGP˙GP˙GQ˙W
10 simp1 KHLWHPA¬P˙WQA¬Q˙WFTGT¬Q˙P˙VFGP=PKHLWH
11 simp21 KHLWHPA¬P˙WQA¬Q˙WFTGT¬Q˙P˙VFGP=PPA¬P˙W
12 simp23 KHLWHPA¬P˙WQA¬Q˙WFTGT¬Q˙P˙VFGP=PFT
13 simp31 KHLWHPA¬P˙WQA¬Q˙WFTGT¬Q˙P˙VFGP=PGT
14 simp33 KHLWHPA¬P˙WQA¬Q˙WFTGT¬Q˙P˙VFGP=PFGP=P
15 1 2 3 4 5 cdlemg4a KHLWHPA¬P˙WFTGTFGP=PRF=RG
16 10 11 12 13 14 15 syl131anc KHLWHPA¬P˙WQA¬Q˙WFTGT¬Q˙P˙VFGP=PRF=RG
17 7 16 eqtr4id KHLWHPA¬P˙WQA¬Q˙WFTGT¬Q˙P˙VFGP=PV=RF
18 17 oveq2d KHLWHPA¬P˙WQA¬Q˙WFTGT¬Q˙P˙VFGP=PGQ˙V=GQ˙RF
19 simp22 KHLWHPA¬P˙WQA¬Q˙WFTGT¬Q˙P˙VFGP=PQA¬Q˙W
20 1 2 3 4 5 6 7 cdlemg4b12 KHLWHQA¬Q˙WGTGQ˙V=Q˙V
21 10 19 13 20 syl3anc KHLWHPA¬P˙WQA¬Q˙WFTGT¬Q˙P˙VFGP=PGQ˙V=Q˙V
22 18 21 eqtr3d KHLWHPA¬P˙WQA¬Q˙WFTGT¬Q˙P˙VFGP=PGQ˙RF=Q˙V
23 eqid P˙Q˙W=P˙Q˙W
24 3 4 1 6 2 8 23 cdlemg2m KHLWHPA¬P˙WQA¬Q˙WGTGP˙GQ˙W=P˙Q˙W
25 10 11 19 13 24 syl121anc KHLWHPA¬P˙WQA¬Q˙WFTGT¬Q˙P˙VFGP=PGP˙GQ˙W=P˙Q˙W
26 14 25 oveq12d KHLWHPA¬P˙WQA¬Q˙WFTGT¬Q˙P˙VFGP=PFGP˙GP˙GQ˙W=P˙P˙Q˙W
27 22 26 oveq12d KHLWHPA¬P˙WQA¬Q˙WFTGT¬Q˙P˙VFGP=PGQ˙RF˙FGP˙GP˙GQ˙W=Q˙V˙P˙P˙Q˙W
28 9 27 eqtrd KHLWHPA¬P˙WQA¬Q˙WFTGT¬Q˙P˙VFGP=PFGQ=Q˙V˙P˙P˙Q˙W