This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cdlemg3a

Description: Part of proof of Lemma G in Crawley p. 116, line 19. Show p \/ q = p \/ u. TODO: reformat cdleme0cp to match this, then replace with cdleme0cp . (Contributed by NM, 19-Apr-2013)

Ref Expression
Hypotheses cdlemg3.l ⊢ ≤ ˙ = ≤ K
cdlemg3.j ⊢ ∨ ˙ = join ⁡ K
cdlemg3.m ⊢ ∧ ˙ = meet ⁡ K
cdlemg3.a ⊢ A = Atoms ⁡ K
cdlemg3.h ⊢ H = LHyp ⁡ K
cdlemg3.u ⊢ U = P ∨ ˙ Q ∧ ˙ W
Assertion cdlemg3a ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A → P ∨ ˙ Q = P ∨ ˙ U

Proof

Step Hyp Ref Expression
1 cdlemg3.l ⊢ ≤ ˙ = ≤ K
2 cdlemg3.j ⊢ ∨ ˙ = join ⁡ K
3 cdlemg3.m ⊢ ∧ ˙ = meet ⁡ K
4 cdlemg3.a ⊢ A = Atoms ⁡ K
5 cdlemg3.h ⊢ H = LHyp ⁡ K
6 cdlemg3.u ⊢ U = P ∨ ˙ Q ∧ ˙ W
7 1 2 3 4 5 6 cdleme8 ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A → P ∨ ˙ U = P ∨ ˙ Q
8 7 eqcomd ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A → P ∨ ˙ Q = P ∨ ˙ U