Metamath Proof Explorer


Theorem cdleme27a

Description: Part of proof of Lemma E in Crawley p. 113. cdleme26f with s and t swapped (this case is not mentioned by them). If s <_ t \/ v, then f(s) <_ f_s(t) \/ v. TODO: FIX COMMENT. (Contributed by NM, 3-Feb-2013)

Ref Expression
Hypotheses cdleme26.b
|- B = ( Base ` K )
cdleme26.l
|- .<_ = ( le ` K )
cdleme26.j
|- .\/ = ( join ` K )
cdleme26.m
|- ./\ = ( meet ` K )
cdleme26.a
|- A = ( Atoms ` K )
cdleme26.h
|- H = ( LHyp ` K )
cdleme27.u
|- U = ( ( P .\/ Q ) ./\ W )
cdleme27.f
|- F = ( ( s .\/ U ) ./\ ( Q .\/ ( ( P .\/ s ) ./\ W ) ) )
cdleme27.z
|- Z = ( ( z .\/ U ) ./\ ( Q .\/ ( ( P .\/ z ) ./\ W ) ) )
cdleme27.n
|- N = ( ( P .\/ Q ) ./\ ( Z .\/ ( ( s .\/ z ) ./\ W ) ) )
cdleme27.d
|- D = ( iota_ u e. B A. z e. A ( ( -. z .<_ W /\ -. z .<_ ( P .\/ Q ) ) -> u = N ) )
cdleme27.c
|- C = if ( s .<_ ( P .\/ Q ) , D , F )
cdleme27.g
|- G = ( ( t .\/ U ) ./\ ( Q .\/ ( ( P .\/ t ) ./\ W ) ) )
cdleme27.o
|- O = ( ( P .\/ Q ) ./\ ( Z .\/ ( ( t .\/ z ) ./\ W ) ) )
cdleme27.e
|- E = ( iota_ u e. B A. z e. A ( ( -. z .<_ W /\ -. z .<_ ( P .\/ Q ) ) -> u = O ) )
cdleme27.y
|- Y = if ( t .<_ ( P .\/ Q ) , E , G )
Assertion cdleme27a
|- ( ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) -> C .<_ ( Y .\/ V ) )

Proof

Step Hyp Ref Expression
1 cdleme26.b
 |-  B = ( Base ` K )
2 cdleme26.l
 |-  .<_ = ( le ` K )
3 cdleme26.j
 |-  .\/ = ( join ` K )
4 cdleme26.m
 |-  ./\ = ( meet ` K )
5 cdleme26.a
 |-  A = ( Atoms ` K )
6 cdleme26.h
 |-  H = ( LHyp ` K )
7 cdleme27.u
 |-  U = ( ( P .\/ Q ) ./\ W )
8 cdleme27.f
 |-  F = ( ( s .\/ U ) ./\ ( Q .\/ ( ( P .\/ s ) ./\ W ) ) )
9 cdleme27.z
 |-  Z = ( ( z .\/ U ) ./\ ( Q .\/ ( ( P .\/ z ) ./\ W ) ) )
10 cdleme27.n
 |-  N = ( ( P .\/ Q ) ./\ ( Z .\/ ( ( s .\/ z ) ./\ W ) ) )
11 cdleme27.d
 |-  D = ( iota_ u e. B A. z e. A ( ( -. z .<_ W /\ -. z .<_ ( P .\/ Q ) ) -> u = N ) )
12 cdleme27.c
 |-  C = if ( s .<_ ( P .\/ Q ) , D , F )
13 cdleme27.g
 |-  G = ( ( t .\/ U ) ./\ ( Q .\/ ( ( P .\/ t ) ./\ W ) ) )
14 cdleme27.o
 |-  O = ( ( P .\/ Q ) ./\ ( Z .\/ ( ( t .\/ z ) ./\ W ) ) )
15 cdleme27.e
 |-  E = ( iota_ u e. B A. z e. A ( ( -. z .<_ W /\ -. z .<_ ( P .\/ Q ) ) -> u = O ) )
16 cdleme27.y
 |-  Y = if ( t .<_ ( P .\/ Q ) , E , G )
