Metamath Proof Explorer


Theorem cdleme22gb

Description: Utility lemma for Lemma E in Crawley p. 115. (Contributed by NM, 5-Dec-2012)

Ref Expression
Hypotheses cdleme18d.l ˙ = K
cdleme18d.j ˙ = join K
cdleme18d.m ˙ = meet K
cdleme18d.a A = Atoms K
cdleme18d.h H = LHyp K
cdleme18d.u U = P ˙ Q ˙ W
cdleme18d.f F = S ˙ U ˙ Q ˙ P ˙ S ˙ W
cdleme18d.g G = P ˙ Q ˙ F ˙ R ˙ S ˙ W
cdleme22.b B = Base K
Assertion cdleme22gb K HL W H P A Q A R A S A G B

Proof

Step Hyp Ref Expression
1 cdleme18d.l ˙ = K
2 cdleme18d.j ˙ = join K
3 cdleme18d.m ˙ = meet K
4 cdleme18d.a A = Atoms K
5 cdleme18d.h H = LHyp K
6 cdleme18d.u U = P ˙ Q ˙ W
7 cdleme18d.f F = S ˙ U ˙ Q ˙ P ˙ S ˙ W
8 cdleme18d.g G = P ˙ Q ˙ F ˙ R ˙ S ˙ W
9 cdleme22.b B = Base K
10 simp1l K HL W H P A Q A R A S A K HL
11 10 hllatd K HL W H P A Q A R A S A K Lat
12 simp2l K HL W H P A Q A R A S A P A
13 simp2r K HL W H P A Q A R A S A Q A
14 9 2 4 hlatjcl K HL P A Q A P ˙ Q B
15 10 12 13 14 syl3anc K HL W H P A Q A R A S A P ˙ Q B
16 simp1 K HL W H P A Q A R A S A K HL W H
17 simp3r K HL W H P A Q A R A S A S A
18 1 2 3 4 5 6 7 9 cdleme1b K HL W H P A Q A S A F B
19 16 12 13 17 18 syl13anc K HL W H P A Q A R A S A F B
20 simp3l K HL W H P A Q A R A S A R A
21 9 2 4 hlatjcl K HL R A S A R ˙ S B
22 10 20 17 21 syl3anc K HL W H P A Q A R A S A R ˙ S B
23 simp1r K HL W H P A Q A R A S A W H
24 9 5 lhpbase W H W B
25 23 24 syl K HL W H P A Q A R A S A W B
26 9 3 latmcl K Lat R ˙ S B W B R ˙ S ˙ W B
27 11 22 25 26 syl3anc K HL W H P A Q A R A S A R ˙ S ˙ W B
28 9 2 latjcl K Lat F B R ˙ S ˙ W B F ˙ R ˙ S ˙ W B
29 11 19 27 28 syl3anc K HL W H P A Q A R A S A F ˙ R ˙ S ˙ W B
30 9 3 latmcl K Lat P ˙ Q B F ˙ R ˙ S ˙ W B P ˙ Q ˙ F ˙ R ˙ S ˙ W B
31 11 15 29 30 syl3anc K HL W H P A Q A R A S A P ˙ Q ˙ F ˙ R ˙ S ˙ W B
32 8 31 eqeltrid K HL W H P A Q A R A S A G B