Metamath Proof Explorer


Theorem cdlemg31a

Description: TODO: fix comment. (Contributed by NM, 29-May-2013)

Ref Expression
Hypotheses cdlemg12.l ˙ = K
cdlemg12.j ˙ = join K
cdlemg12.m ˙ = meet K
cdlemg12.a A = Atoms K
cdlemg12.h H = LHyp K
cdlemg12.t T = LTrn K W
cdlemg12b.r R = trL K W
cdlemg31.n N = P ˙ v ˙ Q ˙ R F
Assertion cdlemg31a K HL W H P A Q A v A F T N ˙ P ˙ v

Proof

Step Hyp Ref Expression
1 cdlemg12.l ˙ = K
2 cdlemg12.j ˙ = join K
3 cdlemg12.m ˙ = meet K
4 cdlemg12.a A = Atoms K
5 cdlemg12.h H = LHyp K
6 cdlemg12.t T = LTrn K W
7 cdlemg12b.r R = trL K W
8 cdlemg31.n N = P ˙ v ˙ Q ˙ R F
9 simp1l K HL W H P A Q A v A F T K HL
10 9 hllatd K HL W H P A Q A v A F T K Lat
11 simp2l K HL W H P A Q A v A F T P A
12 simp3l K HL W H P A Q A v A F T v A
13 eqid Base K = Base K
14 13 2 4 hlatjcl K HL P A v A P ˙ v Base K
15 9 11 12 14 syl3anc K HL W H P A Q A v A F T P ˙ v Base K
16 simp2r K HL W H P A Q A v A F T Q A
17 13 4 atbase Q A Q Base K
18 16 17 syl K HL W H P A Q A v A F T Q Base K
19 simp1 K HL W H P A Q A v A F T K HL W H
20 simp3r K HL W H P A Q A v A F T F T
21 13 5 6 7 trlcl K HL W H F T R F Base K
22 19 20 21 syl2anc K HL W H P A Q A v A F T R F Base K
23 13 2 latjcl K Lat Q Base K R F Base K Q ˙ R F Base K
24 10 18 22 23 syl3anc K HL W H P A Q A v A F T Q ˙ R F Base K
25 13 1 3 latmle1 K Lat P ˙ v Base K Q ˙ R F Base K P ˙ v ˙ Q ˙ R F ˙ P ˙ v
26 10 15 24 25 syl3anc K HL W H P A Q A v A F T P ˙ v ˙ Q ˙ R F ˙ P ˙ v
27 8 26 eqbrtrid K HL W H P A Q A v A F T N ˙ P ˙ v