Metamath Proof Explorer


Theorem cdlemg33b0

Description: TODO: Fix comment. (Contributed by NM, 30-May-2013)

Ref Expression
Hypotheses cdlemg12.l
|- .<_ = ( le ` K )
cdlemg12.j
|- .\/ = ( join ` K )
cdlemg12.m
|- ./\ = ( meet ` K )
cdlemg12.a
|- A = ( Atoms ` K )
cdlemg12.h
|- H = ( LHyp ` K )
cdlemg12.t
|- T = ( ( LTrn ` K ) ` W )
cdlemg12b.r
|- R = ( ( trL ` K ) ` W )
cdlemg31.n
|- N = ( ( P .\/ v ) ./\ ( Q .\/ ( R ` F ) ) )
Assertion cdlemg33b0
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( v e. A /\ v .<_ W ) /\ N e. A /\ F e. T ) /\ ( P =/= Q /\ v =/= ( R ` F ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> E. z e. A ( -. z .<_ W /\ ( z =/= N /\ z .<_ ( P .\/ v ) ) ) )

Proof

Step Hyp Ref Expression
1 cdlemg12.l
 |-  .<_ = ( le ` K )
2 cdlemg12.j
 |-  .\/ = ( join ` K )
3 cdlemg12.m
 |-  ./\ = ( meet ` K )
4 cdlemg12.a
 |-  A = ( Atoms ` K )
5 cdlemg12.h
 |-  H = ( LHyp ` K )
6 cdlemg12.t
 |-  T = ( ( LTrn ` K ) ` W )
7 cdlemg12b.r
 |-  R = ( ( trL ` K ) ` W )
8 cdlemg31.n
 |-  N = ( ( P .\/ v ) ./\ ( Q .\/ ( R ` F ) ) )
9 simp11
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( v e. A /\ v .<_ W ) /\ N e. A /\ F e. T ) /\ ( P =/= Q /\ v =/= ( R ` F ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> ( K e. HL /\ W e. H ) )
10 simp12
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( v e. A /\ v .<_ W ) /\ N e. A /\ F e. T ) /\ ( P =/= Q /\ v =/= ( R ` F ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> ( P e. A /\ -. P .<_ W ) )
11 simp13
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( v e. A /\ v .<_ W ) /\ N e. A /\ F e. T ) /\ ( P =/= Q /\ v =/= ( R ` F ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> ( Q e. A /\ -. Q .<_ W ) )
12 simp22
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( v e. A /\ v .<_ W ) /\ N e. A /\ F e. T ) /\ ( P =/= Q /\ v =/= ( R ` F ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> N e. A )
13 simp21l
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( v e. A /\ v .<_ W ) /\ N e. A /\ F e. T ) /\ ( P =/= Q /\ v =/= ( R ` F ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> v e. A )
14 simp21r
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( v e. A /\ v .<_ W ) /\ N e. A /\ F e. T ) /\ ( P =/= Q /\ v =/= ( R ` F ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> v .<_ W )
15 13 14 jca
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( v e. A /\ v .<_ W ) /\ N e. A /\ F e. T ) /\ ( P =/= Q /\ v =/= ( R ` F ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> ( v e. A /\ v .<_ W ) )
16 simp23
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( v e. A /\ v .<_ W ) /\ N e. A /\ F e. T ) /\ ( P =/= Q /\ v =/= ( R ` F ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> F e. T )
17 simp32
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( v e. A /\ v .<_ W ) /\ N e. A /\ F e. T ) /\ ( P =/= Q /\ v =/= ( R ` F ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> v =/= ( R ` F ) )
18 1 2 3 4 5 6 7 8 cdlemg31d
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( v e. A /\ v .<_ W ) ) /\ ( F e. T /\ v =/= ( R ` F ) /\ N e. A ) ) -> -. N .<_ W )
19 9 10 11 15 16 17 12 18 syl133anc
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( v e. A /\ v .<_ W ) /\ N e. A /\ F e. T ) /\ ( P =/= Q /\ v =/= ( R ` F ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> -. N .<_ W )
20 12 19 jca
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( v e. A /\ v .<_ W ) /\ N e. A /\ F e. T ) /\ ( P =/= Q /\ v =/= ( R ` F ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> ( N e. A /\ -. N .<_ W ) )
21 simp31
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( v e. A /\ v .<_ W ) /\ N e. A /\ F e. T ) /\ ( P =/= Q /\ v =/= ( R ` F ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> P =/= Q )
22 nbrne2
 |-  ( ( v .<_ W /\ -. N .<_ W ) -> v =/= N )
23 22 necomd
 |-  ( ( v .<_ W /\ -. N .<_ W ) -> N =/= v )
24 14 19 23 syl2anc
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( v e. A /\ v .<_ W ) /\ N e. A /\ F e. T ) /\ ( P =/= Q /\ v =/= ( R ` F ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> N =/= v )
25 13 24 jca
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( v e. A /\ v .<_ W ) /\ N e. A /\ F e. T ) /\ ( P =/= Q /\ v =/= ( R ` F ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> ( v e. A /\ N =/= v ) )
26 simp33
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( v e. A /\ v .<_ W ) /\ N e. A /\ F e. T ) /\ ( P =/= Q /\ v =/= ( R ` F ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) )
27 1 2 4 5 4atex3
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( N e. A /\ -. N .<_ W ) ) /\ ( P =/= Q /\ ( v e. A /\ N =/= v ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> E. z e. A ( -. z .<_ W /\ ( z =/= N /\ z =/= v /\ z .<_ ( N .\/ v ) ) ) )
28 9 10 11 20 21 25 26 27 syl133anc
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( v e. A /\ v .<_ W ) /\ N e. A /\ F e. T ) /\ ( P =/= Q /\ v =/= ( R ` F ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> E. z e. A ( -. z .<_ W /\ ( z =/= N /\ z =/= v /\ z .<_ ( N .\/ v ) ) ) )
29 df-3an
 |-  ( ( z =/= N /\ z =/= v /\ z .<_ ( N .\/ v ) ) <-> ( ( z =/= N /\ z =/= v ) /\ z .<_ ( N .\/ v ) ) )
30 simpl
 |-  ( ( z =/= N /\ z =/= v ) -> z =/= N )
31 30 a1i
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( v e. A /\ v .<_ W ) /\ N e. A /\ F e. T ) /\ ( P =/= Q /\ v =/= ( R ` F ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ z e. A ) -> ( ( z =/= N /\ z =/= v ) -> z =/= N ) )
32 simp12l
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( v e. A /\ v .<_ W ) /\ N e. A /\ F e. T ) /\ ( P =/= Q /\ v =/= ( R ` F ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> P e. A )
33 simp13l
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( v e. A /\ v .<_ W ) /\ N e. A /\ F e. T ) /\ ( P =/= Q /\ v =/= ( R ` F ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> Q e. A )
34 1 2 3 4 5 6 7 8 cdlemg31a
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A ) /\ ( v e. A /\ F e. T ) ) -> N .<_ ( P .\/ v ) )
35 9 32 33 13 16 34 syl122anc
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( v e. A /\ v .<_ W ) /\ N e. A /\ F e. T ) /\ ( P =/= Q /\ v =/= ( R ` F ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> N .<_ ( P .\/ v ) )
36 simp11l
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( v e. A /\ v .<_ W ) /\ N e. A /\ F e. T ) /\ ( P =/= Q /\ v =/= ( R ` F ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> K e. HL )
37 1 2 4 hlatlej2
 |-  ( ( K e. HL /\ P e. A /\ v e. A ) -> v .<_ ( P .\/ v ) )
38 36 32 13 37 syl3anc
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( v e. A /\ v .<_ W ) /\ N e. A /\ F e. T ) /\ ( P =/= Q /\ v =/= ( R ` F ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> v .<_ ( P .\/ v ) )
39 36 hllatd
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( v e. A /\ v .<_ W ) /\ N e. A /\ F e. T ) /\ ( P =/= Q /\ v =/= ( R ` F ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> K e. Lat )
40 eqid
 |-  ( Base ` K ) = ( Base ` K )
41 40 4 atbase
 |-  ( N e. A -> N e. ( Base ` K ) )
42 12 41 syl
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( v e. A /\ v .<_ W ) /\ N e. A /\ F e. T ) /\ ( P =/= Q /\ v =/= ( R ` F ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> N e. ( Base ` K ) )
43 40 4 atbase
 |-  ( v e. A -> v e. ( Base ` K ) )
44 13 43 syl
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( v e. A /\ v .<_ W ) /\ N e. A /\ F e. T ) /\ ( P =/= Q /\ v =/= ( R ` F ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> v e. ( Base ` K ) )
45 40 2 4 hlatjcl
 |-  ( ( K e. HL /\ P e. A /\ v e. A ) -> ( P .\/ v ) e. ( Base ` K ) )
46 36 32 13 45 syl3anc
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( v e. A /\ v .<_ W ) /\ N e. A /\ F e. T ) /\ ( P =/= Q /\ v =/= ( R ` F ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> ( P .\/ v ) e. ( Base ` K ) )
47 40 1 2 latjle12
 |-  ( ( K e. Lat /\ ( N e. ( Base ` K ) /\ v e. ( Base ` K ) /\ ( P .\/ v ) e. ( Base ` K ) ) ) -> ( ( N .<_ ( P .\/ v ) /\ v .<_ ( P .\/ v ) ) <-> ( N .\/ v ) .<_ ( P .\/ v ) ) )
