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

Theorem diclspsn 31617
 Description: The value of isomorphism C is spanned by vector . Part of proof of Lemma N of [Crawley] p. 121 line 29. (Contributed by NM, 21-Feb-2014.) (Revised by Mario Carneiro, 24-Jun-2014.)
Hypotheses
Ref Expression
diclspsn.l
diclspsn.a
diclspsn.h
diclspsn.p
diclspsn.t
diclspsn.i
diclspsn.u
diclspsn.n
diclspsn.f
Assertion
Ref Expression
diclspsn
Distinct variable groups:   ,   ,   ,   ,   ,   ,   ,   ,
Allowed substitution hints:   ()   ()   ()   ()

Proof of Theorem diclspsn
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-rab 2672 . . 3 Scalar Scalar
2 relopab 4955 . . . . 5
3 diclspsn.l . . . . . . 7
4 diclspsn.a . . . . . . 7
5 diclspsn.h . . . . . . 7
6 diclspsn.p . . . . . . 7
7 diclspsn.t . . . . . . 7
8 eqid 2401 . . . . . . 7
9 diclspsn.i . . . . . . 7
10 diclspsn.f . . . . . . 7
113, 4, 5, 6, 7, 8, 9, 10dicval2 31602 . . . . . 6
1211releqd 4915 . . . . 5
132, 12mpbiri 225 . . . 4
14 ssrab2 3385 . . . . . 6 Scalar
15 relxp 4937 . . . . . 6
16 relss 4917 . . . . . 6 Scalar Scalar
1714, 15, 16mp2 9 . . . . 5 Scalar
1817a1i 11 . . . 4 Scalar
19 id 20 . . . 4
20 vex 2916 . . . . . . 7
21 vex 2916 . . . . . . 7
223, 4, 5, 6, 7, 8, 9, 10, 20, 21dicopelval2 31604 . . . . . 6
23 simprl 733 . . . . . . . . . . 11
24 simpll 731 . . . . . . . . . . . 12
25 simprr 734 . . . . . . . . . . . 12
26 simpl 444 . . . . . . . . . . . . . 14
273, 4, 5, 6lhpocnel2 30441 . . . . . . . . . . . . . . 15
2827adantr 452 . . . . . . . . . . . . . 14
29 simpr 448 . . . . . . . . . . . . . 14
303, 4, 5, 7, 10ltrniotacl 31001 . . . . . . . . . . . . . 14
3126, 28, 29, 30syl3anc 1184 . . . . . . . . . . . . 13
3231adantr 452 . . . . . . . . . . . 12
335, 7, 8tendocl 31189 . . . . . . . . . . . 12
3424, 25, 32, 33syl3anc 1184 . . . . . . . . . . 11
3523, 34eqeltrd 2475 . . . . . . . . . 10
3635, 25, 233jca 1134 . . . . . . . . 9
37 simpr3 965 . . . . . . . . . 10
38 simpr2 964 . . . . . . . . . 10
3937, 38jca 519 . . . . . . . . 9
4036, 39impbida 806 . . . . . . . 8
41 diclspsn.u . . . . . . . . . . . . . 14
42 eqid 2401 . . . . . . . . . . . . . 14 Scalar Scalar
43 eqid 2401 . . . . . . . . . . . . . 14 Scalar Scalar
445, 8, 41, 42, 43dvhbase 31506 . . . . . . . . . . . . 13 Scalar
4544adantr 452 . . . . . . . . . . . 12 Scalar
4645rexeqdv 2868 . . . . . . . . . . 11 Scalar
47 simpll 731 . . . . . . . . . . . . . . . . 17
48 simpr 448 . . . . . . . . . . . . . . . . 17
4931adantr 452 . . . . . . . . . . . . . . . . 17
505, 7, 8tendoidcl 31191 . . . . . . . . . . . . . . . . . 18
5150ad2antrr 707 . . . . . . . . . . . . . . . . 17
52 eqid 2401 . . . . . . . . . . . . . . . . . 18
535, 7, 8, 41, 52dvhopvsca 31525 . . . . . . . . . . . . . . . . 17
5447, 48, 49, 51, 53syl13anc 1186 . . . . . . . . . . . . . . . 16
5554eqeq2d 2412 . . . . . . . . . . . . . . 15
5620, 21opth 4390 . . . . . . . . . . . . . . 15
5755, 56syl6bb 253 . . . . . . . . . . . . . 14
585, 7, 8tendo1mulr 31193 . . . . . . . . . . . . . . . . . 18
5958adantlr 696 . . . . . . . . . . . . . . . . 17
6059eqeq2d 2412 . . . . . . . . . . . . . . . 16
61 equcom 1688 . . . . . . . . . . . . . . . 16
6260, 61syl6bb 253 . . . . . . . . . . . . . . 15
6362anbi2d 685 . . . . . . . . . . . . . 14
6457, 63bitrd 245 . . . . . . . . . . . . 13
65 ancom 438 . . . . . . . . . . . . 13
6664, 65syl6bb 253 . . . . . . . . . . . 12
6766rexbidva 2680 . . . . . . . . . . 11
6846, 67bitrd 245 . . . . . . . . . 10 Scalar
69683anbi3d 1260 . . . . . . . . 9 Scalar
70 fveq1 5681 . . . . . . . . . . . . . 14
7170eqeq2d 2412 . . . . . . . . . . . . 13
7271ceqsrexv 3026 . . . . . . . . . . . 12
7372pm5.32i 619 . . . . . . . . . . 11
7473anbi2i 676 . . . . . . . . . 10
75 3anass 940 . . . . . . . . . 10
76 3anass 940 . . . . . . . . . 10
7774, 75, 763bitr4i 269 . . . . . . . . 9
7869, 77syl6rbb 254 . . . . . . . 8 Scalar
7940, 78bitrd 245 . . . . . . 7 Scalar
80 eqeq1 2407 . . . . . . . . . . 11
8180rexbidv 2684 . . . . . . . . . 10 Scalar Scalar
8281rabxp 4868 . . . . . . . . 9 Scalar Scalar
8382eleq2i 2465 . . . . . . . 8 Scalar Scalar
84 opabid 4416 . . . . . . . 8 Scalar Scalar
8583, 84bitr2i 242 . . . . . . 7 Scalar Scalar
8679, 85syl6bb 253 . . . . . 6 Scalar
8722, 86bitrd 245 . . . . 5 Scalar
8887eqrelrdv2 4929 . . . 4 Scalar Scalar
8913, 18, 19, 88syl21anc 1183 . . 3 Scalar
90 simpll 731 . . . . . . . 8 Scalar
9145eleq2d 2468 . . . . . . . . 9 Scalar
9291biimpa 471 . . . . . . . 8 Scalar
9350adantr 452 . . . . . . . . . 10
94 opelxpi 4864 . . . . . . . . . 10
9531, 93, 94syl2anc 643 . . . . . . . . 9
9695adantr 452 . . . . . . . 8 Scalar
975, 7, 8, 41, 52dvhvscacl 31526 . . . . . . . 8
9890, 92, 96, 97syl12anc 1182 . . . . . . 7 Scalar
99 eleq1a 2470 . . . . . . 7
10098, 99syl 16 . . . . . 6 Scalar
101100rexlimdva 2787 . . . . 5 Scalar
102101pm4.71rd 617 . . . 4 Scalar Scalar
103102abbidv 2515 . . 3 Scalar Scalar
1041, 89, 1033eqtr4a 2459 . 2 Scalar
1055, 41, 26dvhlmod 31533 . . 3
106 eqid 2401 . . . . 5
1075, 7, 8, 41, 106dvhelvbasei 31511 . . . 4
10826, 31, 93, 107syl12anc 1182 . . 3
109 diclspsn.n . . . 4
11042, 43, 106, 52, 109lspsn 16019 . . 3 Scalar
111105, 108, 110syl2anc 643 . 2 Scalar
112104, 111eqtr4d 2436 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wa 359   w3a 936   wceq 1649   wcel 1721  cab 2387  wrex 2664  crab 2667   wss 3277  csn 3771  cop 3774   class class class wbr 4167  copab 4220   cid 4448   cxp 4830   cres 4834   ccom 4836   wrel 4837  cfv 5408  (class class class)co 6034  crio 6492  cbs 13410  Scalarcsca 13473  cvsca 13474  cple 13477  coc 13478  clmod 15891  clspn 15988  catm 29686  chlt 29773  clh 30406  cltrn 30523  ctendo 31174  cdvh 31501  cdic 31595 This theorem is referenced by:  cdlemn5pre  31623  dih1dimc  31665 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2382  ax-rep 4275  ax-sep 4285  ax-nul 4293  ax-pow 4332  ax-pr 4358  ax-un 4655  ax-cnex 8993  ax-resscn 8994  ax-1cn 8995  ax-icn 8996  ax-addcl 8997  ax-addrcl 8998  ax-mulcl 8999  ax-mulrcl 9000  ax-mulcom 9001  ax-addass 9002  ax-mulass 9003  ax-distr 9004  ax-i2m1 9005  ax-1ne0 9006  ax-1rid 9007  ax-rnegex 9008  ax-rrecex 9009  ax-cnre 9010  ax-pre-lttri 9011  ax-pre-lttrn 9012  ax-pre-ltadd 9013  ax-pre-mulgt0 9014 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-fal 1326  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2256  df-mo 2257  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2526  df-ne 2566  df-nel 2567  df-ral 2668  df-rex 2669  df-reu 2670  df-rmo 2671  df-rab 2672  df-v 2915  df-sbc 3119  df-csb 3209  df-dif 3280  df-un 3282  df-in 3284  df-ss 3291  df-pss 3293  df-nul 3586  df-if 3697  df-pw 3758  df-sn 3777  df-pr 3778  df-tp 3779  df-op 3780  df-uni 3972  df-int 4007  df-iun 4051  df-iin 4052  df-br 4168  df-opab 4222  df-mpt 4223  df-tr 4258  df-eprel 4449  df-id 4453  df-po 4458  df-so 4459  df-fr 4496  df-we 4498  df-ord 4539  df-on 4540  df-lim 4541  df-suc 4542  df-om 4800  df-xp 4838  df-rel 4839  df-cnv 4840  df-co 4841  df-dm 4842  df-rn 4843  df-res 4844  df-ima 4845  df-iota 5372  df-fun 5410  df-fn 5411  df-f 5412  df-f1 5413  df-fo 5414  df-f1o 5415  df-fv 5416  df-ov 6037  df-oprab 6038  df-mpt2 6039  df-1st 6302  df-2nd 6303  df-tpos 6429  df-undef 6493  df-riota 6499  df-recs 6583  df-rdg 6618  df-1o 6674  df-oadd 6678  df-er 6855  df-map 6970  df-en 7060  df-dom 7061  df-sdom 7062  df-fin 7063  df-pnf 9069  df-mnf 9070  df-xr 9071  df-ltxr 9072  df-le 9073  df-sub 9239  df-neg 9240  df-nn 9947  df-2 10004  df-3 10005  df-4 10006  df-5 10007  df-6 10008  df-n0 10168  df-z 10229  df-uz 10435  df-fz 10990  df-struct 13412  df-ndx 13413  df-slot 13414  df-base 13415  df-sets 13416  df-ress 13417  df-plusg 13483  df-mulr 13484  df-sca 13486  df-vsca 13487  df-0g 13668  df-poset 14344  df-plt 14356  df-lub 14372  df-glb 14373  df-join 14374  df-meet 14375  df-p0 14409  df-p1 14410  df-lat 14416  df-clat 14478  df-mnd 14631  df-grp 14753  df-minusg 14754  df-sbg 14755  df-mgp 15590  df-rng 15604  df-ur 15606  df-oppr 15669  df-dvdsr 15687  df-unit 15688  df-invr 15718  df-dvr 15729  df-drng 15778  df-lmod 15893  df-lss 15950  df-lsp 15989  df-lvec 16116  df-oposet 29599  df-ol 29601  df-oml 29602  df-covers 29689  df-ats 29690  df-atl 29721  df-cvlat 29745  df-hlat 29774  df-llines 29920  df-lplanes 29921  df-lvols 29922  df-lines 29923  df-psubsp 29925  df-pmap 29926  df-padd 30218  df-lhyp 30410  df-laut 30411  df-ldil 30526  df-ltrn 30527  df-trl 30581  df-tendo 31177  df-edring 31179  df-dvech 31502  df-dic 31596
 Copyright terms: Public domain W3C validator