Metamath Proof Explorer


Theorem cdlemk2

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

Ref Expression
Hypotheses cdlemk.b B = Base K
cdlemk.l ˙ = K
cdlemk.j ˙ = join K
cdlemk.a A = Atoms K
cdlemk.h H = LHyp K
cdlemk.t T = LTrn K W
cdlemk.r R = trL K W
Assertion cdlemk2 K HL W H F T G T P A ¬ P ˙ W G P ˙ R G F -1 = F P ˙ R G F -1

Proof

Step Hyp Ref Expression
1 cdlemk.b B = Base K
2 cdlemk.l ˙ = K
3 cdlemk.j ˙ = join K
4 cdlemk.a A = Atoms K
5 cdlemk.h H = LHyp K
6 cdlemk.t T = LTrn K W
7 cdlemk.r R = trL K W
8 simp1 K HL W H F T G T P A ¬ P ˙ W K HL W H
9 simp2r K HL W H F T G T P A ¬ P ˙ W G T
10 simp2l K HL W H F T G T P A ¬ P ˙ W F T
11 5 6 ltrncnv K HL W H F T F -1 T
12 8 10 11 syl2anc K HL W H F T G T P A ¬ P ˙ W F -1 T
13 5 6 ltrnco K HL W H G T F -1 T G F -1 T
14 8 9 12 13 syl3anc K HL W H F T G T P A ¬ P ˙ W G F -1 T
15 2 4 5 6 ltrnel K HL W H F T P A ¬ P ˙ W F P A ¬ F P ˙ W
16 15 3adant2r K HL W H F T G T P A ¬ P ˙ W F P A ¬ F P ˙ W
17 2 3 4 5 6 7 trljat3 K HL W H G F -1 T F P A ¬ F P ˙ W F P ˙ R G F -1 = G F -1 F P ˙ R G F -1
18 8 14 16 17 syl3anc K HL W H F T G T P A ¬ P ˙ W F P ˙ R G F -1 = G F -1 F P ˙ R G F -1
19 simp3l K HL W H F T G T P A ¬ P ˙ W P A
20 2 4 5 6 ltrncoval K HL W H G F -1 T F T P A G F -1 F P = G F -1 F P
21 8 14 10 19 20 syl121anc K HL W H F T G T P A ¬ P ˙ W G F -1 F P = G F -1 F P
22 coass G F -1 F = G F -1 F
23 1 5 6 ltrn1o K HL W H F T F : B 1-1 onto B
24 8 10 23 syl2anc K HL W H F T G T P A ¬ P ˙ W F : B 1-1 onto B
25 f1ococnv1 F : B 1-1 onto B F -1 F = I B
26 24 25 syl K HL W H F T G T P A ¬ P ˙ W F -1 F = I B
27 26 coeq2d K HL W H F T G T P A ¬ P ˙ W G F -1 F = G I B
28 1 5 6 ltrn1o K HL W H G T G : B 1-1 onto B
29 8 9 28 syl2anc K HL W H F T G T P A ¬ P ˙ W G : B 1-1 onto B
30 f1of G : B 1-1 onto B G : B B
31 fcoi1 G : B B G I B = G
32 29 30 31 3syl K HL W H F T G T P A ¬ P ˙ W G I B = G
33 27 32 eqtrd K HL W H F T G T P A ¬ P ˙ W G F -1 F = G
34 22 33 syl5eq K HL W H F T G T P A ¬ P ˙ W G F -1 F = G
35 34 fveq1d K HL W H F T G T P A ¬ P ˙ W G F -1 F P = G P
36 21 35 eqtr3d K HL W H F T G T P A ¬ P ˙ W G F -1 F P = G P
37 36 oveq1d K HL W H F T G T P A ¬ P ˙ W G F -1 F P ˙ R G F -1 = G P ˙ R G F -1
38 18 37 eqtr2d K HL W H F T G T P A ¬ P ˙ W G P ˙ R G F -1 = F P ˙ R G F -1