Metamath Proof Explorer


Theorem 4atex

Description: Whenever there are at least 4 atoms under P .\/ Q (specifically, P , Q , r , and ( P .\/ Q ) ./\ W ), there are also at least 4 atoms under P .\/ S . This proves the statement in Lemma E of Crawley p. 114, last line, "...p \/ q/0 and hence p \/ s/0 contains at least four atoms..." Note that by cvlsupr2 , our ( P .\/ r ) = ( Q .\/ r ) is a shorter way to express r =/= P /\ r =/= Q /\ r .<_ ( P .\/ Q ) . (Contributed by NM, 27-May-2013)

Ref Expression
Hypotheses 4that.l
|- .<_ = ( le ` K )
4that.j
|- .\/ = ( join ` K )
4that.a
|- A = ( Atoms ` K )
4that.h
|- H = ( LHyp ` K )
Assertion 4atex
|- ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ S e. A ) /\ ( P =/= Q /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> E. z e. A ( -. z .<_ W /\ ( P .\/ z ) = ( S .\/ z ) ) )

Proof

Step Hyp Ref Expression
1 4that.l
 |-  .<_ = ( le ` K )
2 4that.j
 |-  .\/ = ( join ` K )
3 4that.a
 |-  A = ( Atoms ` K )
4 4that.h
 |-  H = ( LHyp ` K )
5 simp21l
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ S e. A ) /\ ( P =/= Q /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> P e. A )
6 5 ad2antrr
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ S e. A ) /\ ( P =/= Q /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ S .<_ ( P .\/ Q ) ) /\ S = P ) -> P e. A )
7 simp21r
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ S e. A ) /\ ( P =/= Q /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> -. P .<_ W )
8 7 ad2antrr
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ S e. A ) /\ ( P =/= Q /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ S .<_ ( P .\/ Q ) ) /\ S = P ) -> -. P .<_ W )
9 oveq1
 |-  ( P = S -> ( P .\/ P ) = ( S .\/ P ) )
10 9 eqcoms
 |-  ( S = P -> ( P .\/ P ) = ( S .\/ P ) )
11 10 adantl
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ S e. A ) /\ ( P =/= Q /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ S .<_ ( P .\/ Q ) ) /\ S = P ) -> ( P .\/ P ) = ( S .\/ P ) )
12 breq1
 |-  ( z = P -> ( z .<_ W <-> P .<_ W ) )
13 12 notbid
 |-  ( z = P -> ( -. z .<_ W <-> -. P .<_ W ) )
14 oveq2
 |-  ( z = P -> ( P .\/ z ) = ( P .\/ P ) )
15 oveq2
 |-  ( z = P -> ( S .\/ z ) = ( S .\/ P ) )
16 14 15 eqeq12d
 |-  ( z = P -> ( ( P .\/ z ) = ( S .\/ z ) <-> ( P .\/ P ) = ( S .\/ P ) ) )
17 13 16 anbi12d
 |-  ( z = P -> ( ( -. z .<_ W /\ ( P .\/ z ) = ( S .\/ z ) ) <-> ( -. P .<_ W /\ ( P .\/ P ) = ( S .\/ P ) ) ) )
18 17 rspcev
 |-  ( ( P e. A /\ ( -. P .<_ W /\ ( P .\/ P ) = ( S .\/ P ) ) ) -> E. z e. A ( -. z .<_ W /\ ( P .\/ z ) = ( S .\/ z ) ) )
19 6 8 11 18 syl12anc
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ S e. A ) /\ ( P =/= Q /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ S .<_ ( P .\/ Q ) ) /\ S = P ) -> E. z e. A ( -. z .<_ W /\ ( P .\/ z ) = ( S .\/ z ) ) )
20 simpl3r
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ S e. A ) /\ ( P =/= Q /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ S .<_ ( P .\/ Q ) ) -> E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) )
21 20 ad2antrr
 |-  ( ( ( ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ S e. A ) /\ ( P =/= Q /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ S .<_ ( P .\/ Q ) ) /\ S =/= P ) /\ S = Q ) -> E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) )
