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
|- .<_ = ( le ` 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 e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( Q e. A /\ S e. A /\ T e. A ) /\ ( P =/= Q /\ S =/= T /\ -. U .<_ ( S .\/ T ) ) ) -> ( S .\/ U ) =/= ( T .\/ U ) )

Proof

Step Hyp Ref Expression
1 cdleme11.l
 |-  .<_ = ( le ` 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 e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( Q e. A /\ S e. A /\ T e. A ) /\ ( P =/= Q /\ S =/= T /\ -. U .<_ ( S .\/ T ) ) ) -> K e. HL )
8 simp22
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( Q e. A /\ S e. A /\ T e. A ) /\ ( P =/= Q /\ S =/= T /\ -. U .<_ ( S .\/ T ) ) ) -> S e. A )
9 simp23
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( Q e. A /\ S e. A /\ T e. A ) /\ ( P =/= Q /\ S =/= T /\ -. U .<_ ( S .\/ T ) ) ) -> T e. A )
10 simp1l
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( Q e. A /\ S e. A /\ T e. A ) /\ ( P =/= Q /\ S =/= T /\ -. U .<_ ( S .\/ T ) ) ) -> ( K e. HL /\ W e. H ) )
11 simp1r
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( Q e. A /\ S e. A /\ T e. A ) /\ ( P =/= Q /\ S =/= T /\ -. U .<_ ( S .\/ T ) ) ) -> ( P e. A /\ -. P .<_ W ) )
12 simp21
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( Q e. A /\ S e. A /\ T e. A ) /\ ( P =/= Q /\ S =/= T /\ -. U .<_ ( S .\/ T ) ) ) -> Q e. A )
13 simp31
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( Q e. A /\ S e. A /\ T e. A ) /\ ( P =/= Q /\ S =/= T /\ -. U .<_ ( S .\/ T ) ) ) -> P =/= Q )
14 1 2 3 4 5 6 lhpat2
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ P =/= Q ) ) -> U e. A )
15 10 11 12 13 14 syl112anc
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( Q e. A /\ S e. A /\ T e. A ) /\ ( P =/= Q /\ S =/= T /\ -. U .<_ ( S .\/ T ) ) ) -> U e. A )
16 simp32
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( Q e. A /\ S e. A /\ T e. A ) /\ ( P =/= Q /\ S =/= T /\ -. U .<_ ( S .\/ T ) ) ) -> S =/= T )
17 simp33
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( Q e. A /\ S e. A /\ T e. A ) /\ ( P =/= Q /\ S =/= T /\ -. U .<_ ( S .\/ T ) ) ) -> -. U .<_ ( S .\/ T ) )
18 eqid
 |-  ( LPlanes ` K ) = ( LPlanes ` K )
19 1 2 4 18 lplni2
 |-  ( ( K e. HL /\ ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) -> ( ( S .\/ T ) .\/ U ) e. ( LPlanes ` K ) )
20 7 8 9 15 16 17 19 syl132anc
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( Q e. A /\ S e. A /\ T e. A ) /\ ( P =/= Q /\ S =/= T /\ -. U .<_ ( S .\/ T ) ) ) -> ( ( S .\/ T ) .\/ U ) e. ( LPlanes ` K ) )
21 eqid
 |-  ( ( S .\/ T ) .\/ U ) = ( ( S .\/ T ) .\/ U )
22 2 4 18 21 lplnllnneN
 |-  ( ( K e. HL /\ ( S e. A /\ T e. A /\ U e. A ) /\ ( ( S .\/ T ) .\/ U ) e. ( LPlanes ` K ) ) -> ( S .\/ U ) =/= ( T .\/ U ) )
23 7 8 9 15 20 22 syl131anc
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( Q e. A /\ S e. A /\ T e. A ) /\ ( P =/= Q /\ S =/= T /\ -. U .<_ ( S .\/ T ) ) ) -> ( S .\/ U ) =/= ( T .\/ U ) )