Metamath Proof Explorer


Theorem cdleme28

Description: Quantified version of cdleme28c . (Compare cdleme24 .) (Contributed by NM, 7-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
cdleme27.g G = t ˙ U ˙ Q ˙ P ˙ t ˙ W
cdleme27.o O = P ˙ Q ˙ Z ˙ t ˙ z ˙ W
cdleme27.e E = ι u B | z A ¬ z ˙ W ¬ z ˙ P ˙ Q u = O
cdleme27.y Y = if t ˙ P ˙ Q E G
Assertion cdleme28 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q X B ¬ X ˙ W s A t A ¬ s ˙ W s ˙ X ˙ W = X ¬ t ˙ W t ˙ X ˙ W = X C ˙ X ˙ W = Y ˙ 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 cdleme27.g G = t ˙ U ˙ Q ˙ P ˙ t ˙ W
14 cdleme27.o O = P ˙ Q ˙ Z ˙ t ˙ z ˙ W
15 cdleme27.e E = ι u B | z A ¬ z ˙ W ¬ z ˙ P ˙ Q u = O
16 cdleme27.y Y = if t ˙ P ˙ Q E G
17 simp11 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q X B ¬ X ˙ W s A t A ¬ s ˙ W s ˙ X ˙ W = X ¬ t ˙ W t ˙ X ˙ W = X K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W
18 simp12 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q X B ¬ X ˙ W s A t A ¬ s ˙ W s ˙ X ˙ W = X ¬ t ˙ W t ˙ X ˙ W = X P Q
19 simp2l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q X B ¬ X ˙ W s A t A ¬ s ˙ W s ˙ X ˙ W = X ¬ t ˙ W t ˙ X ˙ W = X s A
20 simp3ll K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q X B ¬ X ˙ W s A t A ¬ s ˙ W s ˙ X ˙ W = X ¬ t ˙ W t ˙ X ˙ W = X ¬ s ˙ W
21 19 20 jca K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q X B ¬ X ˙ W s A t A ¬ s ˙ W s ˙ X ˙ W = X ¬ t ˙ W t ˙ X ˙ W = X s A ¬ s ˙ W
22 simp2r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q X B ¬ X ˙ W s A t A ¬ s ˙ W s ˙ X ˙ W = X ¬ t ˙ W t ˙ X ˙ W = X t A
23 simp3rl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q X B ¬ X ˙ W s A t A ¬ s ˙ W s ˙ X ˙ W = X ¬ t ˙ W t ˙ X ˙ W = X ¬ t ˙ W
24 22 23 jca K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q X B ¬ X ˙ W s A t A ¬ s ˙ W s ˙ X ˙ W = X ¬ t ˙ W t ˙ X ˙ W = X t A ¬ t ˙ W
25 simp3lr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q X B ¬ X ˙ W s A t A ¬ s ˙ W s ˙ X ˙ W = X ¬ t ˙ W t ˙ X ˙ W = X s ˙ X ˙ W = X
26 simp3rr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q X B ¬ X ˙ W s A t A ¬ s ˙ W s ˙ X ˙ W = X ¬ t ˙ W t ˙ X ˙ W = X t ˙ X ˙ W = X
27 simp13 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q X B ¬ X ˙ W s A t A ¬ s ˙ W s ˙ X ˙ W = X ¬ t ˙ W t ˙ X ˙ W = X X B ¬ X ˙ W
28 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 cdleme28c K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q s A ¬ s ˙ W t A ¬ t ˙ W s ˙ X ˙ W = X t ˙ X ˙ W = X X B ¬ X ˙ W C ˙ X ˙ W = Y ˙ X ˙ W
29 17 18 21 24 25 26 27 28 syl133anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q X B ¬ X ˙ W s A t A ¬ s ˙ W s ˙ X ˙ W = X ¬ t ˙ W t ˙ X ˙ W = X C ˙ X ˙ W = Y ˙ X ˙ W
30 29 3exp K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q X B ¬ X ˙ W s A t A ¬ s ˙ W s ˙ X ˙ W = X ¬ t ˙ W t ˙ X ˙ W = X C ˙ X ˙ W = Y ˙ X ˙ W
31 30 ralrimivv K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q X B ¬ X ˙ W s A t A ¬ s ˙ W s ˙ X ˙ W = X ¬ t ˙ W t ˙ X ˙ W = X C ˙ X ˙ W = Y ˙ X ˙ W