This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cdlemd4

Description: Part of proof of Lemma D in Crawley p. 113. (Contributed by NM, 30-May-2012)

Ref Expression
Hypotheses cdlemd4.l 
|- .<_ = ( le ` K )
cdlemd4.j 
|- .\/ = ( join ` K )
cdlemd4.a 
|- A = ( Atoms ` K )
cdlemd4.h 
|- H = ( LHyp ` K )
cdlemd4.t 
|- T = ( ( LTrn ` K ) ` W )
Assertion cdlemd4 
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ R =/= P ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> ( F ` R ) = ( G ` R ) )

Proof

Step Hyp Ref Expression
1 cdlemd4.l 
 |-  .<_ = ( le ` K )
2 cdlemd4.j 
 |-  .\/ = ( join ` K )
3 cdlemd4.a 
 |-  A = ( Atoms ` K )
4 cdlemd4.h 
 |-  H = ( LHyp ` K )
5 cdlemd4.t 
 |-  T = ( ( LTrn ` K ) ` W )
6 simp11l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ R =/= P ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> K e. HL )
7 simp11r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ R =/= P ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> W e. H )
8 simp21 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ R =/= P ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> ( P e. A /\ -. P .<_ W ) )
9 simp22 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ R =/= P ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> ( Q e. A /\ -. Q .<_ W ) )
10 simp231 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ R =/= P ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> P =/= Q )
11 1 2 3 4 cdlemb2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ P =/= Q ) -> E. s e. A ( -. s .<_ W /\ -. s .<_ ( P .\/ Q ) ) )
12 6 7 8 9 10 11 syl221anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ R =/= P ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> E. s e. A ( -. s .<_ W /\ -. s .<_ ( P .\/ Q ) ) )
13 simpl11 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ R =/= P ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) /\ ( s e. A /\ ( -. s .<_ W /\ -. s .<_ ( P .\/ Q ) ) ) ) -> ( K e. HL /\ W e. H ) )
14 simpl12 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ R =/= P ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) /\ ( s e. A /\ ( -. s .<_ W /\ -. s .<_ ( P .\/ Q ) ) ) ) -> ( F e. T /\ G e. T ) )
15 simpl13 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ R =/= P ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) /\ ( s e. A /\ ( -. s .<_ W /\ -. s .<_ ( P .\/ Q ) ) ) ) -> R e. A )
16 simpl21 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ R =/= P ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) /\ ( s e. A /\ ( -. s .<_ W /\ -. s .<_ ( P .\/ Q ) ) ) ) -> ( P e. A /\ -. P .<_ W ) )
17 simprl 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ R =/= P ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) /\ ( s e. A /\ ( -. s .<_ W /\ -. s .<_ ( P .\/ Q ) ) ) ) -> s e. A )
18 simprrl 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ R =/= P ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) /\ ( s e. A /\ ( -. s .<_ W /\ -. s .<_ ( P .\/ Q ) ) ) ) -> -. s .<_ W )
19 17 18 jca 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ R =/= P ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) /\ ( s e. A /\ ( -. s .<_ W /\ -. s .<_ ( P .\/ Q ) ) ) ) -> ( s e. A /\ -. s .<_ W ) )
20 6 hllatd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ R =/= P ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> K e. Lat )
21 20 adantr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ R =/= P ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) /\ ( s e. A /\ ( -. s .<_ W /\ -. s .<_ ( P .\/ Q ) ) ) ) -> K e. Lat )
22 eqid 
 |-  ( Base ` K ) = ( Base ` K )
23 22 3 atbase 
 |-  ( s e. A -> s e. ( Base ` K ) )
24 23 ad2antrl 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ R =/= P ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) /\ ( s e. A /\ ( -. s .<_ W /\ -. s .<_ ( P .\/ Q ) ) ) ) -> s e. ( Base ` K ) )
25 simp21l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ R =/= P ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> P e. A )
26 22 3 atbase 
 |-  ( P e. A -> P e. ( Base ` K ) )
27 25 26 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ R =/= P ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> P e. ( Base ` K ) )
28 27 adantr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ R =/= P ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) /\ ( s e. A /\ ( -. s .<_ W /\ -. s .<_ ( P .\/ Q ) ) ) ) -> P e. ( Base ` K ) )
29 simp22l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ R =/= P ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> Q e. A )
30 22 3 atbase 
 |-  ( Q e. A -> Q e. ( Base ` K ) )
