Metamath Proof Explorer


Theorem cdleme50eq

Description: Part of proof of Lemma D in Crawley p. 113. TODO: fix comment. (Contributed by NM, 9-Apr-2013)

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

Proof

Step Hyp Ref Expression
1 cdlemef50.b B = Base K
2 cdlemef50.l ˙ = K
3 cdlemef50.j ˙ = join K
4 cdlemef50.m ˙ = meet K
5 cdlemef50.a A = Atoms K
6 cdlemef50.h H = LHyp K
7 cdlemef50.u U = P ˙ Q ˙ W
8 cdlemef50.d D = t ˙ U ˙ Q ˙ P ˙ t ˙ W
9 cdlemefs50.e E = P ˙ Q ˙ D ˙ s ˙ t ˙ W
10 cdlemef50.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 cdleme50lebi K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B X ˙ Y F X ˙ F Y
12 1 2 3 4 5 6 7 8 9 10 cdleme50lebi K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W Y B X B Y ˙ X F Y ˙ F X
13 12 ancom2s K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B Y ˙ X F Y ˙ F X
14 11 13 anbi12d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B X ˙ Y Y ˙ X F X ˙ F Y F Y ˙ F X
15 simpl1l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B K HL
16 15 hllatd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B K Lat
17 simprl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B X B
18 simprr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B Y B
19 1 2 latasymb K Lat X B Y B X ˙ Y Y ˙ X X = Y
20 16 17 18 19 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B X ˙ Y Y ˙ X X = Y
21 eqid s ˙ U ˙ Q ˙ P ˙ s ˙ W = s ˙ U ˙ Q ˙ P ˙ s ˙ W
22 eqid ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = E = ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = E
23 biid s ˙ P ˙ Q s ˙ P ˙ Q
24 vex s V
25 8 21 cdleme31sc s V s / t D = s ˙ U ˙ Q ˙ P ˙ s ˙ W
26 24 25 ax-mp s / t D = s ˙ U ˙ Q ˙ P ˙ s ˙ W
27 23 26 ifbieq2i 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 ˙ U ˙ Q ˙ P ˙ s ˙ W
28 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
29 1 2 3 4 5 6 7 21 8 9 22 27 28 10 cdleme32fvcl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B F X B
30 29 adantrr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B F X B
31 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
32 1 2 3 4 5 6 7 26 8 9 22 31 28 10 cdleme32fvcl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W Y B F Y B
33 32 adantrl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B F Y B
34 1 2 latasymb K Lat F X B F Y B F X ˙ F Y F Y ˙ F X F X = F Y
35 16 30 33 34 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B F X ˙ F Y F Y ˙ F X F X = F Y
36 14 20 35 3bitr3rd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B F X = F Y X = Y