Metamath Proof Explorer


Theorem cdleme42ke

Description: Part of proof of Lemma E in Crawley p. 113. Remove R =/= S condition. TODO: FIX COMMENT. (Contributed by NM, 2-Apr-2013)

Ref Expression
Hypotheses cdleme41.b B = Base K
cdleme41.l ˙ = K
cdleme41.j ˙ = join K
cdleme41.m ˙ = meet K
cdleme41.a A = Atoms K
cdleme41.h H = LHyp K
cdleme41.u U = P ˙ Q ˙ W
cdleme41.d D = s ˙ U ˙ Q ˙ P ˙ s ˙ W
cdleme41.e E = t ˙ U ˙ Q ˙ P ˙ t ˙ W
cdleme41.g G = P ˙ Q ˙ E ˙ s ˙ t ˙ W
cdleme41.i I = ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = G
cdleme41.n N = if s ˙ P ˙ Q I D
cdleme41.o O = ι z B | s A ¬ s ˙ W s ˙ x ˙ W = x z = N ˙ x ˙ W
cdleme41.f F = x B if P Q ¬ x ˙ W O x
cdleme34e.v V = R ˙ S ˙ W
Assertion cdleme42ke K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W F R ˙ F S = F R ˙ V

Proof

Step Hyp Ref Expression
1 cdleme41.b B = Base K
2 cdleme41.l ˙ = K
3 cdleme41.j ˙ = join K
4 cdleme41.m ˙ = meet K
5 cdleme41.a A = Atoms K
6 cdleme41.h H = LHyp K
7 cdleme41.u U = P ˙ Q ˙ W
8 cdleme41.d D = s ˙ U ˙ Q ˙ P ˙ s ˙ W
9 cdleme41.e E = t ˙ U ˙ Q ˙ P ˙ t ˙ W
10 cdleme41.g G = P ˙ Q ˙ E ˙ s ˙ t ˙ W
11 cdleme41.i I = ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = G
12 cdleme41.n N = if s ˙ P ˙ Q I D
13 cdleme41.o O = ι z B | s A ¬ s ˙ W s ˙ x ˙ W = x z = N ˙ x ˙ W
14 cdleme41.f F = x B if P Q ¬ x ˙ W O x
15 cdleme34e.v V = R ˙ S ˙ W
16 simpl1l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W K HL
17 simpr2 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R A ¬ R ˙ W
18 1 2 3 4 5 6 7 8 9 10 11 12 13 14 cdleme32fvaw K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W F R A ¬ F R ˙ W
19 17 18 syldan K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W F R A ¬ F R ˙ W
20 19 simpld K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W F R A
21 3 5 hlatjidm K HL F R A F R ˙ F R = F R
22 16 20 21 syl2anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W F R ˙ F R = F R
23 fveq2 R = S F R = F S
24 23 oveq2d R = S F R ˙ F R = F R ˙ F S
25 22 24 sylan9req K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R = S F R = F R ˙ F S
26 simpr2l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R A
27 3 5 hlatjidm K HL R A R ˙ R = R
28 16 26 27 syl2anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R ˙ R = R
29 28 oveq1d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R ˙ R ˙ W = R ˙ W
30 simpl1 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W K HL W H
31 eqid 0. K = 0. K
32 2 4 31 5 6 lhpmat K HL W H R A ¬ R ˙ W R ˙ W = 0. K
33 30 17 32 syl2anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R ˙ W = 0. K
34 29 33 eqtrd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R ˙ R ˙ W = 0. K
35 34 oveq2d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W F R ˙ R ˙ R ˙ W = F R ˙ 0. K
36 hlol K HL K OL
37 16 36 syl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W K OL
38 1 5 atbase F R A F R B
39 20 38 syl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W F R B
40 1 3 31 olj01 K OL F R B F R ˙ 0. K = F R
41 37 39 40 syl2anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W F R ˙ 0. K = F R
42 35 41 eqtrd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W F R ˙ R ˙ R ˙ W = F R
43 oveq2 R = S R ˙ R = R ˙ S
44 43 oveq1d R = S R ˙ R ˙ W = R ˙ S ˙ W
45 44 15 eqtr4di R = S R ˙ R ˙ W = V
46 45 oveq2d R = S F R ˙ R ˙ R ˙ W = F R ˙ V
47 42 46 sylan9req K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R = S F R = F R ˙ V
48 25 47 eqtr3d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R = S F R ˙ F S = F R ˙ V
49 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 cdleme42k K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R S F R ˙ F S = F R ˙ V
50 49 3expa K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R S F R ˙ F S = F R ˙ V
51 48 50 pm2.61dane K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W F R ˙ F S = F R ˙ V