Metamath Proof Explorer

Theorem dia2dimlem1

Description: Lemma for dia2dim . Show properties of the auxiliary atom Q . Part of proof of Lemma M in Crawley p. 121 line 3. (Contributed by NM, 8-Sep-2014)

Ref Expression
Hypotheses dia2dimlem1.l 
|- .<_ = ( le ` K )
dia2dimlem1.j 
|- .\/ = ( join ` K )
dia2dimlem1.m 
|- ./\ = ( meet ` K )
dia2dimlem1.a 
|- A = ( Atoms ` K )
dia2dimlem1.h 
|- H = ( LHyp ` K )
dia2dimlem1.t 
|- T = ( ( LTrn ` K ) ` W )
dia2dimlem1.r 
|- R = ( ( trL ` K ) ` W )
dia2dimlem1.q 
|- Q = ( ( P .\/ U ) ./\ ( ( F ` P ) .\/ V ) )
dia2dimlem1.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
dia2dimlem1.u 
|- ( ph -> ( U e. A /\ U .<_ W ) )
dia2dimlem1.v 
|- ( ph -> ( V e. A /\ V .<_ W ) )
dia2dimlem1.p 
|- ( ph -> ( P e. A /\ -. P .<_ W ) )
dia2dimlem1.f 
|- ( ph -> ( F e. T /\ ( F ` P ) =/= P ) )
dia2dimlem1.rf 
|- ( ph -> ( R ` F ) .<_ ( U .\/ V ) )
dia2dimlem1.uv 
|- ( ph -> U =/= V )
dia2dimlem1.ru 
|- ( ph -> ( R ` F ) =/= U )
Assertion dia2dimlem1 
|- ( ph -> ( Q e. A /\ -. Q .<_ W ) )

Proof

Step Hyp Ref Expression
1 dia2dimlem1.l 
 |-  .<_ = ( le ` K )
2 dia2dimlem1.j 
 |-  .\/ = ( join ` K )
3 dia2dimlem1.m 
 |-  ./\ = ( meet ` K )
4 dia2dimlem1.a 
 |-  A = ( Atoms ` K )
5 dia2dimlem1.h 
 |-  H = ( LHyp ` K )
6 dia2dimlem1.t 
 |-  T = ( ( LTrn ` K ) ` W )
7 dia2dimlem1.r 
 |-  R = ( ( trL ` K ) ` W )
8 dia2dimlem1.q 
 |-  Q = ( ( P .\/ U ) ./\ ( ( F ` P ) .\/ V ) )
9 dia2dimlem1.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
10 dia2dimlem1.u 
 |-  ( ph -> ( U e. A /\ U .<_ W ) )
11 dia2dimlem1.v 
 |-  ( ph -> ( V e. A /\ V .<_ W ) )
12 dia2dimlem1.p 
 |-  ( ph -> ( P e. A /\ -. P .<_ W ) )
13 dia2dimlem1.f 
 |-  ( ph -> ( F e. T /\ ( F ` P ) =/= P ) )
14 dia2dimlem1.rf 
 |-  ( ph -> ( R ` F ) .<_ ( U .\/ V ) )
15 dia2dimlem1.uv 
 |-  ( ph -> U =/= V )
16 dia2dimlem1.ru 
 |-  ( ph -> ( R ` F ) =/= U )
17 9 simpld 
 |-  ( ph -> K e. HL )
18 12 simpld 
 |-  ( ph -> P e. A )
19 1 4 5 6 7 trlat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( F e. T /\ ( F ` P ) =/= P ) ) -> ( R ` F ) e. A )
20 9 12 13 19 syl3anc 
 |-  ( ph -> ( R ` F ) e. A )
21 10 simpld 
 |-  ( ph -> U e. A )
22 13 simpld 
 |-  ( ph -> F e. T )
23 1 4 5 6 ltrnel 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( F ` P ) e. A /\ -. ( F ` P ) .<_ W ) )
24 9 22 12 23 syl3anc 
 |-  ( ph -> ( ( F ` P ) e. A /\ -. ( F ` P ) .<_ W ) )
25 24 simpld 
 |-  ( ph -> ( F ` P ) e. A )
26 11 simpld 
 |-  ( ph -> V e. A )
27 12 simprd 
 |-  ( ph -> -. P .<_ W )
28 1 5 6 7 trlle 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( R ` F ) .<_ W )
29 9 22 28 syl2anc 
 |-  ( ph -> ( R ` F ) .<_ W )
30 10 simprd 
 |-  ( ph -> U .<_ W )
31 17 hllatd 
 |-  ( ph -> K e. Lat )
32 eqid 
 |-  ( Base ` K ) = ( Base ` K )
33 32 4 atbase 
 |-  ( ( R ` F ) e. A -> ( R ` F ) e. ( Base ` K ) )
34 20 33 syl 
 |-  ( ph -> ( R ` F ) e. ( Base ` K ) )
35 32 4 atbase 
 |-  ( U e. A -> U e. ( Base ` K ) )
36 21 35 syl 
 |-  ( ph -> U e. ( Base ` K ) )
37 9 simprd 
 |-  ( ph -> W e. H )
38 32 5 lhpbase 
 |-  ( W e. H -> W e. ( Base ` K ) )
39 37 38 syl 
 |-  ( ph -> W e. ( Base ` K ) )
40 32 1 2 latjle12 
 |-  ( ( K e. Lat /\ ( ( R ` F ) e. ( Base ` K ) /\ U e. ( Base ` K ) /\ W e. ( Base ` K ) ) ) -> ( ( ( R ` F ) .<_ W /\ U .<_ W ) <-> ( ( R ` F ) .\/ U ) .<_ W ) )
41 31 34 36 39 40 syl13anc 
 |-  ( ph -> ( ( ( R ` F ) .<_ W /\ U .<_ W ) <-> ( ( R ` F ) .\/ U ) .<_ W ) )
42 29 30 41 mpbi2and 
 |-  ( ph -> ( ( R ` F ) .\/ U ) .<_ W )
43 32 4 atbase 
 |-  ( P e. A -> P e. ( Base ` K ) )
44 18 43 syl 
 |-  ( ph -> P e. ( Base ` K ) )
45 32 2 4 hlatjcl 
 |-  ( ( K e. HL /\ ( R ` F ) e. A /\ U e. A ) -> ( ( R ` F ) .\/ U ) e. ( Base ` K ) )
46 17 20 21 45 syl3anc 
 |-  ( ph -> ( ( R ` F ) .\/ U ) e. ( Base ` K ) )
47 32 1 lattr 
 |-  ( ( K e. Lat /\ ( P e. ( Base ` K ) /\ ( ( R ` F ) .\/ U ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) ) -> ( ( P .<_ ( ( R ` F ) .\/ U ) /\ ( ( R ` F ) .\/ U ) .<_ W ) -> P .<_ W ) )
48 31 44 46 39 47 syl13anc 
 |-  ( ph -> ( ( P .<_ ( ( R ` F ) .\/ U ) /\ ( ( R ` F ) .\/ U ) .<_ W ) -> P .<_ W ) )
49 42 48 mpan2d 
 |-  ( ph -> ( P .<_ ( ( R ` F ) .\/ U ) -> P .<_ W ) )
