Metamath Proof Explorer


Theorem cdleme42e

Description: Part of proof of Lemma E in Crawley p. 113. (Contributed by NM, 8-Mar-2013)

Ref Expression
Hypotheses cdleme41.b B = Base K
cdleme41.l ˙ = K
cdleme41.j ˙ = join K
cdleme41.m ˙ = meet K
cdleme41.a A = Atoms K
cdleme41.h H = LHyp K
cdleme41.u U = P ˙ Q ˙ W
cdleme41.d D = s ˙ U ˙ Q ˙ P ˙ s ˙ W
cdleme41.e E = t ˙ U ˙ Q ˙ P ˙ t ˙ W
cdleme41.g G = P ˙ Q ˙ E ˙ s ˙ t ˙ W
cdleme41.i I = ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = G
cdleme41.n N = if s ˙ P ˙ Q I D
cdleme41.o O = ι z B | s A ¬ s ˙ W s ˙ x ˙ W = x z = N ˙ x ˙ W
cdleme41.f F = x B if P Q ¬ x ˙ W O x
cdleme34e.v V = R ˙ S ˙ W
Assertion cdleme42e K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q F R ˙ V = R / s N ˙ R ˙ V ˙ W

Proof

Step Hyp Ref Expression
1 cdleme41.b B = Base K
2 cdleme41.l ˙ = K
3 cdleme41.j ˙ = join K
4 cdleme41.m ˙ = meet K
5 cdleme41.a A = Atoms K
6 cdleme41.h H = LHyp K
7 cdleme41.u U = P ˙ Q ˙ W
8 cdleme41.d D = s ˙ U ˙ Q ˙ P ˙ s ˙ W
9 cdleme41.e E = t ˙ U ˙ Q ˙ P ˙ t ˙ W
10 cdleme41.g G = P ˙ Q ˙ E ˙ s ˙ t ˙ W
11 cdleme41.i I = ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = G
12 cdleme41.n N = if s ˙ P ˙ Q I D
13 cdleme41.o O = ι z B | s A ¬ s ˙ W s ˙ x ˙ W = x z = N ˙ x ˙ W
14 cdleme41.f F = x B if P Q ¬ x ˙ W O x
15 cdleme34e.v V = R ˙ S ˙ W
16 simp1 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W
17 simp11l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q K HL
18 17 hllatd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q K Lat
19 simp2ll K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q R A
20 1 5 atbase R A R B
21 19 20 syl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q R B
22 simp11 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q K HL W H
23 simp2rl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q S A
24 2 3 4 5 6 15 1 cdleme0aa K HL W H R A S A V B
25 22 19 23 24 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q V B
26 1 3 latjcl K Lat R B V B R ˙ V B
27 18 21 25 26 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q R ˙ V B
28 simp3 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q P Q
29 simp2l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q R A ¬ R ˙ W
30 simp2r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q S A ¬ S ˙ W
31 1 2 3 4 5 6 15 cdleme42c K HL W H R A ¬ R ˙ W S A ¬ S ˙ W ¬ R ˙ V ˙ W
32 22 29 30 31 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q ¬ R ˙ V ˙ W
33 28 32 jca K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q P Q ¬ R ˙ V ˙ W
34 1 2 3 4 5 6 15 cdleme42d K HL W H R A ¬ R ˙ W S A ¬ S ˙ W R ˙ R ˙ V ˙ W = R ˙ V
35 22 29 30 34 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q R ˙ R ˙ V ˙ W = R ˙ V
36 1 2 3 4 5 6 7 8 9 10 11 12 13 14 cdleme42b K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R ˙ V B P Q ¬ R ˙ V ˙ W R A ¬ R ˙ W R ˙ R ˙ V ˙ W = R ˙ V F R ˙ V = R / s N ˙ R ˙ V ˙ W
37 16 27 33 29 35 36 syl122anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q F R ˙ V = R / s N ˙ R ˙ V ˙ W