Metamath Proof Explorer


Theorem cdlemk26b-3

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

Ref Expression
Hypotheses cdlemk3.b B = Base K
cdlemk3.l ˙ = K
cdlemk3.j ˙ = join K
cdlemk3.m ˙ = meet K
cdlemk3.a A = Atoms K
cdlemk3.h H = LHyp K
cdlemk3.t T = LTrn K W
cdlemk3.r R = trL K W
cdlemk3.s S = f T ι i T | i P = P ˙ R f ˙ N P ˙ R f F -1
cdlemk3.u1 Y = d T , e T ι j T | j P = P ˙ R e ˙ S d P ˙ R e d -1
Assertion cdlemk26b-3 K HL W H F T F I B N T G T G I B R F = R N P A ¬ P ˙ W x T x I B R x R F R x R G x Y G T

Proof

Step Hyp Ref Expression
1 cdlemk3.b B = Base K
2 cdlemk3.l ˙ = K
3 cdlemk3.j ˙ = join K
4 cdlemk3.m ˙ = meet K
5 cdlemk3.a A = Atoms K
6 cdlemk3.h H = LHyp K
7 cdlemk3.t T = LTrn K W
8 cdlemk3.r R = trL K W
9 cdlemk3.s S = f T ι i T | i P = P ˙ R f ˙ N P ˙ R f F -1
10 cdlemk3.u1 Y = d T , e T ι j T | j P = P ˙ R e ˙ S d P ˙ R e d -1
11 simpl1 K HL W H F T F I B N T G T G I B R F = R N P A ¬ P ˙ W K HL W H
12 1 6 7 8 cdlemftr2 K HL W H x T x I B R x R F R x R G
13 11 12 syl K HL W H F T F I B N T G T G I B R F = R N P A ¬ P ˙ W x T x I B R x R F R x R G
14 simp3r K HL W H F T F I B N T G T G I B R F = R N P A ¬ P ˙ W x T x I B R x R F R x R G x I B R x R F R x R G
15 simp11 K HL W H F T F I B N T G T G I B R F = R N P A ¬ P ˙ W x T x I B R x R F R x R G K HL W H
16 simp133 K HL W H F T F I B N T G T G I B R F = R N P A ¬ P ˙ W x T x I B R x R F R x R G R F = R N
17 simp131 K HL W H F T F I B N T G T G I B R F = R N P A ¬ P ˙ W x T x I B R x R F R x R G G T
18 simp121 K HL W H F T F I B N T G T G I B R F = R N P A ¬ P ˙ W x T x I B R x R F R x R G F T
19 simp3l K HL W H F T F I B N T G T G I B R F = R N P A ¬ P ˙ W x T x I B R x R F R x R G x T
20 simp123 K HL W H F T F I B N T G T G I B R F = R N P A ¬ P ˙ W x T x I B R x R F R x R G N T
21 simp3r2 K HL W H F T F I B N T G T G I B R F = R N P A ¬ P ˙ W x T x I B R x R F R x R G R x R F
22 simp3r3 K HL W H F T F I B N T G T G I B R F = R N P A ¬ P ˙ W x T x I B R x R F R x R G R x R G
23 21 22 jca K HL W H F T F I B N T G T G I B R F = R N P A ¬ P ˙ W x T x I B R x R F R x R G R x R F R x R G
24 simp122 K HL W H F T F I B N T G T G I B R F = R N P A ¬ P ˙ W x T x I B R x R F R x R G F I B
25 simp132 K HL W H F T F I B N T G T G I B R F = R N P A ¬ P ˙ W x T x I B R x R F R x R G G I B
26 simp3r1 K HL W H F T F I B N T G T G I B R F = R N P A ¬ P ˙ W x T x I B R x R F R x R G x I B
27 24 25 26 3jca K HL W H F T F I B N T G T G I B R F = R N P A ¬ P ˙ W x T x I B R x R F R x R G F I B G I B x I B
28 simp2 K HL W H F T F I B N T G T G I B R F = R N P A ¬ P ˙ W x T x I B R x R F R x R G P A ¬ P ˙ W
29 1 2 3 4 5 6 7 8 9 10 cdlemkuel-3 K HL W H R F = R N G T F T x T N T R x R F R x R G F I B G I B x I B P A ¬ P ˙ W x Y G T
30 15 16 17 18 19 20 23 27 28 29 syl333anc K HL W H F T F I B N T G T G I B R F = R N P A ¬ P ˙ W x T x I B R x R F R x R G x Y G T
31 14 30 jca K HL W H F T F I B N T G T G I B R F = R N P A ¬ P ˙ W x T x I B R x R F R x R G x I B R x R F R x R G x Y G T
32 31 3expia K HL W H F T F I B N T G T G I B R F = R N P A ¬ P ˙ W x T x I B R x R F R x R G x I B R x R F R x R G x Y G T
33 32 expd K HL W H F T F I B N T G T G I B R F = R N P A ¬ P ˙ W x T x I B R x R F R x R G x I B R x R F R x R G x Y G T
34 33 reximdvai K HL W H F T F I B N T G T G I B R F = R N P A ¬ P ˙ W x T x I B R x R F R x R G x T x I B R x R F R x R G x Y G T
35 13 34 mpd K HL W H F T F I B N T G T G I B R F = R N P A ¬ P ˙ W x T x I B R x R F R x R G x Y G T