dalawlem11

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

Metamath Proof Explorer

Theorem dalawlem11

Proof