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

Metamath Proof Explorer

Theorem cdlemg2jOLDN

Description: TODO: Replace this with ltrnj . (Contributed by NM, 22-Apr-2013) (New usage is discouraged.)

Ref Expression
Hypotheses cdlemg2inv.h ⊢ H = LHyp ⁡ K
cdlemg2inv.t ⊢ T = LTrn ⁡ K ⁡ W
cdlemg2j.l ⊢ ≤ ˙ = ≤ K
cdlemg2j.j ⊢ ∨ ˙ = join ⁡ K
cdlemg2j.a ⊢ A = Atoms ⁡ K
Assertion cdlemg2jOLDN ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T → F ⁡ P ∨ ˙ Q = F ⁡ P ∨ ˙ F ⁡ Q

Proof

Step Hyp Ref Expression
1 cdlemg2inv.h ⊢ H = LHyp ⁡ K
2 cdlemg2inv.t ⊢ T = LTrn ⁡ K ⁡ W
3 cdlemg2j.l ⊢ ≤ ˙ = ≤ K
4 cdlemg2j.j ⊢ ∨ ˙ = join ⁡ K
5 cdlemg2j.a ⊢ A = Atoms ⁡ K
6 eqid ⊢ Base K = Base K
7 eqid ⊢ meet ⁡ K = meet ⁡ K
8 eqid ⊢ p ∨ ˙ q meet ⁡ K W = p ∨ ˙ q meet ⁡ K W
9 eqid ⊢ t ∨ ˙ p ∨ ˙ q meet ⁡ K W meet ⁡ K q ∨ ˙ p ∨ ˙ t meet ⁡ K W = t ∨ ˙ p ∨ ˙ q meet ⁡ K W meet ⁡ K q ∨ ˙ p ∨ ˙ t meet ⁡ K W
10 eqid ⊢ p ∨ ˙ q meet ⁡ K t ∨ ˙ p ∨ ˙ q meet ⁡ K W meet ⁡ K q ∨ ˙ p ∨ ˙ t meet ⁡ K W ∨ ˙ s ∨ ˙ t meet ⁡ K W = p ∨ ˙ q meet ⁡ K t ∨ ˙ p ∨ ˙ q meet ⁡ K W meet ⁡ K q ∨ ˙ p ∨ ˙ t meet ⁡ K W ∨ ˙ s ∨ ˙ t meet ⁡ K W
11 eqid ⊢ x ∈ Base K ⟼ if p ≠ q ∧ ¬ x ≤ ˙ W ι z ∈ Base K | ∀ s ∈ A ¬ s ≤ ˙ W ∧ s ∨ ˙ x meet ⁡ K W = x → z = if s ≤ ˙ p ∨ ˙ q ι y ∈ Base K | ∀ t ∈ A ¬ t ≤ ˙ W ∧ ¬ t ≤ ˙ p ∨ ˙ q → y = p ∨ ˙ q meet ⁡ K t ∨ ˙ p ∨ ˙ q meet ⁡ K W meet ⁡ K q ∨ ˙ p ∨ ˙ t meet ⁡ K W ∨ ˙ s ∨ ˙ t meet ⁡ K W ⦋ s / t⦌ t ∨ ˙ p ∨ ˙ q meet ⁡ K W meet ⁡ K q ∨ ˙ p ∨ ˙ t meet ⁡ K W ∨ ˙ x meet ⁡ K W x = x ∈ Base K ⟼ if p ≠ q ∧ ¬ x ≤ ˙ W ι z ∈ Base K | ∀ s ∈ A ¬ s ≤ ˙ W ∧ s ∨ ˙ x meet ⁡ K W = x → z = if s ≤ ˙ p ∨ ˙ q ι y ∈ Base K | ∀ t ∈ A ¬ t ≤ ˙ W ∧ ¬ t ≤ ˙ p ∨ ˙ q → y = p ∨ ˙ q meet ⁡ K t ∨ ˙ p ∨ ˙ q meet ⁡ K W meet ⁡ K q ∨ ˙ p ∨ ˙ t meet ⁡ K W ∨ ˙ s ∨ ˙ t meet ⁡ K W ⦋ s / t⦌ t ∨ ˙ p ∨ ˙ q meet ⁡ K W meet ⁡ K q ∨ ˙ p ∨ ˙ t meet ⁡ K W ∨ ˙ x meet ⁡ K W x
12 6 3 4 7 5 1 2 8 9 10 11 cdlemg2jlemOLDN ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T → F ⁡ P ∨ ˙ Q = F ⁡ P ∨ ˙ F ⁡ Q