48 39 42 44 46 47 syl13anc
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( v e. A /\ v .<_ W ) /\ N e. A /\ F e. T ) /\ ( P =/= Q /\ v =/= ( R ` F ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> ( ( N .<_ ( P .\/ v ) /\ v .<_ ( P .\/ v ) ) <-> ( N .\/ v ) .<_ ( P .\/ v ) ) )
49 35 38 48 mpbi2and
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( v e. A /\ v .<_ W ) /\ N e. A /\ F e. T ) /\ ( P =/= Q /\ v =/= ( R ` F ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> ( N .\/ v ) .<_ ( P .\/ v ) )
50 49 adantr
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( v e. A /\ v .<_ W ) /\ N e. A /\ F e. T ) /\ ( P =/= Q /\ v =/= ( R ` F ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ z e. A ) -> ( N .\/ v ) .<_ ( P .\/ v ) )
51 39 adantr
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( v e. A /\ v .<_ W ) /\ N e. A /\ F e. T ) /\ ( P =/= Q /\ v =/= ( R ` F ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ z e. A ) -> K e. Lat )
52 40 4 atbase
 |-  ( z e. A -> z e. ( Base ` K ) )
53 52 adantl
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( v e. A /\ v .<_ W ) /\ N e. A /\ F e. T ) /\ ( P =/= Q /\ v =/= ( R ` F ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ z e. A ) -> z e. ( Base ` K ) )
54 40 2 4 hlatjcl
 |-  ( ( K e. HL /\ N e. A /\ v e. A ) -> ( N .\/ v ) e. ( Base ` K ) )