22 breq1
 |-  ( r = z -> ( r .<_ W <-> z .<_ W ) )
23 22 notbid
 |-  ( r = z -> ( -. r .<_ W <-> -. z .<_ W ) )
24 oveq2
 |-  ( r = z -> ( P .\/ r ) = ( P .\/ z ) )
25 oveq2
 |-  ( r = z -> ( Q .\/ r ) = ( Q .\/ z ) )
26 24 25 eqeq12d
 |-  ( r = z -> ( ( P .\/ r ) = ( Q .\/ r ) <-> ( P .\/ z ) = ( Q .\/ z ) ) )
27 23 26 anbi12d
 |-  ( r = z -> ( ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) <-> ( -. z .<_ W /\ ( P .\/ z ) = ( Q .\/ z ) ) ) )
28 27 cbvrexvw
 |-  ( E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) <-> E. z e. A ( -. z .<_ W /\ ( P .\/ z ) = ( Q .\/ z ) ) )
29 oveq1
 |-  ( S = Q -> ( S .\/ z ) = ( Q .\/ z ) )
30 29 eqeq2d
 |-  ( S = Q -> ( ( P .\/ z ) = ( S .\/ z ) <-> ( P .\/ z ) = ( Q .\/ z ) ) )
31 30 anbi2d
 |-  ( S = Q -> ( ( -. z .<_ W /\ ( P .\/ z ) = ( S .\/ z ) ) <-> ( -. z .<_ W /\ ( P .\/ z ) = ( Q .\/ z ) ) ) )
32 31 rexbidv
 |-  ( S = Q -> ( E. z e. A ( -. z .<_ W /\ ( P .\/ z ) = ( S .\/ z ) ) <-> E. z e. A ( -. z .<_ W /\ ( P .\/ z ) = ( Q .\/ z ) ) ) )
33 28 32 bitr4id
 |-  ( S = Q -> ( E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) <-> E. z e. A ( -. z .<_ W /\ ( P .\/ z ) = ( S .\/ z ) ) ) )
34 33 adantl
 |-  ( ( ( ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ S e. A ) /\ ( P =/= Q /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ S .<_ ( P .\/ Q ) ) /\ S =/= P ) /\ S = Q ) -> ( E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) <-> E. z e. A ( -. z .<_ W /\ ( P .\/ z ) = ( S .\/ z ) ) ) )
35 21 34 mpbid
 |-  ( ( ( ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ S e. A ) /\ ( P =/= Q /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ S .<_ ( P .\/ Q ) ) /\ S =/= P ) /\ S = Q ) -> E. z e. A ( -. z .<_ W /\ ( P .\/ z ) = ( S .\/ z ) ) )
36 simp22l
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ S e. A ) /\ ( P =/= Q /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> Q e. A )
37 36 ad3antrrr
 |-  ( ( ( ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ S e. A ) /\ ( P =/= Q /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ S .<_ ( P .\/ Q ) ) /\ S =/= P ) /\ S =/= Q ) -> Q e. A )
38 simp22r
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ S e. A ) /\ ( P =/= Q /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> -. Q .<_ W )
39 38 ad3antrrr
 |-  ( ( ( ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ S e. A ) /\ ( P =/= Q /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ S .<_ ( P .\/ Q ) ) /\ S =/= P ) /\ S =/= Q ) -> -. Q .<_ W )
40 simp3l
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ S e. A ) /\ ( P =/= Q /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> P =/= Q )
41 40 necomd
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ S e. A ) /\ ( P =/= Q /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> Q =/= P )
42 41 ad3antrrr
 |-  ( ( ( ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ S e. A ) /\ ( P =/= Q /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ S .<_ ( P .\/ Q ) ) /\ S =/= P ) /\ S =/= Q ) -> Q =/= P )
