Metamath Proof Explorer


Theorem cdleme19f

Description: Part of proof of Lemma E in Crawley p. 113, 5th paragraph on p. 114, line 3. D , F , N , Y , G , O represent s_2, f(s), f_s(r), t_2, f(t), f_t(r). We prove that if r <_ s \/ t, then f_t(r) = f_t(r). (Contributed by NM, 14-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
cdleme19.n N = P ˙ Q ˙ F ˙ D
cdleme19.o O = P ˙ Q ˙ G ˙ Y
Assertion cdleme19f K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W R A P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q R ˙ S ˙ T N = O

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 cdleme19.n N = P ˙ Q ˙ F ˙ D
12 cdleme19.o O = P ˙ Q ˙ G ˙ Y
13 1 2 3 4 5 6 7 8 9 10 cdleme19e K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W R A P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q R ˙ S ˙ T F ˙ D = G ˙ Y
14 13 oveq2d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W R A P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q R ˙ S ˙ T P ˙ Q ˙ F ˙ D = P ˙ Q ˙ G ˙ Y
15 14 11 12 3eqtr4g K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W R A P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q R ˙ S ˙ T N = O