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

Theorem dia2dimlem7 31795
 Description: Lemma for dia2dim 31802. Eliminate condition. (Contributed by NM, 8-Sep-2014.)
Hypotheses
Ref Expression
dia2dimlem7.l
dia2dimlem7.j
dia2dimlem7.m
dia2dimlem7.a
dia2dimlem7.h
dia2dimlem7.t
dia2dimlem7.r
dia2dimlem7.y
dia2dimlem7.s
dia2dimlem7.pl
dia2dimlem7.n
dia2dimlem7.i
dia2dimlem7.q
dia2dimlem7.k
dia2dimlem7.u
dia2dimlem7.v
dia2dimlem7.p
dia2dimlem7.f
dia2dimlem7.rf
dia2dimlem7.uv
dia2dimlem7.ru
dia2dimlem7.rv
Assertion
Ref Expression
dia2dimlem7

Proof of Theorem dia2dimlem7
StepHypRef Expression
1 dia2dimlem7.k . . . . 5
2 dia2dimlem7.f . . . . 5
3 dia2dimlem7.p . . . . 5
4 eqid 2435 . . . . . 6
5 dia2dimlem7.l . . . . . 6
6 dia2dimlem7.a . . . . . 6
7 dia2dimlem7.h . . . . . 6
8 dia2dimlem7.t . . . . . 6
94, 5, 6, 7, 8ltrnideq 30899 . . . . 5
101, 2, 3, 9syl3anc 1184 . . . 4
11 dia2dimlem7.y . . . . . . . 8
12 eqid 2435 . . . . . . . 8
134, 7, 8, 11, 12dva0g 31752 . . . . . . 7
141, 13syl 16 . . . . . 6
157, 11dvalvec 31751 . . . . . . . 8
16 lveclmod 16170 . . . . . . . 8
171, 15, 163syl 19 . . . . . . 7
18 dia2dimlem7.u . . . . . . . . . . 11
1918simpld 446 . . . . . . . . . 10
204, 6atbase 30014 . . . . . . . . . 10
2119, 20syl 16 . . . . . . . . 9
2218simprd 450 . . . . . . . . 9
23 dia2dimlem7.i . . . . . . . . . 10
24 dia2dimlem7.s . . . . . . . . . 10
254, 5, 7, 11, 23, 24dialss 31771 . . . . . . . . 9
261, 21, 22, 25syl12anc 1182 . . . . . . . 8
27 dia2dimlem7.v . . . . . . . . . . 11
2827simpld 446 . . . . . . . . . 10
294, 6atbase 30014 . . . . . . . . . 10
3028, 29syl 16 . . . . . . . . 9
3127simprd 450 . . . . . . . . 9
324, 5, 7, 11, 23, 24dialss 31771 . . . . . . . . 9
331, 30, 31, 32syl12anc 1182 . . . . . . . 8
34 dia2dimlem7.pl . . . . . . . . 9
3524, 34lsmcl 16147 . . . . . . . 8
3617, 26, 33, 35syl3anc 1184 . . . . . . 7
3712, 24lss0cl 16015 . . . . . . 7
3817, 36, 37syl2anc 643 . . . . . 6
3914, 38eqeltrrd 2510 . . . . 5
40 eleq1a 2504 . . . . 5
4139, 40syl 16 . . . 4
4210, 41sylbird 227 . . 3
4342imp 419 . 2
44 dia2dimlem7.j . . 3
45 dia2dimlem7.m . . 3
46 dia2dimlem7.r . . 3
47 dia2dimlem7.n . . 3
48 dia2dimlem7.q . . 3