Metamath Proof Explorer


Theorem cdleme16g

Description: Part of proof of Lemma E in Crawley p. 113, 3rd paragraph on p. 114, Eq. (1). F and G represent f(s) and f(t) respectively. We show, in their notation, (s \/ t) /\ w=(f(s) \/ f(t)) /\ w. (Contributed by NM, 11-Oct-2012)

Ref Expression
Hypotheses cdleme12.l ˙ = K
cdleme12.j ˙ = join K
cdleme12.m ˙ = meet K
cdleme12.a A = Atoms K
cdleme12.h H = LHyp K
cdleme12.u U = P ˙ Q ˙ W
cdleme12.f F = S ˙ U ˙ Q ˙ P ˙ S ˙ W
cdleme12.g G = T ˙ U ˙ Q ˙ P ˙ T ˙ W
Assertion cdleme16g K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q ¬ U ˙ S ˙ T S ˙ T ˙ W = F ˙ G ˙ W

Proof

Step Hyp Ref Expression
1 cdleme12.l ˙ = K
2 cdleme12.j ˙ = join K
3 cdleme12.m ˙ = meet K
4 cdleme12.a A = Atoms K
5 cdleme12.h H = LHyp K
6 cdleme12.u U = P ˙ Q ˙ W
7 cdleme12.f F = S ˙ U ˙ Q ˙ P ˙ S ˙ W
8 cdleme12.g G = T ˙ U ˙ Q ˙ P ˙ T ˙ W
9 1 2 3 4 5 6 7 8 cdleme16e K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q ¬ U ˙ S ˙ T S ˙ T ˙ F ˙ G = S ˙ T ˙ W
10 1 2 3 4 5 6 7 8 cdleme16f K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q ¬ U ˙ S ˙ T S ˙ T ˙ F ˙ G = F ˙ G ˙ W
11 9 10 eqtr3d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q ¬ U ˙ S ˙ T S ˙ T ˙ W = F ˙ G ˙ W