Metamath Proof Explorer


Theorem cdlemk26-3

Description: Part of proof of Lemma K of Crawley p. 118. Eliminate the x requirements from cdlemk25-3 . (Contributed by NM, 10-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 cdlemk26-3 K HL W H F T D T N T G T C T P A ¬ P ˙ W R F = R N F I B D I B G I B C I B R G R C R C R F R D R F R G R D D Y G P = C Y G P

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 simp11l K HL W H F T D T N T G T C T P A ¬ P ˙ W R F = R N F I B D I B G I B C I B R G R C R C R F R D R F R G R D K HL
12 simp11r K HL W H F T D T N T G T C T P A ¬ P ˙ W R F = R N F I B D I B G I B C I B R G R C R C R F R D R F R G R D W H
13 1 6 7 8 cdlemftr3 K HL W H x T x I B R x R F R x R G R x R D
14 11 12 13 syl2anc K HL W H F T D T N T G T C T P A ¬ P ˙ W R F = R N F I B D I B G I B C I B R G R C R C R F R D R F R G R D x T x I B R x R F R x R G R x R D
15 simp111 K HL W H F T D T N T G T C T P A ¬ P ˙ W R F = R N F I B D I B G I B C I B R G R C R C R F R D R F R G R D x T x I B R x R F R x R G R x R D K HL W H
16 simp112 K HL W H F T D T N T G T C T P A ¬ P ˙ W R F = R N F I B D I B G I B C I B R G R C R C R F R D R F R G R D x T x I B R x R F R x R G R x R D F T D T N T
17 simp13l K HL W H F T D T N T G T C T P A ¬ P ˙ W R F = R N F I B D I B G I B C I B R G R C R C R F R D R F R G R D G T
18 17 3ad2ant1 K HL W H F T D T N T G T C T P A ¬ P ˙ W R F = R N F I B D I B G I B C I B R G R C R C R F R D R F R G R D x T x I B R x R F R x R G R x R D G T
19 simp13r K HL W H F T D T N T G T C T P A ¬ P ˙ W R F = R N F I B D I B G I B C I B R G R C R C R F R D R F R G R D C T
20 19 3ad2ant1 K HL W H F T D T N T G T C T P A ¬ P ˙ W R F = R N F I B D I B G I B C I B R G R C R C R F R D R F R G R D x T x I B R x R F R x R G R x R D C T
21 simp2 K HL W H F T D T N T G T C T P A ¬ P ˙ W R F = R N F I B D I B G I B C I B R G R C R C R F R D R F R G R D x T x I B R x R F R x R G R x R D x T
22 18 20 21 3jca K HL W H F T D T N T G T C T P A ¬ P ˙ W R F = R N F I B D I B G I B C I B R G R C R C R F R D R F R G R D x T x I B R x R F R x R G R x R D G T C T x T
23 simp121 K HL W H F T D T N T G T C T P A ¬ P ˙ W R F = R N F I B D I B G I B C I B R G R C R C R F R D R F R G R D x T x I B R x R F R x R G R x R D P A ¬ P ˙ W
24 simp122 K HL W H F T D T N T G T C T P A ¬ P ˙ W R F = R N F I B D I B G I B C I B R G R C R C R F R D R F R G R D x T x I B R x R F R x R G R x R D R F = R N F I B D I B
25 simp23l K HL W H F T D T N T G T C T P A ¬ P ˙ W R F = R N F I B D I B G I B C I B R G R C R C R F R D R F R G R D G I B
26 25 3ad2ant1 K HL W H F T D T N T G T C T P A ¬ P ˙ W R F = R N F I B D I B G I B C I B R G R C R C R F R D R F R G R D x T x I B R x R F R x R G R x R D G I B
27 simp23r K HL W H F T D T N T G T C T P A ¬ P ˙ W R F = R N F I B D I B G I B C I B R G R C R C R F R D R F R G R D C I B
28 27 3ad2ant1 K HL W H F T D T N T G T C T P A ¬ P ˙ W R F = R N F I B D I B G I B C I B R G R C R C R F R D R F R G R D x T x I B R x R F R x R G R x R D C I B
29 simp3l K HL W H F T D T N T G T C T P A ¬ P ˙ W R F = R N F I B D I B G I B C I B R G R C R C R F R D R F R G R D x T x I B R x R F R x R G R x R D x I B
30 26 28 29 3jca K HL W H F T D T N T G T C T P A ¬ P ˙ W R F = R N F I B D I B G I B C I B R G R C R C R F R D R F R G R D x T x I B R x R F R x R G R x R D G I B C I B x I B
31 simp13l K HL W H F T D T N T G T C T P A ¬ P ˙ W R F = R N F I B D I B G I B C I B R G R C R C R F R D R F R G R D x T x I B R x R F R x R G R x R D R G R C R C R F R D R F
32 simp13r K HL W H F T D T N T G T C T P A ¬ P ˙ W R F = R N F I B D I B G I B C I B R G R C R C R F R D R F R G R D x T x I B R x R F R x R G R x R D R G R D
33 simp3r3 K HL W H F T D T N T G T C T P A ¬ P ˙ W R F = R N F I B D I B G I B C I B R G R C R C R F R D R F R G R D x T x I B R x R F R x R G R x R D R x R D
34 simp3r1 K HL W H F T D T N T G T C T P A ¬ P ˙ W R F = R N F I B D I B G I B C I B R G R C R C R F R D R F R G R D x T x I B R x R F R x R G R x R D R x R F
35 simp3r2 K HL W H F T D T N T G T C T P A ¬ P ˙ W R F = R N F I B D I B G I B C I B R G R C R C R F R D R F R G R D x T x I B R x R F R x R G R x R D R x R G
36 35 necomd K HL W H F T D T N T G T C T P A ¬ P ˙ W R F = R N F I B D I B G I B C I B R G R C R C R F R D R F R G R D x T x I B R x R F R x R G R x R D R G R x
37 33 34 36 3jca K HL W H F T D T N T G T C T P A ¬ P ˙ W R F = R N F I B D I B G I B C I B R G R C R C R F R D R F R G R D x T x I B R x R F R x R G R x R D R x R D R x R F R G R x
38 1 2 3 4 5 6 7 8 9 10 cdlemk25-3 K HL W H F T D T N T G T C T x T P A ¬ P ˙ W R F = R N F I B D I B G I B C I B x I B R G R C R C R F R D R F R G R D R x R D R x R F R G R x D Y G P = C Y G P
39 15 16 22 23 24 30 31 32 37 38 syl333anc K HL W H F T D T N T G T C T P A ¬ P ˙ W R F = R N F I B D I B G I B C I B R G R C R C R F R D R F R G R D x T x I B R x R F R x R G R x R D D Y G P = C Y G P
40 39 rexlimdv3a K HL W H F T D T N T G T C T P A ¬ P ˙ W R F = R N F I B D I B G I B C I B R G R C R C R F R D R F R G R D x T x I B R x R F R x R G R x R D D Y G P = C Y G P
41 14 40 mpd K HL W H F T D T N T G T C T P A ¬ P ˙ W R F = R N F I B D I B G I B C I B R G R C R C R F R D R F R G R D D Y G P = C Y G P