Metamath Proof Explorer

Theorem lplnexllnN

Description: Given an atom on a lattice plane, there is a lattice line whose join with the atom equals the plane. (Contributed by NM, 26-Jun-2012) (New usage is discouraged.)

Ref Expression
Hypotheses lplnexat.l 
|- .<_ = ( le ` K )
lplnexat.j 
|- .\/ = ( join ` K )
lplnexat.a 
|- A = ( Atoms ` K )
lplnexat.n 
|- N = ( LLines ` K )
lplnexat.p 
|- P = ( LPlanes ` K )
Assertion lplnexllnN 
|- ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) -> E. y e. N ( -. Q .<_ y /\ X = ( y .\/ Q ) ) )

Proof

Step Hyp Ref Expression
1 lplnexat.l 
 |-  .<_ = ( le ` K )
2 lplnexat.j 
 |-  .\/ = ( join ` K )
3 lplnexat.a 
 |-  A = ( Atoms ` K )
4 lplnexat.n 
 |-  N = ( LLines ` K )
5 lplnexat.p 
 |-  P = ( LPlanes ` K )
6 simpl2 
 |-  ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) -> X e. P )
7 simpl1 
 |-  ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) -> K e. HL )
8 eqid 
 |-  ( Base ` K ) = ( Base ` K )
9 8 5 lplnbase 
 |-  ( X e. P -> X e. ( Base ` K ) )
10 6 9 syl 
 |-  ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) -> X e. ( Base ` K ) )
