Theorem 2at0mat0

Description: Special case of 2atmat0 where one atom could be zero. (Contributed by NM, 30-May-2013)

	Ref	Expression
Hypotheses	2atmatz.j	|- .\/ = ( join ` K )
	2atmatz.m	|- ./\ = ( meet ` K )
	2atmatz.z	|- .0. = ( 0. ` K )
	2atmatz.a	|- A = ( Atoms ` K )
Assertion	2at0mat0	|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ ( S e. A \/ S = .0. ) /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) -> ( ( ( P .\/ Q ) ./\ ( R .\/ S ) ) e. A \/ ( ( P .\/ Q ) ./\ ( R .\/ S ) ) = .0. ) )

Proof

Step	Hyp	Ref	Expression
1		2atmatz.j	|- .\/ = ( join ` K )
2		2atmatz.m	|- ./\ = ( meet ` K )
3		2atmatz.z	|- .0. = ( 0. ` K )
4		2atmatz.a	|- A = ( Atoms ` K )
5		simpll	|- ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ ( S e. A \/ S = .0. ) /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) /\ S e. A ) -> ( K e. HL /\ P e. A /\ Q e. A ) )
6		simplr1	|- ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ ( S e. A \/ S = .0. ) /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) /\ S e. A ) -> R e. A )
7		simpr	|- ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ ( S e. A \/ S = .0. ) /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) /\ S e. A ) -> S e. A )
8		simplr3	|- ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ ( S e. A \/ S = .0. ) /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) /\ S e. A ) -> ( P .\/ Q ) =/= ( R .\/ S ) )
9		simpl1	|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) -> K e. HL )
10		hlol	|- ( K e. HL -> K e. OL )
11	9 10	syl	|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) -> K e. OL )
12		simpr1	|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) -> R e. A )
13		simpr2	|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) -> S e. A )
14		eqid	|- ( Base ` K ) = ( Base ` K )
15	14 1 4	hlatjcl	|- ( ( K e. HL /\ R e. A /\ S e. A ) -> ( R .\/ S ) e. ( Base ` K ) )
16	9 12 13 15	syl3anc	|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) -> ( R .\/ S ) e. ( Base ` K ) )
17		simpl3	|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) -> Q e. A )
18	14 2 3 4	meetat2	|- ( ( K e. OL /\ ( R .\/ S ) e. ( Base ` K ) /\ Q e. A ) -> ( ( ( R .\/ S ) ./\ Q ) e. A \/ ( ( R .\/ S ) ./\ Q ) = .0. ) )
19	11 16 17 18	syl3anc	|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) -> ( ( ( R .\/ S ) ./\ Q ) e. A \/ ( ( R .\/ S ) ./\ Q ) = .0. ) )
20	19	adantr	|- ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) /\ P = Q ) -> ( ( ( R .\/ S ) ./\ Q ) e. A \/ ( ( R .\/ S ) ./\ Q ) = .0. ) )
21		oveq1	|- ( P = Q -> ( P .\/ Q ) = ( Q .\/ Q ) )
22	1 4	hlatjidm	|- ( ( K e. HL /\ Q e. A ) -> ( Q .\/ Q ) = Q )
23	9 17 22	syl2anc	|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) -> ( Q .\/ Q ) = Q )
24	21 23	sylan9eqr	|- ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) /\ P = Q ) -> ( P .\/ Q ) = Q )
25	24	oveq1d	|- ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) /\ P = Q ) -> ( ( P .\/ Q ) ./\ ( R .\/ S ) ) = ( Q ./\ ( R .\/ S ) ) )
26	9	hllatd	|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) -> K e. Lat )
27	14 4	atbase	|- ( Q e. A -> Q e. ( Base ` K ) )
28	17 27	syl	|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) -> Q e. ( Base ` K ) )
29	14 2	latmcom	|- ( ( K e. Lat /\ Q e. ( Base ` K ) /\ ( R .\/ S ) e. ( Base ` K ) ) -> ( Q ./\ ( R .\/ S ) ) = ( ( R .\/ S ) ./\ Q ) )
30	26 28 16 29	syl3anc	|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) -> ( Q ./\ ( R .\/ S ) ) = ( ( R .\/ S ) ./\ Q ) )
31	30	adantr	|- ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) /\ P = Q ) -> ( Q ./\ ( R .\/ S ) ) = ( ( R .\/ S ) ./\ Q ) )
32	25 31	eqtrd	|- ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) /\ P = Q ) -> ( ( P .\/ Q ) ./\ ( R .\/ S ) ) = ( ( R .\/ S ) ./\ Q ) )
33	32	eleq1d	|- ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) /\ P = Q ) -> ( ( ( P .\/ Q ) ./\ ( R .\/ S ) ) e. A <-> ( ( R .\/ S ) ./\ Q ) e. A ) )
34	32	eqeq1d	|- ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) /\ P = Q ) -> ( ( ( P .\/ Q ) ./\ ( R .\/ S ) ) = .0. <-> ( ( R .\/ S ) ./\ Q ) = .0. ) )
35	33 34	orbi12d	|- ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) /\ P = Q ) -> ( ( ( ( P .\/ Q ) ./\ ( R .\/ S ) ) e. A \/ ( ( P .\/ Q ) ./\ ( R .\/ S ) ) = .0. ) <-> ( ( ( R .\/ S ) ./\ Q ) e. A \/ ( ( R .\/ S ) ./\ Q ) = .0. ) ) )
36	20 35	mpbird	|- ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) /\ P = Q ) -> ( ( ( P .\/ Q ) ./\ ( R .\/ S ) ) e. A \/ ( ( P .\/ Q ) ./\ ( R .\/ S ) ) = .0. ) )
37	14 1 4	hlatjcl	|- ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( P .\/ Q ) e. ( Base ` K ) )
38	37	adantr	|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) -> ( P .\/ Q ) e. ( Base ` K ) )
39	14 2 3 4	meetat2	|- ( ( K e. OL /\ ( P .\/ Q ) e. ( Base ` K ) /\ S e. A ) -> ( ( ( P .\/ Q ) ./\ S ) e. A \/ ( ( P .\/ Q ) ./\ S ) = .0. ) )
40	11 38 13 39	syl3anc	|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) -> ( ( ( P .\/ Q ) ./\ S ) e. A \/ ( ( P .\/ Q ) ./\ S ) = .0. ) )
41	40	adantr	|- ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) /\ R = S ) -> ( ( ( P .\/ Q ) ./\ S ) e. A \/ ( ( P .\/ Q ) ./\ S ) = .0. ) )
42		oveq1	|- ( R = S -> ( R .\/ S ) = ( S .\/ S ) )
43	1 4	hlatjidm	|- ( ( K e. HL /\ S e. A ) -> ( S .\/ S ) = S )
44	9 13 43	syl2anc	|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) -> ( S .\/ S ) = S )
45	42 44	sylan9eqr	|- ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) /\ R = S ) -> ( R .\/ S ) = S )
46	45	oveq2d	|- ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) /\ R = S ) -> ( ( P .\/ Q ) ./\ ( R .\/ S ) ) = ( ( P .\/ Q ) ./\ S ) )
47	46	eleq1d	|- ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) /\ R = S ) -> ( ( ( P .\/ Q ) ./\ ( R .\/ S ) ) e. A <-> ( ( P .\/ Q ) ./\ S ) e. A ) )
48	46	eqeq1d	|- ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) /\ R = S ) -> ( ( ( P .\/ Q ) ./\ ( R .\/ S ) ) = .0. <-> ( ( P .\/ Q ) ./\ S ) = .0. ) )
49	47 48	orbi12d	|- ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) /\ R = S ) -> ( ( ( ( P .\/ Q ) ./\ ( R .\/ S ) ) e. A \/ ( ( P .\/ Q ) ./\ ( R .\/ S ) ) = .0. ) <-> ( ( ( P .\/ Q ) ./\ S ) e. A \/ ( ( P .\/ Q ) ./\ S ) = .0. ) ) )
50	41 49	mpbird	|- ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) /\ R = S ) -> ( ( ( P .\/ Q ) ./\ ( R .\/ S ) ) e. A \/ ( ( P .\/ Q ) ./\ ( R .\/ S ) ) = .0. ) )
51	50	adantlr	|- ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) /\ P =/= Q ) /\ R = S ) -> ( ( ( P .\/ Q ) ./\ ( R .\/ S ) ) e. A \/ ( ( P .\/ Q ) ./\ ( R .\/ S ) ) = .0. ) )
52		df-ne	|- ( ( ( P .\/ Q ) ./\ ( R .\/ S ) ) =/= .0. <-> -. ( ( P .\/ Q ) ./\ ( R .\/ S ) ) = .0. )
53		simpll1	|- ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) /\ ( P =/= Q /\ R =/= S /\ ( ( P .\/ Q ) ./\ ( R .\/ S ) ) =/= .0. ) ) -> K e. HL )
54		simpll2	|- ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) /\ ( P =/= Q /\ R =/= S /\ ( ( P .\/ Q ) ./\ ( R .\/ S ) ) =/= .0. ) ) -> P e. A )
55		simpll3	|- ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) /\ ( P =/= Q /\ R =/= S /\ ( ( P .\/ Q ) ./\ ( R .\/ S ) ) =/= .0. ) ) -> Q e. A )
56		simpr1	|- ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) /\ ( P =/= Q /\ R =/= S /\ ( ( P .\/ Q ) ./\ ( R .\/ S ) ) =/= .0. ) ) -> P =/= Q )
57		eqid	|- ( LLines ` K ) = ( LLines ` K )
58	1 4 57	llni2	|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ P =/= Q ) -> ( P .\/ Q ) e. ( LLines ` K ) )
59	53 54 55 56 58	syl31anc	|- ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) /\ ( P =/= Q /\ R =/= S /\ ( ( P .\/ Q ) ./\ ( R .\/ S ) ) =/= .0. ) ) -> ( P .\/ Q ) e. ( LLines ` K ) )
60		simplr1	|- ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) /\ ( P =/= Q /\ R =/= S /\ ( ( P .\/ Q ) ./\ ( R .\/ S ) ) =/= .0. ) ) -> R e. A )
61		simplr2	|- ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) /\ ( P =/= Q /\ R =/= S /\ ( ( P .\/ Q ) ./\ ( R .\/ S ) ) =/= .0. ) ) -> S e. A )
62		simpr2	|- ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) /\ ( P =/= Q /\ R =/= S /\ ( ( P .\/ Q ) ./\ ( R .\/ S ) ) =/= .0. ) ) -> R =/= S )
63	1 4 57	llni2	|- ( ( ( K e. HL /\ R e. A /\ S e. A ) /\ R =/= S ) -> ( R .\/ S ) e. ( LLines ` K ) )
64	53 60 61 62 63	syl31anc	|- ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) /\ ( P =/= Q /\ R =/= S /\ ( ( P .\/ Q ) ./\ ( R .\/ S ) ) =/= .0. ) ) -> ( R .\/ S ) e. ( LLines ` K ) )
65		simplr3	|- ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) /\ ( P =/= Q /\ R =/= S /\ ( ( P .\/ Q ) ./\ ( R .\/ S ) ) =/= .0. ) ) -> ( P .\/ Q ) =/= ( R .\/ S ) )
66		simpr3	|- ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) /\ ( P =/= Q /\ R =/= S /\ ( ( P .\/ Q ) ./\ ( R .\/ S ) ) =/= .0. ) ) -> ( ( P .\/ Q ) ./\ ( R .\/ S ) ) =/= .0. )
67	2 3 4 57	2llnmat	|- ( ( ( K e. HL /\ ( P .\/ Q ) e. ( LLines ` K ) /\ ( R .\/ S ) e. ( LLines ` K ) ) /\ ( ( P .\/ Q ) =/= ( R .\/ S ) /\ ( ( P .\/ Q ) ./\ ( R .\/ S ) ) =/= .0. ) ) -> ( ( P .\/ Q ) ./\ ( R .\/ S ) ) e. A )
68	53 59 64 65 66 67	syl32anc	|- ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) /\ ( P =/= Q /\ R =/= S /\ ( ( P .\/ Q ) ./\ ( R .\/ S ) ) =/= .0. ) ) -> ( ( P .\/ Q ) ./\ ( R .\/ S ) ) e. A )
69	68	3exp2	|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) -> ( P =/= Q -> ( R =/= S -> ( ( ( P .\/ Q ) ./\ ( R .\/ S ) ) =/= .0. -> ( ( P .\/ Q ) ./\ ( R .\/ S ) ) e. A ) ) ) )
70	69	imp31	|- ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) /\ P =/= Q ) /\ R =/= S ) -> ( ( ( P .\/ Q ) ./\ ( R .\/ S ) ) =/= .0. -> ( ( P .\/ Q ) ./\ ( R .\/ S ) ) e. A ) )
71	52 70	syl5bir	|- ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) /\ P =/= Q ) /\ R =/= S ) -> ( -. ( ( P .\/ Q ) ./\ ( R .\/ S ) ) = .0. -> ( ( P .\/ Q ) ./\ ( R .\/ S ) ) e. A ) )
72	71	orrd	|- ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) /\ P =/= Q ) /\ R =/= S ) -> ( ( ( P .\/ Q ) ./\ ( R .\/ S ) ) = .0. \/ ( ( P .\/ Q ) ./\ ( R .\/ S ) ) e. A ) )
73	72	orcomd	|- ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) /\ P =/= Q ) /\ R =/= S ) -> ( ( ( P .\/ Q ) ./\ ( R .\/ S ) ) e. A \/ ( ( P .\/ Q ) ./\ ( R .\/ S ) ) = .0. ) )
74	51 73	pm2.61dane	|- ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) /\ P =/= Q ) -> ( ( ( P .\/ Q ) ./\ ( R .\/ S ) ) e. A \/ ( ( P .\/ Q ) ./\ ( R .\/ S ) ) = .0. ) )
75	36 74	pm2.61dane	|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) -> ( ( ( P .\/ Q ) ./\ ( R .\/ S ) ) e. A \/ ( ( P .\/ Q ) ./\ ( R .\/ S ) ) = .0. ) )
76	5 6 7 8 75	syl13anc	|- ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ ( S e. A \/ S = .0. ) /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) /\ S e. A ) -> ( ( ( P .\/ Q ) ./\ ( R .\/ S ) ) e. A \/ ( ( P .\/ Q ) ./\ ( R .\/ S ) ) = .0. ) )
77		simpl1	|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ ( S e. A \/ S = .0. ) /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) -> K e. HL )
78	77 10	syl	|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ ( S e. A \/ S = .0. ) /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) -> K e. OL )
79	37	adantr	|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ ( S e. A \/ S = .0. ) /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) -> ( P .\/ Q ) e. ( Base ` K ) )
80		simpr1	|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ ( S e. A \/ S = .0. ) /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) -> R e. A )
81	14 2 3 4	meetat2	|- ( ( K e. OL /\ ( P .\/ Q ) e. ( Base ` K ) /\ R e. A ) -> ( ( ( P .\/ Q ) ./\ R ) e. A \/ ( ( P .\/ Q ) ./\ R ) = .0. ) )
82	78 79 80 81	syl3anc	|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ ( S e. A \/ S = .0. ) /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) -> ( ( ( P .\/ Q ) ./\ R ) e. A \/ ( ( P .\/ Q ) ./\ R ) = .0. ) )
83	82	adantr	|- ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ ( S e. A \/ S = .0. ) /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) /\ S = .0. ) -> ( ( ( P .\/ Q ) ./\ R ) e. A \/ ( ( P .\/ Q ) ./\ R ) = .0. ) )
84		oveq2	|- ( S = .0. -> ( R .\/ S ) = ( R .\/ .0. ) )
85	14 4	atbase	|- ( R e. A -> R e. ( Base ` K ) )
86	80 85	syl	|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ ( S e. A \/ S = .0. ) /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) -> R e. ( Base ` K ) )
87	14 1 3	olj01	|- ( ( K e. OL /\ R e. ( Base ` K ) ) -> ( R .\/ .0. ) = R )
88	78 86 87	syl2anc	|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ ( S e. A \/ S = .0. ) /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) -> ( R .\/ .0. ) = R )
89	84 88	sylan9eqr	|- ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ ( S e. A \/ S = .0. ) /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) /\ S = .0. ) -> ( R .\/ S ) = R )
90	89	oveq2d	|- ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ ( S e. A \/ S = .0. ) /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) /\ S = .0. ) -> ( ( P .\/ Q ) ./\ ( R .\/ S ) ) = ( ( P .\/ Q ) ./\ R ) )
91	90	eleq1d	|- ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ ( S e. A \/ S = .0. ) /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) /\ S = .0. ) -> ( ( ( P .\/ Q ) ./\ ( R .\/ S ) ) e. A <-> ( ( P .\/ Q ) ./\ R ) e. A ) )
92	90	eqeq1d	|- ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ ( S e. A \/ S = .0. ) /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) /\ S = .0. ) -> ( ( ( P .\/ Q ) ./\ ( R .\/ S ) ) = .0. <-> ( ( P .\/ Q ) ./\ R ) = .0. ) )
93	91 92	orbi12d	|- ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ ( S e. A \/ S = .0. ) /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) /\ S = .0. ) -> ( ( ( ( P .\/ Q ) ./\ ( R .\/ S ) ) e. A \/ ( ( P .\/ Q ) ./\ ( R .\/ S ) ) = .0. ) <-> ( ( ( P .\/ Q ) ./\ R ) e. A \/ ( ( P .\/ Q ) ./\ R ) = .0. ) ) )
94	83 93	mpbird	|- ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ ( S e. A \/ S = .0. ) /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) /\ S = .0. ) -> ( ( ( P .\/ Q ) ./\ ( R .\/ S ) ) e. A \/ ( ( P .\/ Q ) ./\ ( R .\/ S ) ) = .0. ) )
95		simpr2	|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ ( S e. A \/ S = .0. ) /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) -> ( S e. A \/ S = .0. ) )
96	76 94 95	mpjaodan	|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ ( S e. A \/ S = .0. ) /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) -> ( ( ( P .\/ Q ) ./\ ( R .\/ S ) ) e. A \/ ( ( P .\/ Q ) ./\ ( R .\/ S ) ) = .0. ) )