55 36 12 13 54 syl3anc
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( v e. A /\ v .<_ W ) /\ N e. A /\ F e. T ) /\ ( P =/= Q /\ v =/= ( R ` F ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> ( N .\/ v ) e. ( Base ` K ) )
56 55 adantr
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( v e. A /\ v .<_ W ) /\ N e. A /\ F e. T ) /\ ( P =/= Q /\ v =/= ( R ` F ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ z e. A ) -> ( N .\/ v ) e. ( Base ` K ) )
57 46 adantr
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( v e. A /\ v .<_ W ) /\ N e. A /\ F e. T ) /\ ( P =/= Q /\ v =/= ( R ` F ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ z e. A ) -> ( P .\/ v ) e. ( Base ` K ) )
58 40 1 lattr
 |-  ( ( K e. Lat /\ ( z e. ( Base ` K ) /\ ( N .\/ v ) e. ( Base ` K ) /\ ( P .\/ v ) e. ( Base ` K ) ) ) -> ( ( z .<_ ( N .\/ v ) /\ ( N .\/ v ) .<_ ( P .\/ v ) ) -> z .<_ ( P .\/ v ) ) )
59 51 53 56 57 58 syl13anc
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( v e. A /\ v .<_ W ) /\ N e. A /\ F e. T ) /\ ( P =/= Q /\ v =/= ( R ` F ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ z e. A ) -> ( ( z .<_ ( N .\/ v ) /\ ( N .\/ v ) .<_ ( P .\/ v ) ) -> z .<_ ( P .\/ v ) ) )
60 50 59 mpan2d
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( v e. A /\ v .<_ W ) /\ N e. A /\ F e. T ) /\ ( P =/= Q /\ v =/= ( R ` F ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ z e. A ) -> ( z .<_ ( N .\/ v ) -> z .<_ ( P .\/ v ) ) )
61 31 60 anim12d
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( v e. A /\ v .<_ W ) /\ N e. A /\ F e. T ) /\ ( P =/= Q /\ v =/= ( R ` F ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ z e. A ) -> ( ( ( z =/= N /\ z =/= v ) /\ z .<_ ( N .\/ v ) ) -> ( z =/= N /\ z .<_ ( P .\/ v ) ) ) )
62 29 61 syl5bi
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( v e. A /\ v .<_ W ) /\ N e. A /\ F e. T ) /\ ( P =/= Q /\ v =/= ( R ` F ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ z e. A ) -> ( ( z =/= N /\ z =/= v /\ z .<_ ( N .\/ v ) ) -> ( z =/= N /\ z .<_ ( P .\/ v ) ) ) )
63 62 anim2d
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( v e. A /\ v .<_ W ) /\ N e. A /\ F e. T ) /\ ( P =/= Q /\ v =/= ( R ` F ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ z e. A ) -> ( ( -. z .<_ W /\ ( z =/= N /\ z =/= v /\ z .<_ ( N .\/ v ) ) ) -> ( -. z .<_ W /\ ( z =/= N /\ z .<_ ( P .\/ v ) ) ) ) )
64 63 reximdva
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( v e. A /\ v .<_ W ) /\ N e. A /\ F e. T ) /\ ( P =/= Q /\ v =/= ( R ` F ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> ( E. z e. A ( -. z .<_ W /\ ( z =/= N /\ z =/= v /\ z .<_ ( N .\/ v ) ) ) -> E. z e. A ( -. z .<_ W /\ ( z =/= N /\ z .<_ ( P .\/ v ) ) ) ) )
65 28 64 mpd
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( v e. A /\ v .<_ W ) /\ N e. A /\ F e. T ) /\ ( P =/= Q /\ v =/= ( R ` F ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> E. z e. A ( -. z .<_ W /\ ( z =/= N /\ z .<_ ( P .\/ v ) ) ) )