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

Metamath Proof Explorer

Theorem cdlemk12

Description: Part of proof of Lemma K of Crawley p. 118. Eq. 4, line 10, p. 119. (Contributed by NM, 30-Jun-2013)

Ref Expression
Hypotheses cdlemk.b 
|- B = ( Base ` K )
cdlemk.l 
|- .<_ = ( le ` K )
cdlemk.j 
|- .\/ = ( join ` K )
cdlemk.a 
|- A = ( Atoms ` K )
cdlemk.h 
|- H = ( LHyp ` K )
cdlemk.t 
|- T = ( ( LTrn ` K ) ` W )
cdlemk.r 
|- R = ( ( trL ` K ) ` W )
cdlemk.m 
|- ./\ = ( meet ` K )
cdlemk.s 
|- S = ( f e. T |-> ( iota_ i e. T ( i ` P ) = ( ( P .\/ ( R ` f ) ) ./\ ( ( N ` P ) .\/ ( R ` ( f o. `' F ) ) ) ) ) )
Assertion cdlemk12 
|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( N e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ X =/= ( _I |` B ) ) /\ ( ( R ` G ) =/= ( R ` F ) /\ ( R ` X ) =/= ( R ` F ) ) /\ ( R ` G ) =/= ( R ` X ) ) ) -> ( ( S ` G ) ` P ) = ( ( P .\/ ( G ` P ) ) ./\ ( ( ( S ` X ) ` P ) .\/ ( R ` ( X o. `' G ) ) ) ) )

Proof

Step Hyp Ref Expression
1 cdlemk.b 
 |-  B = ( Base ` K )
2 cdlemk.l 
 |-  .<_ = ( le ` K )
3 cdlemk.j 
 |-  .\/ = ( join ` K )
4 cdlemk.a 
 |-  A = ( Atoms ` K )
5 cdlemk.h 
 |-  H = ( LHyp ` K )
6 cdlemk.t 
 |-  T = ( ( LTrn ` K ) ` W )
7 cdlemk.r 
 |-  R = ( ( trL ` K ) ` W )
8 cdlemk.m 
 |-  ./\ = ( meet ` K )
9 cdlemk.s 
 |-  S = ( f e. T |-> ( iota_ i e. T ( i ` P ) = ( ( P .\/ ( R ` f ) ) ./\ ( ( N ` P ) .\/ ( R ` ( f o. `' F ) ) ) ) ) )
10 simp11l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( N e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ X =/= ( _I |` B ) ) /\ ( ( R ` G ) =/= ( R ` F ) /\ ( R ` X ) =/= ( R ` F ) ) /\ ( R ` G ) =/= ( R ` X ) ) ) -> K e. HL )
11 simp22l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( N e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ X =/= ( _I |` B ) ) /\ ( ( R ` G ) =/= ( R ` F ) /\ ( R ` X ) =/= ( R ` F ) ) /\ ( R ` G ) =/= ( R ` X ) ) ) -> P e. A )
12 simp11 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( N e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ X =/= ( _I |` B ) ) /\ ( ( R ` G ) =/= ( R ` F ) /\ ( R ` X ) =/= ( R ` F ) ) /\ ( R ` G ) =/= ( R ` X ) ) ) -> ( K e. HL /\ W e. H ) )
13 simp13 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( N e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ X =/= ( _I |` B ) ) /\ ( ( R ` G ) =/= ( R ` F ) /\ ( R ` X ) =/= ( R ` F ) ) /\ ( R ` G ) =/= ( R ` X ) ) ) -> G e. T )
14 2 4 5 6 ltrnat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ G e. T /\ P e. A ) -> ( G ` P ) e. A )
15 12 13 11 14 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( N e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ X =/= ( _I |` B ) ) /\ ( ( R ` G ) =/= ( R ` F ) /\ ( R ` X ) =/= ( R ` F ) ) /\ ( R ` G ) =/= ( R ` X ) ) ) -> ( G ` P ) e. A )
16 simp12 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( N e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ X =/= ( _I |` B ) ) /\ ( ( R ` G ) =/= ( R ` F ) /\ ( R ` X ) =/= ( R ` F ) ) /\ ( R ` G ) =/= ( R ` X ) ) ) -> F e. T )
17 simp21r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( N e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ X =/= ( _I |` B ) ) /\ ( ( R ` G ) =/= ( R ` F ) /\ ( R ` X ) =/= ( R ` F ) ) /\ ( R ` G ) =/= ( R ` X ) ) ) -> X e. T )
18 12 16 17 3jca 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( N e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ X =/= ( _I |` B ) ) /\ ( ( R ` G ) =/= ( R ` F ) /\ ( R ` X ) =/= ( R ` F ) ) /\ ( R ` G ) =/= ( R ` X ) ) ) -> ( ( K e. HL /\ W e. H ) /\ F e. T /\ X e. T ) )
19 simp21l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( N e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ X =/= ( _I |` B ) ) /\ ( ( R ` G ) =/= ( R ` F ) /\ ( R ` X ) =/= ( R ` F ) ) /\ ( R ` G ) =/= ( R ` X ) ) ) -> N e. T )
20 simp22 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( N e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ X =/= ( _I |` B ) ) /\ ( ( R ` G ) =/= ( R ` F ) /\ ( R ` X ) =/= ( R ` F ) ) /\ ( R ` G ) =/= ( R ` X ) ) ) -> ( P e. A /\ -. P .<_ W ) )
21 simp23 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( N e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ X =/= ( _I |` B ) ) /\ ( ( R ` G ) =/= ( R ` F ) /\ ( R ` X ) =/= ( R ` F ) ) /\ ( R ` G ) =/= ( R ` X ) ) ) -> ( R ` F ) = ( R ` N ) )
22 19 20 21 3jca 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( N e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ X =/= ( _I |` B ) ) /\ ( ( R ` G ) =/= ( R ` F ) /\ ( R ` X ) =/= ( R ` F ) ) /\ ( R ` G ) =/= ( R ` X ) ) ) -> ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) )
23 simp311 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( N e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ X =/= ( _I |` B ) ) /\ ( ( R ` G ) =/= ( R ` F ) /\ ( R ` X ) =/= ( R ` F ) ) /\ ( R ` G ) =/= ( R ` X ) ) ) -> F =/= ( _I |` B ) )
24 simp313 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( N e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ X =/= ( _I |` B ) ) /\ ( ( R ` G ) =/= ( R ` F ) /\ ( R ` X ) =/= ( R ` F ) ) /\ ( R ` G ) =/= ( R ` X ) ) ) -> X =/= ( _I |` B ) )
25 simp32r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( N e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ X =/= ( _I |` B ) ) /\ ( ( R ` G ) =/= ( R ` F ) /\ ( R ` X ) =/= ( R ` F ) ) /\ ( R ` G ) =/= ( R ` X ) ) ) -> ( R ` X ) =/= ( R ` F ) )
26 1 2 3 4 5 6 7 8 9 cdlemksat 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ X e. T ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( F =/= ( _I |` B ) /\ X =/= ( _I |` B ) /\ ( R ` X ) =/= ( R ` F ) ) ) -> ( ( S ` X ) ` P ) e. A )
27 18 22 23 24 25 26 syl113anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( N e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ X =/= ( _I |` B ) ) /\ ( ( R ` G ) =/= ( R ` F ) /\ ( R ` X ) =/= ( R ` F ) ) /\ ( R ` G ) =/= ( R ` X ) ) ) -> ( ( S ` X ) ` P ) e. A )
28 simp33 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( N e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ X =/= ( _I |` B ) ) /\ ( ( R ` G ) =/= ( R ` F ) /\ ( R ` X ) =/= ( R ` F ) ) /\ ( R ` G ) =/= ( R ` X ) ) ) -> ( R ` G ) =/= ( R ` X ) )
29 28 necomd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( N e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ X =/= ( _I |` B ) ) /\ ( ( R ` G ) =/= ( R ` F ) /\ ( R ` X ) =/= ( R ` F ) ) /\ ( R ` G ) =/= ( R ` X ) ) ) -> ( R ` X ) =/= ( R ` G ) )
30 4 5 6 7 trlcocnvat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. T /\ G e. T ) /\ ( R ` X ) =/= ( R ` G ) ) -> ( R ` ( X o. `' G ) ) e. A )
31 12 17 13 29 30 syl121anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( N e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ X =/= ( _I |` B ) ) /\ ( ( R ` G ) =/= ( R ` F ) /\ ( R ` X ) =/= ( R ` F ) ) /\ ( R ` G ) =/= ( R ` X ) ) ) -> ( R ` ( X o. `' G ) ) e. A )
32 simp1 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( N e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ X =/= ( _I |` B ) ) /\ ( ( R ` G ) =/= ( R ` F ) /\ ( R ` X ) =/= ( R ` F ) ) /\ ( R ` G ) =/= ( R ` X ) ) ) -> ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) )
33 simp312 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( N e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ X =/= ( _I |` B ) ) /\ ( ( R ` G ) =/= ( R ` F ) /\ ( R ` X ) =/= ( R ` F ) ) /\ ( R ` G ) =/= ( R ` X ) ) ) -> G =/= ( _I |` B ) )
34 simp32l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( N e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ X =/= ( _I |` B ) ) /\ ( ( R ` G ) =/= ( R ` F ) /\ ( R ` X ) =/= ( R ` F ) ) /\ ( R ` G ) =/= ( R ` X ) ) ) -> ( R ` G ) =/= ( R ` F ) )
35 1 2 3 4 5 6 7 8 9 cdlemksat 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ ( R ` G ) =/= ( R ` F ) ) ) -> ( ( S ` G ) ` P ) e. A )
36 32 22 23 33 34 35 syl113anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( N e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ X =/= ( _I |` B ) ) /\ ( ( R ` G ) =/= ( R ` F ) /\ ( R ` X ) =/= ( R ` F ) ) /\ ( R ` G ) =/= ( R ` X ) ) ) -> ( ( S ` G ) ` P ) e. A )
37 1 2 3 4 5 6 7 8 9 cdlemksv2 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ ( R ` G ) =/= ( R ` F ) ) ) -> ( ( S ` G ) ` P ) = ( ( P .\/ ( R ` G ) ) ./\ ( ( N ` P ) .\/ ( R ` ( G o. `' F ) ) ) ) )
38 32 22 23 33 34 37 syl113anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( N e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ X =/= ( _I |` B ) ) /\ ( ( R ` G ) =/= ( R ` F ) /\ ( R ` X ) =/= ( R ` F ) ) /\ ( R ` G ) =/= ( R ` X ) ) ) -> ( ( S ` G ) ` P ) = ( ( P .\/ ( R ` G ) ) ./\ ( ( N ` P ) .\/ ( R ` ( G o. `' F ) ) ) ) )
39 10 hllatd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( N e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ X =/= ( _I |` B ) ) /\ ( ( R ` G ) =/= ( R ` F ) /\ ( R ` X ) =/= ( R ` F ) ) /\ ( R ` G ) =/= ( R ` X ) ) ) -> K e. Lat )
40 1 4 5 6 7 trlnidat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ G e. T /\ G =/= ( _I |` B ) ) -> ( R ` G ) e. A )
41 12 13 33 40 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( N e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ X =/= ( _I |` B ) ) /\ ( ( R ` G ) =/= ( R ` F ) /\ ( R ` X ) =/= ( R ` F ) ) /\ ( R ` G ) =/= ( R ` X ) ) ) -> ( R ` G ) e. A )
42 1 3 4 hlatjcl 
 |-  ( ( K e. HL /\ P e. A /\ ( R ` G ) e. A ) -> ( P .\/ ( R ` G ) ) e. B )
