Metamath Proof Explorer


Theorem cdleme48bw

Description: TODO: fix comment. TODO: Remove unnecessary P =/= Q from cdleme48bw cdlemeg46c cdlemeg46fvaw cdlemeg46rgv cdlemeg46gfv ? cdleme48d ? and possibly others they affect. (Contributed by NM, 9-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 cdleme48bw 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

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 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
12 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
13 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
14 11 12 13 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
15 14 simprd 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 ˙ W
16 simp11l 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
17 16 hllatd 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 Lat
18 14 simpld 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
19 1 5 atbase F S A F S B
20 18 19 syl 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 B
21 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
22 simp11r 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 W H
23 1 6 lhpbase W H W B
24 22 23 syl 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 W B
25 1 4 latmcl K Lat X B W B X ˙ W B
26 17 21 24 25 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 X ˙ W B
27 1 2 3 latlej1 K Lat F S B X ˙ W B F S ˙ F S ˙ X ˙ W
28 17 20 26 27 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 ˙ F S ˙ X ˙ W
29 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
30 28 29 breqtrrd 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 ˙ F X
31 vex s V
32 eqid s ˙ U ˙ Q ˙ P ˙ s ˙ W = s ˙ U ˙ Q ˙ P ˙ s ˙ W
33 8 32 cdleme31sc s V s / t D = s ˙ U ˙ Q ˙ P ˙ s ˙ W
34 31 33 ax-mp s / t D = s ˙ U ˙ Q ˙ P ˙ s ˙ W
35 eqid ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = E = ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = E
36 eqid if s ˙ P ˙ Q ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = E s / t D = if s ˙ P ˙ Q ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = E s / t D
37 eqid ι 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 = ι 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
38 1 2 3 4 5 6 7 34 8 9 35 36 37 10 cdleme32fvcl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B F X B
39 11 21 38 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 X B
40 1 2 lattr K Lat F S B F X B W B F S ˙ F X F X ˙ W F S ˙ W
41 17 20 39 24 40 syl13anc 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 ˙ F X F X ˙ W F S ˙ W
42 30 41 mpand 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 ˙ W
43 15 42 mtod 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