11 8 1 2 3 4 5 islpln3 
 |-  ( ( K e. HL /\ X e. ( Base ` K ) ) -> ( X e. P <-> E. z e. N E. r e. A ( -. r .<_ z /\ X = ( z .\/ r ) ) ) )
12 7 10 11 syl2anc 
 |-  ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) -> ( X e. P <-> E. z e. N E. r e. A ( -. r .<_ z /\ X = ( z .\/ r ) ) ) )
13 6 12 mpbid 
 |-  ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) -> E. z e. N E. r e. A ( -. r .<_ z /\ X = ( z .\/ r ) ) )
14 simpll1 
 |-  ( ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) /\ ( Q .<_ z /\ ( z e. N /\ r e. A ) /\ ( -. r .<_ z /\ X = ( z .\/ r ) ) ) ) -> K e. HL )
15 simpr2l 
 |-  ( ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) /\ ( Q .<_ z /\ ( z e. N /\ r e. A ) /\ ( -. r .<_ z /\ X = ( z .\/ r ) ) ) ) -> z e. N )
16 simpll3 
 |-  ( ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) /\ ( Q .<_ z /\ ( z e. N /\ r e. A ) /\ ( -. r .<_ z /\ X = ( z .\/ r ) ) ) ) -> Q e. A )
17 simpr1 
 |-  ( ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) /\ ( Q .<_ z /\ ( z e. N /\ r e. A ) /\ ( -. r .<_ z /\ X = ( z .\/ r ) ) ) ) -> Q .<_ z )
18 1 2 3 4 llnexatN 
 |-  ( ( ( K e. HL /\ z e. N /\ Q e. A ) /\ Q .<_ z ) -> E. s e. A ( Q =/= s /\ z = ( Q .\/ s ) ) )
19 14 15 16 17 18 syl31anc 
 |-  ( ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) /\ ( Q .<_ z /\ ( z e. N /\ r e. A ) /\ ( -. r .<_ z /\ X = ( z .\/ r ) ) ) ) -> E. s e. A ( Q =/= s /\ z = ( Q .\/ s ) ) )
20 simp1l1 
 |-  ( ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) /\ ( Q .<_ z /\ ( z e. N /\ r e. A ) /\ ( -. r .<_ z /\ X = ( z .\/ r ) ) ) /\ ( s e. A /\ ( Q =/= s /\ z = ( Q .\/ s ) ) ) ) -> K e. HL )
21 simp22r 
 |-  ( ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) /\ ( Q .<_ z /\ ( z e. N /\ r e. A ) /\ ( -. r .<_ z /\ X = ( z .\/ r ) ) ) /\ ( s e. A /\ ( Q =/= s /\ z = ( Q .\/ s ) ) ) ) -> r e. A )
22 simp3l 
 |-  ( ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) /\ ( Q .<_ z /\ ( z e. N /\ r e. A ) /\ ( -. r .<_ z /\ X = ( z .\/ r ) ) ) /\ ( s e. A /\ ( Q =/= s /\ z = ( Q .\/ s ) ) ) ) -> s e. A )
23 simp1l3 
 |-  ( ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) /\ ( Q .<_ z /\ ( z e. N /\ r e. A ) /\ ( -. r .<_ z /\ X = ( z .\/ r ) ) ) /\ ( s e. A /\ ( Q =/= s /\ z = ( Q .\/ s ) ) ) ) -> Q e. A )
24 simp23l 
 |-  ( ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) /\ ( Q .<_ z /\ ( z e. N /\ r e. A ) /\ ( -. r .<_ z /\ X = ( z .\/ r ) ) ) /\ ( s e. A /\ ( Q =/= s /\ z = ( Q .\/ s ) ) ) ) -> -. r .<_ z )
25 simp3rr 
 |-  ( ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) /\ ( Q .<_ z /\ ( z e. N /\ r e. A ) /\ ( -. r .<_ z /\ X = ( z .\/ r ) ) ) /\ ( s e. A /\ ( Q =/= s /\ z = ( Q .\/ s ) ) ) ) -> z = ( Q .\/ s ) )
26 25 breq2d 
 |-  ( ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) /\ ( Q .<_ z /\ ( z e. N /\ r e. A ) /\ ( -. r .<_ z /\ X = ( z .\/ r ) ) ) /\ ( s e. A /\ ( Q =/= s /\ z = ( Q .\/ s ) ) ) ) -> ( r .<_ z <-> r .<_ ( Q .\/ s ) ) )
27 24 26 mtbid 
 |-  ( ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) /\ ( Q .<_ z /\ ( z e. N /\ r e. A ) /\ ( -. r .<_ z /\ X = ( z .\/ r ) ) ) /\ ( s e. A /\ ( Q =/= s /\ z = ( Q .\/ s ) ) ) ) -> -. r .<_ ( Q .\/ s ) )
28 1 2 3 atnlej2 
 |-  ( ( K e. HL /\ ( r e. A /\ Q e. A /\ s e. A ) /\ -. r .<_ ( Q .\/ s ) ) -> r =/= s )
29 20 21 23 22 27 28 syl131anc 
 |-  ( ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) /\ ( Q .<_ z /\ ( z e. N /\ r e. A ) /\ ( -. r .<_ z /\ X = ( z .\/ r ) ) ) /\ ( s e. A /\ ( Q =/= s /\ z = ( Q .\/ s ) ) ) ) -> r =/= s )
30 2 3 4 llni2 
 |-  ( ( ( K e. HL /\ r e. A /\ s e. A ) /\ r =/= s ) -> ( r .\/ s ) e. N )
31 20 21 22 29 30 syl31anc 
 |-  ( ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) /\ ( Q .<_ z /\ ( z e. N /\ r e. A ) /\ ( -. r .<_ z /\ X = ( z .\/ r ) ) ) /\ ( s e. A /\ ( Q =/= s /\ z = ( Q .\/ s ) ) ) ) -> ( r .\/ s ) e. N )
32 simp3rl 
 |-  ( ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) /\ ( Q .<_ z /\ ( z e. N /\ r e. A ) /\ ( -. r .<_ z /\ X = ( z .\/ r ) ) ) /\ ( s e. A /\ ( Q =/= s /\ z = ( Q .\/ s ) ) ) ) -> Q =/= s )
33 1 2 3 hlatcon2 
 |-  ( ( K e. HL /\ ( Q e. A /\ s e. A /\ r e. A ) /\ ( Q =/= s /\ -. r .<_ ( Q .\/ s ) ) ) -> -. Q .<_ ( r .\/ s ) )
34 20 23 22 21 32 27 33 syl132anc 
 |-  ( ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) /\ ( Q .<_ z /\ ( z e. N /\ r e. A ) /\ ( -. r .<_ z /\ X = ( z .\/ r ) ) ) /\ ( s e. A /\ ( Q =/= s /\ z = ( Q .\/ s ) ) ) ) -> -. Q .<_ ( r .\/ s ) )
35 simp23r 
 |-  ( ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) /\ ( Q .<_ z /\ ( z e. N /\ r e. A ) /\ ( -. r .<_ z /\ X = ( z .\/ r ) ) ) /\ ( s e. A /\ ( Q =/= s /\ z = ( Q .\/ s ) ) ) ) -> X = ( z .\/ r ) )
36 25 oveq1d 
 |-  ( ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) /\ ( Q .<_ z /\ ( z e. N /\ r e. A ) /\ ( -. r .<_ z /\ X = ( z .\/ r ) ) ) /\ ( s e. A /\ ( Q =/= s /\ z = ( Q .\/ s ) ) ) ) -> ( z .\/ r ) = ( ( Q .\/ s ) .\/ r ) )
37 20 hllatd 
 |-  ( ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) /\ ( Q .<_ z /\ ( z e. N /\ r e. A ) /\ ( -. r .<_ z /\ X = ( z .\/ r ) ) ) /\ ( s e. A /\ ( Q =/= s /\ z = ( Q .\/ s ) ) ) ) -> K e. Lat )
38 8 3 atbase 
 |-  ( Q e. A -> Q e. ( Base ` K ) )
39 23 38 syl 
 |-  ( ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) /\ ( Q .<_ z /\ ( z e. N /\ r e. A ) /\ ( -. r .<_ z /\ X = ( z .\/ r ) ) ) /\ ( s e. A /\ ( Q =/= s /\ z = ( Q .\/ s ) ) ) ) -> Q e. ( Base ` K ) )
40 8 3 atbase 
 |-  ( s e. A -> s e. ( Base ` K ) )
