Metamath Proof Explorer


Theorem cdleme20h

Description: Part of proof of Lemma E in Crawley p. 113, last paragraph on p. 114, antepenultimate line. D , F , Y , G represent s_2, f(s), t_2, f(t). (Contributed by NM, 18-Nov-2012)

Ref Expression
Hypotheses cdleme19.l ˙ = K
cdleme19.j ˙ = join K
cdleme19.m ˙ = meet K
cdleme19.a A = Atoms K
cdleme19.h H = LHyp K
cdleme19.u U = P ˙ Q ˙ W
cdleme19.f F = S ˙ U ˙ Q ˙ P ˙ S ˙ W
cdleme19.g G = T ˙ U ˙ Q ˙ P ˙ T ˙ W
cdleme19.d D = R ˙ S ˙ W
cdleme19.y Y = R ˙ T ˙ W
cdleme20.v V = S ˙ T ˙ W
Assertion cdleme20h K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T ¬ U ˙ S ˙ T S ˙ R ˙ T ˙ R ˙ S ˙ U ˙ T ˙ U = R ˙ U

Proof

Step Hyp Ref Expression
1 cdleme19.l ˙ = K
2 cdleme19.j ˙ = join K
3 cdleme19.m ˙ = meet K
4 cdleme19.a A = Atoms K
5 cdleme19.h H = LHyp K
6 cdleme19.u U = P ˙ Q ˙ W
7 cdleme19.f F = S ˙ U ˙ Q ˙ P ˙ S ˙ W
8 cdleme19.g G = T ˙ U ˙ Q ˙ P ˙ T ˙ W
9 cdleme19.d D = R ˙ S ˙ W
10 cdleme19.y Y = R ˙ T ˙ W
11 cdleme20.v V = S ˙ T ˙ W
12 simp11l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T ¬ U ˙ S ˙ T K HL
13 simp21l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T ¬ U ˙ S ˙ T R A
14 simp22l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T ¬ U ˙ S ˙ T S A
15 simp23l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T ¬ U ˙ S ˙ T T A
16 simp31r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T ¬ U ˙ S ˙ T S T
17 simp33l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T ¬ U ˙ S ˙ T ¬ R ˙ S ˙ T
18 1 2 3 4 cdleme20y K HL R A S A T A S T ¬ R ˙ S ˙ T S ˙ R ˙ T ˙ R = R
19 12 13 14 15 16 17 18 syl132anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T ¬ U ˙ S ˙ T S ˙ R ˙ T ˙ R = R
20 simp11r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T ¬ U ˙ S ˙ T W H
21 simp12l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T ¬ U ˙ S ˙ T P A
22 simp12r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T ¬ U ˙ S ˙ T ¬ P ˙ W
23 simp13l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T ¬ U ˙ S ˙ T Q A
24 simp31l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T ¬ U ˙ S ˙ T P Q
25 1 2 3 4 5 6 lhpat2 K HL W H P A ¬ P ˙ W Q A P Q U A
26 12 20 21 22 23 24 25 syl222anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T ¬ U ˙ S ˙ T U A
27 simp33r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T ¬ U ˙ S ˙ T ¬ U ˙ S ˙ T
28 1 2 3 4 cdleme20y K HL U A S A T A S T ¬ U ˙ S ˙ T S ˙ U ˙ T ˙ U = U
29 12 26 14 15 16 27 28 syl132anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T ¬ U ˙ S ˙ T S ˙ U ˙ T ˙ U = U
30 19 29 oveq12d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T ¬ U ˙ S ˙ T S ˙ R ˙ T ˙ R ˙ S ˙ U ˙ T ˙ U = R ˙ U