Metamath Proof Explorer


Theorem cdleme29c

Description: Transform cdleme28b . (Compare cdleme25c .) TODO: FIX COMMENT. (Contributed by NM, 8-Feb-2013)

Ref Expression
Hypotheses cdleme26.b B = Base K
cdleme26.l ˙ = K
cdleme26.j ˙ = join K
cdleme26.m ˙ = meet K
cdleme26.a A = Atoms K
cdleme26.h H = LHyp K
cdleme27.u U = P ˙ Q ˙ W
cdleme27.f F = s ˙ U ˙ Q ˙ P ˙ s ˙ W
cdleme27.z Z = z ˙ U ˙ Q ˙ P ˙ z ˙ W
cdleme27.n N = P ˙ Q ˙ Z ˙ s ˙ z ˙ W
cdleme27.d D = ι u B | z A ¬ z ˙ W ¬ z ˙ P ˙ Q u = N
cdleme27.c C = if s ˙ P ˙ Q D F
Assertion cdleme29c K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q X B ¬ X ˙ W ∃! v B s A ¬ s ˙ W s ˙ X ˙ W = X v = C ˙ X ˙ W

Proof

Step Hyp Ref Expression
1 cdleme26.b B = Base K
2 cdleme26.l ˙ = K
3 cdleme26.j ˙ = join K
4 cdleme26.m ˙ = meet K
5 cdleme26.a A = Atoms K
6 cdleme26.h H = LHyp K
7 cdleme27.u U = P ˙ Q ˙ W
8 cdleme27.f F = s ˙ U ˙ Q ˙ P ˙ s ˙ W
9 cdleme27.z Z = z ˙ U ˙ Q ˙ P ˙ z ˙ W
10 cdleme27.n N = P ˙ Q ˙ Z ˙ s ˙ z ˙ W
11 cdleme27.d D = ι u B | z A ¬ z ˙ W ¬ z ˙ P ˙ Q u = N
12 cdleme27.c C = if s ˙ P ˙ Q D F
13 1 2 3 4 5 6 7 8 9 10 11 12 cdleme29b K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q X B ¬ X ˙ W v B s A ¬ s ˙ W s ˙ X ˙ W = X v = C ˙ X ˙ W
14 simp11 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q X B ¬ X ˙ W K HL W H
15 simp3 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q X B ¬ X ˙ W X B ¬ X ˙ W
16 1 2 3 4 5 6 lhpmcvr2 K HL W H X B ¬ X ˙ W s A ¬ s ˙ W s ˙ X ˙ W = X
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
18 reusv1 s A ¬ s ˙ W s ˙ X ˙ W = X ∃! v B s A ¬ s ˙ W s ˙ X ˙ W = X v = C ˙ X ˙ W v B s A ¬ s ˙ W s ˙ X ˙ W = X v = C ˙ X ˙ W
19 17 18 syl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q X B ¬ X ˙ W ∃! v B s A ¬ s ˙ W s ˙ X ˙ W = X v = C ˙ X ˙ W v B s A ¬ s ˙ W s ˙ X ˙ W = X v = C ˙ X ˙ W
20 13 19 mpbird K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q X B ¬ X ˙ W ∃! v B s A ¬ s ˙ W s ˙ X ˙ W = X v = C ˙ X ˙ W