This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 biimtrrid 
 |-  ( ( ( ( ( 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. ) )