Theorem dalawlem12

Description: Lemma for dalaw . Second part of dalawlem13 . (Contributed by NM, 17-Sep-2012)

	Ref	Expression
Hypotheses	dalawlem.l	|- .<_ = ( le ` K )
	dalawlem.j	|- .\/ = ( join ` K )
	dalawlem.m	|- ./\ = ( meet ` K )
	dalawlem.a	|- A = ( Atoms ` K )
Assertion	dalawlem12	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( P .\/ Q ) ./\ ( S .\/ T ) ) .<_ ( ( ( Q .\/ R ) ./\ ( T .\/ U ) ) .\/ ( ( R .\/ P ) ./\ ( U .\/ S ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		dalawlem.l	|- .<_ = ( le ` K )
2		dalawlem.j	|- .\/ = ( join ` K )
3		dalawlem.m	|- ./\ = ( meet ` K )
4		dalawlem.a	|- A = ( Atoms ` K )
5		eqid	|- ( Base ` K ) = ( Base ` K )
6		simp11	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> K e. HL )
7	6	hllatd	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> K e. Lat )
8		simp21	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> P e. A )
9		simp22	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> Q e. A )
10	5 2 4	hlatjcl	|- ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( P .\/ Q ) e. ( Base ` K ) )
11	6 8 9 10	syl3anc	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( P .\/ Q ) e. ( Base ` K ) )
12		simp31	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> S e. A )
13		simp32	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> T e. A )
14	5 2 4	hlatjcl	|- ( ( K e. HL /\ S e. A /\ T e. A ) -> ( S .\/ T ) e. ( Base ` K ) )
15	6 12 13 14	syl3anc	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( S .\/ T ) e. ( Base ` K ) )
16	5 3	latmcl	|- ( ( K e. Lat /\ ( P .\/ Q ) e. ( Base ` K ) /\ ( S .\/ T ) e. ( Base ` K ) ) -> ( ( P .\/ Q ) ./\ ( S .\/ T ) ) e. ( Base ` K ) )
17	7 11 15 16	syl3anc	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( P .\/ Q ) ./\ ( S .\/ T ) ) e. ( Base ` K ) )
18	5 4	atbase	|- ( S e. A -> S e. ( Base ` K ) )
19	12 18	syl	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> S e. ( Base ` K ) )
20	5 2	latjcl	|- ( ( K e. Lat /\ ( P .\/ Q ) e. ( Base ` K ) /\ S e. ( Base ` K ) ) -> ( ( P .\/ Q ) .\/ S ) e. ( Base ` K ) )
21	7 11 19 20	syl3anc	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( P .\/ Q ) .\/ S ) e. ( Base ` K ) )
22	5 4	atbase	|- ( T e. A -> T e. ( Base ` K ) )
23	13 22	syl	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> T e. ( Base ` K ) )
24	5 3	latmcl	|- ( ( K e. Lat /\ ( ( P .\/ Q ) .\/ S ) e. ( Base ` K ) /\ T e. ( Base ` K ) ) -> ( ( ( P .\/ Q ) .\/ S ) ./\ T ) e. ( Base ` K ) )
25	7 21 23 24	syl3anc	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( ( P .\/ Q ) .\/ S ) ./\ T ) e. ( Base ` K ) )
26	5 2	latjcl	|- ( ( K e. Lat /\ ( ( ( P .\/ Q ) .\/ S ) ./\ T ) e. ( Base ` K ) /\ S e. ( Base ` K ) ) -> ( ( ( ( P .\/ Q ) .\/ S ) ./\ T ) .\/ S ) e. ( Base ` K ) )
27	7 25 19 26	syl3anc	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( ( ( P .\/ Q ) .\/ S ) ./\ T ) .\/ S ) e. ( Base ` K ) )
28	5 4	atbase	|- ( Q e. A -> Q e. ( Base ` K ) )
29	9 28	syl	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> Q e. ( Base ` K ) )
30		simp33	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> U e. A )
31	5 2 4	hlatjcl	|- ( ( K e. HL /\ T e. A /\ U e. A ) -> ( T .\/ U ) e. ( Base ` K ) )
32	6 13 30 31	syl3anc	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( T .\/ U ) e. ( Base ` K ) )
33	5 3	latmcl	|- ( ( K e. Lat /\ Q e. ( Base ` K ) /\ ( T .\/ U ) e. ( Base ` K ) ) -> ( Q ./\ ( T .\/ U ) ) e. ( Base ` K ) )
34	7 29 32 33	syl3anc	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( Q ./\ ( T .\/ U ) ) e. ( Base ` K ) )
35	5 2 4	hlatjcl	|- ( ( K e. HL /\ U e. A /\ S e. A ) -> ( U .\/ S ) e. ( Base ` K ) )
36	6 30 12 35	syl3anc	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( U .\/ S ) e. ( Base ` K ) )
37	5 2	latjcl	|- ( ( K e. Lat /\ ( Q ./\ ( T .\/ U ) ) e. ( Base ` K ) /\ ( U .\/ S ) e. ( Base ` K ) ) -> ( ( Q ./\ ( T .\/ U ) ) .\/ ( U .\/ S ) ) e. ( Base ` K ) )
38	7 34 36 37	syl3anc	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( Q ./\ ( T .\/ U ) ) .\/ ( U .\/ S ) ) e. ( Base ` K ) )
39	5 1 2	latlej1	|- ( ( K e. Lat /\ ( P .\/ Q ) e. ( Base ` K ) /\ S e. ( Base ` K ) ) -> ( P .\/ Q ) .<_ ( ( P .\/ Q ) .\/ S ) )
40	7 11 19 39	syl3anc	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( P .\/ Q ) .<_ ( ( P .\/ Q ) .\/ S ) )
41	5 2 4	hlatjcl	|- ( ( K e. HL /\ T e. A /\ S e. A ) -> ( T .\/ S ) e. ( Base ` K ) )
42	6 13 12 41	syl3anc	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( T .\/ S ) e. ( Base ` K ) )
43	5 1 3	latmlem1	|- ( ( K e. Lat /\ ( ( P .\/ Q ) e. ( Base ` K ) /\ ( ( P .\/ Q ) .\/ S ) e. ( Base ` K ) /\ ( T .\/ S ) e. ( Base ` K ) ) ) -> ( ( P .\/ Q ) .<_ ( ( P .\/ Q ) .\/ S ) -> ( ( P .\/ Q ) ./\ ( T .\/ S ) ) .<_ ( ( ( P .\/ Q ) .\/ S ) ./\ ( T .\/ S ) ) ) )
44	7 11 21 42 43	syl13anc	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( P .\/ Q ) .<_ ( ( P .\/ Q ) .\/ S ) -> ( ( P .\/ Q ) ./\ ( T .\/ S ) ) .<_ ( ( ( P .\/ Q ) .\/ S ) ./\ ( T .\/ S ) ) ) )
45	40 44	mpd	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( P .\/ Q ) ./\ ( T .\/ S ) ) .<_ ( ( ( P .\/ Q ) .\/ S ) ./\ ( T .\/ S ) ) )
46	2 4	hlatjcom	|- ( ( K e. HL /\ S e. A /\ T e. A ) -> ( S .\/ T ) = ( T .\/ S ) )
47	6 12 13 46	syl3anc	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( S .\/ T ) = ( T .\/ S ) )
48	47	oveq2d	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( P .\/ Q ) ./\ ( S .\/ T ) ) = ( ( P .\/ Q ) ./\ ( T .\/ S ) ) )
49	5 1 2	latlej2	|- ( ( K e. Lat /\ ( P .\/ Q ) e. ( Base ` K ) /\ S e. ( Base ` K ) ) -> S .<_ ( ( P .\/ Q ) .\/ S ) )
50	7 11 19 49	syl3anc	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> S .<_ ( ( P .\/ Q ) .\/ S ) )
51	5 1 2 3 4	atmod2i2	|- ( ( K e. HL /\ ( T e. A /\ ( ( P .\/ Q ) .\/ S ) e. ( Base ` K ) /\ S e. ( Base ` K ) ) /\ S .<_ ( ( P .\/ Q ) .\/ S ) ) -> ( ( ( ( P .\/ Q ) .\/ S ) ./\ T ) .\/ S ) = ( ( ( P .\/ Q ) .\/ S ) ./\ ( T .\/ S ) ) )
52	6 13 21 19 50 51	syl131anc	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( ( ( P .\/ Q ) .\/ S ) ./\ T ) .\/ S ) = ( ( ( P .\/ Q ) .\/ S ) ./\ ( T .\/ S ) ) )
53	45 48 52	3brtr4d	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( P .\/ Q ) ./\ ( S .\/ T ) ) .<_ ( ( ( ( P .\/ Q ) .\/ S ) ./\ T ) .\/ S ) )
54		hlol	|- ( K e. HL -> K e. OL )
55	6 54	syl	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> K e. OL )
56	5 2 4	hlatjcl	|- ( ( K e. HL /\ P e. A /\ S e. A ) -> ( P .\/ S ) e. ( Base ` K ) )
57	6 8 12 56	syl3anc	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( P .\/ S ) e. ( Base ` K ) )
58	5 2	latjcl	|- ( ( K e. Lat /\ Q e. ( Base ` K ) /\ ( P .\/ S ) e. ( Base ` K ) ) -> ( Q .\/ ( P .\/ S ) ) e. ( Base ` K ) )
59	7 29 57 58	syl3anc	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( Q .\/ ( P .\/ S ) ) e. ( Base ` K ) )
60	5 2 4	hlatjcl	|- ( ( K e. HL /\ Q e. A /\ T e. A ) -> ( Q .\/ T ) e. ( Base ` K ) )
61	6 9 13 60	syl3anc	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( Q .\/ T ) e. ( Base ` K ) )
62	5 3	latmassOLD	|- ( ( K e. OL /\ ( ( Q .\/ ( P .\/ S ) ) e. ( Base ` K ) /\ ( Q .\/ T ) e. ( Base ` K ) /\ T e. ( Base ` K ) ) ) -> ( ( ( Q .\/ ( P .\/ S ) ) ./\ ( Q .\/ T ) ) ./\ T ) = ( ( Q .\/ ( P .\/ S ) ) ./\ ( ( Q .\/ T ) ./\ T ) ) )
63	55 59 61 23 62	syl13anc	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( ( Q .\/ ( P .\/ S ) ) ./\ ( Q .\/ T ) ) ./\ T ) = ( ( Q .\/ ( P .\/ S ) ) ./\ ( ( Q .\/ T ) ./\ T ) ) )
64	2 4	hlatjass	|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ S e. A ) ) -> ( ( P .\/ Q ) .\/ S ) = ( P .\/ ( Q .\/ S ) ) )
65	6 8 9 12 64	syl13anc	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( P .\/ Q ) .\/ S ) = ( P .\/ ( Q .\/ S ) ) )
66	2 4	hlatj12	|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ S e. A ) ) -> ( P .\/ ( Q .\/ S ) ) = ( Q .\/ ( P .\/ S ) ) )
67	6 8 9 12 66	syl13anc	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( P .\/ ( Q .\/ S ) ) = ( Q .\/ ( P .\/ S ) ) )
68	65 67	eqtr2d	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( Q .\/ ( P .\/ S ) ) = ( ( P .\/ Q ) .\/ S ) )
69	1 2 4	hlatlej2	|- ( ( K e. HL /\ Q e. A /\ T e. A ) -> T .<_ ( Q .\/ T ) )
70	6 9 13 69	syl3anc	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> T .<_ ( Q .\/ T ) )
71	5 1 3	latleeqm2	|- ( ( K e. Lat /\ T e. ( Base ` K ) /\ ( Q .\/ T ) e. ( Base ` K ) ) -> ( T .<_ ( Q .\/ T ) <-> ( ( Q .\/ T ) ./\ T ) = T ) )
72	7 23 61 71	syl3anc	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( T .<_ ( Q .\/ T ) <-> ( ( Q .\/ T ) ./\ T ) = T ) )
73	70 72	mpbid	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( Q .\/ T ) ./\ T ) = T )
74	68 73	oveq12d	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( Q .\/ ( P .\/ S ) ) ./\ ( ( Q .\/ T ) ./\ T ) ) = ( ( ( P .\/ Q ) .\/ S ) ./\ T ) )
75	63 74	eqtr2d	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( ( P .\/ Q ) .\/ S ) ./\ T ) = ( ( ( Q .\/ ( P .\/ S ) ) ./\ ( Q .\/ T ) ) ./\ T ) )
76	1 2 4	hlatlej1	|- ( ( K e. HL /\ Q e. A /\ T e. A ) -> Q .<_ ( Q .\/ T ) )
77	6 9 13 76	syl3anc	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> Q .<_ ( Q .\/ T ) )
78	5 1 2 3 4	atmod1i1	|- ( ( K e. HL /\ ( Q e. A /\ ( P .\/ S ) e. ( Base ` K ) /\ ( Q .\/ T ) e. ( Base ` K ) ) /\ Q .<_ ( Q .\/ T ) ) -> ( Q .\/ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) ) = ( ( Q .\/ ( P .\/ S ) ) ./\ ( Q .\/ T ) ) )
79	6 9 57 61 77 78	syl131anc	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( Q .\/ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) ) = ( ( Q .\/ ( P .\/ S ) ) ./\ ( Q .\/ T ) ) )
80	1 2 4	hlatlej2	|- ( ( K e. HL /\ U e. A /\ Q e. A ) -> Q .<_ ( U .\/ Q ) )
81	6 30 9 80	syl3anc	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> Q .<_ ( U .\/ Q ) )
82		simp13	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) )
83		simp12	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> Q = R )
84	83	oveq1d	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( Q .\/ U ) = ( R .\/ U ) )
85	2 4	hlatjcom	|- ( ( K e. HL /\ Q e. A /\ U e. A ) -> ( Q .\/ U ) = ( U .\/ Q ) )
86	6 9 30 85	syl3anc	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( Q .\/ U ) = ( U .\/ Q ) )
87	84 86	eqtr3d	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( R .\/ U ) = ( U .\/ Q ) )
88	82 87	breqtrd	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( U .\/ Q ) )
89	5 3	latmcl	|- ( ( K e. Lat /\ ( P .\/ S ) e. ( Base ` K ) /\ ( Q .\/ T ) e. ( Base ` K ) ) -> ( ( P .\/ S ) ./\ ( Q .\/ T ) ) e. ( Base ` K ) )
90	7 57 61 89	syl3anc	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( P .\/ S ) ./\ ( Q .\/ T ) ) e. ( Base ` K ) )
91	5 2 4	hlatjcl	|- ( ( K e. HL /\ U e. A /\ Q e. A ) -> ( U .\/ Q ) e. ( Base ` K ) )
92	6 30 9 91	syl3anc	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( U .\/ Q ) e. ( Base ` K ) )
93	5 1 2	latjle12	|- ( ( K e. Lat /\ ( Q e. ( Base ` K ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) e. ( Base ` K ) /\ ( U .\/ Q ) e. ( Base ` K ) ) ) -> ( ( Q .<_ ( U .\/ Q ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( U .\/ Q ) ) <-> ( Q .\/ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) ) .<_ ( U .\/ Q ) ) )
94	7 29 90 92 93	syl13anc	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( Q .<_ ( U .\/ Q ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( U .\/ Q ) ) <-> ( Q .\/ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) ) .<_ ( U .\/ Q ) ) )
95	81 88 94	mpbi2and	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( Q .\/ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) ) .<_ ( U .\/ Q ) )
96	79 95	eqbrtrrd	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( Q .\/ ( P .\/ S ) ) ./\ ( Q .\/ T ) ) .<_ ( U .\/ Q ) )
97	1 2 4	hlatlej1	|- ( ( K e. HL /\ T e. A /\ U e. A ) -> T .<_ ( T .\/ U ) )
98	6 13 30 97	syl3anc	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> T .<_ ( T .\/ U ) )
99	5 3	latmcl	|- ( ( K e. Lat /\ ( Q .\/ ( P .\/ S ) ) e. ( Base ` K ) /\ ( Q .\/ T ) e. ( Base ` K ) ) -> ( ( Q .\/ ( P .\/ S ) ) ./\ ( Q .\/ T ) ) e. ( Base ` K ) )
100	7 59 61 99	syl3anc	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( Q .\/ ( P .\/ S ) ) ./\ ( Q .\/ T ) ) e. ( Base ` K ) )
101	5 1 3	latmlem12	|- ( ( K e. Lat /\ ( ( ( Q .\/ ( P .\/ S ) ) ./\ ( Q .\/ T ) ) e. ( Base ` K ) /\ ( U .\/ Q ) e. ( Base ` K ) ) /\ ( T e. ( Base ` K ) /\ ( T .\/ U ) e. ( Base ` K ) ) ) -> ( ( ( ( Q .\/ ( P .\/ S ) ) ./\ ( Q .\/ T ) ) .<_ ( U .\/ Q ) /\ T .<_ ( T .\/ U ) ) -> ( ( ( Q .\/ ( P .\/ S ) ) ./\ ( Q .\/ T ) ) ./\ T ) .<_ ( ( U .\/ Q ) ./\ ( T .\/ U ) ) ) )
102	7 100 92 23 32 101	syl122anc	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( ( ( Q .\/ ( P .\/ S ) ) ./\ ( Q .\/ T ) ) .<_ ( U .\/ Q ) /\ T .<_ ( T .\/ U ) ) -> ( ( ( Q .\/ ( P .\/ S ) ) ./\ ( Q .\/ T ) ) ./\ T ) .<_ ( ( U .\/ Q ) ./\ ( T .\/ U ) ) ) )
103	96 98 102	mp2and	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( ( Q .\/ ( P .\/ S ) ) ./\ ( Q .\/ T ) ) ./\ T ) .<_ ( ( U .\/ Q ) ./\ ( T .\/ U ) ) )
104	75 103	eqbrtrd	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( ( P .\/ Q ) .\/ S ) ./\ T ) .<_ ( ( U .\/ Q ) ./\ ( T .\/ U ) ) )
105	1 2 4	hlatlej2	|- ( ( K e. HL /\ T e. A /\ U e. A ) -> U .<_ ( T .\/ U ) )
106	6 13 30 105	syl3anc	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> U .<_ ( T .\/ U ) )
107	5 1 2 3 4	atmod1i1	|- ( ( K e. HL /\ ( U e. A /\ Q e. ( Base ` K ) /\ ( T .\/ U ) e. ( Base ` K ) ) /\ U .<_ ( T .\/ U ) ) -> ( U .\/ ( Q ./\ ( T .\/ U ) ) ) = ( ( U .\/ Q ) ./\ ( T .\/ U ) ) )
108	6 30 29 32 106 107	syl131anc	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( U .\/ ( Q ./\ ( T .\/ U ) ) ) = ( ( U .\/ Q ) ./\ ( T .\/ U ) ) )
109	5 4	atbase	|- ( U e. A -> U e. ( Base ` K ) )
110	30 109	syl	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> U e. ( Base ` K ) )
111	5 2	latjcom	|- ( ( K e. Lat /\ U e. ( Base ` K ) /\ ( Q ./\ ( T .\/ U ) ) e. ( Base ` K ) ) -> ( U .\/ ( Q ./\ ( T .\/ U ) ) ) = ( ( Q ./\ ( T .\/ U ) ) .\/ U ) )
112	7 110 34 111	syl3anc	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( U .\/ ( Q ./\ ( T .\/ U ) ) ) = ( ( Q ./\ ( T .\/ U ) ) .\/ U ) )
113	108 112	eqtr3d	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( U .\/ Q ) ./\ ( T .\/ U ) ) = ( ( Q ./\ ( T .\/ U ) ) .\/ U ) )
114	104 113	breqtrd	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( ( P .\/ Q ) .\/ S ) ./\ T ) .<_ ( ( Q ./\ ( T .\/ U ) ) .\/ U ) )
115	5 2	latjcl	|- ( ( K e. Lat /\ ( Q ./\ ( T .\/ U ) ) e. ( Base ` K ) /\ U e. ( Base ` K ) ) -> ( ( Q ./\ ( T .\/ U ) ) .\/ U ) e. ( Base ` K ) )
116	7 34 110 115	syl3anc	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( Q ./\ ( T .\/ U ) ) .\/ U ) e. ( Base ` K ) )
117	5 1 2	latjlej1	|- ( ( K e. Lat /\ ( ( ( ( P .\/ Q ) .\/ S ) ./\ T ) e. ( Base ` K ) /\ ( ( Q ./\ ( T .\/ U ) ) .\/ U ) e. ( Base ` K ) /\ S e. ( Base ` K ) ) ) -> ( ( ( ( P .\/ Q ) .\/ S ) ./\ T ) .<_ ( ( Q ./\ ( T .\/ U ) ) .\/ U ) -> ( ( ( ( P .\/ Q ) .\/ S ) ./\ T ) .\/ S ) .<_ ( ( ( Q ./\ ( T .\/ U ) ) .\/ U ) .\/ S ) ) )
118	7 25 116 19 117	syl13anc	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( ( ( P .\/ Q ) .\/ S ) ./\ T ) .<_ ( ( Q ./\ ( T .\/ U ) ) .\/ U ) -> ( ( ( ( P .\/ Q ) .\/ S ) ./\ T ) .\/ S ) .<_ ( ( ( Q ./\ ( T .\/ U ) ) .\/ U ) .\/ S ) ) )
119	114 118	mpd	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( ( ( P .\/ Q ) .\/ S ) ./\ T ) .\/ S ) .<_ ( ( ( Q ./\ ( T .\/ U ) ) .\/ U ) .\/ S ) )
120	5 2	latjass	|- ( ( K e. Lat /\ ( ( Q ./\ ( T .\/ U ) ) e. ( Base ` K ) /\ U e. ( Base ` K ) /\ S e. ( Base ` K ) ) ) -> ( ( ( Q ./\ ( T .\/ U ) ) .\/ U ) .\/ S ) = ( ( Q ./\ ( T .\/ U ) ) .\/ ( U .\/ S ) ) )
121	7 34 110 19 120	syl13anc	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( ( Q ./\ ( T .\/ U ) ) .\/ U ) .\/ S ) = ( ( Q ./\ ( T .\/ U ) ) .\/ ( U .\/ S ) ) )
122	119 121	breqtrd	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( ( ( P .\/ Q ) .\/ S ) ./\ T ) .\/ S ) .<_ ( ( Q ./\ ( T .\/ U ) ) .\/ ( U .\/ S ) ) )
123	5 1 7 17 27 38 53 122	lattrd	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( P .\/ Q ) ./\ ( S .\/ T ) ) .<_ ( ( Q ./\ ( T .\/ U ) ) .\/ ( U .\/ S ) ) )
124	5 1 3	latmle1	|- ( ( K e. Lat /\ ( P .\/ Q ) e. ( Base ` K ) /\ ( S .\/ T ) e. ( Base ` K ) ) -> ( ( P .\/ Q ) ./\ ( S .\/ T ) ) .<_ ( P .\/ Q ) )
125	7 11 15 124	syl3anc	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( P .\/ Q ) ./\ ( S .\/ T ) ) .<_ ( P .\/ Q ) )
126	5 1 3	latlem12	|- ( ( K e. Lat /\ ( ( ( P .\/ Q ) ./\ ( S .\/ T ) ) e. ( Base ` K ) /\ ( ( Q ./\ ( T .\/ U ) ) .\/ ( U .\/ S ) ) e. ( Base ` K ) /\ ( P .\/ Q ) e. ( Base ` K ) ) ) -> ( ( ( ( P .\/ Q ) ./\ ( S .\/ T ) ) .<_ ( ( Q ./\ ( T .\/ U ) ) .\/ ( U .\/ S ) ) /\ ( ( P .\/ Q ) ./\ ( S .\/ T ) ) .<_ ( P .\/ Q ) ) <-> ( ( P .\/ Q ) ./\ ( S .\/ T ) ) .<_ ( ( ( Q ./\ ( T .\/ U ) ) .\/ ( U .\/ S ) ) ./\ ( P .\/ Q ) ) ) )
127	7 17 38 11 126	syl13anc	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( ( ( P .\/ Q ) ./\ ( S .\/ T ) ) .<_ ( ( Q ./\ ( T .\/ U ) ) .\/ ( U .\/ S ) ) /\ ( ( P .\/ Q ) ./\ ( S .\/ T ) ) .<_ ( P .\/ Q ) ) <-> ( ( P .\/ Q ) ./\ ( S .\/ T ) ) .<_ ( ( ( Q ./\ ( T .\/ U ) ) .\/ ( U .\/ S ) ) ./\ ( P .\/ Q ) ) ) )
128	123 125 127	mpbi2and	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( P .\/ Q ) ./\ ( S .\/ T ) ) .<_ ( ( ( Q ./\ ( T .\/ U ) ) .\/ ( U .\/ S ) ) ./\ ( P .\/ Q ) ) )
129	5 4	atbase	|- ( P e. A -> P e. ( Base ` K ) )
130	8 129	syl	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> P e. ( Base ` K ) )
131	5 1 2 3	latmlej12	|- ( ( K e. Lat /\ ( Q e. ( Base ` K ) /\ ( T .\/ U ) e. ( Base ` K ) /\ P e. ( Base ` K ) ) ) -> ( Q ./\ ( T .\/ U ) ) .<_ ( P .\/ Q ) )
132	7 29 32 130 131	syl13anc	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( Q ./\ ( T .\/ U ) ) .<_ ( P .\/ Q ) )
133	5 1 2 3 4	llnmod1i2	|- ( ( ( K e. HL /\ ( Q ./\ ( T .\/ U ) ) e. ( Base ` K ) /\ ( P .\/ Q ) e. ( Base ` K ) ) /\ ( U e. A /\ S e. A ) /\ ( Q ./\ ( T .\/ U ) ) .<_ ( P .\/ Q ) ) -> ( ( Q ./\ ( T .\/ U ) ) .\/ ( ( U .\/ S ) ./\ ( P .\/ Q ) ) ) = ( ( ( Q ./\ ( T .\/ U ) ) .\/ ( U .\/ S ) ) ./\ ( P .\/ Q ) ) )
134	6 34 11 30 12 132 133	syl321anc	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( Q ./\ ( T .\/ U ) ) .\/ ( ( U .\/ S ) ./\ ( P .\/ Q ) ) ) = ( ( ( Q ./\ ( T .\/ U ) ) .\/ ( U .\/ S ) ) ./\ ( P .\/ Q ) ) )
135	2 4	hlatjidm	|- ( ( K e. HL /\ Q e. A ) -> ( Q .\/ Q ) = Q )
136	6 9 135	syl2anc	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( Q .\/ Q ) = Q )
137	83	oveq2d	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( Q .\/ Q ) = ( Q .\/ R ) )
138	136 137	eqtr3d	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> Q = ( Q .\/ R ) )
139	138	oveq1d	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( Q ./\ ( T .\/ U ) ) = ( ( Q .\/ R ) ./\ ( T .\/ U ) ) )
140	5 3	latmcom	|- ( ( K e. Lat /\ ( U .\/ S ) e. ( Base ` K ) /\ ( P .\/ Q ) e. ( Base ` K ) ) -> ( ( U .\/ S ) ./\ ( P .\/ Q ) ) = ( ( P .\/ Q ) ./\ ( U .\/ S ) ) )
141	7 36 11 140	syl3anc	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( U .\/ S ) ./\ ( P .\/ Q ) ) = ( ( P .\/ Q ) ./\ ( U .\/ S ) ) )
142	2 4	hlatjcom	|- ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( P .\/ Q ) = ( Q .\/ P ) )
143	6 8 9 142	syl3anc	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( P .\/ Q ) = ( Q .\/ P ) )
144	83	oveq1d	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( Q .\/ P ) = ( R .\/ P ) )
145	143 144	eqtrd	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( P .\/ Q ) = ( R .\/ P ) )
146	145	oveq1d	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( P .\/ Q ) ./\ ( U .\/ S ) ) = ( ( R .\/ P ) ./\ ( U .\/ S ) ) )
147	141 146	eqtrd	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( U .\/ S ) ./\ ( P .\/ Q ) ) = ( ( R .\/ P ) ./\ ( U .\/ S ) ) )
148	139 147	oveq12d	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( Q ./\ ( T .\/ U ) ) .\/ ( ( U .\/ S ) ./\ ( P .\/ Q ) ) ) = ( ( ( Q .\/ R ) ./\ ( T .\/ U ) ) .\/ ( ( R .\/ P ) ./\ ( U .\/ S ) ) ) )
149	134 148	eqtr3d	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( ( Q ./\ ( T .\/ U ) ) .\/ ( U .\/ S ) ) ./\ ( P .\/ Q ) ) = ( ( ( Q .\/ R ) ./\ ( T .\/ U ) ) .\/ ( ( R .\/ P ) ./\ ( U .\/ S ) ) ) )
150	128 149	breqtrd	|- ( ( ( K e. HL /\ Q = R /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( P .\/ Q ) ./\ ( S .\/ T ) ) .<_ ( ( ( Q .\/ R ) ./\ ( T .\/ U ) ) .\/ ( ( R .\/ P ) ./\ ( U .\/ S ) ) ) )