41 22 40 syl 
 |-  ( ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) /\ ( Q .<_ z /\ ( z e. N /\ r e. A ) /\ ( -. r .<_ z /\ X = ( z .\/ r ) ) ) /\ ( s e. A /\ ( Q =/= s /\ z = ( Q .\/ s ) ) ) ) -> s e. ( Base ` K ) )
42 8 3 atbase 
 |-  ( r e. A -> r e. ( Base ` K ) )
43 21 42 syl 
 |-  ( ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) /\ ( Q .<_ z /\ ( z e. N /\ r e. A ) /\ ( -. r .<_ z /\ X = ( z .\/ r ) ) ) /\ ( s e. A /\ ( Q =/= s /\ z = ( Q .\/ s ) ) ) ) -> r e. ( Base ` K ) )
44 8 2 latj31 
 |-  ( ( K e. Lat /\ ( Q e. ( Base ` K ) /\ s e. ( Base ` K ) /\ r e. ( Base ` K ) ) ) -> ( ( Q .\/ s ) .\/ r ) = ( ( r .\/ s ) .\/ Q ) )
45 37 39 41 43 44 syl13anc 
 |-  ( ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) /\ ( Q .<_ z /\ ( z e. N /\ r e. A ) /\ ( -. r .<_ z /\ X = ( z .\/ r ) ) ) /\ ( s e. A /\ ( Q =/= s /\ z = ( Q .\/ s ) ) ) ) -> ( ( Q .\/ s ) .\/ r ) = ( ( r .\/ s ) .\/ Q ) )
46 35 36 45 3eqtrd 
 |-  ( ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) /\ ( Q .<_ z /\ ( z e. N /\ r e. A ) /\ ( -. r .<_ z /\ X = ( z .\/ r ) ) ) /\ ( s e. A /\ ( Q =/= s /\ z = ( Q .\/ s ) ) ) ) -> X = ( ( r .\/ s ) .\/ Q ) )
47 breq2 
 |-  ( y = ( r .\/ s ) -> ( Q .<_ y <-> Q .<_ ( r .\/ s ) ) )
48 47 notbid 
 |-  ( y = ( r .\/ s ) -> ( -. Q .<_ y <-> -. Q .<_ ( r .\/ s ) ) )
49 oveq1 
 |-  ( y = ( r .\/ s ) -> ( y .\/ Q ) = ( ( r .\/ s ) .\/ Q ) )
50 49 eqeq2d 
 |-  ( y = ( r .\/ s ) -> ( X = ( y .\/ Q ) <-> X = ( ( r .\/ s ) .\/ Q ) ) )