50 27 49 mtod 
 |-  ( ph -> -. P .<_ ( ( R ` F ) .\/ U ) )
51 11 simprd 
 |-  ( ph -> V .<_ W )
52 24 simprd 
 |-  ( ph -> -. ( F ` P ) .<_ W )
53 nbrne2 
 |-  ( ( V .<_ W /\ -. ( F ` P ) .<_ W ) -> V =/= ( F ` P ) )
54 51 52 53 syl2anc 
 |-  ( ph -> V =/= ( F ` P ) )
55 54 necomd 
 |-  ( ph -> ( F ` P ) =/= V )
56 50 55 jca 
 |-  ( ph -> ( -. P .<_ ( ( R ` F ) .\/ U ) /\ ( F ` P ) =/= V ) )
57 31 adantr 
 |-  ( ( ph /\ ( P .\/ U ) = ( ( F ` P ) .\/ V ) ) -> K e. Lat )
58 44 adantr 
 |-  ( ( ph /\ ( P .\/ U ) = ( ( F ` P ) .\/ V ) ) -> P e. ( Base ` K ) )
59 32 2 4 hlatjcl 
 |-  ( ( K e. HL /\ V e. A /\ U e. A ) -> ( V .\/ U ) e. ( Base ` K ) )
60 17 26 21 59 syl3anc 
 |-  ( ph -> ( V .\/ U ) e. ( Base ` K ) )
61 60 adantr 
 |-  ( ( ph /\ ( P .\/ U ) = ( ( F ` P ) .\/ V ) ) -> ( V .\/ U ) e. ( Base ` K ) )
62 39 adantr 
 |-  ( ( ph /\ ( P .\/ U ) = ( ( F ` P ) .\/ V ) ) -> W e. ( Base ` K ) )
63 1 2 4 hlatlej2 
 |-  ( ( K e. HL /\ ( F ` P ) e. A /\ V e. A ) -> V .<_ ( ( F ` P ) .\/ V ) )
64 17 25 26 63 syl3anc 
 |-  ( ph -> V .<_ ( ( F ` P ) .\/ V ) )
