Theorem cdlemk12 34429

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

Hypotheses

Ref	Expression
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

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

Distinct variable groups:   ./\ , f   .\/ , f   f, F, i   f, G, i   f, N   P, f   R, f   T, f   f, W   ./\ , i   .<_ , i   .\/ , i   A, i   i, F   i, H   i, K   i, N   P, i   R, i   T, i   i, W   f, X, i

Allowed substitution hints:   A( f)   B( f, i)   S( f, i)   H( f)   K( f)   .<_ ( f)

Proof of Theorem cdlemk12

Step	Hyp	Ref	Expression
1		simp11l 1120	. 2 |- ( ( ( ( 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 )
2		simp22l 1128	. 2 |- ( ( ( ( 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 )
3		simp11 1039	. . 3 |- ( ( ( ( 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 ) )
4		simp13 1041	. . 3 |- ( ( ( ( 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 )
5		cdlemk.l	. . . 4 |- .<_ = ( le ` K )
6		cdlemk.a	. . . 4 |- A = ( Atoms ` K )
7		cdlemk.h	. . . 4 |- H = ( LHyp ` K )
8		cdlemk.t	. . . 4 |- T = ( ( LTrn ` K ) ` W )
9	5, 6, 7, 8	ltrnat 33717	. . 3 |- ( ( ( K e. HL /\ W e. H ) /\ G e. T /\ P e. A ) -> ( G ` P ) e. A )
10	3, 4, 2, 9	syl3anc 1269	. 2 |- ( ( ( ( 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 )
11		simp12 1040	. . . 4 |- ( ( ( ( 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 )
12		simp21r 1127	. . . 4 |- ( ( ( ( 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 )
13	3, 11, 12	3jca 1189	. . 3 |- ( ( ( ( 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 ) )
14		simp21l 1126	. . . 4 |- ( ( ( ( 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 )
15		simp22 1043	. . . 4 |- ( ( ( ( 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 ) )
16		simp23 1044	. . . 4 |- ( ( ( ( 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 ) )
17	14, 15, 16	3jca 1189	. . 3 |- ( ( ( ( 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 ) ) )
18		simp311 1156	. . 3 |- ( ( ( ( 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 ) )
19		simp313 1158	. . 3 |- ( ( ( ( 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 ) )
20		simp32r 1135	. . 3 |- ( ( ( ( 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 ) )
21		cdlemk.b	. . . 4 |- B = ( Base ` K )
22		cdlemk.j	. . . 4 |- .\/ = ( join ` K )
23		cdlemk.r	. . . 4 |- R = ( ( trL ` K ) ` W )
24		cdlemk.m	. . . 4 |- ./\ = ( meet ` K )
25		cdlemk.s	. . . 4 |- S = ( f e. T |-> ( iota_ i e. T ( i ` P ) = ( ( P .\/ ( R ` f ) ) ./\ ( ( N ` P ) .\/ ( R ` ( f o. `' F ) ) ) ) ) )
26	21, 5, 22, 6, 7, 8, 23, 24, 25	cdlemksat 34425	. . 3 |- ( ( ( ( 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	13, 17, 18, 19, 20, 26	syl113anc 1281	. 2 |- ( ( ( ( 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 1047	. . . 4 |- ( ( ( ( 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 2681	. . 3 |- ( ( ( ( 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	6, 7, 8, 23	trlcocnvat 34303	. . 3 |- ( ( ( K e. HL /\ W e. H ) /\ ( X e. T /\ G e. T ) /\ ( R ` X ) =/= ( R ` G ) ) -> ( R ` ( X o. `' G ) ) e. A )
31	3, 12, 4, 29, 30	syl121anc 1274	. 2 |- ( ( ( ( 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 1009	. . 3 |- ( ( ( ( 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 1157	. . 3 |- ( ( ( ( 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 1134	. . 3 |- ( ( ( ( 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	21, 5, 22, 6, 7, 8, 23, 24, 25	cdlemksat 34425	. . 3 |- ( ( ( ( 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, 17, 18, 33, 34, 35	syl113anc 1281	. 2 |- ( ( ( ( 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	21, 5, 22, 6, 7, 8, 23, 24, 25	cdlemksv2 34426	. . . . 5 |- ( ( ( ( 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, 17, 18, 33, 34, 37	syl113anc 1281	. . . 4 |- ( ( ( ( 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		hllat 32941	. . . . . 6 |- ( K e. HL -> K e. Lat )
40	1, 39	syl 17	. . . . 5 |- ( ( ( ( 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 )
41	21, 6, 7, 8, 23	trlnidat 33751	. . . . . . 7 |- ( ( ( K e. HL /\ W e. H ) /\ G e. T /\ G =/= ( _I |` B ) ) -> ( R ` G ) e. A )
42	3, 4, 33, 41	syl3anc 1269	. . . . . 6 |- ( ( ( ( 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 )
43	21, 22, 6	hlatjcl 32944	. . . . . 6 |- ( ( K e. HL /\ P e. A /\ ( R ` G ) e. A ) -> ( P .\/ ( R ` G ) ) e. B )
44	1, 2, 42, 43	syl3anc 1269	. . . . 5 |- ( ( ( ( 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 )
45	5, 6, 7, 8	ltrnat 33717	. . . . . . 7 |- ( ( ( K e. HL /\ W e. H ) /\ N e. T /\ P e. A ) -> ( N ` P ) e. A )
46	3, 14, 2, 45	syl3anc 1269	. . . . . 6 |- ( ( ( ( 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 )
47	6, 7, 8, 23	trlcocnvat 34303	. . . . . . 7 |- ( ( ( K e. HL /\ W e. H ) /\ ( G e. T /\ F e. T ) /\ ( R ` G ) =/= ( R ` F ) ) -> ( R ` ( G o. `' F ) ) e. A )
48	3, 4, 11, 34, 47	syl121anc 1274	. . . . . 6 |- ( ( ( ( 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 )
49	21, 22, 6	hlatjcl 32944	. . . . . 6 |- ( ( K e. HL /\ ( N ` P ) e. A /\ ( R ` ( G o. `' F ) ) e. A ) -> ( ( N ` P ) .\/ ( R ` ( G o. `' F ) ) ) e. B )
50	1, 46, 48, 49	syl3anc 1269	. . . . 5 |- ( ( ( ( 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 )
51	21, 5, 24	latmle1 16334	. . . . 5 |- ( ( 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 ) ) )
52	40, 44, 50, 51	syl3anc 1269	. . . 4 |- ( ( ( ( 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 ) ) )
53	38, 52	eqbrtrd 4426	. . 3 |- ( ( ( ( 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 ) ) )
54	5, 22, 6, 7, 8, 23	trljat1 33744	. . . 4 |- ( ( ( K e. HL /\ W e. H ) /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) -> ( P .\/ ( R ` G ) ) = ( P .\/ ( G ` P ) ) )
55	3, 4, 15, 54	syl3anc 1269	. . 3 |- ( ( ( ( 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 ) ) )
56	53, 55	breqtrd 4430	. 2 |- ( ( ( ( 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 ) ) )
57		simp2 1010	. . 3 |- ( ( ( ( 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 ) ) )
58		simp31 1045	. . 3 |- ( ( ( ( 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 ) ) )
59		eqid 2453	. . . 4 |- ( ( ( G ` P ) .\/ ( X ` P ) ) ./\ ( ( R ` ( G o. `' F ) ) .\/ ( R ` ( X o. `' F ) ) ) ) = ( ( ( G ` P ) .\/ ( X ` P ) ) ./\ ( ( R ` ( G o. `' F ) ) .\/ ( R ` ( X o. `' F ) ) ) )
60	21, 5, 22, 6, 7, 8, 23, 24, 25, 59	cdlemk11 34428	. . 3 |- ( ( ( ( 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 ) ) ) )
61	32, 57, 58, 34, 20, 60	syl113anc 1281	. 2 |- ( ( ( ( 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 ) ) ) )
62	5, 22, 6	hlatlej2 32953	. . . . 5 |- ( ( K e. HL /\ P e. A /\ ( R ` G ) e. A ) -> ( R ` G ) .<_ ( P .\/ ( R ` G ) ) )
63	1, 2, 42, 62	syl3anc 1269	. . . 4 |- ( ( ( ( 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 ) ) )
64	63, 55	breqtrd 4430	. . 3 |- ( ( ( ( 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 ) ) )
65	21, 5, 22, 6, 7, 8, 23, 24, 25	cdlemksel 34424	. . . . . 6 |- ( ( ( ( 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 )
66	13, 17, 18, 19, 20, 65	syl113anc 1281	. . . . 5 |- ( ( ( ( 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 )
67	5, 6, 7, 8	ltrnel 33716	. . . . 5 |- ( ( ( K e. HL /\ W e. H ) /\ ( S ` X ) e. T /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( ( S ` X ) ` P ) e. A /\ -. ( ( S ` X ) ` P ) .<_ W ) )
68	3, 66, 15, 67	syl3anc 1269	. . . 4 |- ( ( ( ( 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 ) )
69	7, 8	ltrncnv 33723	. . . . . . . 8 |- ( ( ( K e. HL /\ W e. H ) /\ G e. T ) -> `' G e. T )
70	3, 4, 69	syl2anc 667	. . . . . . 7 |- ( ( ( ( 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 )
71	7, 8, 23	trlcnv 33743	. . . . . . . . 9 |- ( ( ( K e. HL /\ W e. H ) /\ G e. T ) -> ( R ` `' G ) = ( R ` G ) )
72	3, 4, 71	syl2anc 667	. . . . . . . 8 |- ( ( ( ( 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 ) )
73	72, 28	eqnetrd 2693	. . . . . . 7 |- ( ( ( ( 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 ) )
74	21, 7, 8, 23	trlcone 34307	. . . . . . 7 |- ( ( ( 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 ) ) )
75	3, 70, 12, 73, 19, 74	syl122anc 1278	. . . . . 6 |- ( ( ( ( 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 ) ) )
76	75	necomd 2681	. . . . 5 |- ( ( ( ( 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 ) )
77	7, 8	ltrncom 34317	. . . . . . 7 |- ( ( ( K e. HL /\ W e. H ) /\ `' G e. T /\ X e. T ) -> ( `' G o. X ) = ( X o. `' G ) )
78	3, 70, 12, 77	syl3anc 1269	. . . . . 6 |- ( ( ( ( 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 ) )
79	78	fveq2d 5874	. . . . 5 |- ( ( ( ( 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 ) ) )
80	76, 79, 72	3netr3d 2702	. . . 4 |- ( ( ( ( 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 ) )
81	7, 8	ltrnco 34298	. . . . . 6 |- ( ( ( K e. HL /\ W e. H ) /\ X e. T /\ `' G e. T ) -> ( X o. `' G ) e. T )
82	3, 12, 70, 81	syl3anc 1269	. . . . 5 |- ( ( ( ( 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 )
83	5, 7, 8, 23	trlle 33762	. . . . 5 |- ( ( ( K e. HL /\ W e. H ) /\ ( X o. `' G ) e. T ) -> ( R ` ( X o. `' G ) ) .<_ W )
84	3, 82, 83	syl2anc 667	. . . 4 |- ( ( ( ( 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 )
85	5, 7, 8, 23	trlle 33762	. . . . 5 |- ( ( ( K e. HL /\ W e. H ) /\ G e. T ) -> ( R ` G ) .<_ W )
86	3, 4, 85	syl2anc 667	. . . 4 |- ( ( ( ( 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 )
87	5, 22, 6, 7	lhp2atnle 33610	. . . 4 |- ( ( ( ( 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 ) ) ) )
88	3, 68, 80, 31, 84, 42, 86, 87	syl322anc 1297	. . 3 |- ( ( ( ( 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 ) ) ) )
89		nbrne1 4423	. . 3 |- ( ( ( R ` G ) .<_ ( P .\/ ( G ` P ) ) /\ -. ( R ` G ) .<_ ( ( ( S ` X ) ` P ) .\/ ( R ` ( X o. `' G ) ) ) ) -> ( P .\/ ( G ` P ) ) =/= ( ( ( S ` X ) ` P ) .\/ ( R ` ( X o. `' G ) ) ) )
90	64, 88, 89	syl2anc 667	. 2 |- ( ( ( ( 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 ) ) ) )
91	5, 22, 24, 6	2atm 33104	. 2 |- ( ( ( 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 ) ) ) ) )
92	1, 2, 10, 27, 31, 36, 56, 61, 90, 91	syl333anc 1301	1 |- ( ( ( ( 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 ) ) ) ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 371   /\ w3a 986   = wceq 1446   e. wcel 1889   =/= wne 2624   class class class wbr 4405   |-> cmpt 4464   _I cid 4747   `'ccnv 4836   |` cres 4839   o. ccom 4841   ` cfv 5585   iota_crio 6256  (class class class)co 6295   Basecbs 15133   lecple 15209   joincjn 16201   meetcmee 16202   Latclat 16303   Atomscatm 32841   HLchlt 32928   LHypclh 33561   LTrncltrn 33678   trLctrl 33736

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-8 1891  ax-9 1898  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433  ax-rep 4518  ax-sep 4528  ax-nul 4537  ax-pow 4584  ax-pr 4642  ax-un 6588  ax-riotaBAD 32537

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 987  df-3an 988  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-eu 2305  df-mo 2306  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ne 2626  df-nel 2627  df-ral 2744  df-rex 2745  df-reu 2746  df-rmo 2747  df-rab 2748  df-v 3049  df-sbc 3270  df-csb 3366  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-nul 3734  df-if 3884  df-pw 3955  df-sn 3971  df-pr 3973  df-op 3977  df-uni 4202  df-iun 4283  df-iin 4284  df-br 4406  df-opab 4465  df-mpt 4466  df-id 4752  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5549  df-fun 5587  df-fn 5588  df-f 5589  df-f1 5590  df-fo 5591  df-f1o 5592  df-fv 5593  df-riota 6257  df-ov 6298  df-oprab 6299  df-mpt2 6300  df-1st 6798  df-2nd 6799  df-undef 7025  df-map 7479  df-preset 16185  df-poset 16203  df-plt 16216  df-lub 16232  df-glb 16233  df-join 16234  df-meet 16235  df-p0 16297  df-p1 16298  df-lat 16304  df-clat 16366  df-oposet 32754  df-ol 32756  df-oml 32757  df-covers 32844  df-ats 32845  df-atl 32876  df-cvlat 32900  df-hlat 32929  df-llines 33075  df-lplanes 33076  df-lvols 33077  df-lines 33078  df-psubsp 33080  df-pmap 33081  df-padd 33373  df-lhyp 33565  df-laut 33566  df-ldil 33681  df-ltrn 33682  df-trl 33737

This theorem is referenced by:  cdlemk21N  34452  cdlemk20  34453