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