65 64 adantr 
 |-  ( ( ph /\ ( P .\/ U ) = ( ( F ` P ) .\/ V ) ) -> V .<_ ( ( F ` P ) .\/ V ) )
66 simpr 
 |-  ( ( ph /\ ( P .\/ U ) = ( ( F ` P ) .\/ V ) ) -> ( P .\/ U ) = ( ( F ` P ) .\/ V ) )
67 65 66 breqtrrd 
 |-  ( ( ph /\ ( P .\/ U ) = ( ( F ` P ) .\/ V ) ) -> V .<_ ( P .\/ U ) )
68 15 necomd 
 |-  ( ph -> V =/= U )
69 1 2 4 hlatexch2 
 |-  ( ( K e. HL /\ ( V e. A /\ P e. A /\ U e. A ) /\ V =/= U ) -> ( V .<_ ( P .\/ U ) -> P .<_ ( V .\/ U ) ) )
70 17 26 18 21 68 69 syl131anc 
 |-  ( ph -> ( V .<_ ( P .\/ U ) -> P .<_ ( V .\/ U ) ) )
71 70 adantr 
 |-  ( ( ph /\ ( P .\/ U ) = ( ( F ` P ) .\/ V ) ) -> ( V .<_ ( P .\/ U ) -> P .<_ ( V .\/ U ) ) )
72 67 71 mpd 
 |-  ( ( ph /\ ( P .\/ U ) = ( ( F ` P ) .\/ V ) ) -> P .<_ ( V .\/ U ) )
73 32 4 atbase 
 |-  ( V e. A -> V e. ( Base ` K ) )
74 26 73 syl 
 |-  ( ph -> V e. ( Base ` K ) )
75 32 1 2 latjle12 
 |-  ( ( K e. Lat /\ ( V e. ( Base ` K ) /\ U e. ( Base ` K ) /\ W e. ( Base ` K ) ) ) -> ( ( V .<_ W /\ U .<_ W ) <-> ( V .\/ U ) .<_ W ) )
76 31 74 36 39 75 syl13anc 
 |-  ( ph -> ( ( V .<_ W /\ U .<_ W ) <-> ( V .\/ U ) .<_ W ) )
77 51 30 76 mpbi2and 
 |-  ( ph -> ( V .\/ U ) .<_ W )
78 77 adantr 
 |-  ( ( ph /\ ( P .\/ U ) = ( ( F ` P ) .\/ V ) ) -> ( V .\/ U ) .<_ W )
79 32 1 57 58 61 62 72 78 lattrd 
 |-  ( ( ph /\ ( P .\/ U ) = ( ( F ` P ) .\/ V ) ) -> P .<_ W )
80 79 ex 
 |-  ( ph -> ( ( P .\/ U ) = ( ( F ` P ) .\/ V ) -> P .<_ W ) )
81 80 necon3bd 
 |-  ( ph -> ( -. P .<_ W -> ( P .\/ U ) =/= ( ( F ` P ) .\/ V ) ) )
82 27 81 mpd 
 |-  ( ph -> ( P .\/ U ) =/= ( ( F ` P ) .\/ V ) )
83 1 2 4 hlatlej2 
 |-  ( ( K e. HL /\ P e. A /\ ( F ` P ) e. A ) -> ( F ` P ) .<_ ( P .\/ ( F ` P ) ) )
84 17 18 25 83 syl3anc 
 |-  ( ph -> ( F ` P ) .<_ ( P .\/ ( F ` P ) ) )
