Metamath Proof Explorer


Theorem cdlemk8

Description: Part of proof of Lemma K of Crawley p. 118. (Contributed by NM, 26-Jun-2013)

Ref Expression
Hypotheses cdlemk.b B=BaseK
cdlemk.l ˙=K
cdlemk.j ˙=joinK
cdlemk.a A=AtomsK
cdlemk.h H=LHypK
cdlemk.t T=LTrnKW
cdlemk.r R=trLKW
cdlemk.m ˙=meetK
Assertion cdlemk8 KHLWHGTXTPA¬P˙WGP˙XP=GP˙RXG-1

Proof

Step Hyp Ref Expression
1 cdlemk.b B=BaseK
2 cdlemk.l ˙=K
3 cdlemk.j ˙=joinK
4 cdlemk.a A=AtomsK
5 cdlemk.h H=LHypK
6 cdlemk.t T=LTrnKW
7 cdlemk.r R=trLKW
8 cdlemk.m ˙=meetK
9 coass XG-1G=XG-1G
10 simp1 KHLWHGTXTPA¬P˙WKHLWH
11 simp2l KHLWHGTXTPA¬P˙WGT
12 1 5 6 ltrn1o KHLWHGTG:B1-1 ontoB
13 10 11 12 syl2anc KHLWHGTXTPA¬P˙WG:B1-1 ontoB
14 f1ococnv1 G:B1-1 ontoBG-1G=IB
15 13 14 syl KHLWHGTXTPA¬P˙WG-1G=IB
16 15 coeq2d KHLWHGTXTPA¬P˙WXG-1G=XIB
17 simp2r KHLWHGTXTPA¬P˙WXT
18 1 5 6 ltrn1o KHLWHXTX:B1-1 ontoB
19 10 17 18 syl2anc KHLWHGTXTPA¬P˙WX:B1-1 ontoB
20 f1of X:B1-1 ontoBX:BB
21 fcoi1 X:BBXIB=X
22 19 20 21 3syl KHLWHGTXTPA¬P˙WXIB=X
23 16 22 eqtrd KHLWHGTXTPA¬P˙WXG-1G=X
24 9 23 eqtrid KHLWHGTXTPA¬P˙WXG-1G=X
25 24 fveq1d KHLWHGTXTPA¬P˙WXG-1GP=XP
26 5 6 ltrncnv KHLWHGTG-1T
27 10 11 26 syl2anc KHLWHGTXTPA¬P˙WG-1T
28 5 6 ltrnco KHLWHXTG-1TXG-1T
29 10 17 27 28 syl3anc KHLWHGTXTPA¬P˙WXG-1T
30 simp3l KHLWHGTXTPA¬P˙WPA
31 2 4 5 6 ltrncoval KHLWHXG-1TGTPAXG-1GP=XG-1GP
32 10 29 11 30 31 syl121anc KHLWHGTXTPA¬P˙WXG-1GP=XG-1GP
33 25 32 eqtr3d KHLWHGTXTPA¬P˙WXP=XG-1GP
34 33 oveq2d KHLWHGTXTPA¬P˙WGP˙XP=GP˙XG-1GP
35 2 4 5 6 ltrnel KHLWHGTPA¬P˙WGPA¬GP˙W
36 35 3adant2r KHLWHGTXTPA¬P˙WGPA¬GP˙W
37 2 3 4 5 6 7 trljat1 KHLWHXG-1TGPA¬GP˙WGP˙RXG-1=GP˙XG-1GP
38 10 29 36 37 syl3anc KHLWHGTXTPA¬P˙WGP˙RXG-1=GP˙XG-1GP
39 34 38 eqtr4d KHLWHGTXTPA¬P˙WGP˙XP=GP˙RXG-1