Metamath Proof Explorer


Theorem cdlemk5a

Description: Part of proof of Lemma K of Crawley p. 118. (Contributed by NM, 3-Jul-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
cdlemk.m ˙ = meet K
Assertion cdlemk5a K HL W H F T G T X T R G R F F I B G I B P A ¬ P ˙ W F P ˙ R F ˙ F P ˙ R G F -1 ˙ X P ˙ R X 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 cdlemk.m ˙ = meet K
9 simp1l K HL W H F T G T X T R G R F F I B G I B P A ¬ P ˙ W K HL
10 simp1r K HL W H F T G T X T R G R F F I B G I B P A ¬ P ˙ W W H
11 simp21 K HL W H F T G T X T R G R F F I B G I B P A ¬ P ˙ W F T
12 simp22 K HL W H F T G T X T R G R F F I B G I B P A ¬ P ˙ W G T
13 simp3 K HL W H F T G T X T R G R F F I B G I B P A ¬ P ˙ W R G R F F I B G I B P A ¬ P ˙ W
14 1 2 3 4 5 6 7 8 cdlemk3 K HL W H F T G T R G R F F I B G I B P A ¬ P ˙ W F P ˙ R F ˙ F P ˙ R G F -1 = F P
15 9 10 11 12 13 14 syl221anc K HL W H F T G T X T R G R F F I B G I B P A ¬ P ˙ W F P ˙ R F ˙ F P ˙ R G F -1 = F P
16 simp23 K HL W H F T G T X T R G R F F I B G I B P A ¬ P ˙ W X T
17 simp33l K HL W H F T G T X T R G R F F I B G I B P A ¬ P ˙ W P A
18 simp33r K HL W H F T G T X T R G R F F I B G I B P A ¬ P ˙ W ¬ P ˙ W
19 1 2 3 4 5 6 7 8 cdlemk4 K HL W H F T X T P A ¬ P ˙ W F P ˙ X P ˙ R X F -1
20 9 10 11 16 17 18 19 syl222anc K HL W H F T G T X T R G R F F I B G I B P A ¬ P ˙ W F P ˙ X P ˙ R X F -1
21 15 20 eqbrtrd K HL W H F T G T X T R G R F F I B G I B P A ¬ P ˙ W F P ˙ R F ˙ F P ˙ R G F -1 ˙ X P ˙ R X F -1