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

Theorem dia2dimlem13 31948
 Description: Lemma for dia2dim 31949. Eliminate condition. (Contributed by NM, 8-Sep-2014.)
Hypotheses
Ref Expression
dia2dimlem12.l
dia2dimlem12.j
dia2dimlem12.m
dia2dimlem12.a
dia2dimlem12.h
dia2dimlem12.t
dia2dimlem12.r
dia2dimlem12.y
dia2dimlem12.s
dia2dimlem12.pl
dia2dimlem12.n
dia2dimlem12.i
dia2dimlem12.k
dia2dimlem12.u
dia2dimlem12.v
Assertion
Ref Expression
dia2dimlem13

Proof of Theorem dia2dimlem13
StepHypRef Expression
1 oveq2 6092 . . . . . . 7
21adantl 454 . . . . . 6
3 dia2dimlem12.k . . . . . . . . 9
43simpld 447 . . . . . . . 8
5 dia2dimlem12.u . . . . . . . . 9
65simpld 447 . . . . . . . 8
7 dia2dimlem12.j . . . . . . . . 9
8 dia2dimlem12.a . . . . . . . . 9
97, 8hlatjidm 30240 . . . . . . . 8
104, 6, 9syl2anc 644 . . . . . . 7
1110adantr 453 . . . . . 6
122, 11eqtr3d 2472 . . . . 5
1312fveq2d 5735 . . . 4
14 ssid 3369 . . . 4
1513, 14syl6eqss 3400 . . 3
16 dia2dimlem12.h . . . . . . . 8
17 dia2dimlem12.y . . . . . . . 8
1816, 17dvalvec 31898 . . . . . . 7
19 lveclmod 16183 . . . . . . 7
203, 18, 193syl 19 . . . . . 6
21 eqid 2438 . . . . . . . . 9
2221, 8atbase 30161 . . . . . . . 8
236, 22syl 16 . . . . . . 7
245simprd 451 . . . . . . 7
25 dia2dimlem12.l . . . . . . . 8
26 dia2dimlem12.i . . . . . . . 8
27 dia2dimlem12.s . . . . . . . 8
2821, 25, 16, 17, 26, 27dialss 31918 . . . . . . 7
293, 23, 24, 28syl12anc 1183 . . . . . 6
3027lsssubg 16038 . . . . . 6 SubGrp
3120, 29, 30syl2anc 644 . . . . 5 SubGrp
32 dia2dimlem12.pl . . . . . 6
3332lsmidm 15301 . . . . 5 SubGrp
3431, 33syl 16 . . . 4
35 fveq2 5731 . . . . 5
3635oveq2d 6100 . . . 4
3734, 36sylan9req 2491 . . 3
3815, 37sseqtrd 3386 . 2
39 dia2dimlem12.m . . 3
40 dia2dimlem12.t . . 3
41 dia2dimlem12.r . . 3
42 dia2dimlem12.n . . 3