51 48 50 anbi12d 
 |-  ( y = ( r .\/ s ) -> ( ( -. Q .<_ y /\ X = ( y .\/ Q ) ) <-> ( -. Q .<_ ( r .\/ s ) /\ X = ( ( r .\/ s ) .\/ Q ) ) ) )
52 51 rspcev 
 |-  ( ( ( r .\/ s ) e. N /\ ( -. Q .<_ ( r .\/ s ) /\ X = ( ( r .\/ s ) .\/ Q ) ) ) -> E. y e. N ( -. Q .<_ y /\ X = ( y .\/ Q ) ) )
53 31 34 46 52 syl12anc 
 |-  ( ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) /\ ( Q .<_ z /\ ( z e. N /\ r e. A ) /\ ( -. r .<_ z /\ X = ( z .\/ r ) ) ) /\ ( s e. A /\ ( Q =/= s /\ z = ( Q .\/ s ) ) ) ) -> E. y e. N ( -. Q .<_ y /\ X = ( y .\/ Q ) ) )
54 53 3expia 
 |-  ( ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) /\ ( Q .<_ z /\ ( z e. N /\ r e. A ) /\ ( -. r .<_ z /\ X = ( z .\/ r ) ) ) ) -> ( ( s e. A /\ ( Q =/= s /\ z = ( Q .\/ s ) ) ) -> E. y e. N ( -. Q .<_ y /\ X = ( y .\/ Q ) ) ) )
55 54 expd 
 |-  ( ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) /\ ( Q .<_ z /\ ( z e. N /\ r e. A ) /\ ( -. r .<_ z /\ X = ( z .\/ r ) ) ) ) -> ( s e. A -> ( ( Q =/= s /\ z = ( Q .\/ s ) ) -> E. y e. N ( -. Q .<_ y /\ X = ( y .\/ Q ) ) ) ) )
56 55 rexlimdv 
 |-  ( ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) /\ ( Q .<_ z /\ ( z e. N /\ r e. A ) /\ ( -. r .<_ z /\ X = ( z .\/ r ) ) ) ) -> ( E. s e. A ( Q =/= s /\ z = ( Q .\/ s ) ) -> E. y e. N ( -. Q .<_ y /\ X = ( y .\/ Q ) ) ) )
57 19 56 mpd 
 |-  ( ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) /\ ( Q .<_ z /\ ( z e. N /\ r e. A ) /\ ( -. r .<_ z /\ X = ( z .\/ r ) ) ) ) -> E. y e. N ( -. Q .<_ y /\ X = ( y .\/ Q ) ) )
58 57 3exp2 
 |-  ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) -> ( Q .<_ z -> ( ( z e. N /\ r e. A ) -> ( ( -. r .<_ z /\ X = ( z .\/ r ) ) -> E. y e. N ( -. Q .<_ y /\ X = ( y .\/ Q ) ) ) ) ) )
59 simpr2l 
 |-  ( ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) /\ ( -. Q .<_ z /\ ( z e. N /\ r e. A ) /\ ( -. r .<_ z /\ X = ( z .\/ r ) ) ) ) -> z e. N )
60 simpr1 
 |-  ( ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) /\ ( -. Q .<_ z /\ ( z e. N /\ r e. A ) /\ ( -. r .<_ z /\ X = ( z .\/ r ) ) ) ) -> -. Q .<_ z )
61 simpll1 
 |-  ( ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) /\ ( -. Q .<_ z /\ ( z e. N /\ r e. A ) /\ ( -. r .<_ z /\ X = ( z .\/ r ) ) ) ) -> K e. HL )
62 61 hllatd 
 |-  ( ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) /\ ( -. Q .<_ z /\ ( z e. N /\ r e. A ) /\ ( -. r .<_ z /\ X = ( z .\/ r ) ) ) ) -> K e. Lat )
63 8 4 llnbase 
 |-  ( z e. N -> z e. ( Base ` K ) )
64 59 63 syl 
 |-  ( ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) /\ ( -. Q .<_ z /\ ( z e. N /\ r e. A ) /\ ( -. r .<_ z /\ X = ( z .\/ r ) ) ) ) -> z e. ( Base ` K ) )
65 simpr2r 
 |-  ( ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) /\ ( -. Q .<_ z /\ ( z e. N /\ r e. A ) /\ ( -. r .<_ z /\ X = ( z .\/ r ) ) ) ) -> r e. A )
