Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dia2dimlem1 Unicode version

Theorem dia2dimlem1 31547
 Description: Lemma for dia2dim 31560. Show properties of the auxiliary atom . Part of proof of Lemma M in [Crawley] p. 121 line 3. (Contributed by NM, 8-Sep-2014.)
Hypotheses
Ref Expression
dia2dimlem1.l
dia2dimlem1.j
dia2dimlem1.m
dia2dimlem1.a
dia2dimlem1.h
dia2dimlem1.t
dia2dimlem1.r
dia2dimlem1.q
dia2dimlem1.k
dia2dimlem1.u
dia2dimlem1.v
dia2dimlem1.p
dia2dimlem1.f
dia2dimlem1.rf
dia2dimlem1.uv
dia2dimlem1.ru
Assertion
Ref Expression
dia2dimlem1

Proof of Theorem dia2dimlem1
StepHypRef Expression
1 dia2dimlem1.q . . 3
2 dia2dimlem1.k . . . . 5
32simpld 446 . . . 4
4 dia2dimlem1.p . . . . 5
54simpld 446 . . . 4
6 dia2dimlem1.f . . . . 5
7 dia2dimlem1.l . . . . . 6
8 dia2dimlem1.a . . . . . 6
9 dia2dimlem1.h . . . . . 6
10 dia2dimlem1.t . . . . . 6
11 dia2dimlem1.r . . . . . 6
127, 8, 9, 10, 11trlat 30651 . . . . 5
132, 4, 6, 12syl3anc 1184 . . . 4
14 dia2dimlem1.u . . . . 5
1514simpld 446 . . . 4
166simpld 446 . . . . . 6
177, 8, 9, 10ltrnel 30621 . . . . . 6
182, 16, 4, 17syl3anc 1184 . . . . 5
1918simpld 446 . . . 4
20 dia2dimlem1.v . . . . 5
2120simpld 446 . . . 4
224simprd 450 . . . . . 6
237, 9, 10, 11trlle 30666 . . . . . . . . 9
242, 16, 23syl2anc 643 . . . . . . . 8
2514simprd 450 . . . . . . . 8
26 hllat 29846 . . . . . . . . . 10
273, 26syl 16 . . . . . . . . 9
28 eqid 2404 . . . . . . . . . . 11
2928, 8atbase 29772 . . . . . . . . . 10
3013, 29syl 16 . . . . . . . . 9
3128, 8atbase 29772 . . . . . . . . . 10
3215, 31syl 16 . . . . . . . . 9
332simprd 450 . . . . . . . . . 10
3428, 9lhpbase 30480 . . . . . . . . . 10
3533, 34syl 16 . . . . . . . . 9
36 dia2dimlem1.j . . . . . . . . . 10
3728, 7, 36latjle12 14446 . . . . . . . . 9
3827, 30, 32, 35, 37syl13anc 1186 . . . . . . . 8
3924, 25, 38mpbi2and 888 . . . . . . 7
4028, 8atbase 29772 . . . . . . . . 9
415, 40syl 16 . . . . . . . 8
4228, 36, 8hlatjcl 29849 . . . . . . . . 9
433, 13, 15, 42syl3anc 1184 . . . . . . . 8
4428, 7lattr 14440 . . . . . . . 8
4527, 41, 43, 35, 44syl13anc 1186 . . . . . . 7
4639, 45mpan2d 656 . . . . . 6
4722, 46mtod 170 . . . . 5
4820simprd 450 . . . . . . 7
4918simprd 450 . . . . . . 7
50 nbrne2 4190 . . . . . . 7
5148, 49, 50syl2anc 643 . . . . . 6
5251necomd 2650 . . . . 5
5347, 52jca 519 . . . 4
5427adantr 452 . . . . . . . 8
5541adantr 452 . . . . . . . 8
5628, 36, 8hlatjcl 29849 . . . . . . . . . 10
573, 21, 15, 56syl3anc 1184 . . . . . . . . 9
5857adantr 452 . . . . . . . 8
5935adantr 452 . . . . . . . 8
607, 36, 8hlatlej2 29858 . . . . . . . . . . . 12
613, 19, 21, 60syl3anc 1184 . . . . . . . . . . 11
6261adantr 452 . . . . . . . . . 10
63 simpr 448 . . . . . . . . . 10
6462, 63breqtrrd 4198 . . . . . . . . 9
65 dia2dimlem1.uv . . . . . . . . . . . 12
6665necomd 2650 . . . . . . . . . . 11
677, 36, 8hlatexch2 29878 . . . . . . . . . . 11
683, 21, 5, 15, 66, 67syl131anc 1197 . . . . . . . . . 10
6968adantr 452 . . . . . . . . 9
7064, 69mpd 15 . . . . . . . 8
7128, 8atbase 29772 . . . . . . . . . . . 12
7221, 71syl 16 . . . . . . . . . . 11
7328, 7, 36latjle12 14446 . . . . . . . . . . 11
7427, 72, 32, 35, 73syl13anc 1186 . . . . . . . . . 10
7548, 25, 74mpbi2and 888 . . . . . . . . 9
7675adantr 452 . . . . . . . 8
7728, 7, 54, 55, 58, 59, 70, 76lattrd 14442 . . . . . . 7
7877ex 424 . . . . . 6
7978necon3bd 2604 . . . . 5
8022, 79mpd 15 . . . 4
817, 36, 8hlatlej2 29858 . . . . . . 7
823, 5, 19, 81syl3anc 1184 . . . . . 6
83 dia2dimlem1.m . . . . . . . . . 10
847, 36, 83, 8, 9, 10, 11trlval2 30645 . . . . . . . . 9
852, 16, 4, 84syl3anc 1184 . . . . . . . 8
8685oveq2d 6056 . . . . . . 7
8728, 36, 8hlatjcl 29849 . . . . . . . . . 10
883, 5, 19, 87syl3anc 1184 . . . . . . . . 9
897, 36, 8hlatlej1 29857 . . . . . . . . . 10
903, 5, 19, 89syl3anc 1184 . . . . . . . . 9
9128, 7, 36, 83, 8atmod3i1 30346 . . . . . . . . 9
923, 5, 88, 35, 90, 91syl131anc 1197 . . . . . . . 8
93 eqid 2404 . . . . . . . . . . . 12
947, 36, 93, 8, 9lhpjat2 30503 . . . . . . . . . . 11
952, 4, 94syl2anc 643 . . . . . . . . . 10
9695oveq2d 6056 . . . . . . . . 9
97 hlol 29844 . . . . . . . . . . 11
983, 97syl 16 . . . . . . . . . 10
9928, 83, 93olm11 29710 . . . . . . . . . 10
10098, 88, 99syl2anc 643 . . . . . . . . 9
10196, 100eqtrd 2436 . . . . . . . 8
10292, 101eqtrd 2436 . . . . . . 7
10386, 102eqtrd 2436 . . . . . 6
10482, 103breqtrrd 4198 . . . . 5
105 dia2dimlem1.rf . . . . . . 7
10636, 8hlatjcom 29850 . . . . . . . 8
1073, 15, 21, 106syl3anc 1184 . . . . . . 7
108105, 107breqtrd 4196 . . . . . 6
109 dia2dimlem1.ru . . . . . . 7
1107, 36, 8hlatexch2 29878 . . . . . . 7
1113, 13, 21, 15, 109, 110syl131anc 1197 . . . . . 6
112108, 111mpd 15 . . . . 5
113104, 112jca 519 . . . 4
1147, 36, 83, 8ps-2c 30010 . . . 4
1153, 5, 13, 15, 19, 21, 53, 80, 113, 114syl333anc 1216 . . 3
1161, 115syl5eqel 2488 . 2
11728, 36, 8hlatjcl 29849 . . . . . . . . . . . . 13
1183, 5, 15, 117syl3anc 1184 . . . . . . . . . . . 12
11928, 36, 8hlatjcl 29849 . . . . . . . . . . . . 13
1203, 19, 21, 119syl3anc 1184 . . . . . . . . . . . 12
12128, 7, 83latmle1 14460 . . . . . . . . . . . 12
12227, 118, 120, 121syl3anc 1184 . . . . . . . . . . 11
1231, 122syl5eqbr 4205 . . . . . . . . . 10
12428, 8atbase 29772 . . . . . . . . . . . . 13
125116, 124syl 16 . . . . . . . . . . . 12
12628, 7, 83latlem12 14462 . . . . . . . . . . . 12
12727, 125, 118, 35, 126syl13anc 1186 . . . . . . . . . . 11
128127biimpd 199 . . . . . . . . . 10
129123, 128mpand 657 . . . . . . . . 9
130129imp 419 . . . . . . . 8
131 eqid 2404 . . . . . . . . . . . . 13
1327, 83, 131, 8, 9lhpmat 30512 . . . . . . . . . . . 12
1332, 4, 132syl2anc 643 . . . . . . . . . . 11
134133oveq1d 6055 . . . . . . . . . 10
13528, 7, 36, 83, 8atmod4i1 30348 . . . . . . . . . . 11
1363, 15, 41, 35, 25, 135syl131anc 1197 . . . . . . . . . 10
13728, 36, 131olj02 29709 . . . . . . . . . . 11
13898, 32, 137syl2anc 643 . . . . . . . . . 10
139134, 136, 1383eqtr3d 2444 . . . . . . . . 9
140139adantr 452 . . . . . . . 8
141130, 140breqtrd 4196 . . . . . . 7
142 hlatl 29843 . . . . . . . . . 10
1433, 142syl 16 . . . . . . . . 9
144143adantr 452 . . . . . . . 8
145116adantr 452 . . . . . . . 8
14615adantr 452 . . . . . . . 8
1477, 8atcmp 29794 . . . . . . . 8
148144, 145, 146, 147syl3anc 1184 . . . . . . 7
149141, 148mpbid 202 . . . . . 6
15028, 7, 83latmle2 14461 . . . . . . . . . . . 12
15127, 118, 120, 150syl3anc 1184 . . . . . . . . . . 11
1521, 151syl5eqbr 4205 . . . . . . . . . 10
15328, 7, 83latlem12 14462 . . . . . . . . . . . 12
15427, 125, 120, 35, 153syl13anc 1186 . . . . . . . . . . 11
155154biimpd 199 . . . . . . . . . 10
156152, 155mpand 657 . . . . . . . . 9
157156imp 419 . . . . . . . 8
1587, 83, 131, 8, 9lhpmat 30512 . . . . . . . . . . . 12
1592, 18, 158syl2anc 643 . . . . . . . . . . 11
160159oveq1d 6055 . . . . . . . . . 10
16128, 8atbase 29772 . . . . . . . . . . . 12
16219, 161syl 16 . . . . . . . . . . 11
16328, 7, 36, 83, 8atmod4i1 30348 . . . . . . . . . . 11
1643, 21, 162, 35, 48, 163syl131anc 1197 . . . . . . . . . 10
16528, 36, 131olj02 29709 . . . . . . . . . . 11
16698, 72, 165syl2anc 643 . . . . . . . . . 10
167160, 164, 1663eqtr3d 2444 . . . . . . . . 9
168167adantr 452 . . . . . . . 8
169157, 168breqtrd 4196 . . . . . . 7
17021adantr 452 . . . . . . . 8
1717, 8atcmp 29794 . . . . . . . 8
172144, 145, 170, 171syl3anc 1184 . . . . . . 7
173169, 172mpbid 202 . . . . . 6
174149, 173eqtr3d 2438 . . . . 5
175174ex 424 . . . 4