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 ) )