Metamath Proof Explorer


Theorem cdleme32fva

Description: Part of proof of Lemma D in Crawley p. 113. Value of F at an atom not under W . (Contributed by NM, 2-Mar-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 cdleme32fva K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q R / x O = R / s N

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 simp2l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q R A
16 1 5 atbase R A R B
17 15 16 syl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q R B
18 eqid ι z B | s A ¬ s ˙ W s ˙ R ˙ W = R z = N ˙ R ˙ W = ι z B | s A ¬ s ˙ W s ˙ R ˙ W = R z = N ˙ R ˙ W
19 13 18 cdleme31so R B R / x O = ι z B | s A ¬ s ˙ W s ˙ R ˙ W = R z = N ˙ R ˙ W
20 17 19 syl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q R / x O = ι z B | s A ¬ s ˙ W s ˙ R ˙ W = R z = N ˙ R ˙ W
21 simp1 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W
22 simp3 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q P Q
23 simp2 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q R A ¬ R ˙ W
24 1 2 3 4 5 6 7 8 9 10 11 12 cdleme32snb K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W R / s N B
25 21 22 23 24 syl12anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q R / s N B
26 nfv s ¬ R ˙ W
27 nfcsb1v _ s R / s N
28 27 nfeq2 s z = R / s N
29 26 28 nfim s ¬ R ˙ W z = R / s N
30 breq1 s = R s ˙ W R ˙ W
31 30 notbid s = R ¬ s ˙ W ¬ R ˙ W
32 csbeq1a s = R N = R / s N
33 32 eqeq2d s = R z = N z = R / s N
34 31 33 imbi12d s = R ¬ s ˙ W z = N ¬ R ˙ W z = R / s N
35 34 ax-gen s s = R ¬ s ˙ W z = N ¬ R ˙ W z = R / s N
36 ceqsralt s ¬ R ˙ W z = R / s N s s = R ¬ s ˙ W z = N ¬ R ˙ W z = R / s N R A s A s = R ¬ s ˙ W z = N ¬ R ˙ W z = R / s N
37 29 35 36 mp3an12 R A s A s = R ¬ s ˙ W z = N ¬ R ˙ W z = R / s N
38 37 adantr R A ¬ R ˙ W s A s = R ¬ s ˙ W z = N ¬ R ˙ W z = R / s N
39 38 3ad2ant2 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q s A s = R ¬ s ˙ W z = N ¬ R ˙ W z = R / s N
40 simp11 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q K HL W H
41 eqid 0. K = 0. K
42 2 4 41 5 6 lhpmat K HL W H R A ¬ R ˙ W R ˙ W = 0. K
43 40 23 42 syl2anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q R ˙ W = 0. K
44 43 adantr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q s A ¬ s ˙ W R ˙ W = 0. K
45 44 oveq2d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q s A ¬ s ˙ W s ˙ R ˙ W = s ˙ 0. K
46 simp11l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q K HL
47 46 adantr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q s A ¬ s ˙ W K HL
48 hlol K HL K OL
49 47 48 syl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q s A ¬ s ˙ W K OL
50 1 5 atbase s A s B
51 50 ad2antrl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q s A ¬ s ˙ W s B
52 1 3 41 olj01 K OL s B s ˙ 0. K = s
53 49 51 52 syl2anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q s A ¬ s ˙ W s ˙ 0. K = s
54 45 53 eqtrd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q s A ¬ s ˙ W s ˙ R ˙ W = s
55 54 eqeq1d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q s A ¬ s ˙ W s ˙ R ˙ W = R s = R
56 44 oveq2d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q s A ¬ s ˙ W N ˙ R ˙ W = N ˙ 0. K
57 simpl11 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q s A ¬ s ˙ W K HL W H
58 simpl12 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q s A ¬ s ˙ W P A ¬ P ˙ W
59 simpl13 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q s A ¬ s ˙ W Q A ¬ Q ˙ W
60 simpr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q s A ¬ s ˙ W s A ¬ s ˙ W
61 simpl3 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q s A ¬ s ˙ W P Q
62 1 2 3 4 5 6 7 8 9 10 11 12 cdleme27cl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W s A ¬ s ˙ W P Q N B
63 57 58 59 60 61 62 syl122anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q s A ¬ s ˙ W N B
64 1 3 41 olj01 K OL N B N ˙ 0. K = N
65 49 63 64 syl2anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q s A ¬ s ˙ W N ˙ 0. K = N
66 56 65 eqtrd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q s A ¬ s ˙ W N ˙ R ˙ W = N
67 66 eqeq2d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q s A ¬ s ˙ W z = N ˙ R ˙ W z = N
68 55 67 imbi12d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q s A ¬ s ˙ W s ˙ R ˙ W = R z = N ˙ R ˙ W s = R z = N
69 68 expr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q s A ¬ s ˙ W s ˙ R ˙ W = R z = N ˙ R ˙ W s = R z = N
70 69 pm5.74d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q s A ¬ s ˙ W s ˙ R ˙ W = R z = N ˙ R ˙ W ¬ s ˙ W s = R z = N
71 impexp ¬ s ˙ W s ˙ R ˙ W = R z = N ˙ R ˙ W ¬ s ˙ W s ˙ R ˙ W = R z = N ˙ R ˙ W
72 bi2.04 s = R ¬ s ˙ W z = N ¬ s ˙ W s = R z = N
73 70 71 72 3bitr4g K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q s A ¬ s ˙ W s ˙ R ˙ W = R z = N ˙ R ˙ W s = R ¬ s ˙ W z = N
74 73 ralbidva K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q s A ¬ s ˙ W s ˙ R ˙ W = R z = N ˙ R ˙ W s A s = R ¬ s ˙ W z = N
75 simp2r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q ¬ R ˙ W
76 biimt ¬ R ˙ W z = R / s N ¬ R ˙ W z = R / s N
77 75 76 syl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q z = R / s N ¬ R ˙ W z = R / s N
78 39 74 77 3bitr4d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q s A ¬ s ˙ W s ˙ R ˙ W = R z = N ˙ R ˙ W z = R / s N
79 78 adantr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q z B s A ¬ s ˙ W s ˙ R ˙ W = R z = N ˙ R ˙ W z = R / s N
80 25 79 riota5 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q ι z B | s A ¬ s ˙ W s ˙ R ˙ W = R z = N ˙ R ˙ W = R / s N
81 20 80 eqtrd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q R / x O = R / s N