Metamath Proof Explorer


Theorem cdlemeg49lebilem

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

Ref Expression
Hypotheses cdlemef46g.b B = Base K
cdlemef46g.l ˙ = K
cdlemef46g.j ˙ = join K
cdlemef46g.m ˙ = meet K
cdlemef46g.a A = Atoms K
cdlemef46g.h H = LHyp K
cdlemef46g.u U = P ˙ Q ˙ W
cdlemef46g.d D = t ˙ U ˙ Q ˙ P ˙ t ˙ W
cdlemefs46g.e E = P ˙ Q ˙ D ˙ s ˙ t ˙ W
cdlemef46g.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
cdlemef46.v V = Q ˙ P ˙ W
cdlemef46.n N = v ˙ V ˙ P ˙ Q ˙ v ˙ W
cdlemefs46.o O = Q ˙ P ˙ N ˙ u ˙ v ˙ W
cdlemef46.g G = a B if Q P ¬ a ˙ W ι c B | u A ¬ u ˙ W u ˙ a ˙ W = a c = if u ˙ Q ˙ P ι b B | v A ¬ v ˙ W ¬ v ˙ Q ˙ P b = O u / v N ˙ a ˙ W a
Assertion cdlemeg49lebilem K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B X ˙ Y F X ˙ F Y

Proof

Step Hyp Ref Expression
1 cdlemef46g.b B = Base K
2 cdlemef46g.l ˙ = K
3 cdlemef46g.j ˙ = join K
4 cdlemef46g.m ˙ = meet K
5 cdlemef46g.a A = Atoms K
6 cdlemef46g.h H = LHyp K
7 cdlemef46g.u U = P ˙ Q ˙ W
8 cdlemef46g.d D = t ˙ U ˙ Q ˙ P ˙ t ˙ W
9 cdlemefs46g.e E = P ˙ Q ˙ D ˙ s ˙ t ˙ W
10 cdlemef46g.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 cdlemef46.v V = Q ˙ P ˙ W
12 cdlemef46.n N = v ˙ V ˙ P ˙ Q ˙ v ˙ W
13 cdlemefs46.o O = Q ˙ P ˙ N ˙ u ˙ v ˙ W
14 cdlemef46.g G = a B if Q P ¬ a ˙ W ι c B | u A ¬ u ˙ W u ˙ a ˙ W = a c = if u ˙ Q ˙ P ι b B | v A ¬ v ˙ W ¬ v ˙ Q ˙ P b = O u / v N ˙ a ˙ W a
15 vex s V
16 eqid s ˙ U ˙ Q ˙ P ˙ s ˙ W = s ˙ U ˙ Q ˙ P ˙ s ˙ W
17 8 16 cdleme31sc s V s / t D = s ˙ U ˙ Q ˙ P ˙ s ˙ W
18 15 17 ax-mp s / t D = s ˙ U ˙ Q ˙ P ˙ s ˙ W
19 eqid ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = E = ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = E
20 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
21 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
22 1 2 3 4 5 6 7 18 8 9 19 20 21 10 cdleme32le K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B X ˙ Y F X ˙ F Y
23 22 3expia K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B X ˙ Y F X ˙ F Y
24 simp1 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B F X ˙ F Y K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W
25 simp2l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B F X ˙ F Y X B
26 biid s ˙ P ˙ Q s ˙ P ˙ Q
27 26 18 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 1 2 3 4 5 6 7 16 8 9 19 27 21 10 cdleme32fvcl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B F X B
29 24 25 28 syl2anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B F X ˙ F Y F X B
30 simp2r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B F X ˙ F Y Y B
31 1 2 3 4 5 6 7 16 8 9 19 27 21 10 cdleme32fvcl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W Y B F Y B
32 24 30 31 syl2anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B F X ˙ F Y F Y B
33 simp3 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B F X ˙ F Y F X ˙ F Y
34 1 2 3 4 5 6 11 12 13 14 cdlemeg49le K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F X B F Y B F X ˙ F Y G F X ˙ G F Y
35 24 29 32 33 34 syl121anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B F X ˙ F Y G F X ˙ G F Y
36 1 2 3 4 5 6 7 8 9 10 11 12 13 14 cdleme48gfv K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B G F X = X
37 36 adantrr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B G F X = X
38 1 2 3 4 5 6 7 8 9 10 11 12 13 14 cdleme48gfv K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W Y B G F Y = Y
39 38 adantrl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B G F Y = Y
40 37 39 breq12d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B G F X ˙ G F Y X ˙ Y
41 40 3adant3 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B F X ˙ F Y G F X ˙ G F Y X ˙ Y
42 35 41 mpbid K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B F X ˙ F Y X ˙ Y
43 42 3expia K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B F X ˙ F Y X ˙ Y
44 23 43 impbid K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B X ˙ Y F X ˙ F Y