Metamath Proof Explorer


Theorem cdleme7ga

Description: Part of proof of Lemma E in Crawley p. 113. See cdleme7 . (Contributed by NM, 8-Jun-2012)

Ref Expression
Hypotheses cdleme4.l
|- .<_ = ( le ` K )
cdleme4.j
|- .\/ = ( join ` K )
cdleme4.m
|- ./\ = ( meet ` K )
cdleme4.a
|- A = ( Atoms ` K )
cdleme4.h
|- H = ( LHyp ` K )
cdleme4.u
|- U = ( ( P .\/ Q ) ./\ W )
cdleme4.f
|- F = ( ( S .\/ U ) ./\ ( Q .\/ ( ( P .\/ S ) ./\ W ) ) )
cdleme4.g
|- G = ( ( P .\/ Q ) ./\ ( F .\/ ( ( R .\/ S ) ./\ W ) ) )
Assertion cdleme7ga
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> G e. A )

Proof

Step Hyp Ref Expression
1 cdleme4.l
 |-  .<_ = ( le ` K )
2 cdleme4.j
 |-  .\/ = ( join ` K )
3 cdleme4.m
 |-  ./\ = ( meet ` K )
4 cdleme4.a
 |-  A = ( Atoms ` K )
5 cdleme4.h
 |-  H = ( LHyp ` K )
6 cdleme4.u
 |-  U = ( ( P .\/ Q ) ./\ W )
7 cdleme4.f
 |-  F = ( ( S .\/ U ) ./\ ( Q .\/ ( ( P .\/ S ) ./\ W ) ) )
8 cdleme4.g
 |-  G = ( ( P .\/ Q ) ./\ ( F .\/ ( ( R .\/ S ) ./\ W ) ) )
9 simp11l
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> K e. HL )
10 simp12l
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> P e. A )
11 simp13l
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> Q e. A )
12 eqid
 |-  ( Base ` K ) = ( Base ` K )
13 12 2 4 hlatjcl
 |-  ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( P .\/ Q ) e. ( Base ` K ) )
14 9 10 11 13 syl3anc
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> ( P .\/ Q ) e. ( Base ` K ) )
15 simp11
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> ( K e. HL /\ W e. H ) )
16 simp12
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> ( P e. A /\ -. P .<_ W ) )
17 simp13
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> ( Q e. A /\ -. Q .<_ W ) )
18 simp2r
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> ( S e. A /\ -. S .<_ W ) )
19 simp31
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> P =/= Q )
20 simp33
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> -. S .<_ ( P .\/ Q ) )
21 1 2 3 4 5 6 7 cdleme3fa
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ -. S .<_ ( P .\/ Q ) ) ) -> F e. A )
22 15 16 17 18 19 20 21 syl132anc
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> F e. A )
23 simp2l
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> ( R e. A /\ -. R .<_ W ) )
24 simp2rl
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> S e. A )
25 simp32
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> R .<_ ( P .\/ Q ) )
26 eqid
 |-  ( ( R .\/ S ) ./\ W ) = ( ( R .\/ S ) ./\ W )
27 1 2 3 4 5 6 7 8 26 cdleme7b
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ ( P .\/ Q ) /\ R .<_ ( P .\/ Q ) ) ) -> ( ( R .\/ S ) ./\ W ) e. A )
28 15 23 24 20 25 27 syl113anc
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> ( ( R .\/ S ) ./\ W ) e. A )
29 12 2 4 hlatjcl
 |-  ( ( K e. HL /\ F e. A /\ ( ( R .\/ S ) ./\ W ) e. A ) -> ( F .\/ ( ( R .\/ S ) ./\ W ) ) e. ( Base ` K ) )
30 9 22 28 29 syl3anc
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> ( F .\/ ( ( R .\/ S ) ./\ W ) ) e. ( Base ` K ) )
31 9 hllatd
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> K e. Lat )
32 eqid
 |-  ( Lines ` K ) = ( Lines ` K )
33 eqid
 |-  ( pmap ` K ) = ( pmap ` K )
