Metamath Proof Explorer


Theorem cdlemg1b2

Description: This theorem can be used to shorten G = hypothesis. TODO: Fix comment. (Contributed by NM, 18-Apr-2013)

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
cdlemg1.u U = P ˙ Q ˙ W
cdlemg1.d D = t ˙ U ˙ Q ˙ P ˙ t ˙ W
cdlemg1.e E = P ˙ Q ˙ D ˙ s ˙ t ˙ W
cdlemg1.g G = 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
cdlemg1.t T = LTrn K W
cdlemg1.f F = ι f T | f P = Q
Assertion cdlemg1b2 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F = G

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 cdlemg1.u U = P ˙ Q ˙ W
8 cdlemg1.d D = t ˙ U ˙ Q ˙ P ˙ t ˙ W
9 cdlemg1.e E = P ˙ Q ˙ D ˙ s ˙ t ˙ W
10 cdlemg1.g G = 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
11 cdlemg1.t T = LTrn K W
12 cdlemg1.f F = ι f T | f P = Q
13 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
14 1 2 3 4 5 6 7 8 9 13 11 cdlemg1a K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W 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 = ι f T | f P = Q
15 12 14 eqtr4id 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
16 15 10 eqtr4di K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F = G