85 1 2 3 4 5 6 7 trlval2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) -> ( R ` F ) = ( ( P .\/ ( F ` P ) ) ./\ W ) )
86 9 22 12 85 syl3anc 
 |-  ( ph -> ( R ` F ) = ( ( P .\/ ( F ` P ) ) ./\ W ) )
87 86 oveq2d 
 |-  ( ph -> ( P .\/ ( R ` F ) ) = ( P .\/ ( ( P .\/ ( F ` P ) ) ./\ W ) ) )
88 32 2 4 hlatjcl 
 |-  ( ( K e. HL /\ P e. A /\ ( F ` P ) e. A ) -> ( P .\/ ( F ` P ) ) e. ( Base ` K ) )
89 17 18 25 88 syl3anc 
 |-  ( ph -> ( P .\/ ( F ` P ) ) e. ( Base ` K ) )
90 1 2 4 hlatlej1 
 |-  ( ( K e. HL /\ P e. A /\ ( F ` P ) e. A ) -> P .<_ ( P .\/ ( F ` P ) ) )
91 17 18 25 90 syl3anc 
 |-  ( ph -> P .<_ ( P .\/ ( F ` P ) ) )
92 32 1 2 3 4 atmod3i1 
 |-  ( ( K e. HL /\ ( P e. A /\ ( P .\/ ( F ` P ) ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) /\ P .<_ ( P .\/ ( F ` P ) ) ) -> ( P .\/ ( ( P .\/ ( F ` P ) ) ./\ W ) ) = ( ( P .\/ ( F ` P ) ) ./\ ( P .\/ W ) ) )
93 17 18 89 39 91 92 syl131anc 
 |-  ( ph -> ( P .\/ ( ( P .\/ ( F ` P ) ) ./\ W ) ) = ( ( P .\/ ( F ` P ) ) ./\ ( P .\/ W ) ) )
94 eqid 
 |-  ( 1. ` K ) = ( 1. ` K )
95 1 2 94 4 5 lhpjat2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( P .\/ W ) = ( 1. ` K ) )
96 9 12 95 syl2anc 
 |-  ( ph -> ( P .\/ W ) = ( 1. ` K ) )
97 96 oveq2d 
 |-  ( ph -> ( ( P .\/ ( F ` P ) ) ./\ ( P .\/ W ) ) = ( ( P .\/ ( F ` P ) ) ./\ ( 1. ` K ) ) )
98 hlol 
 |-  ( K e. HL -> K e. OL )
99 17 98 syl 
 |-  ( ph -> K e. OL )
100 32 3 94 olm11 
 |-  ( ( K e. OL /\ ( P .\/ ( F ` P ) ) e. ( Base ` K ) ) -> ( ( P .\/ ( F ` P ) ) ./\ ( 1. ` K ) ) = ( P .\/ ( F ` P ) ) )