43 simpr
 |-  ( ( ( ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ S e. A ) /\ ( P =/= Q /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ S .<_ ( P .\/ Q ) ) /\ S =/= P ) /\ S =/= Q ) -> S =/= Q )
44 43 necomd
 |-  ( ( ( ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ S e. A ) /\ ( P =/= Q /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ S .<_ ( P .\/ Q ) ) /\ S =/= P ) /\ S =/= Q ) -> Q =/= S )
45 simpllr
 |-  ( ( ( ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ S e. A ) /\ ( P =/= Q /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ S .<_ ( P .\/ Q ) ) /\ S =/= P ) /\ S =/= Q ) -> S .<_ ( P .\/ Q ) )
46 simp1l
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ S e. A ) /\ ( P =/= Q /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> K e. HL )
47 hlcvl
 |-  ( K e. HL -> K e. CvLat )
48 46 47 syl
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ S e. A ) /\ ( P =/= Q /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> K e. CvLat )
49 48 ad3antrrr
 |-  ( ( ( ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ S e. A ) /\ ( P =/= Q /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ S .<_ ( P .\/ Q ) ) /\ S =/= P ) /\ S =/= Q ) -> K e. CvLat )
50 simp23
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ S e. A ) /\ ( P =/= Q /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> S e. A )
51 50 ad3antrrr
 |-  ( ( ( ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ S e. A ) /\ ( P =/= Q /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ S .<_ ( P .\/ Q ) ) /\ S =/= P ) /\ S =/= Q ) -> S e. A )
52 5 ad3antrrr
 |-  ( ( ( ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ S e. A ) /\ ( P =/= Q /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ S .<_ ( P .\/ Q ) ) /\ S =/= P ) /\ S =/= Q ) -> P e. A )
53 simplr
 |-  ( ( ( ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ S e. A ) /\ ( P =/= Q /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ S .<_ ( P .\/ Q ) ) /\ S =/= P ) /\ S =/= Q ) -> S =/= P )
54 1 2 3 cvlatexch1
 |-  ( ( K e. CvLat /\ ( S e. A /\ Q e. A /\ P e. A ) /\ S =/= P ) -> ( S .<_ ( P .\/ Q ) -> Q .<_ ( P .\/ S ) ) )
55 49 51 37 52 53 54 syl131anc
 |-  ( ( ( ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ S e. A ) /\ ( P =/= Q /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ S .<_ ( P .\/ Q ) ) /\ S =/= P ) /\ S =/= Q ) -> ( S .<_ ( P .\/ Q ) -> Q .<_ ( P .\/ S ) ) )
56 45 55 mpd
 |-  ( ( ( ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ S e. A ) /\ ( P =/= Q /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ S .<_ ( P .\/ Q ) ) /\ S =/= P ) /\ S =/= Q ) -> Q .<_ ( P .\/ S ) )
57 53 necomd
 |-  ( ( ( ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ S e. A ) /\ ( P =/= Q /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ S .<_ ( P .\/ Q ) ) /\ S =/= P ) /\ S =/= Q ) -> P =/= S )
58 3 1 2 cvlsupr2
 |-  ( ( K e. CvLat /\ ( P e. A /\ S e. A /\ Q e. A ) /\ P =/= S ) -> ( ( P .\/ Q ) = ( S .\/ Q ) <-> ( Q =/= P /\ Q =/= S /\ Q .<_ ( P .\/ S ) ) ) )
59 49 52 51 37 57 58 syl131anc
 |-  ( ( ( ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ S e. A ) /\ ( P =/= Q /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ S .<_ ( P .\/ Q ) ) /\ S =/= P ) /\ S =/= Q ) -> ( ( P .\/ Q ) = ( S .\/ Q ) <-> ( Q =/= P /\ Q =/= S /\ Q .<_ ( P .\/ S ) ) ) )