43 10 11 41 42 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( N e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ X =/= ( _I |` B ) ) /\ ( ( R ` G ) =/= ( R ` F ) /\ ( R ` X ) =/= ( R ` F ) ) /\ ( R ` G ) =/= ( R ` X ) ) ) -> ( P .\/ ( R ` G ) ) e. B )
44 2 4 5 6 ltrnat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ N e. T /\ P e. A ) -> ( N ` P ) e. A )
45 12 19 11 44 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( N e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ X =/= ( _I |` B ) ) /\ ( ( R ` G ) =/= ( R ` F ) /\ ( R ` X ) =/= ( R ` F ) ) /\ ( R ` G ) =/= ( R ` X ) ) ) -> ( N ` P ) e. A )
46 4 5 6 7 trlcocnvat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( G e. T /\ F e. T ) /\ ( R ` G ) =/= ( R ` F ) ) -> ( R ` ( G o. `' F ) ) e. A )
47 12 13 16 34 46 syl121anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( N e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ X =/= ( _I |` B ) ) /\ ( ( R ` G ) =/= ( R ` F ) /\ ( R ` X ) =/= ( R ` F ) ) /\ ( R ` G ) =/= ( R ` X ) ) ) -> ( R ` ( G o. `' F ) ) e. A )
48 1 3 4 hlatjcl 
 |-  ( ( K e. HL /\ ( N ` P ) e. A /\ ( R ` ( G o. `' F ) ) e. A ) -> ( ( N ` P ) .\/ ( R ` ( G o. `' F ) ) ) e. B )
49 10 45 47 48 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( N e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ X =/= ( _I |` B ) ) /\ ( ( R ` G ) =/= ( R ` F ) /\ ( R ` X ) =/= ( R ` F ) ) /\ ( R ` G ) =/= ( R ` X ) ) ) -> ( ( N ` P ) .\/ ( R ` ( G o. `' F ) ) ) e. B )
50 1 2 8 latmle1 
 |-  ( ( K e. Lat /\ ( P .\/ ( R ` G ) ) e. B /\ ( ( N ` P ) .\/ ( R ` ( G o. `' F ) ) ) e. B ) -> ( ( P .\/ ( R ` G ) ) ./\ ( ( N ` P ) .\/ ( R ` ( G o. `' F ) ) ) ) .<_ ( P .\/ ( R ` G ) ) )
51 39 43 49 50 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( N e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ X =/= ( _I |` B ) ) /\ ( ( R ` G ) =/= ( R ` F ) /\ ( R ` X ) =/= ( R ` F ) ) /\ ( R ` G ) =/= ( R ` X ) ) ) -> ( ( P .\/ ( R ` G ) ) ./\ ( ( N ` P ) .\/ ( R ` ( G o. `' F ) ) ) ) .<_ ( P .\/ ( R ` G ) ) )
52 38 51 eqbrtrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( N e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ X =/= ( _I |` B ) ) /\ ( ( R ` G ) =/= ( R ` F ) /\ ( R ` X ) =/= ( R ` F ) ) /\ ( R ` G ) =/= ( R ` X ) ) ) -> ( ( S ` G ) ` P ) .<_ ( P .\/ ( R ` G ) ) )
53 2 3 4 5 6 7 trljat1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) -> ( P .\/ ( R ` G ) ) = ( P .\/ ( G ` P ) ) )
54 12 13 20 53 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( N e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ X =/= ( _I |` B ) ) /\ ( ( R ` G ) =/= ( R ` F ) /\ ( R ` X ) =/= ( R ` F ) ) /\ ( R ` G ) =/= ( R ` X ) ) ) -> ( P .\/ ( R ` G ) ) = ( P .\/ ( G ` P ) ) )
55 52 54 breqtrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( N e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ X =/= ( _I |` B ) ) /\ ( ( R ` G ) =/= ( R ` F ) /\ ( R ` X ) =/= ( R ` F ) ) /\ ( R ` G ) =/= ( R ` X ) ) ) -> ( ( S ` G ) ` P ) .<_ ( P .\/ ( G ` P ) ) )
56 simp2 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( N e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ X =/= ( _I |` B ) ) /\ ( ( R ` G ) =/= ( R ` F ) /\ ( R ` X ) =/= ( R ` F ) ) /\ ( R ` G ) =/= ( R ` X ) ) ) -> ( ( N e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) )
57 simp31 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( N e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ X =/= ( _I |` B ) ) /\ ( ( R ` G ) =/= ( R ` F ) /\ ( R ` X ) =/= ( R ` F ) ) /\ ( R ` G ) =/= ( R ` X ) ) ) -> ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ X =/= ( _I |` B ) ) )
58 eqid 
 |-  ( ( ( G ` P ) .\/ ( X ` P ) ) ./\ ( ( R ` ( G o. `' F ) ) .\/ ( R ` ( X o. `' F ) ) ) ) = ( ( ( G ` P ) .\/ ( X ` P ) ) ./\ ( ( R ` ( G o. `' F ) ) .\/ ( R ` ( X o. `' F ) ) ) )