101 99 89 100 syl2anc 
 |-  ( ph -> ( ( P .\/ ( F ` P ) ) ./\ ( 1. ` K ) ) = ( P .\/ ( F ` P ) ) )
102 97 101 eqtrd 
 |-  ( ph -> ( ( P .\/ ( F ` P ) ) ./\ ( P .\/ W ) ) = ( P .\/ ( F ` P ) ) )
103 93 102 eqtrd 
 |-  ( ph -> ( P .\/ ( ( P .\/ ( F ` P ) ) ./\ W ) ) = ( P .\/ ( F ` P ) ) )
104 87 103 eqtrd 
 |-  ( ph -> ( P .\/ ( R ` F ) ) = ( P .\/ ( F ` P ) ) )
105 84 104 breqtrrd 
 |-  ( ph -> ( F ` P ) .<_ ( P .\/ ( R ` F ) ) )
106 2 4 hlatjcom 
 |-  ( ( K e. HL /\ U e. A /\ V e. A ) -> ( U .\/ V ) = ( V .\/ U ) )
107 17 21 26 106 syl3anc 
 |-  ( ph -> ( U .\/ V ) = ( V .\/ U ) )
108 14 107 breqtrd 
 |-  ( ph -> ( R ` F ) .<_ ( V .\/ U ) )
109 1 2 4 hlatexch2 
 |-  ( ( K e. HL /\ ( ( R ` F ) e. A /\ V e. A /\ U e. A ) /\ ( R ` F ) =/= U ) -> ( ( R ` F ) .<_ ( V .\/ U ) -> V .<_ ( ( R ` F ) .\/ U ) ) )
110 17 20 26 21 16 109 syl131anc 
 |-  ( ph -> ( ( R ` F ) .<_ ( V .\/ U ) -> V .<_ ( ( R ` F ) .\/ U ) ) )
111 108 110 mpd 
 |-  ( ph -> V .<_ ( ( R ` F ) .\/ U ) )
112 105 111 jca 
 |-  ( ph -> ( ( F ` P ) .<_ ( P .\/ ( R ` F ) ) /\ V .<_ ( ( R ` F ) .\/ U ) ) )
113 1 2 3 4 ps-2c 
 |-  ( ( ( K e. HL /\ P e. A /\ ( R ` F ) e. A ) /\ ( U e. A /\ ( F ` P ) e. A /\ V e. A ) /\ ( ( -. P .<_ ( ( R ` F ) .\/ U ) /\ ( F ` P ) =/= V ) /\ ( P .\/ U ) =/= ( ( F ` P ) .\/ V ) /\ ( ( F ` P ) .<_ ( P .\/ ( R ` F ) ) /\ V .<_ ( ( R ` F ) .\/ U ) ) ) ) -> ( ( P .\/ U ) ./\ ( ( F ` P ) .\/ V ) ) e. A )
114 17 18 20 21 25 26 56 82 112 113 syl333anc 
 |-  ( ph -> ( ( P .\/ U ) ./\ ( ( F ` P ) .\/ V ) ) e. A )
115 8 114 eqeltrid 
 |-  ( ph -> Q e. A )
116 32 2 4 hlatjcl 
 |-  ( ( K e. HL /\ P e. A /\ U e. A ) -> ( P .\/ U ) e. ( Base ` K ) )
117 17 18 21 116 syl3anc 
 |-  ( ph -> ( P .\/ U ) e. ( Base ` K ) )
118 32 2 4 hlatjcl 
 |-  ( ( K e. HL /\ ( F ` P ) e. A /\ V e. A ) -> ( ( F ` P ) .\/ V ) e. ( Base ` K ) )
119 17 25 26 118 syl3anc 
 |-  ( ph -> ( ( F ` P ) .\/ V ) e. ( Base ` K ) )
120 32 1 3 latmle1 
 |-  ( ( K e. Lat /\ ( P .\/ U ) e. ( Base ` K ) /\ ( ( F ` P ) .\/ V ) e. ( Base ` K ) ) -> ( ( P .\/ U ) ./\ ( ( F ` P ) .\/ V ) ) .<_ ( P .\/ U ) )
121 31 117 119 120 syl3anc 
 |-  ( ph -> ( ( P .\/ U ) ./\ ( ( F ` P ) .\/ V ) ) .<_ ( P .\/ U ) )
122 8 121 eqbrtrid 
 |-  ( ph -> Q .<_ ( P .\/ U ) )
123 32 4 atbase 
 |-  ( Q e. A -> Q e. ( Base ` K ) )
124 115 123 syl 
 |-  ( ph -> Q e. ( Base ` K ) )