66 65 42 syl 
 |-  ( ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) /\ ( -. Q .<_ z /\ ( z e. N /\ r e. A ) /\ ( -. r .<_ z /\ X = ( z .\/ r ) ) ) ) -> r e. ( Base ` K ) )
67 8 1 2 latlej1 
 |-  ( ( K e. Lat /\ z e. ( Base ` K ) /\ r e. ( Base ` K ) ) -> z .<_ ( z .\/ r ) )
68 62 64 66 67 syl3anc 
 |-  ( ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) /\ ( -. Q .<_ z /\ ( z e. N /\ r e. A ) /\ ( -. r .<_ z /\ X = ( z .\/ r ) ) ) ) -> z .<_ ( z .\/ r ) )
69 simpr3r 
 |-  ( ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) /\ ( -. Q .<_ z /\ ( z e. N /\ r e. A ) /\ ( -. r .<_ z /\ X = ( z .\/ r ) ) ) ) -> X = ( z .\/ r ) )
70 68 69 breqtrrd 
 |-  ( ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) /\ ( -. Q .<_ z /\ ( z e. N /\ r e. A ) /\ ( -. r .<_ z /\ X = ( z .\/ r ) ) ) ) -> z .<_ X )
71 simplr 
 |-  ( ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) /\ ( -. Q .<_ z /\ ( z e. N /\ r e. A ) /\ ( -. r .<_ z /\ X = ( z .\/ r ) ) ) ) -> Q .<_ X )
72 simpll3 
 |-  ( ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) /\ ( -. Q .<_ z /\ ( z e. N /\ r e. A ) /\ ( -. r .<_ z /\ X = ( z .\/ r ) ) ) ) -> Q e. A )
73 72 38 syl 
 |-  ( ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) /\ ( -. Q .<_ z /\ ( z e. N /\ r e. A ) /\ ( -. r .<_ z /\ X = ( z .\/ r ) ) ) ) -> Q e. ( Base ` K ) )
74 simpll2 
 |-  ( ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) /\ ( -. Q .<_ z /\ ( z e. N /\ r e. A ) /\ ( -. r .<_ z /\ X = ( z .\/ r ) ) ) ) -> X e. P )
75 74 9 syl 
 |-  ( ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) /\ ( -. Q .<_ z /\ ( z e. N /\ r e. A ) /\ ( -. r .<_ z /\ X = ( z .\/ r ) ) ) ) -> X e. ( Base ` K ) )
76 8 1 2 latjle12 
 |-  ( ( K e. Lat /\ ( z e. ( Base ` K ) /\ Q e. ( Base ` K ) /\ X e. ( Base ` K ) ) ) -> ( ( z .<_ X /\ Q .<_ X ) <-> ( z .\/ Q ) .<_ X ) )
77 62 64 73 75 76 syl13anc 
 |-  ( ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) /\ ( -. Q .<_ z /\ ( z e. N /\ r e. A ) /\ ( -. r .<_ z /\ X = ( z .\/ r ) ) ) ) -> ( ( z .<_ X /\ Q .<_ X ) <-> ( z .\/ Q ) .<_ X ) )
78 70 71 77 mpbi2and 
 |-  ( ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) /\ ( -. Q .<_ z /\ ( z e. N /\ r e. A ) /\ ( -. r .<_ z /\ X = ( z .\/ r ) ) ) ) -> ( z .\/ Q ) .<_ X )
79 8 2 latjcl 
 |-  ( ( K e. Lat /\ z e. ( Base ` K ) /\ Q e. ( Base ` K ) ) -> ( z .\/ Q ) e. ( Base ` K ) )
80 62 64 73 79 syl3anc 
 |-  ( ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) /\ ( -. Q .<_ z /\ ( z e. N /\ r e. A ) /\ ( -. r .<_ z /\ X = ( z .\/ r ) ) ) ) -> ( z .\/ Q ) e. ( Base ` K ) )