17 simp211
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) /\ ( t .\/ V ) = ( P .\/ Q ) ) -> ( K e. HL /\ W e. H ) )
18 simp221
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) /\ ( t .\/ V ) = ( P .\/ Q ) ) -> ( P e. A /\ -. P .<_ W ) )
19 simp222
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) /\ ( t .\/ V ) = ( P .\/ Q ) ) -> ( Q e. A /\ -. Q .<_ W ) )
20 simp213
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) /\ ( t .\/ V ) = ( P .\/ Q ) ) -> ( s e. A /\ -. s .<_ W ) )
21 simp223
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) /\ ( t .\/ V ) = ( P .\/ Q ) ) -> ( t e. A /\ -. t .<_ W ) )
22 simp23r
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) /\ ( t .\/ V ) = ( P .\/ Q ) ) -> ( V e. A /\ V .<_ W ) )
23 simp212
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) /\ ( t .\/ V ) = ( P .\/ Q ) ) -> P =/= Q )
24 simp1l
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) /\ ( t .\/ V ) = ( P .\/ Q ) ) -> s .<_ ( P .\/ Q ) )
25 simp1r
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) /\ ( t .\/ V ) = ( P .\/ Q ) ) -> t .<_ ( P .\/ Q ) )
26 23 24 25 3jca
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) /\ ( t .\/ V ) = ( P .\/ Q ) ) -> ( P =/= Q /\ s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) )
27 simp3
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) /\ ( t .\/ V ) = ( P .\/ Q ) ) -> ( t .\/ V ) = ( P .\/ Q ) )
28 1 2 3 4 5 6 7 9 10 14 11 15 cdleme26ee
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( s e. A /\ -. s .<_ W ) /\ ( t e. A /\ -. t .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( ( P =/= Q /\ s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( t .\/ V ) = ( P .\/ Q ) ) ) -> D .<_ ( E .\/ V ) )
29 17 18 19 20 21 22 26 27 28 syl332anc
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) /\ ( t .\/ V ) = ( P .\/ Q ) ) -> D .<_ ( E .\/ V ) )
30 29 3expia
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> ( ( t .\/ V ) = ( P .\/ Q ) -> D .<_ ( E .\/ V ) ) )
31 simp1r
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) /\ ( t .\/ V ) =/= ( P .\/ Q ) ) -> t .<_ ( P .\/ Q ) )
32 simp11l
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) -> K e. HL )
33 32 3ad2ant2
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) /\ ( t .\/ V ) =/= ( P .\/ Q ) ) -> K e. HL )
34 simp13l
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) -> s e. A )
35 34 3ad2ant2
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) /\ ( t .\/ V ) =/= ( P .\/ Q ) ) -> s e. A )
36 simp23l
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) -> t e. A )
37 36 3ad2ant2
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) /\ ( t .\/ V ) =/= ( P .\/ Q ) ) -> t e. A )
38 simp3ll
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) -> s =/= t )
39 38 3ad2ant2
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) /\ ( t .\/ V ) =/= ( P .\/ Q ) ) -> s =/= t )
40 35 37 39 3jca
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) /\ ( t .\/ V ) =/= ( P .\/ Q ) ) -> ( s e. A /\ t e. A /\ s =/= t ) )
41 simp21l
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) -> P e. A )
42 41 3ad2ant2
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) /\ ( t .\/ V ) =/= ( P .\/ Q ) ) -> P e. A )
43 simp22l
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) -> Q e. A )
44 43 3ad2ant2
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) /\ ( t .\/ V ) =/= ( P .\/ Q ) ) -> Q e. A )
45 simp212
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) /\ ( t .\/ V ) =/= ( P .\/ Q ) ) -> P =/= Q )
46 simp3rl
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) -> V e. A )
47 46 3ad2ant2
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) /\ ( t .\/ V ) =/= ( P .\/ Q ) ) -> V e. A )
48 simp3
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) /\ ( t .\/ V ) =/= ( P .\/ Q ) ) -> ( t .\/ V ) =/= ( P .\/ Q ) )
49 simp3lr
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) -> s .<_ ( t .\/ V ) )
50 49 3ad2ant2
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) /\ ( t .\/ V ) =/= ( P .\/ Q ) ) -> s .<_ ( t .\/ V ) )
51 simp1l
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) /\ ( t .\/ V ) =/= ( P .\/ Q ) ) -> s .<_ ( P .\/ Q ) )
52 48 50 51 3jca
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) /\ ( t .\/ V ) =/= ( P .\/ Q ) ) -> ( ( t .\/ V ) =/= ( P .\/ Q ) /\ s .<_ ( t .\/ V ) /\ s .<_ ( P .\/ Q ) ) )
53 2 3 4 5 6 cdleme22b
 |-  ( ( ( K e. HL /\ ( s e. A /\ t e. A /\ s =/= t ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ ( ( t .\/ V ) =/= ( P .\/ Q ) /\ s .<_ ( t .\/ V ) /\ s .<_ ( P .\/ Q ) ) ) ) -> -. t .<_ ( P .\/ Q ) )
54 33 40 42 44 45 47 52 53 syl232anc
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) /\ ( t .\/ V ) =/= ( P .\/ Q ) ) -> -. t .<_ ( P .\/ Q ) )
55 31 54 pm2.21dd
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) /\ ( t .\/ V ) =/= ( P .\/ Q ) ) -> D .<_ ( E .\/ V ) )
56 55 3expia
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> ( ( t .\/ V ) =/= ( P .\/ Q ) -> D .<_ ( E .\/ V ) ) )
57 30 56 pm2.61dne
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> D .<_ ( E .\/ V ) )
58 iftrue
 |-  ( s .<_ ( P .\/ Q ) -> if ( s .<_ ( P .\/ Q ) , D , F ) = D )
