Metamath Proof Explorer


Theorem cdleme43cN

Description: Part of proof of Lemma E in Crawley p. 113. TODO: FIX COMMENT p. 115 last line: r v g(s) = r v v_2. (Contributed by NM, 20-Mar-2013) (New usage is discouraged.)

Ref Expression
Hypotheses cdleme43.b B = Base K
cdleme43.l ˙ = K
cdleme43.j ˙ = join K
cdleme43.m ˙ = meet K
cdleme43.a A = Atoms K
cdleme43.h H = LHyp K
cdleme43.u U = P ˙ Q ˙ W
cdleme43.x X = Q ˙ P ˙ W
cdleme43.c C = S ˙ U ˙ Q ˙ P ˙ S ˙ W
cdleme43.f Z = P ˙ Q ˙ C ˙ R ˙ S ˙ W
cdleme43.d D = S ˙ X ˙ P ˙ Q ˙ S ˙ W
cdleme43.g G = Q ˙ P ˙ D ˙ Z ˙ S ˙ W
cdleme43.e E = D ˙ U ˙ Q ˙ P ˙ D ˙ W
cdleme43.v V = Z ˙ S ˙ W
cdleme43.y Y = R ˙ D ˙ W
Assertion cdleme43cN K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W ¬ S ˙ P ˙ Q R ˙ D = R ˙ Y

Proof

Step Hyp Ref Expression
1 cdleme43.b B = Base K
2 cdleme43.l ˙ = K
3 cdleme43.j ˙ = join K
4 cdleme43.m ˙ = meet K
5 cdleme43.a A = Atoms K
6 cdleme43.h H = LHyp K
7 cdleme43.u U = P ˙ Q ˙ W
8 cdleme43.x X = Q ˙ P ˙ W
9 cdleme43.c C = S ˙ U ˙ Q ˙ P ˙ S ˙ W
10 cdleme43.f Z = P ˙ Q ˙ C ˙ R ˙ S ˙ W
11 cdleme43.d D = S ˙ X ˙ P ˙ Q ˙ S ˙ W
12 cdleme43.g G = Q ˙ P ˙ D ˙ Z ˙ S ˙ W
13 cdleme43.e E = D ˙ U ˙ Q ˙ P ˙ D ˙ W
14 cdleme43.v V = Z ˙ S ˙ W
15 cdleme43.y Y = R ˙ D ˙ W
16 simp11 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W ¬ S ˙ P ˙ Q K HL W H
17 simp22 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W ¬ S ˙ P ˙ Q R A ¬ R ˙ W
18 simp1 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W ¬ S ˙ P ˙ Q K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W
19 simp21 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W ¬ S ˙ P ˙ Q P Q
20 simp23 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W ¬ S ˙ P ˙ Q S A ¬ S ˙ W
21 simp3 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W ¬ S ˙ P ˙ Q ¬ S ˙ P ˙ Q
22 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 cdleme43bN K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q S A ¬ S ˙ W ¬ S ˙ P ˙ Q D A ¬ D ˙ W
23 18 19 20 21 22 syl121anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W ¬ S ˙ P ˙ Q D A ¬ D ˙ W
24 1 2 3 4 5 6 15 cdleme42a K HL W H R A ¬ R ˙ W D A ¬ D ˙ W R ˙ D = R ˙ Y
25 16 17 23 24 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W ¬ S ˙ P ˙ Q R ˙ D = R ˙ Y