Metamath Proof Explorer

Theorem cdlemg1idN

Description: Version of cdleme31id with simpler hypotheses. TODO: Fix comment. (Contributed by NM, 18-Apr-2013) (New usage is discouraged.)

Ref Expression
Hypotheses cdlemg1ltrn.l ⊢ ≤ ˙ = ≤ K
cdlemg1ltrn.a ⊢ A = Atoms ⁡ K
cdlemg1ltrn.h ⊢ H = LHyp ⁡ K
cdlemg1ltrn.f ⊢ F = ι f ∈ T | f ⁡ P = Q
cdlemg1ltrn.t ⊢ T = LTrn ⁡ K ⁡ W
cdlemg1id.b ⊢ B = Base K
Assertion cdlemg1idN ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ X ∈ B ∧ P = Q → F ⁡ X = X

Proof

Step Hyp Ref Expression
1 cdlemg1ltrn.l ⊢ ≤ ˙ = ≤ K
2 cdlemg1ltrn.a ⊢ A = Atoms ⁡ K
3 cdlemg1ltrn.h ⊢ H = LHyp ⁡ K
4 cdlemg1ltrn.f ⊢ F = ι f ∈ T | f ⁡ P = Q
5 cdlemg1ltrn.t ⊢ T = LTrn ⁡ K ⁡ W
6 cdlemg1id.b ⊢ B = Base K
7 eqid ⊢ join ⁡ K = join ⁡ K
8 eqid ⊢ meet ⁡ K = meet ⁡ K
9 eqid ⊢ P join ⁡ K Q meet ⁡ K W = P join ⁡ K Q meet ⁡ K W
10 eqid ⊢ t join ⁡ K P join ⁡ K Q meet ⁡ K W meet ⁡ K Q join ⁡ K P join ⁡ K t meet ⁡ K W = t join ⁡ K P join ⁡ K Q meet ⁡ K W meet ⁡ K Q join ⁡ K P join ⁡ K t meet ⁡ K W
11 eqid ⊢ P join ⁡ K Q meet ⁡ K t join ⁡ K P join ⁡ K Q meet ⁡ K W meet ⁡ K Q join ⁡ K P join ⁡ K t meet ⁡ K W join ⁡ K s join ⁡ K t meet ⁡ K W = P join ⁡ K Q meet ⁡ K t join ⁡ K P join ⁡ K Q meet ⁡ K W meet ⁡ K Q join ⁡ K P join ⁡ K t meet ⁡ K W join ⁡ K s join ⁡ K t meet ⁡ K W
12 eqid ⊢ x ∈ B ⟼ if P ≠ Q ∧ ¬ x ≤ ˙ W ι z ∈ B | ∀ s ∈ A ¬ s ≤ ˙ W ∧ s join ⁡ K x meet ⁡ K W = x → z = if s ≤ ˙ P join ⁡ K Q ι y ∈ B | ∀ t ∈ A ¬ t ≤ ˙ W ∧ ¬ t ≤ ˙ P join ⁡ K Q → y = P join ⁡ K Q meet ⁡ K t join ⁡ K P join ⁡ K Q meet ⁡ K W meet ⁡ K Q join ⁡ K P join ⁡ K t meet ⁡ K W join ⁡ K s join ⁡ K t meet ⁡ K W ⦋ s / t⦌ t join ⁡ K P join ⁡ K Q meet ⁡ K W meet ⁡ K Q join ⁡ K P join ⁡ K t meet ⁡ K W join ⁡ K x meet ⁡ K W x = x ∈ B ⟼ if P ≠ Q ∧ ¬ x ≤ ˙ W ι z ∈ B | ∀ s ∈ A ¬ s ≤ ˙ W ∧ s join ⁡ K x meet ⁡ K W = x → z = if s ≤ ˙ P join ⁡ K Q ι y ∈ B | ∀ t ∈ A ¬ t ≤ ˙ W ∧ ¬ t ≤ ˙ P join ⁡ K Q → y = P join ⁡ K Q meet ⁡ K t join ⁡ K P join ⁡ K Q meet ⁡ K W meet ⁡ K Q join ⁡ K P join ⁡ K t meet ⁡ K W join ⁡ K s join ⁡ K t meet ⁡ K W ⦋ s / t⦌ t join ⁡ K P join ⁡ K Q meet ⁡ K W meet ⁡ K Q join ⁡ K P join ⁡ K t meet ⁡ K W join ⁡ K x meet ⁡ K W x
13 6 1 7 8 2 3 9 10 11 12 5 4 cdlemg1idlemN ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ X ∈ B ∧ P = Q → F ⁡ X = X