Metamath Proof Explorer


Theorem cdleme2

Description: Part of proof of Lemma E in Crawley p. 113. F represents f(r). W is the fiducial co-atom (hyperplane) w. Here we show that (r \/ f(r)) /\ w = u in their notation (4th line from bottom on p. 113). (Contributed by NM, 5-Jun-2012)

Ref Expression
Hypotheses cdleme1.l ˙ = K
cdleme1.j ˙ = join K
cdleme1.m ˙ = meet K
cdleme1.a A = Atoms K
cdleme1.h H = LHyp K
cdleme1.u U = P ˙ Q ˙ W
cdleme1.f F = R ˙ U ˙ Q ˙ P ˙ R ˙ W
Assertion cdleme2 K HL W H P A Q A R A ¬ R ˙ W R ˙ F ˙ W = U

Proof

Step Hyp Ref Expression
1 cdleme1.l ˙ = K
2 cdleme1.j ˙ = join K
3 cdleme1.m ˙ = meet K
4 cdleme1.a A = Atoms K
5 cdleme1.h H = LHyp K
6 cdleme1.u U = P ˙ Q ˙ W
7 cdleme1.f F = R ˙ U ˙ Q ˙ P ˙ R ˙ W
8 1 2 3 4 5 6 7 cdleme1 K HL W H P A Q A R A ¬ R ˙ W R ˙ F = R ˙ U
9 8 oveq1d K HL W H P A Q A R A ¬ R ˙ W R ˙ F ˙ W = R ˙ U ˙ W
10 simpll K HL W H P A Q A R A ¬ R ˙ W K HL
11 simpr3l K HL W H P A Q A R A ¬ R ˙ W R A
12 hllat K HL K Lat
13 12 ad2antrr K HL W H P A Q A R A ¬ R ˙ W K Lat
14 simpr1 K HL W H P A Q A R A ¬ R ˙ W P A
15 eqid Base K = Base K
16 15 4 atbase P A P Base K
17 14 16 syl K HL W H P A Q A R A ¬ R ˙ W P Base K
18 simpr2 K HL W H P A Q A R A ¬ R ˙ W Q A
19 15 4 atbase Q A Q Base K
20 18 19 syl K HL W H P A Q A R A ¬ R ˙ W Q Base K
21 15 2 latjcl K Lat P Base K Q Base K P ˙ Q Base K
22 13 17 20 21 syl3anc K HL W H P A Q A R A ¬ R ˙ W P ˙ Q Base K
23 15 5 lhpbase W H W Base K
24 23 ad2antlr K HL W H P A Q A R A ¬ R ˙ W W Base K
25 15 3 latmcl K Lat P ˙ Q Base K W Base K P ˙ Q ˙ W Base K
26 13 22 24 25 syl3anc K HL W H P A Q A R A ¬ R ˙ W P ˙ Q ˙ W Base K
27 6 26 eqeltrid K HL W H P A Q A R A ¬ R ˙ W U Base K
28 15 1 3 latmle2 K Lat P ˙ Q Base K W Base K P ˙ Q ˙ W ˙ W
29 13 22 24 28 syl3anc K HL W H P A Q A R A ¬ R ˙ W P ˙ Q ˙ W ˙ W
30 6 29 eqbrtrid K HL W H P A Q A R A ¬ R ˙ W U ˙ W
31 15 1 2 3 4 atmod4i2 K HL R A U Base K W Base K U ˙ W R ˙ W ˙ U = R ˙ U ˙ W
32 10 11 27 24 30 31 syl131anc K HL W H P A Q A R A ¬ R ˙ W R ˙ W ˙ U = R ˙ U ˙ W
33 eqid 0. K = 0. K
34 1 3 33 4 5 lhpmat K HL W H R A ¬ R ˙ W R ˙ W = 0. K
35 34 3ad2antr3 K HL W H P A Q A R A ¬ R ˙ W R ˙ W = 0. K
36 35 oveq1d K HL W H P A Q A R A ¬ R ˙ W R ˙ W ˙ U = 0. K ˙ U
37 hlol K HL K OL
38 37 ad2antrr K HL W H P A Q A R A ¬ R ˙ W K OL
39 15 2 33 olj02 K OL U Base K 0. K ˙ U = U
40 38 27 39 syl2anc K HL W H P A Q A R A ¬ R ˙ W 0. K ˙ U = U
41 36 40 eqtrd K HL W H P A Q A R A ¬ R ˙ W R ˙ W ˙ U = U
42 9 32 41 3eqtr2d K HL W H P A Q A R A ¬ R ˙ W R ˙ F ˙ W = U