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