125 32 1 3 latlem12 
 |-  ( ( K e. Lat /\ ( Q e. ( Base ` K ) /\ ( P .\/ U ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) ) -> ( ( Q .<_ ( P .\/ U ) /\ Q .<_ W ) <-> Q .<_ ( ( P .\/ U ) ./\ W ) ) )
126 31 124 117 39 125 syl13anc 
 |-  ( ph -> ( ( Q .<_ ( P .\/ U ) /\ Q .<_ W ) <-> Q .<_ ( ( P .\/ U ) ./\ W ) ) )
127 126 biimpd 
 |-  ( ph -> ( ( Q .<_ ( P .\/ U ) /\ Q .<_ W ) -> Q .<_ ( ( P .\/ U ) ./\ W ) ) )
128 122 127 mpand 
 |-  ( ph -> ( Q .<_ W -> Q .<_ ( ( P .\/ U ) ./\ W ) ) )
129 128 imp 
 |-  ( ( ph /\ Q .<_ W ) -> Q .<_ ( ( P .\/ U ) ./\ W ) )
130 eqid 
 |-  ( 0. ` K ) = ( 0. ` K )
131 1 3 130 4 5 lhpmat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( P ./\ W ) = ( 0. ` K ) )
132 9 12 131 syl2anc 
 |-  ( ph -> ( P ./\ W ) = ( 0. ` K ) )
133 132 oveq1d 
 |-  ( ph -> ( ( P ./\ W ) .\/ U ) = ( ( 0. ` K ) .\/ U ) )
134 32 1 2 3 4 atmod4i1 
 |-  ( ( K e. HL /\ ( U e. A /\ P e. ( Base ` K ) /\ W e. ( Base ` K ) ) /\ U .<_ W ) -> ( ( P ./\ W ) .\/ U ) = ( ( P .\/ U ) ./\ W ) )
135 17 21 44 39 30 134 syl131anc 
 |-  ( ph -> ( ( P ./\ W ) .\/ U ) = ( ( P .\/ U ) ./\ W ) )
136 32 2 130 olj02 
 |-  ( ( K e. OL /\ U e. ( Base ` K ) ) -> ( ( 0. ` K ) .\/ U ) = U )
137 99 36 136 syl2anc 
 |-  ( ph -> ( ( 0. ` K ) .\/ U ) = U )
138 133 135 137 3eqtr3d 
 |-  ( ph -> ( ( P .\/ U ) ./\ W ) = U )
139 138 adantr 
 |-  ( ( ph /\ Q .<_ W ) -> ( ( P .\/ U ) ./\ W ) = U )
140 129 139 breqtrd 
 |-  ( ( ph /\ Q .<_ W ) -> Q .<_ U )
141 hlatl 
 |-  ( K e. HL -> K e. AtLat )
142 17 141 syl 
 |-  ( ph -> K e. AtLat )
143 142 adantr 
 |-  ( ( ph /\ Q .<_ W ) -> K e. AtLat )
144 115 adantr 
 |-  ( ( ph /\ Q .<_ W ) -> Q e. A )
145 21 adantr 
 |-  ( ( ph /\ Q .<_ W ) -> U e. A )
146 1 4 atcmp 
 |-  ( ( K e. AtLat /\ Q e. A /\ U e. A ) -> ( Q .<_ U <-> Q = U ) )
147 143 144 145 146 syl3anc 
 |-  ( ( ph /\ Q .<_ W ) -> ( Q .<_ U <-> Q = U ) )
148 140 147 mpbid 
 |-  ( ( ph /\ Q .<_ W ) -> Q = U )
149 32 1 3 latmle2 
 |-  ( ( K e. Lat /\ ( P .\/ U ) e. ( Base ` K ) /\ ( ( F ` P ) .\/ V ) e. ( Base ` K ) ) -> ( ( P .\/ U ) ./\ ( ( F ` P ) .\/ V ) ) .<_ ( ( F ` P ) .\/ V ) )
150 31 117 119 149 syl3anc 
 |-  ( ph -> ( ( P .\/ U ) ./\ ( ( F ` P ) .\/ V ) ) .<_ ( ( F ` P ) .\/ V ) )
151 8 150 eqbrtrid 
 |-  ( ph -> Q .<_ ( ( F ` P ) .\/ V ) )
152 32 1 3 latlem12 
 |-  ( ( K e. Lat /\ ( Q e. ( Base ` K ) /\ ( ( F ` P ) .\/ V ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) ) -> ( ( Q .<_ ( ( F ` P ) .\/ V ) /\ Q .<_ W ) <-> Q .<_ ( ( ( F ` P ) .\/ V ) ./\ W ) ) )
153 31 124 119 39 152 syl13anc 
 |-  ( ph -> ( ( Q .<_ ( ( F ` P ) .\/ V ) /\ Q .<_ W ) <-> Q .<_ ( ( ( F ` P ) .\/ V ) ./\ W ) ) )
154 153 biimpd 
 |-  ( ph -> ( ( Q .<_ ( ( F ` P ) .\/ V ) /\ Q .<_ W ) -> Q .<_ ( ( ( F ` P ) .\/ V ) ./\ W ) ) )
155 151 154 mpand 
 |-  ( ph -> ( Q .<_ W -> Q .<_ ( ( ( F ` P ) .\/ V ) ./\ W ) ) )
156 155 imp 
 |-  ( ( ph /\ Q .<_ W ) -> Q .<_ ( ( ( F ` P ) .\/ V ) ./\ W ) )
157 1 3 130 4 5 lhpmat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( F ` P ) e. A /\ -. ( F ` P ) .<_ W ) ) -> ( ( F ` P ) ./\ W ) = ( 0. ` K ) )
158 9 24 157 syl2anc 
 |-  ( ph -> ( ( F ` P ) ./\ W ) = ( 0. ` K ) )
159 158 oveq1d 
 |-  ( ph -> ( ( ( F ` P ) ./\ W ) .\/ V ) = ( ( 0. ` K ) .\/ V ) )
160 32 4 atbase 
 |-  ( ( F ` P ) e. A -> ( F ` P ) e. ( Base ` K ) )
161 25 160 syl 
 |-  ( ph -> ( F ` P ) e. ( Base ` K ) )
162 32 1 2 3 4 atmod4i1 
 |-  ( ( K e. HL /\ ( V e. A /\ ( F ` P ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) /\ V .<_ W ) -> ( ( ( F ` P ) ./\ W ) .\/ V ) = ( ( ( F ` P ) .\/ V ) ./\ W ) )
163 17 26 161 39 51 162 syl131anc 
 |-  ( ph -> ( ( ( F ` P ) ./\ W ) .\/ V ) = ( ( ( F ` P ) .\/ V ) ./\ W ) )
164 32 2 130 olj02 
 |-  ( ( K e. OL /\ V e. ( Base ` K ) ) -> ( ( 0. ` K ) .\/ V ) = V )
165 99 74 164 syl2anc 
 |-  ( ph -> ( ( 0. ` K ) .\/ V ) = V )
166 159 163 165 3eqtr3d 
 |-  ( ph -> ( ( ( F ` P ) .\/ V ) ./\ W ) = V )
167 166 adantr 
 |-  ( ( ph /\ Q .<_ W ) -> ( ( ( F ` P ) .\/ V ) ./\ W ) = V )
168 156 167 breqtrd 
 |-  ( ( ph /\ Q .<_ W ) -> Q .<_ V )
169 26 adantr 
 |-  ( ( ph /\ Q .<_ W ) -> V e. A )
170 1 4 atcmp 
 |-  ( ( K e. AtLat /\ Q e. A /\ V e. A ) -> ( Q .<_ V <-> Q = V ) )
171 143 144 169 170 syl3anc 
 |-  ( ( ph /\ Q .<_ W ) -> ( Q .<_ V <-> Q = V ) )
172 168 171 mpbid 
 |-  ( ( ph /\ Q .<_ W ) -> Q = V )
173 148 172 eqtr3d 
 |-  ( ( ph /\ Q .<_ W ) -> U = V )
174 173 ex 
 |-  ( ph -> ( Q .<_ W -> U = V ) )
175 174 necon3ad 
 |-  ( ph -> ( U =/= V -> -. Q .<_ W ) )
176 15 175 mpd 
 |-  ( ph -> -. Q .<_ W )
177 115 176 jca 
 |-  ( ph -> ( Q e. A /\ -. Q .<_ W ) )