Metamath Proof Explorer


Theorem cdleme32f

Description: Part of proof of Lemma D in Crawley p. 113. (Contributed by NM, 20-Feb-2013)

Ref Expression
Hypotheses cdleme32.b B = Base K
cdleme32.l ˙ = K
cdleme32.j ˙ = join K
cdleme32.m ˙ = meet K
cdleme32.a A = Atoms K
cdleme32.h H = LHyp K
cdleme32.u U = P ˙ Q ˙ W
cdleme32.c C = s ˙ U ˙ Q ˙ P ˙ s ˙ W
cdleme32.d D = t ˙ U ˙ Q ˙ P ˙ t ˙ W
cdleme32.e E = P ˙ Q ˙ D ˙ s ˙ t ˙ W
cdleme32.i I = ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = E
cdleme32.n N = if s ˙ P ˙ Q I C
cdleme32.o O = ι z B | s A ¬ s ˙ W s ˙ x ˙ W = x z = N ˙ x ˙ W
cdleme32.f F = x B if P Q ¬ x ˙ W O x
Assertion cdleme32f K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B ¬ P Q ¬ X ˙ W P Q ¬ Y ˙ W X ˙ Y F X ˙ F Y

Proof

Step Hyp Ref Expression
1 cdleme32.b B = Base K
2 cdleme32.l ˙ = K
3 cdleme32.j ˙ = join K
4 cdleme32.m ˙ = meet K
5 cdleme32.a A = Atoms K
6 cdleme32.h H = LHyp K
7 cdleme32.u U = P ˙ Q ˙ W
8 cdleme32.c C = s ˙ U ˙ Q ˙ P ˙ s ˙ W
9 cdleme32.d D = t ˙ U ˙ Q ˙ P ˙ t ˙ W
10 cdleme32.e E = P ˙ Q ˙ D ˙ s ˙ t ˙ W
11 cdleme32.i I = ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = E
12 cdleme32.n N = if s ˙ P ˙ Q I C
13 cdleme32.o O = ι z B | s A ¬ s ˙ W s ˙ x ˙ W = x z = N ˙ x ˙ W
14 cdleme32.f F = x B if P Q ¬ x ˙ W O x
15 simp11 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B ¬ P Q ¬ X ˙ W P Q ¬ Y ˙ W X ˙ Y K HL W H
16 simp21r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B ¬ P Q ¬ X ˙ W P Q ¬ Y ˙ W X ˙ Y Y B
17 simp23r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B ¬ P Q ¬ X ˙ W P Q ¬ Y ˙ W X ˙ Y ¬ Y ˙ W
18 1 2 3 4 5 6 lhpmcvr2 K HL W H Y B ¬ Y ˙ W s A ¬ s ˙ W s ˙ Y ˙ W = Y
19 15 16 17 18 syl12anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B ¬ P Q ¬ X ˙ W P Q ¬ Y ˙ W X ˙ Y s A ¬ s ˙ W s ˙ Y ˙ W = Y
20 nfv s K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B ¬ P Q ¬ X ˙ W P Q ¬ Y ˙ W X ˙ Y
21 nfcv _ s B
22 nfv s P Q ¬ x ˙ W
23 nfra1 s s A ¬ s ˙ W s ˙ x ˙ W = x z = N ˙ x ˙ W
24 23 21 nfriota _ s ι z B | s A ¬ s ˙ W s ˙ x ˙ W = x z = N ˙ x ˙ W
25 13 24 nfcxfr _ s O
26 nfcv _ s x
27 22 25 26 nfif _ s if P Q ¬ x ˙ W O x
28 21 27 nfmpt _ s x B if P Q ¬ x ˙ W O x
29 14 28 nfcxfr _ s F
30 nfcv _ s X
31 29 30 nffv _ s F X
32 nfcv _ s ˙
33 nfcv _ s Y
34 29 33 nffv _ s F Y
35 31 32 34 nfbr s F X ˙ F Y
36 simpl1 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B ¬ P Q ¬ X ˙ W P Q ¬ Y ˙ W X ˙ Y s A ¬ s ˙ W s ˙ Y ˙ W = Y K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W
37 simpl2 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B ¬ P Q ¬ X ˙ W P Q ¬ Y ˙ W X ˙ Y s A ¬ s ˙ W s ˙ Y ˙ W = Y X B Y B ¬ P Q ¬ X ˙ W P Q ¬ Y ˙ W
38 simprl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B ¬ P Q ¬ X ˙ W P Q ¬ Y ˙ W X ˙ Y s A ¬ s ˙ W s ˙ Y ˙ W = Y s A
39 simprrl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B ¬ P Q ¬ X ˙ W P Q ¬ Y ˙ W X ˙ Y s A ¬ s ˙ W s ˙ Y ˙ W = Y ¬ s ˙ W
40 38 39 jca K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B ¬ P Q ¬ X ˙ W P Q ¬ Y ˙ W X ˙ Y s A ¬ s ˙ W s ˙ Y ˙ W = Y s A ¬ s ˙ W
41 simprrr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B ¬ P Q ¬ X ˙ W P Q ¬ Y ˙ W X ˙ Y s A ¬ s ˙ W s ˙ Y ˙ W = Y s ˙ Y ˙ W = Y
42 simpl3 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B ¬ P Q ¬ X ˙ W P Q ¬ Y ˙ W X ˙ Y s A ¬ s ˙ W s ˙ Y ˙ W = Y X ˙ Y
43 1 2 3 4 5 6 7 8 9 10 11 12 13 14 cdleme32e K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B ¬ P Q ¬ X ˙ W P Q ¬ Y ˙ W s A ¬ s ˙ W s ˙ Y ˙ W = Y X ˙ Y F X ˙ F Y
44 36 37 40 41 42 43 syl113anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B ¬ P Q ¬ X ˙ W P Q ¬ Y ˙ W X ˙ Y s A ¬ s ˙ W s ˙ Y ˙ W = Y F X ˙ F Y
45 44 exp32 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B ¬ P Q ¬ X ˙ W P Q ¬ Y ˙ W X ˙ Y s A ¬ s ˙ W s ˙ Y ˙ W = Y F X ˙ F Y
46 20 35 45 rexlimd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B ¬ P Q ¬ X ˙ W P Q ¬ Y ˙ W X ˙ Y s A ¬ s ˙ W s ˙ Y ˙ W = Y F X ˙ F Y
47 19 46 mpd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B ¬ P Q ¬ X ˙ W P Q ¬ Y ˙ W X ˙ Y F X ˙ F Y