Metamath Proof Explorer


Theorem cdlemg1bOLDN

Description: This theorem can be used to shorten F = hypothesis that have the form of the conclusion. TODO: fix comment. (Contributed by NM, 16-Apr-2013) (New usage is discouraged.)

Ref Expression
Hypotheses cdlemg1.b B = Base K
cdlemg1.l ˙ = K
cdlemg1.j ˙ = join K
cdlemg1.m ˙ = meet K
cdlemg1.a A = Atoms K
cdlemg1.h H = LHyp K
cdlemg1b.u U = P ˙ Q ˙ W
cdlemg1b.d D = t ˙ U ˙ Q ˙ P ˙ t ˙ W
cdlemg1b.e E = P ˙ Q ˙ D ˙ s ˙ t ˙ W
cdlemg1b.f F = ι f T | f P = Q
cdlemg1b.t T = LTrn K W
Assertion cdlemg1bOLDN K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F = x B if P Q ¬ x ˙ W ι z B | s A ¬ s ˙ W s ˙ x ˙ W = x z = if s ˙ P ˙ Q ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = E s / t D ˙ x ˙ W x

Proof

Step Hyp Ref Expression
1 cdlemg1.b B = Base K
2 cdlemg1.l ˙ = K
3 cdlemg1.j ˙ = join K
4 cdlemg1.m ˙ = meet K
5 cdlemg1.a A = Atoms K
6 cdlemg1.h H = LHyp K
7 cdlemg1b.u U = P ˙ Q ˙ W
8 cdlemg1b.d D = t ˙ U ˙ Q ˙ P ˙ t ˙ W
9 cdlemg1b.e E = P ˙ Q ˙ D ˙ s ˙ t ˙ W
10 cdlemg1b.f F = ι f T | f P = Q
11 cdlemg1b.t T = LTrn K W
12 eqid x B if P Q ¬ x ˙ W ι z B | s A ¬ s ˙ W s ˙ x ˙ W = x z = if s ˙ P ˙ Q ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = E s / t D ˙ x ˙ W x = x B if P Q ¬ x ˙ W ι z B | s A ¬ s ˙ W s ˙ x ˙ W = x z = if s ˙ P ˙ Q ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = E s / t D ˙ x ˙ W x
13 1 2 3 4 5 6 7 8 9 12 11 10 cdlemg1b2 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F = x B if P Q ¬ x ˙ W ι z B | s A ¬ s ˙ W s ˙ x ˙ W = x z = if s ˙ P ˙ Q ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = E s / t D ˙ x ˙ W x