Metamath Proof Explorer


Theorem cdlemk33N

Description: Part of proof of Lemma K of Crawley p. 118. TODO: fix comment. Part of attempt to simplify hypotheses. TODO: not needed, is embodied in cdlemk34 . (Contributed by NM, 18-Jul-2013) (New usage is discouraged.)

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
cdlemk3.x X = ι z T | b T b I B R b R F R b R G z = b Y G
Assertion cdlemk33N K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W X = ι z T | b T b I B R b R F R b R G z P = b 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 cdlemk3.x X = ι z T | b T b I B R b R F R b R G z = b Y G
12 fveq1 z = b Y G z P = b Y G P
13 simpl11 K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W z T b T b I B R b R F R b R G z P = b Y G P K HL
14 simpl12 K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W z T b T b I B R b R F R b R G z P = b Y G P W H
15 13 14 jca K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W z T b T b I B R b R F R b R G z P = b Y G P K HL W H
16 simpl31 K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W z T b T b I B R b R F R b R G z P = b Y G P z T
17 simp11 K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W z T b T b I B R b R F R b R G K HL
18 simp12 K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W z T b T b I B R b R F R b R G W H
19 17 18 jca K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W z T b T b I B R b R F R b R G K HL W H
20 simp13 K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W z T b T b I B R b R F R b R G R F = R N
21 simp22l K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W z T b T b I B R b R F R b R G G T
22 19 20 21 3jca K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W z T b T b I B R b R F R b R G K HL W H R F = R N G T
23 22 adantr K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W z T b T b I B R b R F R b R G z P = b Y G P K HL W H R F = R N G T
24 simp211 K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W z T b T b I B R b R F R b R G F T
25 simp32 K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W z T b T b I B R b R F R b R G b T
26 simp213 K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W z T b T b I B R b R F R b R G N T
27 24 25 26 3jca K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W z T b T b I B R b R F R b R G F T b T N T
28 27 adantr K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W z T b T b I B R b R F R b R G z P = b Y G P F T b T N T
29 simp332 K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W z T b T b I B R b R F R b R G R b R F
30 simp333 K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W z T b T b I B R b R F R b R G R b R G
31 29 30 jca K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W z T b T b I B R b R F R b R G R b R F R b R G
32 simp212 K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W z T b T b I B R b R F R b R G F I B
33 simp22r K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W z T b T b I B R b R F R b R G G I B
34 simp331 K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W z T b T b I B R b R F R b R G b I B
35 32 33 34 3jca K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W z T b T b I B R b R F R b R G F I B G I B b I B
36 simp23 K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W z T b T b I B R b R F R b R G P A ¬ P ˙ W
37 31 35 36 3jca K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W z T b T b I B R b R F R b R G R b R F R b R G F I B G I B b I B P A ¬ P ˙ W
38 37 adantr K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W z T b T b I B R b R F R b R G z P = b Y G P R b R F R b R G F I B G I B b I B P A ¬ P ˙ W
39 1 2 3 4 5 6 7 8 9 10 cdlemkuel-3 K HL W H R F = R N G T F T b T N T R b R F R b R G F I B G I B b I B P A ¬ P ˙ W b Y G T
40 23 28 38 39 syl3anc K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W z T b T b I B R b R F R b R G z P = b Y G P b Y G T
41 simpl23 K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W z T b T b I B R b R F R b R G z P = b Y G P P A ¬ P ˙ W
42 simpr K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W z T b T b I B R b R F R b R G z P = b Y G P z P = b Y G P
43 2 5 6 7 cdlemd K HL W H z T b Y G T P A ¬ P ˙ W z P = b Y G P z = b Y G
44 15 16 40 41 42 43 syl311anc K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W z T b T b I B R b R F R b R G z P = b Y G P z = b Y G
45 44 ex K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W z T b T b I B R b R F R b R G z P = b Y G P z = b Y G
46 12 45 impbid2 K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W z T b T b I B R b R F R b R G z = b Y G z P = b Y G P
47 46 3expia K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W z T b T b I B R b R F R b R G z = b Y G z P = b Y G P
48 47 3expd K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W z T b T b I B R b R F R b R G z = b Y G z P = b Y G P
49 48 imp31 K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W z T b T b I B R b R F R b R G z = b Y G z P = b Y G P
50 49 pm5.74d K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W z T b T b I B R b R F R b R G z = b Y G b I B R b R F R b R G z P = b Y G P
51 50 ralbidva K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W z T b T b I B R b R F R b R G z = b Y G b T b I B R b R F R b R G z P = b Y G P
52 51 riotabidva K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W ι z T | b T b I B R b R F R b R G z = b Y G = ι z T | b T b I B R b R F R b R G z P = b Y G P
53 11 52 syl5eq K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W X = ι z T | b T b I B R b R F R b R G z P = b Y G P