Theorem ps2 17079

Description: Lattice analog for the projective geometry axiom, "if a line intersects two sides of a triangle at different points then it also intersects the third side." Projective space condition PS2 in [MaedaMaeda] p. 68 and part of Theorem 16.4 in [MaedaMaeda] p. 69.

Hypotheses

Ref	Expression
ps2.l	|- L = (le` K)
ps2.j	|- J = (join` K)
ps2.a	|- A = (AtomsNEW` K)

Assertion

Ref	Expression
ps2	|- ((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) -> (((-. PL(QJR) /\ S =/= T) /\ (SL(PJQ) /\ TL(QJR))) -> E.u e. A (uL(PJR) /\ uL(SJT))))

Distinct variable groups:   u,A   u,J   u,K   u,L   u,P   u,Q   u,R   u,S   u,T

Proof of Theorem ps2

Step	Hyp	Ref	Expression
1		simpl21 954	. . . 4 |- (((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) /\ S = P) -> P e. A)
2		hllat 17026	. . . . . . 7 |- (K e. HL -> K e. LatNEW)
3	2	3ad2ant1 897	. . . . . 6 |- ((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) -> K e. LatNEW)
4		simp21 909	. . . . . . 7 |- ((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) -> P e. A)
5		eqid 1884	. . . . . . . 8 |- (base` K) = (base` K)
6		ps2.a	. . . . . . . 8 |- A = (AtomsNEW` K)
7	5, 6	atombase 17003	. . . . . . 7 |- (P e. A -> P e. (base` K))
8	4, 7	syl 12	. . . . . 6 |- ((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) -> P e. (base` K))
9		simp23 911	. . . . . . 7 |- ((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) -> R e. A)
10	5, 6	atombase 17003	. . . . . . 7 |- (R e. A -> R e. (base` K))
11	9, 10	syl 12	. . . . . 6 |- ((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) -> R e. (base` K))
12		ps2.l	. . . . . . 7 |- L = (le` K)
13		ps2.j	. . . . . . 7 |- J = (join` K)
14	5, 12, 13	latlej1 16861	. . . . . 6 |- ((K e. LatNEW /\ P e. (base` K) /\ R e. (base` K)) -> PL(PJR))
15	3, 8, 11, 14	syl111anc 1100	. . . . 5 |- ((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) -> PL(PJR))
16	15	adantr 425	. . . 4 |- (((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) /\ S = P) -> PL(PJR))
17		opreq1 4889	. . . . . . 7 |- (S = P -> (SJT) = (PJT))
18	17	breq2d 3350	. . . . . 6 |- (S = P -> (PL(SJT) <-> PL(PJT)))
19		simp3r 905	. . . . . . . 8 |- ((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) -> T e. A)
20	5, 6	atombase 17003	. . . . . . . 8 |- (T e. A -> T e. (base` K))
21	19, 20	syl 12	. . . . . . 7 |- ((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) -> T e. (base` K))
22	5, 12, 13	latlej1 16861	. . . . . . 7 |- ((K e. LatNEW /\ P e. (base` K) /\ T e. (base` K)) -> PL(PJT))
23	3, 8, 21, 22	syl111anc 1100	. . . . . 6 |- ((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) -> PL(PJT))
24	18, 23	syl5cbir 228	. . . . 5 |- ((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) -> (S = P -> PL(SJT)))
25	24	imp 377	. . . 4 |- (((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) /\ S = P) -> PL(SJT))
26		breq1 3341	. . . . . 6 |- (u = P -> (uL(PJR) <-> PL(PJR)))
27		breq1 3341	. . . . . 6 |- (u = P -> (uL(SJT) <-> PL(SJT)))
28	26, 27	anbi12d 690	. . . . 5 |- (u = P -> ((uL(PJR) /\ uL(SJT)) <-> (PL(PJR) /\ PL(SJT))))
29	28	rcla4ev 2381	. . . 4 |- ((P e. A /\ (PL(PJR) /\ PL(SJT))) -> E.u e. A (uL(PJR) /\ uL(SJT)))
30	1, 16, 25, 29	syl12anc 1098	. . 3 |- (((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) /\ S = P) -> E.u e. A (uL(PJR) /\ uL(SJT)))
31	30	a1d 15	. 2 |- (((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) /\ S = P) -> (((-. PL(QJR) /\ S =/= T) /\ (SL(PJQ) /\ TL(QJR))) -> E.u e. A (uL(PJR) /\ uL(SJT))))
32		simp1 876	. . . . . . . . . . . . . . . 16 |- ((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) -> K e. HL)
33		hlop 17025	. . . . . . . . . . . . . . . . . 18 |- (K e. HL -> K e. OP)
34	33	3ad2ant1 897	. . . . . . . . . . . . . . . . 17 |- ((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) -> K e. OP)
35		eqid 1884	. . . . . . . . . . . . . . . . . 18 |- (0.` K) = (0.` K)
36	5, 35	op0cl 16914	. . . . . . . . . . . . . . . . 17 |- (K e. OP -> (0.` K) e. (base` K))
37	34, 36	syl 12	. . . . . . . . . . . . . . . 16 |- ((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) -> (0.` K) e. (base` K))
38		eqid 1884	. . . . . . . . . . . . . . . . . 18 |- ( <oNEW ` K) = ( <oNEW ` K)
39	5, 35, 38, 6	atomcvr0 17002	. . . . . . . . . . . . . . . . 17 |- ((K e. HL /\ P e. A) -> (0.` K)( <oNEW ` K)P)
40	32, 4, 39	syl11anc 524	. . . . . . . . . . . . . . . 16 |- ((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) -> (0.` K)( <oNEW ` K)P)
41		eqid 1884	. . . . . . . . . . . . . . . . 17 |- (lt` K) = (lt` K)
42	5, 41, 38	cvrlt 16989	. . . . . . . . . . . . . . . 16 |- (((K e. HL /\ (0.` K) e. (base` K) /\ P e. (base` K)) /\ (0.` K)( <oNEW ` K)P) -> (0.` K)(lt` K)P)
43	32, 37, 8, 40, 42	syl31anc 1103	. . . . . . . . . . . . . . 15 |- ((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) -> (0.` K)(lt` K)P)
44		hlpos 17027	. . . . . . . . . . . . . . . . 17 |- (K e. HL -> K e. PosetNEW)
45	44	3ad2ant1 897	. . . . . . . . . . . . . . . 16 |- ((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) -> K e. PosetNEW)
46	5, 13	latjcl 16852	. . . . . . . . . . . . . . . . 17 |- ((K e. LatNEW /\ P e. (base` K) /\ R e. (base` K)) -> (PJR) e. (base` K))
47	3, 8, 11, 46	syl111anc 1100	. . . . . . . . . . . . . . . 16 |- ((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) -> (PJR) e. (base` K))
48	5, 12, 41	pltletr 16791	. . . . . . . . . . . . . . . 16 |- ((K e. PosetNEW /\ ((0.` K) e. (base` K) /\ P e. (base` K) /\ (PJR) e. (base` K))) -> (((0.` K)(lt` K)P /\ PL(PJR)) -> (0.` K)(lt` K)(PJR)))
49	45, 37, 8, 47, 48	syl13anc 1102	. . . . . . . . . . . . . . 15 |- ((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) -> (((0.` K)(lt` K)P /\ PL(PJR)) -> (0.` K)(lt` K)(PJR)))
50	43, 15, 49	mp2and 767	. . . . . . . . . . . . . 14 |- ((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) -> (0.` K)(lt` K)(PJR))
51	41	pltne 16783	. . . . . . . . . . . . . . 15 |- ((K e. HL /\ (0.` K) e. (base` K) /\ (PJR) e. (base` K)) -> ((0.` K)(lt` K)(PJR) -> (0.` K) =/= (PJR)))
52	32, 37, 47, 51	syl111anc 1100	. . . . . . . . . . . . . 14 |- ((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) -> ((0.` K)(lt` K)(PJR) -> (0.` K) =/= (PJR)))
53	50, 52	mpd 29	. . . . . . . . . . . . 13 |- ((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) -> (0.` K) =/= (PJR))
54	53	necomd 2095	. . . . . . . . . . . 12 |- ((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) -> (PJR) =/= (0.` K))
55	54	adantr 425	. . . . . . . . . . 11 |- (((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) /\ (S =/= P /\ (SL(PJQ) /\ TL(QJR)))) -> (PJR) =/= (0.` K))
56		simp3l 904	. . . . . . . . . . . . . . . . . . 19 |- ((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) -> S e. A)
57	12, 6	atomcmp 17008	. . . . . . . . . . . . . . . . . . 19 |- ((K e. OP /\ S e. A /\ P e. A) -> (SLP <-> S = P))
58	34, 56, 4, 57	syl111anc 1100	. . . . . . . . . . . . . . . . . 18 |- ((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) -> (SLP <-> S = P))
59	58	necon3bbid 2034	. . . . . . . . . . . . . . . . 17 |- ((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) -> (-. SLP <-> S =/= P))
60		simp22 910	. . . . . . . . . . . . . . . . . 18 |- ((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) -> Q e. A)
61	5, 12, 13, 6	hlexch 17034	. . . . . . . . . . . . . . . . . . 19 |- ((K e. HL /\ (S e. A /\ Q e. A /\ P e. (base` K)) /\ -. SLP) -> (SL(PJQ) -> QL(PJS)))
62	61	3expia 1069	. . . . . . . . . . . . . . . . . 18 |- ((K e. HL /\ (S e. A /\ Q e. A /\ P e. (base` K))) -> (-. SLP -> (SL(PJQ) -> QL(PJS))))
63	32, 56, 60, 8, 62	syl13anc 1102	. . . . . . . . . . . . . . . . 17 |- ((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) -> (-. SLP -> (SL(PJQ) -> QL(PJS))))
64	59, 63	sylbird 222	. . . . . . . . . . . . . . . 16 |- ((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) -> (S =/= P -> (SL(PJQ) -> QL(PJS))))
65	64	imp32 390	. . . . . . . . . . . . . . 15 |- (((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) /\ (S =/= P /\ SL(PJQ))) -> QL(PJS))
66	5, 6	atombase 17003	. . . . . . . . . . . . . . . . . 18 |- (Q e. A -> Q e. (base` K))
67	60, 66	syl 12	. . . . . . . . . . . . . . . . 17 |- ((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) -> Q e. (base` K))
68	5, 6	atombase 17003	. . . . . . . . . . . . . . . . . . 19 |- (S e. A -> S e. (base` K))
69	56, 68	syl 12	. . . . . . . . . . . . . . . . . 18 |- ((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) -> S e. (base` K))
70	5, 13	latjcl 16852	. . . . . . . . . . . . . . . . . 18 |- ((K e. LatNEW /\ P e. (base` K) /\ S e. (base` K)) -> (PJS) e. (base` K))
71	3, 8, 69, 70	syl111anc 1100	. . . . . . . . . . . . . . . . 17 |- ((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) -> (PJS) e. (base` K))
72	5, 12, 13	latjlej1 16866	. . . . . . . . . . . . . . . . 17 |- ((K e. LatNEW /\ (Q e. (base` K) /\ (PJS) e. (base` K) /\ R e. (base` K))) -> (QL(PJS) -> (QJR)L((PJS)JR)))
73	3, 67, 71, 11, 72	syl13anc 1102	. . . . . . . . . . . . . . . 16 |- ((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) -> (QL(PJS) -> (QJR)L((PJS)JR)))
74	73	adantr 425	. . . . . . . . . . . . . . 15 |- (((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) /\ (S =/= P /\ SL(PJQ))) -> (QL(PJS) -> (QJR)L((PJS)JR)))
75	65, 74	mpd 29	. . . . . . . . . . . . . 14 |- (((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) /\ (S =/= P /\ SL(PJQ))) -> (QJR)L((PJS)JR))
76	75	adantrrr 439	. . . . . . . . . . . . 13 |- (((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) /\ (S =/= P /\ (SL(PJQ) /\ TL(QJR)))) -> (QJR)L((PJS)JR))
77	5, 13	latjcl 16852	. . . . . . . . . . . . . . . . . 18 |- ((K e. LatNEW /\ Q e. (base` K) /\ R e. (base` K)) -> (QJR) e. (base` K))
78	3, 67, 11, 77	syl111anc 1100	. . . . . . . . . . . . . . . . 17 |- ((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) -> (QJR) e. (base` K))
79	5, 13	latjcl 16852	. . . . . . . . . . . . . . . . . 18 |- ((K e. LatNEW /\ (PJS) e. (base` K) /\ R e. (base` K)) -> ((PJS)JR) e. (base` K))
80	3, 71, 11, 79	syl111anc 1100	. . . . . . . . . . . . . . . . 17 |- ((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) -> ((PJS)JR) e. (base` K))
81	5, 12	lattr 16858	. . . . . . . . . . . . . . . . 17 |- ((K e. LatNEW /\ (T e. (base` K) /\ (QJR) e. (base` K) /\ ((PJS)JR) e. (base` K))) -> ((TL(QJR) /\ (QJR)L((PJS)JR)) -> TL((PJS)JR)))
82	3, 21, 78, 80, 81	syl13anc 1102	. . . . . . . . . . . . . . . 16 |- ((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) -> ((TL(QJR) /\ (QJR)L((PJS)JR)) -> TL((PJS)JR)))
83	82	expdimp 406	. . . . . . . . . . . . . . 15 |- (((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) /\ TL(QJR)) -> ((QJR)L((PJS)JR) -> TL((PJS)JR)))
84	83	adantrl 430	. . . . . . . . . . . . . 14 |- (((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) /\ (SL(PJQ) /\ TL(QJR))) -> ((QJR)L((PJS)JR) -> TL((PJS)JR)))
85	84	adantrl 430	. . . . . . . . . . . . 13 |- (((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) /\ (S =/= P /\ (SL(PJQ) /\ TL(QJR)))) -> ((QJR)L((PJS)JR) -> TL((PJS)JR)))
86	76, 85	mpd 29	. . . . . . . . . . . 12 |- (((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) /\ (S =/= P /\ (SL(PJQ) /\ TL(QJR)))) -> TL((PJS)JR))
87	5, 13	latj23 16887	. . . . . . . . . . . . . . 15 |- ((K e. LatNEW /\ (P e. (base` K) /\ S e. (base` K) /\ R e. (base` K))) -> ((PJS)JR) = ((PJR)JS))
88	3, 8, 69, 11, 87	syl13anc 1102	. . . . . . . . . . . . . 14 |- ((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) -> ((PJS)JR) = ((PJR)JS))
89	88	breq2d 3350	. . . . . . . . . . . . 13 |- ((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) -> (TL((PJS)JR) <-> TL((PJR)JS)))
90	89	adantr 425	. . . . . . . . . . . 12 |- (((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) /\ (S =/= P /\ (SL(PJQ) /\ TL(QJR)))) -> (TL((PJS)JR) <-> TL((PJR)JS)))
91	86, 90	mpbid 212	. . . . . . . . . . 11 |- (((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) /\ (S =/= P /\ (SL(PJQ) /\ TL(QJR)))) -> TL((PJR)JS))
92	55, 91	jca 310	. . . . . . . . . 10 |- (((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) /\ (S =/= P /\ (SL(PJQ) /\ TL(QJR)))) -> ((PJR) =/= (0.` K) /\ TL((PJR)JS)))
93	92	adantrrl 438	. . . . . . . . 9 |- (((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) /\ (S =/= P /\ (-. PL(QJR) /\ (SL(PJQ) /\ TL(QJR))))) -> ((PJR) =/= (0.` K) /\ TL((PJR)JS)))
94	93	ex 402	. . . . . . . 8 |- ((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) -> ((S =/= P /\ (-. PL(QJR) /\ (SL(PJQ) /\ TL(QJR)))) -> ((PJR) =/= (0.` K) /\ TL((PJR)JS))))
95	5, 12, 13, 35, 6	cvrat4 17076	. . . . . . . . 9 |- ((K e. HL /\ ((PJR) e. (base` K) /\ T e. A /\ S e. A)) -> (((PJR) =/= (0.` K) /\ TL((PJR)JS)) -> E.u e. A (uL(PJR) /\ TL(SJu))))
96	32, 47, 19, 56, 95	syl13anc 1102	. . . . . . . 8 |- ((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) -> (((PJR) =/= (0.` K) /\ TL((PJR)JS)) -> E.u e. A (uL(PJR) /\ TL(SJu))))
97	94, 96	syld 30	. . . . . . 7 |- ((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) -> ((S =/= P /\ (-. PL(QJR) /\ (SL(PJQ) /\ TL(QJR)))) -> E.u e. A (uL(PJR) /\ TL(SJu))))
98	97	imp 377	. . . . . 6 |- (((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) /\ (S =/= P /\ (-. PL(QJR) /\ (SL(PJQ) /\ TL(QJR))))) -> E.u e. A (uL(PJR) /\ TL(SJu)))
99	98	anassrs 489	. . . . 5 |- ((((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) /\ S =/= P) /\ (-. PL(QJR) /\ (SL(PJQ) /\ TL(QJR)))) -> E.u e. A (uL(PJR) /\ TL(SJu)))
100	99	adantrlr 437	. . . 4 |- ((((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) /\ S =/= P) /\ ((-. PL(QJR) /\ S =/= T) /\ (SL(PJQ) /\ TL(QJR)))) -> E.u e. A (uL(PJR) /\ TL(SJu)))
101	12, 6	atomcmp 17008	. . . . . . . . . . . . . . 15 |- ((K e. OP /\ T e. A /\ S e. A) -> (TLS <-> T = S))
102	34, 19, 56, 101	syl111anc 1100	. . . . . . . . . . . . . 14 |- ((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) -> (TLS <-> T = S))
103		eqcom 1886	. . . . . . . . . . . . . 14 |- (T = S <-> S = T)
104	102, 103	syl6bb 595	. . . . . . . . . . . . 13 |- ((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) -> (TLS <-> S = T))
105	104	necon3bbid 2034	. . . . . . . . . . . 12 |- ((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) -> (-. TLS <-> S =/= T))
106	105	adantr 425	. . . . . . . . . . 11 |- (((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) /\ u e. A) -> (-. TLS <-> S =/= T))
107		simpl1 879	. . . . . . . . . . . 12 |- (((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) /\ u e. A) -> K e. HL)
108		simpl3r 932	. . . . . . . . . . . 12 |- (((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) /\ u e. A) -> T e. A)
109		simpr 350	. . . . . . . . . . . 12 |- (((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) /\ u e. A) -> u e. A)
110	69	adantr 425	. . . . . . . . . . . 12 |- (((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) /\ u e. A) -> S e. (base` K))
111	5, 12, 13, 6	hlexch 17034	. . . . . . . . . . . . 13 |- ((K e. HL /\ (T e. A /\ u e. A /\ S e. (base` K)) /\ -. TLS) -> (TL(SJu) -> uL(SJT)))
112	111	3expia 1069	. . . . . . . . . . . 12 |- ((K e. HL /\ (T e. A /\ u e. A /\ S e. (base` K))) -> (-. TLS -> (TL(SJu) -> uL(SJT))))
113	107, 108, 109, 110, 112	syl13anc 1102	. . . . . . . . . . 11 |- (((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) /\ u e. A) -> (-. TLS -> (TL(SJu) -> uL(SJT))))
114	106, 113	sylbird 222	. . . . . . . . . 10 |- (((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) /\ u e. A) -> (S =/= T -> (TL(SJu) -> uL(SJT))))
115	114	imp 377	. . . . . . . . 9 |- ((((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) /\ u e. A) /\ S =/= T) -> (TL(SJu) -> uL(SJT)))
116	115	an1rs 547	. . . . . . . 8 |- ((((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) /\ S =/= T) /\ u e. A) -> (TL(SJu) -> uL(SJT)))
117	116	anim2d 620	. . . . . . 7 |- ((((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) /\ S =/= T) /\ u e. A) -> ((uL(PJR) /\ TL(SJu)) -> (uL(PJR) /\ uL(SJT))))
118	117	reximdva 2203	. . . . . 6 |- (((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) /\ S =/= T) -> (E.u e. A (uL(PJR) /\ TL(SJu)) -> E.u e. A (uL(PJR) /\ uL(SJT))))
119	118	ad2ant2rl 447	. . . . 5 |- ((((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) /\ S =/= P) /\ (-. PL(QJR) /\ S =/= T)) -> (E.u e. A (uL(PJR) /\ TL(SJu)) -> E.u e. A (uL(PJR) /\ uL(SJT))))
120	119	adantrr 431	. . . 4 |- ((((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) /\ S =/= P) /\ ((-. PL(QJR) /\ S =/= T) /\ (SL(PJQ) /\ TL(QJR)))) -> (E.u e. A (uL(PJR) /\ TL(SJu)) -> E.u e. A (uL(PJR) /\ uL(SJT))))
121	100, 120	mpd 29	. . 3 |- ((((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) /\ S =/= P) /\ ((-. PL(QJR) /\ S =/= T) /\ (SL(PJQ) /\ TL(QJR)))) -> E.u e. A (uL(PJR) /\ uL(SJT)))
122	121	ex 402	. 2 |- (((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) /\ S =/= P) -> (((-. PL(QJR) /\ S =/= T) /\ (SL(PJQ) /\ TL(QJR))) -> E.u e. A (uL(PJR) /\ uL(SJT))))
123	31, 122	pm2.61dane 2093	1 |- ((K e. HL /\ (P e. A /\ Q e. A /\ R e. A) /\ (S e. A /\ T e. A)) -> (((-. PL(QJR) /\ S =/= T) /\ (SL(PJQ) /\ TL(QJR))) -> E.u e. A (uL(PJR) /\ uL(SJT))))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300   =/= wne 2017  E.wrex 2106   class class class wbr 3338  ` cfv 3998  (class class class)co 4884  basecbs 16758  lecple 16759  PosetNEWcpo 16760  ltcplt 16761  joincjn 16766  0.cp0 16832  LatNEWclat 16834  OPcops 16837   <o_NEW ccvr 16980  AtomsNEWcatm 16981  HLchlt 16983

This theorem is referenced by:  paddasslem3 17283

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-tru 1262  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-id 3586  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-opr 4886  df-oprab 4887  df-mpt 5006  df-mpt2 5007  df-iota 5089  df-er 5318  df-en 5427  df-dom 5428  df-sdom 5429  df-undef 5556  df-riota 5560  df-struct 16708  df-poset 16772  df-plt 16780  df-pge 16792  df-lub 16799  df-glb 16800  df-join 16801  df-meet 16802  df-p0 16841  df-lat 16847  df-clat 16848  df-oposet 16905  df-ol 16907  df-oml 16908  df-covers 16984  df-atoms 16985  df-atlat 16986  df-hlat 17017

Copyright terms: Public domain