Metamath Proof Explorer


Theorem ltrniotafvawN

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

Ref Expression
Hypotheses ltrniotaval.l ˙ = K
ltrniotaval.a A = Atoms K
ltrniotaval.h H = LHyp K
ltrniotaval.t T = LTrn K W
ltrniotaval.f F = ι f T | f P = Q
Assertion ltrniotafvawN K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W F R A ¬ F R ˙ W

Proof

Step Hyp Ref Expression
1 ltrniotaval.l ˙ = K
2 ltrniotaval.a A = Atoms K
3 ltrniotaval.h H = LHyp K
4 ltrniotaval.t T = LTrn K W
5 ltrniotaval.f F = ι f T | f P = Q
6 eqid Base K = 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 Base K if P Q ¬ x ˙ W ι z Base K | s A ¬ s ˙ W s join K x meet K W = x z = if s ˙ P join K Q ι y Base K | 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 Base K if P Q ¬ x ˙ W ι z Base K | s A ¬ s ˙ W s join K x meet K W = x z = if s ˙ P join K Q ι y Base K | 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 4 5 cdlemg1fvawlemN K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W F R A ¬ F R ˙ W