34 2 4 32 33 linepmap
 |-  ( ( ( K e. Lat /\ P e. A /\ Q e. A ) /\ P =/= Q ) -> ( ( pmap ` K ) ` ( P .\/ Q ) ) e. ( Lines ` K ) )
35 31 10 11 19 34 syl31anc
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> ( ( pmap ` K ) ` ( P .\/ Q ) ) e. ( Lines ` K ) )
36 simp2ll
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> R e. A )
37 12 2 4 hlatjcl
 |-  ( ( K e. HL /\ R e. A /\ S e. A ) -> ( R .\/ S ) e. ( Base ` K ) )
38 9 36 24 37 syl3anc
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> ( R .\/ S ) e. ( Base ` K ) )
39 simp11r
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> W e. H )
40 12 5 lhpbase
 |-  ( W e. H -> W e. ( Base ` K ) )
41 39 40 syl
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> W e. ( Base ` K ) )
42 12 1 3 latmle2
 |-  ( ( K e. Lat /\ ( R .\/ S ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) -> ( ( R .\/ S ) ./\ W ) .<_ W )
43 31 38 41 42 syl3anc
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> ( ( R .\/ S ) ./\ W ) .<_ W )
44 1 2 3 4 5 6 7 cdleme3
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ -. S .<_ ( P .\/ Q ) ) ) -> -. F .<_ W )
45 15 16 17 18 19 20 44 syl132anc
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> -. F .<_ W )
46 nbrne2
 |-  ( ( ( ( R .\/ S ) ./\ W ) .<_ W /\ -. F .<_ W ) -> ( ( R .\/ S ) ./\ W ) =/= F )
47 46 necomd
 |-  ( ( ( ( R .\/ S ) ./\ W ) .<_ W /\ -. F .<_ W ) -> F =/= ( ( R .\/ S ) ./\ W ) )
48 43 45 47 syl2anc
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> F =/= ( ( R .\/ S ) ./\ W ) )
49 2 4 32 33 linepmap
 |-  ( ( ( K e. Lat /\ F e. A /\ ( ( R .\/ S ) ./\ W ) e. A ) /\ F =/= ( ( R .\/ S ) ./\ W ) ) -> ( ( pmap ` K ) ` ( F .\/ ( ( R .\/ S ) ./\ W ) ) ) e. ( Lines ` K ) )
50 31 22 28 48 49 syl31anc
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> ( ( pmap ` K ) ` ( F .\/ ( ( R .\/ S ) ./\ W ) ) ) e. ( Lines ` K ) )
51 12 4 atbase
 |-  ( F e. A -> F e. ( Base ` K ) )
52 22 51 syl
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> F e. ( Base ` K ) )
53 12 3 latmcl
 |-  ( ( K e. Lat /\ ( R .\/ S ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) -> ( ( R .\/ S ) ./\ W ) e. ( Base ` K ) )
54 31 38 41 53 syl3anc
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> ( ( R .\/ S ) ./\ W ) e. ( Base ` K ) )
55 12 1 2 latlej2
 |-  ( ( K e. Lat /\ F e. ( Base ` K ) /\ ( ( R .\/ S ) ./\ W ) e. ( Base ` K ) ) -> ( ( R .\/ S ) ./\ W ) .<_ ( F .\/ ( ( R .\/ S ) ./\ W ) ) )
56 31 52 54 55 syl3anc
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> ( ( R .\/ S ) ./\ W ) .<_ ( F .\/ ( ( R .\/ S ) ./\ W ) ) )
57 1 2 3 4 5 6 7 8 26 cdleme7c
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> U =/= ( ( R .\/ S ) ./\ W ) )
58 15 16 11 23 18 19 25 20 57 syl323anc
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> U =/= ( ( R .\/ S ) ./\ W ) )
59 58 necomd
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> ( ( R .\/ S ) ./\ W ) =/= U )
60 hlatl
 |-  ( K e. HL -> K e. AtLat )
61 9 60 syl
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> K e. AtLat )
62 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 )
63 15 16 11 19 62 syl112anc
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> U e. A )
64 1 4 atncmp
 |-  ( ( K e. AtLat /\ ( ( R .\/ S ) ./\ W ) e. A /\ U e. A ) -> ( -. ( ( R .\/ S ) ./\ W ) .<_ U <-> ( ( R .\/ S ) ./\ W ) =/= U ) )