60 42 44 56 59 mpbir3and
 |-  ( ( ( ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ S e. A ) /\ ( P =/= Q /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ S .<_ ( P .\/ Q ) ) /\ S =/= P ) /\ S =/= Q ) -> ( P .\/ Q ) = ( S .\/ Q ) )
61 breq1
 |-  ( z = Q -> ( z .<_ W <-> Q .<_ W ) )
62 61 notbid
 |-  ( z = Q -> ( -. z .<_ W <-> -. Q .<_ W ) )
63 oveq2
 |-  ( z = Q -> ( P .\/ z ) = ( P .\/ Q ) )
64 oveq2
 |-  ( z = Q -> ( S .\/ z ) = ( S .\/ Q ) )
65 63 64 eqeq12d
 |-  ( z = Q -> ( ( P .\/ z ) = ( S .\/ z ) <-> ( P .\/ Q ) = ( S .\/ Q ) ) )
66 62 65 anbi12d
 |-  ( z = Q -> ( ( -. z .<_ W /\ ( P .\/ z ) = ( S .\/ z ) ) <-> ( -. Q .<_ W /\ ( P .\/ Q ) = ( S .\/ Q ) ) ) )
67 66 rspcev
 |-  ( ( Q e. A /\ ( -. Q .<_ W /\ ( P .\/ Q ) = ( S .\/ Q ) ) ) -> E. z e. A ( -. z .<_ W /\ ( P .\/ z ) = ( S .\/ z ) ) )
68 37 39 60 67 syl12anc
 |-  ( ( ( ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ S e. A ) /\ ( P =/= Q /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ S .<_ ( P .\/ Q ) ) /\ S =/= P ) /\ S =/= Q ) -> E. z e. A ( -. z .<_ W /\ ( P .\/ z ) = ( S .\/ z ) ) )
69 35 68 pm2.61dane
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ S e. A ) /\ ( P =/= Q /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ S .<_ ( P .\/ Q ) ) /\ S =/= P ) -> E. z e. A ( -. z .<_ W /\ ( P .\/ z ) = ( S .\/ z ) ) )
70 19 69 pm2.61dane
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ S e. A ) /\ ( P =/= Q /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ S .<_ ( P .\/ Q ) ) -> E. z e. A ( -. z .<_ W /\ ( P .\/ z ) = ( S .\/ z ) ) )
71 simpl1
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ S e. A ) /\ ( P =/= Q /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ -. S .<_ ( P .\/ Q ) ) -> ( K e. HL /\ W e. H ) )
72 simpl2
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ S e. A ) /\ ( P =/= Q /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ -. S .<_ ( P .\/ Q ) ) -> ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ S e. A ) )
73 simpl3l
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ S e. A ) /\ ( P =/= Q /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ -. S .<_ ( P .\/ Q ) ) -> P =/= Q )
74 simpr
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ S e. A ) /\ ( P =/= Q /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ -. S .<_ ( P .\/ Q ) ) -> -. S .<_ ( P .\/ Q ) )
75 simpl3r
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ S e. A ) /\ ( P =/= Q /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ -. S .<_ ( P .\/ Q ) ) -> E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) )
76 1 2 3 4 4atexlem7
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ S e. A ) /\ ( P =/= Q /\ -. S .<_ ( P .\/ Q ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> E. z e. A ( -. z .<_ W /\ ( P .\/ z ) = ( S .\/ z ) ) )
77 71 72 73 74 75 76 syl113anc
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ S e. A ) /\ ( P =/= Q /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ -. S .<_ ( P .\/ Q ) ) -> E. z e. A ( -. z .<_ W /\ ( P .\/ z ) = ( S .\/ z ) ) )
78 70 77 pm2.61dan
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ S e. A ) /\ ( P =/= Q /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> E. z e. A ( -. z .<_ W /\ ( P .\/ z ) = ( S .\/ z ) ) )