![]() |
Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > mapdrvallem3 | Structured version Visualization version GIF version |
Description: Lemma for mapdrval 40223. (Contributed by NM, 2-Feb-2015.) |
Ref | Expression |
---|---|
mapdrval.h | β’ π» = (LHypβπΎ) |
mapdrval.o | β’ π = ((ocHβπΎ)βπ) |
mapdrval.m | β’ π = ((mapdβπΎ)βπ) |
mapdrval.u | β’ π = ((DVecHβπΎ)βπ) |
mapdrval.s | β’ π = (LSubSpβπ) |
mapdrval.f | β’ πΉ = (LFnlβπ) |
mapdrval.l | β’ πΏ = (LKerβπ) |
mapdrval.d | β’ π· = (LDualβπ) |
mapdrval.t | β’ π = (LSubSpβπ·) |
mapdrval.c | β’ πΆ = {π β πΉ β£ (πβ(πβ(πΏβπ))) = (πΏβπ)} |
mapdrval.k | β’ (π β (πΎ β HL β§ π β π»)) |
mapdrval.r | β’ (π β π β π) |
mapdrval.e | β’ (π β π β πΆ) |
mapdrval.q | β’ π = βͺ β β π (πβ(πΏββ)) |
mapdrval.v | β’ π = (Baseβπ) |
mapdrvallem2.a | β’ π΄ = (LSAtomsβπ) |
mapdrvallem2.n | β’ π = (LSpanβπ) |
mapdrvallem2.z | β’ 0 = (0gβπ) |
mapdrvallem2.y | β’ π = (0gβπ·) |
Ref | Expression |
---|---|
mapdrvallem3 | β’ (π β {π β πΆ β£ (πβ(πΏβπ)) β π} = π ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mapdrval.h | . . 3 β’ π» = (LHypβπΎ) | |
2 | mapdrval.o | . . 3 β’ π = ((ocHβπΎ)βπ) | |
3 | mapdrval.m | . . 3 β’ π = ((mapdβπΎ)βπ) | |
4 | mapdrval.u | . . 3 β’ π = ((DVecHβπΎ)βπ) | |
5 | mapdrval.s | . . 3 β’ π = (LSubSpβπ) | |
6 | mapdrval.f | . . 3 β’ πΉ = (LFnlβπ) | |
7 | mapdrval.l | . . 3 β’ πΏ = (LKerβπ) | |
8 | mapdrval.d | . . 3 β’ π· = (LDualβπ) | |
9 | mapdrval.t | . . 3 β’ π = (LSubSpβπ·) | |
10 | mapdrval.c | . . 3 β’ πΆ = {π β πΉ β£ (πβ(πβ(πΏβπ))) = (πΏβπ)} | |
11 | mapdrval.k | . . 3 β’ (π β (πΎ β HL β§ π β π»)) | |
12 | mapdrval.r | . . 3 β’ (π β π β π) | |
13 | mapdrval.e | . . 3 β’ (π β π β πΆ) | |
14 | mapdrval.q | . . 3 β’ π = βͺ β β π (πβ(πΏββ)) | |
15 | mapdrval.v | . . 3 β’ π = (Baseβπ) | |
16 | mapdrvallem2.a | . . 3 β’ π΄ = (LSAtomsβπ) | |
17 | mapdrvallem2.n | . . 3 β’ π = (LSpanβπ) | |
18 | mapdrvallem2.z | . . 3 β’ 0 = (0gβπ) | |
19 | mapdrvallem2.y | . . 3 β’ π = (0gβπ·) | |
20 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19 | mapdrvallem2 40221 | . 2 β’ (π β {π β πΆ β£ (πβ(πΏβπ)) β π} β π ) |
21 | 2fveq3 6874 | . . . . . 6 β’ (β = π β (πβ(πΏββ)) = (πβ(πΏβπ))) | |
22 | 21 | ssiun2s 5035 | . . . . 5 β’ (π β π β (πβ(πΏβπ)) β βͺ β β π (πβ(πΏββ))) |
23 | 22 | adantl 482 | . . . 4 β’ ((π β§ π β π ) β (πβ(πΏβπ)) β βͺ β β π (πβ(πΏββ))) |
24 | 23, 14 | sseqtrrdi 4020 | . . 3 β’ ((π β§ π β π ) β (πβ(πΏβπ)) β π) |
25 | 13, 24 | ssrabdv 4058 | . 2 β’ (π β π β {π β πΆ β£ (πβ(πΏβπ)) β π}) |
26 | 20, 25 | eqssd 3986 | 1 β’ (π β {π β πΆ β£ (πβ(πΏβπ)) β π} = π ) |
Colors of variables: wff setvar class |
Syntax hints: β wi 4 β§ wa 396 = wceq 1541 β wcel 2106 {crab 3425 β wss 3935 βͺ ciun 4981 βcfv 6523 Basecbs 17116 0gc0g 17357 LSubSpclss 20471 LSpanclspn 20511 LSAtomsclsa 37549 LFnlclfn 37632 LKerclk 37660 LDualcld 37698 HLchlt 37925 LHypclh 38560 DVecHcdvh 39654 ocHcoch 39923 mapdcmpd 40200 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2702 ax-rep 5269 ax-sep 5283 ax-nul 5290 ax-pow 5347 ax-pr 5411 ax-un 7699 ax-cnex 11138 ax-resscn 11139 ax-1cn 11140 ax-icn 11141 ax-addcl 11142 ax-addrcl 11143 ax-mulcl 11144 ax-mulrcl 11145 ax-mulcom 11146 ax-addass 11147 ax-mulass 11148 ax-distr 11149 ax-i2m1 11150 ax-1ne0 11151 ax-1rid 11152 ax-rnegex 11153 ax-rrecex 11154 ax-cnre 11155 ax-pre-lttri 11156 ax-pre-lttrn 11157 ax-pre-ltadd 11158 ax-pre-mulgt0 11159 ax-riotaBAD 37528 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ne 2940 df-nel 3046 df-ral 3061 df-rex 3070 df-rmo 3371 df-reu 3372 df-rab 3426 df-v 3468 df-sbc 3765 df-csb 3881 df-dif 3938 df-un 3940 df-in 3942 df-ss 3952 df-pss 3954 df-nul 4310 df-if 4514 df-pw 4589 df-sn 4614 df-pr 4616 df-tp 4618 df-op 4620 df-uni 4893 df-int 4935 df-iun 4983 df-iin 4984 df-br 5133 df-opab 5195 df-mpt 5216 df-tr 5250 df-id 5558 df-eprel 5564 df-po 5572 df-so 5573 df-fr 5615 df-we 5617 df-xp 5666 df-rel 5667 df-cnv 5668 df-co 5669 df-dm 5670 df-rn 5671 df-res 5672 df-ima 5673 df-pred 6280 df-ord 6347 df-on 6348 df-lim 6349 df-suc 6350 df-iota 6475 df-fun 6525 df-fn 6526 df-f 6527 df-f1 6528 df-fo 6529 df-f1o 6530 df-fv 6531 df-riota 7340 df-ov 7387 df-oprab 7388 df-mpo 7389 df-of 7644 df-om 7830 df-1st 7948 df-2nd 7949 df-tpos 8184 df-undef 8231 df-frecs 8239 df-wrecs 8270 df-recs 8344 df-rdg 8383 df-1o 8439 df-er 8677 df-map 8796 df-en 8913 df-dom 8914 df-sdom 8915 df-fin 8916 df-pnf 11222 df-mnf 11223 df-xr 11224 df-ltxr 11225 df-le 11226 df-sub 11418 df-neg 11419 df-nn 12185 df-2 12247 df-3 12248 df-4 12249 df-5 12250 df-6 12251 df-n0 12445 df-z 12531 df-uz 12795 df-fz 13457 df-struct 17052 df-sets 17069 df-slot 17087 df-ndx 17099 df-base 17117 df-ress 17146 df-plusg 17182 df-mulr 17183 df-sca 17185 df-vsca 17186 df-0g 17359 df-proset 18220 df-poset 18238 df-plt 18255 df-lub 18271 df-glb 18272 df-join 18273 df-meet 18274 df-p0 18350 df-p1 18351 df-lat 18357 df-clat 18424 df-mgm 18533 df-sgrp 18582 df-mnd 18593 df-submnd 18638 df-grp 18787 df-minusg 18788 df-sbg 18789 df-subg 18961 df-cntz 19133 df-lsm 19454 df-cmn 19600 df-abl 19601 df-mgp 19933 df-ur 19950 df-ring 20002 df-oppr 20085 df-dvdsr 20106 df-unit 20107 df-invr 20137 df-dvr 20148 df-drng 20249 df-lmod 20402 df-lss 20472 df-lsp 20512 df-lvec 20643 df-lsatoms 37551 df-lshyp 37552 df-lfl 37633 df-lkr 37661 df-ldual 37699 df-oposet 37751 df-ol 37753 df-oml 37754 df-covers 37841 df-ats 37842 df-atl 37873 df-cvlat 37897 df-hlat 37926 df-llines 38074 df-lplanes 38075 df-lvols 38076 df-lines 38077 df-psubsp 38079 df-pmap 38080 df-padd 38372 df-lhyp 38564 df-laut 38565 df-ldil 38680 df-ltrn 38681 df-trl 38735 df-tgrp 39319 df-tendo 39331 df-edring 39333 df-dveca 39579 df-disoa 39605 df-dvech 39655 df-dib 39715 df-dic 39749 df-dih 39805 df-doch 39924 df-djh 39971 |
This theorem is referenced by: mapdrval 40223 |
Copyright terms: Public domain | W3C validator |