Metamath Proof Explorer


Theorem cdleme50ex

Description: Part of Lemma E in Crawley p. 113. TODO: fix comment. (Contributed by NM, 11-Apr-2013)

Ref Expression
Hypotheses cdleme.l ˙ = K
cdleme.a A = Atoms K
cdleme.h H = LHyp K
cdleme.t T = LTrn K W
Assertion cdleme50ex K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W f T f P = Q

Proof

Step Hyp Ref Expression
1 cdleme.l ˙ = K
2 cdleme.a A = Atoms K
3 cdleme.h H = LHyp K
4 cdleme.t T = LTrn K W
5 eqid Base K = Base K
6 eqid join K = join K
7 eqid meet K = meet K
8 eqid P join K Q meet K W = P join K Q meet K W
9 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
10 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
11 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
12 5 1 6 7 2 3 8 9 10 11 4 cdleme50ltrn K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W 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 T
13 5 1 6 7 2 3 8 9 10 11 cdleme17d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W 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 P = Q
14 fveq1 f = 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 f P = 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 P
15 14 eqeq1d f = 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 f P = Q 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 P = Q
16 15 rspcev 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 T 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 P = Q f T f P = Q
17 12 13 16 syl2anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W f T f P = Q