59 1 2 3 4 5 6 7 8 9 58 cdlemk11 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( N e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ X =/= ( _I |` B ) ) /\ ( R ` G ) =/= ( R ` F ) /\ ( R ` X ) =/= ( R ` F ) ) ) -> ( ( S ` G ) ` P ) .<_ ( ( ( S ` X ) ` P ) .\/ ( R ` ( X o. `' G ) ) ) )
60 32 56 57 34 25 59 syl113anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( N e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ X =/= ( _I |` B ) ) /\ ( ( R ` G ) =/= ( R ` F ) /\ ( R ` X ) =/= ( R ` F ) ) /\ ( R ` G ) =/= ( R ` X ) ) ) -> ( ( S ` G ) ` P ) .<_ ( ( ( S ` X ) ` P ) .\/ ( R ` ( X o. `' G ) ) ) )
61 2 3 4 hlatlej2 
 |-  ( ( K e. HL /\ P e. A /\ ( R ` G ) e. A ) -> ( R ` G ) .<_ ( P .\/ ( R ` G ) ) )
62 10 11 41 61 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( N e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ X =/= ( _I |` B ) ) /\ ( ( R ` G ) =/= ( R ` F ) /\ ( R ` X ) =/= ( R ` F ) ) /\ ( R ` G ) =/= ( R ` X ) ) ) -> ( R ` G ) .<_ ( P .\/ ( R ` G ) ) )
63 62 54 breqtrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( N e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ X =/= ( _I |` B ) ) /\ ( ( R ` G ) =/= ( R ` F ) /\ ( R ` X ) =/= ( R ` F ) ) /\ ( R ` G ) =/= ( R ` X ) ) ) -> ( R ` G ) .<_ ( P .\/ ( G ` P ) ) )
64 1 2 3 4 5 6 7 8 9 cdlemksel 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ X e. T ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( F =/= ( _I |` B ) /\ X =/= ( _I |` B ) /\ ( R ` X ) =/= ( R ` F ) ) ) -> ( S ` X ) e. T )
65 18 22 23 24 25 64 syl113anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( N e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ X =/= ( _I |` B ) ) /\ ( ( R ` G ) =/= ( R ` F ) /\ ( R ` X ) =/= ( R ` F ) ) /\ ( R ` G ) =/= ( R ` X ) ) ) -> ( S ` X ) e. T )
66 2 4 5 6 ltrnel 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S ` X ) e. T /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( ( S ` X ) ` P ) e. A /\ -. ( ( S ` X ) ` P ) .<_ W ) )
67 12 65 20 66 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( N e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ X =/= ( _I |` B ) ) /\ ( ( R ` G ) =/= ( R ` F ) /\ ( R ` X ) =/= ( R ` F ) ) /\ ( R ` G ) =/= ( R ` X ) ) ) -> ( ( ( S ` X ) ` P ) e. A /\ -. ( ( S ` X ) ` P ) .<_ W ) )
68 5 6 ltrncnv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ G e. T ) -> `' G e. T )
69 12 13 68 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( N e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ X =/= ( _I |` B ) ) /\ ( ( R ` G ) =/= ( R ` F ) /\ ( R ` X ) =/= ( R ` F ) ) /\ ( R ` G ) =/= ( R ` X ) ) ) -> `' G e. T )
70 5 6 7 trlcnv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ G e. T ) -> ( R ` `' G ) = ( R ` G ) )
71 12 13 70 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( N e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ X =/= ( _I |` B ) ) /\ ( ( R ` G ) =/= ( R ` F ) /\ ( R ` X ) =/= ( R ` F ) ) /\ ( R ` G ) =/= ( R ` X ) ) ) -> ( R ` `' G ) = ( R ` G ) )
72 71 28 eqnetrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( N e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ X =/= ( _I |` B ) ) /\ ( ( R ` G ) =/= ( R ` F ) /\ ( R ` X ) =/= ( R ` F ) ) /\ ( R ` G ) =/= ( R ` X ) ) ) -> ( R ` `' G ) =/= ( R ` X ) )
73 1 5 6 7 trlcone 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( `' G e. T /\ X e. T ) /\ ( ( R ` `' G ) =/= ( R ` X ) /\ X =/= ( _I |` B ) ) ) -> ( R ` `' G ) =/= ( R ` ( `' G o. X ) ) )
74 12 69 17 72 24 73 syl122anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( N e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ X =/= ( _I |` B ) ) /\ ( ( R ` G ) =/= ( R ` F ) /\ ( R ` X ) =/= ( R ` F ) ) /\ ( R ` G ) =/= ( R ` X ) ) ) -> ( R ` `' G ) =/= ( R ` ( `' G o. X ) ) )
75 74 necomd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( N e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ X =/= ( _I |` B ) ) /\ ( ( R ` G ) =/= ( R ` F ) /\ ( R ` X ) =/= ( R ` F ) ) /\ ( R ` G ) =/= ( R ` X ) ) ) -> ( R ` ( `' G o. X ) ) =/= ( R ` `' G ) )
76 5 6 ltrncom 
 |-  ( ( ( K e. HL /\ W e. H ) /\ `' G e. T /\ X e. T ) -> ( `' G o. X ) = ( X o. `' G ) )
77 12 69 17 76 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( N e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ X =/= ( _I |` B ) ) /\ ( ( R ` G ) =/= ( R ` F ) /\ ( R ` X ) =/= ( R ` F ) ) /\ ( R ` G ) =/= ( R ` X ) ) ) -> ( `' G o. X ) = ( X o. `' G ) )
78 77 fveq2d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( N e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ X =/= ( _I |` B ) ) /\ ( ( R ` G ) =/= ( R ` F ) /\ ( R ` X ) =/= ( R ` F ) ) /\ ( R ` G ) =/= ( R ` X ) ) ) -> ( R ` ( `' G o. X ) ) = ( R ` ( X o. `' G ) ) )
79 75 78 71 3netr3d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( N e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ X =/= ( _I |` B ) ) /\ ( ( R ` G ) =/= ( R ` F ) /\ ( R ` X ) =/= ( R ` F ) ) /\ ( R ` G ) =/= ( R ` X ) ) ) -> ( R ` ( X o. `' G ) ) =/= ( R ` G ) )
80 5 6 ltrnco 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. T /\ `' G e. T ) -> ( X o. `' G ) e. T )
81 12 17 69 80 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( N e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ X =/= ( _I |` B ) ) /\ ( ( R ` G ) =/= ( R ` F ) /\ ( R ` X ) =/= ( R ` F ) ) /\ ( R ` G ) =/= ( R ` X ) ) ) -> ( X o. `' G ) e. T )
82 2 5 6 7 trlle 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X o. `' G ) e. T ) -> ( R ` ( X o. `' G ) ) .<_ W )
83 12 81 82 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( N e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ X =/= ( _I |` B ) ) /\ ( ( R ` G ) =/= ( R ` F ) /\ ( R ` X ) =/= ( R ` F ) ) /\ ( R ` G ) =/= ( R ` X ) ) ) -> ( R ` ( X o. `' G ) ) .<_ W )
84 2 5 6 7 trlle 
 |-  ( ( ( K e. HL /\ W e. H ) /\ G e. T ) -> ( R ` G ) .<_ W )
85 12 13 84 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( N e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ X =/= ( _I |` B ) ) /\ ( ( R ` G ) =/= ( R ` F ) /\ ( R ` X ) =/= ( R ` F ) ) /\ ( R ` G ) =/= ( R ` X ) ) ) -> ( R ` G ) .<_ W )
86 2 3 4 5 lhp2atnle 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( ( ( S ` X ) ` P ) e. A /\ -. ( ( S ` X ) ` P ) .<_ W ) /\ ( R ` ( X o. `' G ) ) =/= ( R ` G ) ) /\ ( ( R ` ( X o. `' G ) ) e. A /\ ( R ` ( X o. `' G ) ) .<_ W ) /\ ( ( R ` G ) e. A /\ ( R ` G ) .<_ W ) ) -> -. ( R ` G ) .<_ ( ( ( S ` X ) ` P ) .\/ ( R ` ( X o. `' G ) ) ) )
87 12 67 79 31 83 41 85 86 syl322anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( N e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ X =/= ( _I |` B ) ) /\ ( ( R ` G ) =/= ( R ` F ) /\ ( R ` X ) =/= ( R ` F ) ) /\ ( R ` G ) =/= ( R ` X ) ) ) -> -. ( R ` G ) .<_ ( ( ( S ` X ) ` P ) .\/ ( R ` ( X o. `' G ) ) ) )
88 nbrne1 
 |-  ( ( ( R ` G ) .<_ ( P .\/ ( G ` P ) ) /\ -. ( R ` G ) .<_ ( ( ( S ` X ) ` P ) .\/ ( R ` ( X o. `' G ) ) ) ) -> ( P .\/ ( G ` P ) ) =/= ( ( ( S ` X ) ` P ) .\/ ( R ` ( X o. `' G ) ) ) )
