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

Theorem dia2dimlem9 32266
Description: Lemma for dia2dim 32271. Eliminate , conditions. (Contributed by NM, 8-Sep-2014.)
Hypotheses
Ref Expression
dia2dimlem9.l
dia2dimlem9.j
dia2dimlem9.m
dia2dimlem9.a
dia2dimlem9.h
dia2dimlem9.t
dia2dimlem9.r
dia2dimlem9.y
dia2dimlem9.s
dia2dimlem9.pl
dia2dimlem9.n
dia2dimlem9.i
dia2dimlem9.k
dia2dimlem9.u
dia2dimlem9.v
dia2dimlem9.f
dia2dimlem9.rf
dia2dimlem9.uv
Assertion
Ref Expression
dia2dimlem9

Proof of Theorem dia2dimlem9
StepHypRef Expression
1 dia2dimlem9.k . . . . . . 7
2 dia2dimlem9.h . . . . . . . 8
3 dia2dimlem9.y . . . . . . . 8
42, 3dvalvec 32220 . . . . . . 7
5 lveclmod 16214 . . . . . . 7
6 dia2dimlem9.s . . . . . . . 8
76lsssssubg 16070 . . . . . . 7
81, 4, 5, 74syl 20 . . . . . 6
9 dia2dimlem9.u . . . . . . . . 9
109simpld 447 . . . . . . . 8
11 eqid 2447 . . . . . . . . 9
12 dia2dimlem9.a . . . . . . . . 9
1311, 12atbase 30483 . . . . . . . 8
1410, 13syl 16 . . . . . . 7
159simprd 451 . . . . . . 7
16 dia2dimlem9.l . . . . . . . 8
17 dia2dimlem9.i . . . . . . . 8
1811, 16, 2, 3, 17, 6dialss 32240 . . . . . . 7
191, 14, 15, 18syl12anc 1183 . . . . . 6
208, 19sseldd 3342 . . . . 5
21 dia2dimlem9.v . . . . . . . . 9
2221simpld 447 . . . . . . . 8
2311, 12atbase 30483 . . . . . . . 8
2422, 23syl 16 . . . . . . 7
2521simprd 451 . . . . . . 7
2611, 16, 2, 3, 17, 6dialss 32240 . . . . . . 7
271, 24, 25, 26syl12anc 1183 . . . . . 6
288, 27sseldd 3342 . . . . 5
29 dia2dimlem9.pl . . . . . 6
3029lsmub1 15326 . . . . 5
3120, 28, 30syl2anc 644 . . . 4
3231adantr 453 . . 3
33 dia2dimlem9.f . . . . . 6
34 dia2dimlem9.t . . . . . . 7
35 dia2dimlem9.r . . . . . . 7
362, 34, 35, 17dia1dimid 32257 . . . . . 6
371, 33, 36syl2anc 644 . . . . 5
3837adantr 453 . . . 4
39 fveq2 5779 . . . . 5
4039adantl 454 . . . 4
4138, 40eleqtrd 2523 . . 3
4232, 41sseldd 3342 . 2
4320adantr 453 . . . 4
4428adantr 453 . . . 4
4529lsmub2 15327 . . . 4
4643, 44, 45syl2anc 644 . . 3
4737adantr 453 . . . 4
48 fveq2 5779 . . . . 5
4948adantl 454 . . . 4
5047, 49eleqtrd 2523 . . 3
5146, 50sseldd 3342 . 2
52 dia2dimlem9.j . . 3
53 dia2dimlem9.m . . 3
54 dia2dimlem9.n . . 3
551adantr 453 . . 3
569adantr 453 . . 3
5721adantr 453 . . 3
5833adantr 453 . . 3
59 dia2dimlem9.rf . . . 4
6059adantr 453 . . 3
61 dia2dimlem9.uv . . . 4
6261adantr 453 . . 3
63 simprl 734 . . 3
64 simprr 735 . . 3
6516, 52, 53, 12, 2, 34, 35, 3, 6, 29, 54, 17, 55, 56, 57, 58, 60, 62, 63, 64dia2dimlem8 32265 . 2
6642, 51, 65pm2.61da2ne 2694 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  /\wa 360  =wceq 1654  e.wcel 1728  =/=wne 2610  C_wss 3313   class class class wbr 4247  `cfv 5505  (class class class)co 6133   cbs 13524   cple 13591   cjn 14456   cmee 14457   csubg 14974   clsm 15304   clmod 15986   clss 16044   clspn 16083   clvec 16210   catm 30457   chlt 30544   clh 31177   cltrn 31294   ctrl 31351   cdveca 32195   cdia 32222
This theorem is referenced by:  dia2dimlem11  32268
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-13 1730  ax-14 1732  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1955  ax-ext 2428  ax-rep 4358  ax-sep 4368  ax-nul 4376  ax-pow 4420  ax-pr 4446  ax-un 4746  ax-cnex 9101  ax-resscn 9102  ax-1cn 9103  ax-icn 9104  ax-addcl 9105  ax-addrcl 9106  ax-mulcl 9107  ax-mulrcl 9108  ax-mulcom 9109  ax-addass 9110  ax-mulass 9111  ax-distr 9112  ax-i2m1 9113  ax-1ne0 9114  ax-1rid 9115  ax-rnegex 9116  ax-rrecex 9117  ax-cnre 9118  ax-pre-lttri 9119  ax-pre-lttrn 9120  ax-pre-ltadd 9121  ax-pre-mulgt0 9122
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-fal 1330  df-ex 1552  df-nf 1555  df-sb 1661  df-eu 2296  df-mo 2297  df-clab 2434  df-cleq 2440  df-clel 2443  df-nfc 2572  df-ne 2612  df-nel 2613  df-ral 2721  df-rex 2722  df-reu 2723  df-rmo 2724  df-rab 2725  df-v 2971  df-sbc 3175  df-csb 3275  df-dif 3316  df-un 3318  df-in 3320  df-ss 3327  df-pss 3329  df-nul 3621  df-if 3770  df-pw 3832  df-sn 3851  df-pr 3852  df-tp 3853  df-op 3854  df-uni 4048  df-int 4084  df-iun 4128  df-iin 4129  df-br 4248  df-opab 4306  df-mpt 4307  df-tr 4341  df-eprel 4539  df-id 4543  df-po 4548  df-so 4549  df-fr 4586  df-we 4588  df-ord 4629  df-on 4630  df-lim 4631  df-suc 4632  df-om 4891  df-xp 4929  df-rel 4930  df-cnv 4931  df-co 4932  df-dm 4933  df-rn 4934  df-res 4935  df-ima 4936  df-iota 5468  df-fun 5507  df-fn 5508  df-f 5509  df-f1 5510  df-fo 5511  df-f1o 5512  df-fv 5513  df-ov 6136  df-oprab 6137  df-mpt2 6138  df-1st 6403  df-2nd 6404  df-tpos 6533  df-undef 6597  df-riota 6603  df-recs 6686  df-rdg 6721  df-1o 6777  df-oadd 6781  df-er 6958  df-map 7073  df-en 7163  df-dom 7164  df-sdom 7165  df-fin 7166  df-pnf 9177  df-mnf 9178  df-xr 9179  df-ltxr 9180  df-le 9181  df-sub 9348  df-neg 9349  df-nn 10056  df-2 10113  df-3 10114  df-4 10115  df-5 10116  df-6 10117  df-n0 10277  df-z 10338  df-uz 10544  df-fz 11099  df-struct 13526  df-ndx 13527  df-slot 13528  df-base 13529  df-sets 13530  df-ress 13531  df-plusg 13597  df-mulr 13598  df-sca 13600  df-vsca 13601  df-0g 13782  df-poset 14458  df-plt 14470  df-lub 14486  df-glb 14487  df-join 14488  df-meet 14489  df-p0 14523  df-p1 14524  df-lat 14530  df-clat 14592  df-mnd 14726  df-submnd 14775  df-grp 14848  df-minusg 14849  df-sbg 14850  df-subg 14977  df-cntz 15152  df-lsm 15306  df-cmn 15450  df-abl 15451  df-mgp 15685  df-rng 15699  df-ur 15701  df-oppr 15764  df-dvdsr 15782  df-unit 15783  df-invr 15813  df-dvr 15824  df-drng 15873  df-lmod 15988  df-lss 16045  df-lsp 16084  df-lvec 16211  df-oposet 30370  df-ol 30372  df-oml 30373  df-covers 30460  df-ats 30461  df-atl 30492  df-cvlat 30516  df-hlat 30545  df-llines 30691  df-lplanes 30692  df-lvols 30693  df-lines 30694  df-psubsp 30696  df-pmap 30697  df-padd 30989  df-lhyp 31181  df-laut 31182  df-ldil 31297  df-ltrn 31298  df-trl 31352  df-tgrp 31936  df-tendo 31948  df-edring 31950  df-dveca 32196  df-disoa 32223
  Copyright terms: Public domain W3C validator