81 eqid 
 |-  (
82 8 1 2 81 3 cvr1 
 |-  ( ( K e. HL /\ z e. ( Base ` K ) /\ Q e. A ) -> ( -. Q .<_ z <-> z (
83 61 64 72 82 syl3anc 
 |-  ( ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) /\ ( -. Q .<_ z /\ ( z e. N /\ r e. A ) /\ ( -. r .<_ z /\ X = ( z .\/ r ) ) ) ) -> ( -. Q .<_ z <-> z (
84 60 83 mpbid 
 |-  ( ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) /\ ( -. Q .<_ z /\ ( z e. N /\ r e. A ) /\ ( -. r .<_ z /\ X = ( z .\/ r ) ) ) ) -> z (
85 8 81 4 5 lplni 
 |-  ( ( ( K e. HL /\ ( z .\/ Q ) e. ( Base ` K ) /\ z e. N ) /\ z (  ( z .\/ Q ) e. P )
86 61 80 59 84 85 syl31anc 
 |-  ( ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) /\ ( -. Q .<_ z /\ ( z e. N /\ r e. A ) /\ ( -. r .<_ z /\ X = ( z .\/ r ) ) ) ) -> ( z .\/ Q ) e. P )
87 1 5 lplncmp 
 |-  ( ( K e. HL /\ ( z .\/ Q ) e. P /\ X e. P ) -> ( ( z .\/ Q ) .<_ X <-> ( z .\/ Q ) = X ) )
88 61 86 74 87 syl3anc 
 |-  ( ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) /\ ( -. Q .<_ z /\ ( z e. N /\ r e. A ) /\ ( -. r .<_ z /\ X = ( z .\/ r ) ) ) ) -> ( ( z .\/ Q ) .<_ X <-> ( z .\/ Q ) = X ) )
89 78 88 mpbid 
 |-  ( ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) /\ ( -. Q .<_ z /\ ( z e. N /\ r e. A ) /\ ( -. r .<_ z /\ X = ( z .\/ r ) ) ) ) -> ( z .\/ Q ) = X )
90 89 eqcomd 
 |-  ( ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) /\ ( -. Q .<_ z /\ ( z e. N /\ r e. A ) /\ ( -. r .<_ z /\ X = ( z .\/ r ) ) ) ) -> X = ( z .\/ Q ) )
91 breq2 
 |-  ( y = z -> ( Q .<_ y <-> Q .<_ z ) )
92 91 notbid 
 |-  ( y = z -> ( -. Q .<_ y <-> -. Q .<_ z ) )
93 oveq1 
 |-  ( y = z -> ( y .\/ Q ) = ( z .\/ Q ) )
94 93 eqeq2d 
 |-  ( y = z -> ( X = ( y .\/ Q ) <-> X = ( z .\/ Q ) ) )
95 92 94 anbi12d 
 |-  ( y = z -> ( ( -. Q .<_ y /\ X = ( y .\/ Q ) ) <-> ( -. Q .<_ z /\ X = ( z .\/ Q ) ) ) )
96 95 rspcev 
 |-  ( ( z e. N /\ ( -. Q .<_ z /\ X = ( z .\/ Q ) ) ) -> E. y e. N ( -. Q .<_ y /\ X = ( y .\/ Q ) ) )
97 59 60 90 96 syl12anc 
 |-  ( ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) /\ ( -. Q .<_ z /\ ( z e. N /\ r e. A ) /\ ( -. r .<_ z /\ X = ( z .\/ r ) ) ) ) -> E. y e. N ( -. Q .<_ y /\ X = ( y .\/ Q ) ) )
98 97 3exp2 
 |-  ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) -> ( -. Q .<_ z -> ( ( z e. N /\ r e. A ) -> ( ( -. r .<_ z /\ X = ( z .\/ r ) ) -> E. y e. N ( -. Q .<_ y /\ X = ( y .\/ Q ) ) ) ) ) )
99 58 98 pm2.61d 
 |-  ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) -> ( ( z e. N /\ r e. A ) -> ( ( -. r .<_ z /\ X = ( z .\/ r ) ) -> E. y e. N ( -. Q .<_ y /\ X = ( y .\/ Q ) ) ) ) )
100 99 rexlimdvv 
 |-  ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) -> ( E. z e. N E. r e. A ( -. r .<_ z /\ X = ( z .\/ r ) ) -> E. y e. N ( -. Q .<_ y /\ X = ( y .\/ Q ) ) ) )
101 13 100 mpd 
 |-  ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ Q .<_ X ) -> E. y e. N ( -. Q .<_ y /\ X = ( y .\/ Q ) ) )