59 12 58 syl5eq
 |-  ( s .<_ ( P .\/ Q ) -> C = D )
60 59 ad2antrr
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> C = D )
61 iftrue
 |-  ( t .<_ ( P .\/ Q ) -> if ( t .<_ ( P .\/ Q ) , E , G ) = E )
62 16 61 syl5eq
 |-  ( t .<_ ( P .\/ Q ) -> Y = E )
63 62 oveq1d
 |-  ( t .<_ ( P .\/ Q ) -> ( Y .\/ V ) = ( E .\/ V ) )
64 63 ad2antlr
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> ( Y .\/ V ) = ( E .\/ V ) )
65 57 60 64 3brtr4d
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> C .<_ ( Y .\/ V ) )
66 65 ex
 |-  ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) -> ( ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) -> C .<_ ( Y .\/ V ) ) )
67 simpr11
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ -. t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> ( K e. HL /\ W e. H ) )
68 simpr12
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ -. t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> P =/= Q )
69 simpll
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ -. t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> s .<_ ( P .\/ Q ) )
70 68 69 jca
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ -. t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> ( P =/= Q /\ s .<_ ( P .\/ Q ) ) )
71 simpr23
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ -. t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> ( t e. A /\ -. t .<_ W ) )
72 simpr21
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ -. t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> ( P e. A /\ -. P .<_ W ) )
73 simpr22
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ -. t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> ( Q e. A /\ -. Q .<_ W ) )
74 simpr13
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ -. t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> ( s e. A /\ -. s .<_ W ) )
75 simplr
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ -. t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> -. t .<_ ( P .\/ Q ) )
76 simpr3l
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ -. t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> ( s =/= t /\ s .<_ ( t .\/ V ) ) )
77 simpr3r
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ -. t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> ( V e. A /\ V .<_ W ) )
78 eqid
 |-  ( ( P .\/ Q ) ./\ ( G .\/ ( ( s .\/ t ) ./\ W ) ) ) = ( ( P .\/ Q ) ./\ ( G .\/ ( ( s .\/ t ) ./\ W ) ) )
79 eqid
 |-  ( iota_ u e. B A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> u = ( ( P .\/ Q ) ./\ ( G .\/ ( ( s .\/ t ) ./\ W ) ) ) ) ) = ( iota_ u e. B A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> u = ( ( P .\/ Q ) ./\ ( G .\/ ( ( s .\/ t ) ./\ W ) ) ) ) )