31 29 30 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ R =/= P ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> Q e. ( Base ` K ) )
32 31 adantr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ R =/= P ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) /\ ( s e. A /\ ( -. s .<_ W /\ -. s .<_ ( P .\/ Q ) ) ) ) -> Q e. ( Base ` K ) )
33 simprrr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ R =/= P ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) /\ ( s e. A /\ ( -. s .<_ W /\ -. s .<_ ( P .\/ Q ) ) ) ) -> -. s .<_ ( P .\/ Q ) )
34 22 1 2 latnlej1l 
 |-  ( ( K e. Lat /\ ( s e. ( Base ` K ) /\ P e. ( Base ` K ) /\ Q e. ( Base ` K ) ) /\ -. s .<_ ( P .\/ Q ) ) -> s =/= P )
35 34 necomd 
 |-  ( ( K e. Lat /\ ( s e. ( Base ` K ) /\ P e. ( Base ` K ) /\ Q e. ( Base ` K ) ) /\ -. s .<_ ( P .\/ Q ) ) -> P =/= s )
36 21 24 28 32 33 35 syl131anc 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ R =/= P ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) /\ ( s e. A /\ ( -. s .<_ W /\ -. s .<_ ( P .\/ Q ) ) ) ) -> P =/= s )
37 simpl22 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ R =/= P ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) /\ ( s e. A /\ ( -. s .<_ W /\ -. s .<_ ( P .\/ Q ) ) ) ) -> ( Q e. A /\ -. Q .<_ W ) )
38 simpl23 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ R =/= P ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) /\ ( s e. A /\ ( -. s .<_ W /\ -. s .<_ ( P .\/ Q ) ) ) ) -> ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ R =/= P ) )
39 1 2 3 4 cdlemd3 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ R =/= P ) ) /\ ( R e. A /\ s e. A /\ -. s .<_ ( P .\/ Q ) ) ) -> -. R .<_ ( P .\/ s ) )
40 13 16 37 38 15 17 33 39 syl133anc 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ R =/= P ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) /\ ( s e. A /\ ( -. s .<_ W /\ -. s .<_ ( P .\/ Q ) ) ) ) -> -. R .<_ ( P .\/ s ) )
41 36 40 jca 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ R =/= P ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) /\ ( s e. A /\ ( -. s .<_ W /\ -. s .<_ ( P .\/ Q ) ) ) ) -> ( P =/= s /\ -. R .<_ ( P .\/ s ) ) )
42 simpl3l 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ R =/= P ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) /\ ( s e. A /\ ( -. s .<_ W /\ -. s .<_ ( P .\/ Q ) ) ) ) -> ( F ` P ) = ( G ` P ) )
43 10 adantr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ R =/= P ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) /\ ( s e. A /\ ( -. s .<_ W /\ -. s .<_ ( P .\/ Q ) ) ) ) -> P =/= Q )
44 43 33 jca 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ R =/= P ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) /\ ( s e. A /\ ( -. s .<_ W /\ -. s .<_ ( P .\/ Q ) ) ) ) -> ( P =/= Q /\ -. s .<_ ( P .\/ Q ) ) )
45 simpl3 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ R =/= P ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) /\ ( s e. A /\ ( -. s .<_ W /\ -. s .<_ ( P .\/ Q ) ) ) ) -> ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) )
46 1 2 3 4 5 cdlemd2 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ s e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ -. s .<_ ( P .\/ Q ) ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> ( F ` s ) = ( G ` s ) )
47 13 14 17 16 37 44 45 46 syl331anc 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ R =/= P ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) /\ ( s e. A /\ ( -. s .<_ W /\ -. s .<_ ( P .\/ Q ) ) ) ) -> ( F ` s ) = ( G ` s ) )
48 1 2 3 4 5 cdlemd2 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( s e. A /\ -. s .<_ W ) /\ ( P =/= s /\ -. R .<_ ( P .\/ s ) ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` s ) = ( G ` s ) ) ) -> ( F ` R ) = ( G ` R ) )
49 13 14 15 16 19 41 42 47 48 syl332anc 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ R =/= P ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) /\ ( s e. A /\ ( -. s .<_ W /\ -. s .<_ ( P .\/ Q ) ) ) ) -> ( F ` R ) = ( G ` R ) )
50 12 49 rexlimddv 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ R e. A ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ R =/= P ) ) /\ ( ( F ` P ) = ( G ` P ) /\ ( F ` Q ) = ( G ` Q ) ) ) -> ( F ` R ) = ( G ` R ) )