Metamath Proof Explorer


Theorem cdleme16aN

Description: Part of proof of Lemma E in Crawley p. 113, 3rd paragraph on p. 114, showing, in their notation, s \/ u =/= t \/ u. (Contributed by NM, 9-Oct-2012) (New usage is discouraged.)

Ref Expression
Hypotheses cdleme11.l ˙ = K
cdleme11.j ˙ = join K
cdleme11.m ˙ = meet K
cdleme11.a A = Atoms K
cdleme11.h H = LHyp K
cdleme11.u U = P ˙ Q ˙ W
Assertion cdleme16aN K HL W H P A ¬ P ˙ W Q A S A T A P Q S T ¬ U ˙ S ˙ T S ˙ U T ˙ U

Proof

Step Hyp Ref Expression
1 cdleme11.l ˙ = K
2 cdleme11.j ˙ = join K
3 cdleme11.m ˙ = meet K
4 cdleme11.a A = Atoms K
5 cdleme11.h H = LHyp K
6 cdleme11.u U = P ˙ Q ˙ W
7 simp1ll K HL W H P A ¬ P ˙ W Q A S A T A P Q S T ¬ U ˙ S ˙ T K HL
8 simp22 K HL W H P A ¬ P ˙ W Q A S A T A P Q S T ¬ U ˙ S ˙ T S A
9 simp23 K HL W H P A ¬ P ˙ W Q A S A T A P Q S T ¬ U ˙ S ˙ T T A
10 simp1l K HL W H P A ¬ P ˙ W Q A S A T A P Q S T ¬ U ˙ S ˙ T K HL W H
11 simp1r K HL W H P A ¬ P ˙ W Q A S A T A P Q S T ¬ U ˙ S ˙ T P A ¬ P ˙ W
12 simp21 K HL W H P A ¬ P ˙ W Q A S A T A P Q S T ¬ U ˙ S ˙ T Q A
13 simp31 K HL W H P A ¬ P ˙ W Q A S A T A P Q S T ¬ U ˙ S ˙ T P Q
14 1 2 3 4 5 6 lhpat2 K HL W H P A ¬ P ˙ W Q A P Q U A
15 10 11 12 13 14 syl112anc K HL W H P A ¬ P ˙ W Q A S A T A P Q S T ¬ U ˙ S ˙ T U A
16 simp32 K HL W H P A ¬ P ˙ W Q A S A T A P Q S T ¬ U ˙ S ˙ T S T
17 simp33 K HL W H P A ¬ P ˙ W Q A S A T A P Q S T ¬ U ˙ S ˙ T ¬ U ˙ S ˙ T
18 eqid LPlanes K = LPlanes K
19 1 2 4 18 lplni2 K HL S A T A U A S T ¬ U ˙ S ˙ T S ˙ T ˙ U LPlanes K
20 7 8 9 15 16 17 19 syl132anc K HL W H P A ¬ P ˙ W Q A S A T A P Q S T ¬ U ˙ S ˙ T S ˙ T ˙ U LPlanes K
21 eqid S ˙ T ˙ U = S ˙ T ˙ U
22 2 4 18 21 lplnllnneN K HL S A T A U A S ˙ T ˙ U LPlanes K S ˙ U T ˙ U
23 7 8 9 15 20 22 syl131anc K HL W H P A ¬ P ˙ W Q A S A T A P Q S T ¬ U ˙ S ˙ T S ˙ U T ˙ U