80 9 10 13 78 11 79 cdleme25cv
 |-  D = ( iota_ u e. B A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> u = ( ( P .\/ Q ) ./\ ( G .\/ ( ( s .\/ t ) ./\ W ) ) ) ) )
81 1 2 3 4 5 6 7 13 78 80 cdleme26f
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P =/= Q /\ s .<_ ( P .\/ Q ) ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( s e. A /\ -. s .<_ W ) ) /\ ( -. t .<_ ( P .\/ Q ) /\ ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) -> D .<_ ( G .\/ V ) )
82 67 70 71 72 73 74 75 76 77 81 syl333anc
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ -. t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> D .<_ ( G .\/ V ) )
83 59 ad2antrr
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ -. t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> C = D )
84 iffalse
 |-  ( -. t .<_ ( P .\/ Q ) -> if ( t .<_ ( P .\/ Q ) , E , G ) = G )
85 16 84 syl5eq
 |-  ( -. t .<_ ( P .\/ Q ) -> Y = G )
86 85 oveq1d
 |-  ( -. t .<_ ( P .\/ Q ) -> ( Y .\/ V ) = ( G .\/ V ) )
87 86 ad2antlr
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ -. t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> ( Y .\/ V ) = ( G .\/ V ) )
88 82 83 87 3brtr4d
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ -. t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> C .<_ ( Y .\/ V ) )
89 88 ex
 |-  ( ( s .<_ ( P .\/ Q ) /\ -. t .<_ ( P .\/ Q ) ) -> ( ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) -> C .<_ ( Y .\/ V ) ) )