89 63 87 88 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( N e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ X =/= ( _I |` B ) ) /\ ( ( R ` G ) =/= ( R ` F ) /\ ( R ` X ) =/= ( R ` F ) ) /\ ( R ` G ) =/= ( R ` X ) ) ) -> ( P .\/ ( G ` P ) ) =/= ( ( ( S ` X ) ` P ) .\/ ( R ` ( X o. `' G ) ) ) )
90 2 3 8 4 2atm 
 |-  ( ( ( K e. HL /\ P e. A /\ ( G ` P ) e. A ) /\ ( ( ( S ` X ) ` P ) e. A /\ ( R ` ( X o. `' G ) ) e. A /\ ( ( S ` G ) ` P ) e. A ) /\ ( ( ( S ` G ) ` P ) .<_ ( P .\/ ( G ` P ) ) /\ ( ( S ` G ) ` P ) .<_ ( ( ( S ` X ) ` P ) .\/ ( R ` ( X o. `' G ) ) ) /\ ( P .\/ ( G ` P ) ) =/= ( ( ( S ` X ) ` P ) .\/ ( R ` ( X o. `' G ) ) ) ) ) -> ( ( S ` G ) ` P ) = ( ( P .\/ ( G ` P ) ) ./\ ( ( ( S ` X ) ` P ) .\/ ( R ` ( X o. `' G ) ) ) ) )
91 10 11 15 27 31 36 55 60 89 90 syl333anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( N e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ X =/= ( _I |` B ) ) /\ ( ( R ` G ) =/= ( R ` F ) /\ ( R ` X ) =/= ( R ` F ) ) /\ ( R ` G ) =/= ( R ` X ) ) ) -> ( ( S ` G ) ` P ) = ( ( P .\/ ( G ` P ) ) ./\ ( ( ( S ` X ) ` P ) .\/ ( R ` ( X o. `' G ) ) ) ) )