Metamath Proof Explorer


Theorem cdleme48b

Description: TODO: fix comment. (Contributed by NM, 8-Apr-2013)

Ref Expression
Hypotheses cdlemef46.b B = Base K
cdlemef46.l ˙ = K
cdlemef46.j ˙ = join K
cdlemef46.m ˙ = meet K
cdlemef46.a A = Atoms K
cdlemef46.h H = LHyp K
cdlemef46.u U = P ˙ Q ˙ W
cdlemef46.d D = t ˙ U ˙ Q ˙ P ˙ t ˙ W
cdlemefs46.e E = P ˙ Q ˙ D ˙ s ˙ t ˙ W
cdlemef46.f 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
Assertion cdleme48b K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q X B ¬ X ˙ W S A ¬ S ˙ W S ˙ X ˙ W = X F X ˙ W = X ˙ W

Proof

Step Hyp Ref Expression
1 cdlemef46.b B = Base K
2 cdlemef46.l ˙ = K
3 cdlemef46.j ˙ = join K
4 cdlemef46.m ˙ = meet K
5 cdlemef46.a A = Atoms K
6 cdlemef46.h H = LHyp K
7 cdlemef46.u U = P ˙ Q ˙ W
8 cdlemef46.d D = t ˙ U ˙ Q ˙ P ˙ t ˙ W
9 cdlemefs46.e E = P ˙ Q ˙ D ˙ s ˙ t ˙ W
10 cdlemef46.f 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
11 1 2 3 4 5 6 7 8 9 10 cdleme48fv K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q X B ¬ X ˙ W S A ¬ S ˙ W S ˙ X ˙ W = X F X = F S ˙ X ˙ W
12 11 oveq1d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q X B ¬ X ˙ W S A ¬ S ˙ W S ˙ X ˙ W = X F X ˙ W = F S ˙ X ˙ W ˙ W
13 simp11 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q X B ¬ X ˙ W S A ¬ S ˙ W S ˙ X ˙ W = X K HL W H
14 simp1 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q X B ¬ X ˙ W S A ¬ S ˙ W S ˙ X ˙ W = X K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W
15 simp3l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q X B ¬ X ˙ W S A ¬ S ˙ W S ˙ X ˙ W = X S A ¬ S ˙ W
16 1 2 3 4 5 6 7 8 9 10 cdleme46fvaw K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W F S A ¬ F S ˙ W
17 14 15 16 syl2anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q X B ¬ X ˙ W S A ¬ S ˙ W S ˙ X ˙ W = X F S A ¬ F S ˙ W
18 simp2rl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q X B ¬ X ˙ W S A ¬ S ˙ W S ˙ X ˙ W = X X B
19 1 2 3 4 5 6 lhpelim K HL W H F S A ¬ F S ˙ W X B F S ˙ X ˙ W ˙ W = X ˙ W
20 13 17 18 19 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q X B ¬ X ˙ W S A ¬ S ˙ W S ˙ X ˙ W = X F S ˙ X ˙ W ˙ W = X ˙ W
21 12 20 eqtrd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q X B ¬ X ˙ W S A ¬ S ˙ W S ˙ X ˙ W = X F X ˙ W = X ˙ W