90 simpr11
 |-  ( ( ( -. s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> ( K e. HL /\ W e. H ) )
91 simpr12
 |-  ( ( ( -. s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> P =/= Q )
92 simplr
 |-  ( ( ( -. s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> t .<_ ( P .\/ Q ) )
93 91 92 jca
 |-  ( ( ( -. s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> ( P =/= Q /\ t .<_ ( P .\/ Q ) ) )
94 simpr13
 |-  ( ( ( -. s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> ( s e. A /\ -. s .<_ W ) )
95 simpr21
 |-  ( ( ( -. s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> ( P e. A /\ -. P .<_ W ) )
96 simpr22
 |-  ( ( ( -. s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> ( Q e. A /\ -. Q .<_ W ) )
97 simpr23
 |-  ( ( ( -. s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> ( t e. A /\ -. t .<_ W ) )
98 simpll
 |-  ( ( ( -. s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> -. s .<_ ( P .\/ Q ) )
99 simpr3l
 |-  ( ( ( -. s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> ( s =/= t /\ s .<_ ( t .\/ V ) ) )
100 simpr3r
 |-  ( ( ( -. s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> ( V e. A /\ V .<_ W ) )
101 eqid
 |-  ( ( P .\/ Q ) ./\ ( F .\/ ( ( t .\/ s ) ./\ W ) ) ) = ( ( P .\/ Q ) ./\ ( F .\/ ( ( t .\/ s ) ./\ W ) ) )
102 eqid
 |-  ( iota_ u e. B A. s e. A ( ( -. s .<_ W /\ -. s .<_ ( P .\/ Q ) ) -> u = ( ( P .\/ Q ) ./\ ( F .\/ ( ( t .\/ s ) ./\ W ) ) ) ) ) = ( iota_ u e. B A. s e. A ( ( -. s .<_ W /\ -. s .<_ ( P .\/ Q ) ) -> u = ( ( P .\/ Q ) ./\ ( F .\/ ( ( t .\/ s ) ./\ W ) ) ) ) )
103 9 14 8 101 15 102 cdleme25cv
 |-  E = ( iota_ u e. B A. s e. A ( ( -. s .<_ W /\ -. s .<_ ( P .\/ Q ) ) -> u = ( ( P .\/ Q ) ./\ ( F .\/ ( ( t .\/ s ) ./\ W ) ) ) ) )
104 1 2 3 4 5 6 7 8 101 103 cdleme26f2
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P =/= Q /\ t .<_ ( P .\/ Q ) ) /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( -. s .<_ ( P .\/ Q ) /\ ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) -> F .<_ ( E .\/ V ) )
105 90 93 94 95 96 97 98 99 100 104 syl333anc
 |-  ( ( ( -. s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> F .<_ ( E .\/ V ) )
106 iffalse
 |-  ( -. s .<_ ( P .\/ Q ) -> if ( s .<_ ( P .\/ Q ) , D , F ) = F )
107 12 106 syl5eq
 |-  ( -. s .<_ ( P .\/ Q ) -> C = F )
108 107 ad2antrr
 |-  ( ( ( -. s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> C = F )
109 63 ad2antlr
 |-  ( ( ( -. s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> ( Y .\/ V ) = ( E .\/ V ) )
110 105 108 109 3brtr4d
 |-  ( ( ( -. s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> C .<_ ( Y .\/ V ) )
111 110 ex
 |-  ( ( -. s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) -> ( ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) -> C .<_ ( Y .\/ V ) ) )
112 simpr11
 |-  ( ( ( -. s .<_ ( P .\/ Q ) /\ -. t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> ( K e. HL /\ W e. H ) )
113 simpr23
 |-  ( ( ( -. s .<_ ( P .\/ Q ) /\ -. t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> ( t e. A /\ -. t .<_ W ) )
114 simplr
 |-  ( ( ( -. s .<_ ( P .\/ Q ) /\ -. t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> -. t .<_ ( P .\/ Q ) )
115 simpll
 |-  ( ( ( -. s .<_ ( P .\/ Q ) /\ -. t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> -. s .<_ ( P .\/ Q ) )
116 simpr12
 |-  ( ( ( -. s .<_ ( P .\/ Q ) /\ -. t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> P =/= Q )
117 114 115 116 3jca
 |-  ( ( ( -. s .<_ ( P .\/ Q ) /\ -. t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> ( -. t .<_ ( P .\/ Q ) /\ -. s .<_ ( P .\/ Q ) /\ P =/= Q ) )
118 simpr21
 |-  ( ( ( -. s .<_ ( P .\/ Q ) /\ -. t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> ( P e. A /\ -. P .<_ W ) )
119 simpr22
 |-  ( ( ( -. s .<_ ( P .\/ Q ) /\ -. t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> ( Q e. A /\ -. Q .<_ W ) )
120 simpr13
 |-  ( ( ( -. s .<_ ( P .\/ Q ) /\ -. t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> ( s e. A /\ -. s .<_ W ) )
121 simpr3l
 |-  ( ( ( -. s .<_ ( P .\/ Q ) /\ -. t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> ( s =/= t /\ s .<_ ( t .\/ V ) ) )
122 simpr3r
 |-  ( ( ( -. s .<_ ( P .\/ Q ) /\ -. t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> ( V e. A /\ V .<_ W ) )
123 2 3 4 5 6 7 8 13 cdleme22g
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( t e. A /\ -. t .<_ W ) /\ ( -. t .<_ ( P .\/ Q ) /\ -. s .<_ ( P .\/ Q ) /\ P =/= Q ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( s e. A /\ -. s .<_ W ) /\ ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) -> F .<_ ( G .\/ V ) )
124 112 113 117 118 119 120 121 122 123 syl323anc
 |-  ( ( ( -. s .<_ ( P .\/ Q ) /\ -. t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> F .<_ ( G .\/ V ) )
125 107 ad2antrr
 |-  ( ( ( -. s .<_ ( P .\/ Q ) /\ -. t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> C = F )
126 86 ad2antlr
 |-  ( ( ( -. s .<_ ( P .\/ Q ) /\ -. t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> ( Y .\/ V ) = ( G .\/ V ) )
127 124 125 126 3brtr4d
 |-  ( ( ( -. s .<_ ( P .\/ Q ) /\ -. t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> C .<_ ( Y .\/ V ) )
128 127 ex
 |-  ( ( -. s .<_ ( P .\/ Q ) /\ -. t .<_ ( P .\/ Q ) ) -> ( ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) -> C .<_ ( Y .\/ V ) ) )
129 66 89 111 128 4cases
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) -> C .<_ ( Y .\/ V ) )