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⁡Pmeet⁡KW
10 9 3com23 ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧G∈T→R⁡G=P∨˙G⁡Pmeet⁡KW
11 7 10 eqtrid ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧G∈T→V=P∨˙G⁡Pmeet⁡KW
12 11 oveq2d ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧G∈T→G⁡P∨˙V=G⁡P∨˙P∨˙G⁡Pmeet⁡KW
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⁡Pmeet⁡KW=P∨˙G⁡Pmeet⁡KW
18 1 6 8 2 3 17 cdleme0cq ⊢K∈HL∧W∈H∧P∈A∧G⁡P∈A∧¬G⁡P≤˙W→G⁡P∨˙P∨˙G⁡Pmeet⁡KW=P∨˙G⁡P
19 13 14 16 18 syl12anc ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧G∈T→G⁡P∨˙P∨˙G⁡Pmeet⁡KW=P∨˙G⁡P
20 12 19 eqtrd ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧G∈T→G⁡P∨˙V=P∨˙G⁡P