65 61 28 63 64 syl3anc
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> ( -. ( ( R .\/ S ) ./\ W ) .<_ U <-> ( ( R .\/ S ) ./\ W ) =/= U ) )
66 59 65 mpbird
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> -. ( ( R .\/ S ) ./\ W ) .<_ U )
67 12 1 3 latlem12
 |-  ( ( K e. Lat /\ ( ( ( R .\/ S ) ./\ W ) e. ( Base ` K ) /\ ( P .\/ Q ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) ) -> ( ( ( ( R .\/ S ) ./\ W ) .<_ ( P .\/ Q ) /\ ( ( R .\/ S ) ./\ W ) .<_ W ) <-> ( ( R .\/ S ) ./\ W ) .<_ ( ( P .\/ Q ) ./\ W ) ) )
68 31 54 14 41 67 syl13anc
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> ( ( ( ( R .\/ S ) ./\ W ) .<_ ( P .\/ Q ) /\ ( ( R .\/ S ) ./\ W ) .<_ W ) <-> ( ( R .\/ S ) ./\ W ) .<_ ( ( P .\/ Q ) ./\ W ) ) )
69 68 biimpd
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> ( ( ( ( R .\/ S ) ./\ W ) .<_ ( P .\/ Q ) /\ ( ( R .\/ S ) ./\ W ) .<_ W ) -> ( ( R .\/ S ) ./\ W ) .<_ ( ( P .\/ Q ) ./\ W ) ) )
70 43 69 mpan2d
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> ( ( ( R .\/ S ) ./\ W ) .<_ ( P .\/ Q ) -> ( ( R .\/ S ) ./\ W ) .<_ ( ( P .\/ Q ) ./\ W ) ) )
71 6 breq2i
 |-  ( ( ( R .\/ S ) ./\ W ) .<_ U <-> ( ( R .\/ S ) ./\ W ) .<_ ( ( P .\/ Q ) ./\ W ) )
72 70 71 syl6ibr
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> ( ( ( R .\/ S ) ./\ W ) .<_ ( P .\/ Q ) -> ( ( R .\/ S ) ./\ W ) .<_ U ) )
73 66 72 mtod
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> -. ( ( R .\/ S ) ./\ W ) .<_ ( P .\/ Q ) )
74 nbrne1
 |-  ( ( ( ( R .\/ S ) ./\ W ) .<_ ( F .\/ ( ( R .\/ S ) ./\ W ) ) /\ -. ( ( R .\/ S ) ./\ W ) .<_ ( P .\/ Q ) ) -> ( F .\/ ( ( R .\/ S ) ./\ W ) ) =/= ( P .\/ Q ) )
75 74 necomd
 |-  ( ( ( ( R .\/ S ) ./\ W ) .<_ ( F .\/ ( ( R .\/ S ) ./\ W ) ) /\ -. ( ( R .\/ S ) ./\ W ) .<_ ( P .\/ Q ) ) -> ( P .\/ Q ) =/= ( F .\/ ( ( R .\/ S ) ./\ W ) ) )
76 56 73 75 syl2anc
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> ( P .\/ Q ) =/= ( F .\/ ( ( R .\/ S ) ./\ W ) ) )
77 1 2 3 4 5 6 7 8 26 cdleme7e
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> G =/= ( 0. ` K ) )
78 8 77 eqnetrrid
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> ( ( P .\/ Q ) ./\ ( F .\/ ( ( R .\/ S ) ./\ W ) ) ) =/= ( 0. ` K ) )
79 eqid
 |-  ( 0. ` K ) = ( 0. ` K )
80 12 3 79 4 32 33 2lnat
 |-  ( ( ( K e. HL /\ ( P .\/ Q ) e. ( Base ` K ) /\ ( F .\/ ( ( R .\/ S ) ./\ W ) ) e. ( Base ` K ) ) /\ ( ( ( pmap ` K ) ` ( P .\/ Q ) ) e. ( Lines ` K ) /\ ( ( pmap ` K ) ` ( F .\/ ( ( R .\/ S ) ./\ W ) ) ) e. ( Lines ` K ) ) /\ ( ( P .\/ Q ) =/= ( F .\/ ( ( R .\/ S ) ./\ W ) ) /\ ( ( P .\/ Q ) ./\ ( F .\/ ( ( R .\/ S ) ./\ W ) ) ) =/= ( 0. ` K ) ) ) -> ( ( P .\/ Q ) ./\ ( F .\/ ( ( R .\/ S ) ./\ W ) ) ) e. A )
81 9 14 30 35 50 76 78 80 syl322anc
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> ( ( P .\/ Q ) ./\ ( F .\/ ( ( R .\/ S ) ./\ W ) ) ) e. A )
82 8 81 eqeltrid
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> G e. A )