Metamath Proof Explorer

Theorem cdlemg4b1

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 cdlemg4b1 ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ G ∈ T → 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 → P ∨ ˙ V = P ∨ ˙ P ∨ ˙ G ⁡ P meet ⁡ K W
13 simp1 ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ G ∈ T → K ∈ HL ∧ W ∈ H
14 simp2 ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ G ∈ T → P ∈ A ∧ ¬ P ≤ ˙ W
15 1 2 3 4 ltrnel ⊢ K ∈ HL ∧ W ∈ H ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → G ⁡ P ∈ A ∧ ¬ G ⁡ P ≤ ˙ W
16 15 simpld ⊢ K ∈ HL ∧ W ∈ H ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → G ⁡ P ∈ A
17 16 3com23 ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ G ∈ T → G ⁡ P ∈ A
18 eqid ⊢ P ∨ ˙ G ⁡ P meet ⁡ K W = P ∨ ˙ G ⁡ P meet ⁡ K W
19 1 6 8 2 3 18 cdleme0cp ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ G ⁡ P ∈ A → P ∨ ˙ P ∨ ˙ G ⁡ P meet ⁡ K W = P ∨ ˙ G ⁡ P
20 13 14 17 19 syl12anc ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ G ∈ T → P ∨ ˙ P ∨ ˙ G ⁡ P meet ⁡ K W = P ∨ ˙ G ⁡ P
21 12 20 eqtrd ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ G ∈ T → P ∨ ˙ V = P ∨ ˙ G ⁡ P