Metamath Proof Explorer


Theorem cdlemg4b2

Description: TODO: FIX COMMENT. (Contributed by NM, 24-Apr-2013)

Ref Expression
Hypotheses cdlemg4.l ˙ = K
cdlemg4.a A = Atoms K
cdlemg4.h H = LHyp K
cdlemg4.t T = LTrn K W
cdlemg4.r R = trL K W
cdlemg4.j ˙ = join K
cdlemg4b.v V = R G
Assertion cdlemg4b2 K HL W H P A ¬ P ˙ W G T G P ˙ V = P ˙ G P

Proof

Step Hyp Ref Expression
1 cdlemg4.l ˙ = K
2 cdlemg4.a A = Atoms K
3 cdlemg4.h H = LHyp K
4 cdlemg4.t T = LTrn K W
5 cdlemg4.r R = trL K W
6 cdlemg4.j ˙ = join K
7 cdlemg4b.v V = R G
8 eqid meet K = meet K
9 1 6 8 2 3 4 5 trlval2 K HL W H G T P A ¬ P ˙ W R G = P ˙ G P meet K W
10 9 3com23 K HL W H P A ¬ P ˙ W G T R G = P ˙ G P meet K W
11 7 10 syl5eq K HL W H P A ¬ P ˙ W G T V = P ˙ G P meet K W
12 11 oveq2d K HL W H P A ¬ P ˙ W G T G P ˙ V = G P ˙ P ˙ G P meet K W
13 simp1 K HL W H P A ¬ P ˙ W G T K HL W H
14 simp2l K HL W H P A ¬ P ˙ W G T P A
15 1 2 3 4 ltrnel K HL W H G T P A ¬ P ˙ W G P A ¬ G P ˙ W
16 15 3com23 K HL W H P A ¬ P ˙ W G T G P A ¬ G P ˙ W
17 eqid P ˙ G P meet K W = P ˙ G P meet K W
18 1 6 8 2 3 17 cdleme0cq K HL W H P A G P A ¬ G P ˙ W G P ˙ P ˙ G P meet K W = P ˙ G P
19 13 14 16 18 syl12anc K HL W H P A ¬ P ˙ W G T G P ˙ P ˙ G P meet K W = P ˙ G P
20 12 19 eqtrd K HL W H P A ¬ P ˙ W G T G P ˙ V = P ˙ G P