Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > dochlss | Structured version Visualization version GIF version |
Description: A subspace orthocomplement is a subspace of the DVecH vector space. (Contributed by NM, 22-Jul-2014.) |
Ref | Expression |
---|---|
dochlss.h | β’ π» = (LHypβπΎ) |
dochlss.u | β’ π = ((DVecHβπΎ)βπ) |
dochlss.v | β’ π = (Baseβπ) |
dochlss.s | β’ π = (LSubSpβπ) |
dochlss.o | β’ β₯ = ((ocHβπΎ)βπ) |
Ref | Expression |
---|---|
dochlss | β’ (((πΎ β HL β§ π β π») β§ π β π) β ( β₯ βπ) β π) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dochlss.h | . . 3 β’ π» = (LHypβπΎ) | |
2 | eqid 2736 | . . 3 β’ ((DIsoHβπΎ)βπ) = ((DIsoHβπΎ)βπ) | |
3 | dochlss.u | . . 3 β’ π = ((DVecHβπΎ)βπ) | |
4 | dochlss.v | . . 3 β’ π = (Baseβπ) | |
5 | dochlss.o | . . 3 β’ β₯ = ((ocHβπΎ)βπ) | |
6 | 1, 2, 3, 4, 5 | dochcl 39629 | . 2 β’ (((πΎ β HL β§ π β π») β§ π β π) β ( β₯ βπ) β ran ((DIsoHβπΎ)βπ)) |
7 | dochlss.s | . . 3 β’ π = (LSubSpβπ) | |
8 | 1, 3, 2, 7 | dihrnlss 39553 | . 2 β’ (((πΎ β HL β§ π β π») β§ ( β₯ βπ) β ran ((DIsoHβπΎ)βπ)) β ( β₯ βπ) β π) |
9 | 6, 8 | syldan 591 | 1 β’ (((πΎ β HL β§ π β π») β§ π β π) β ( β₯ βπ) β π) |
Colors of variables: wff setvar class |
Syntax hints: β wi 4 β§ wa 396 = wceq 1540 β wcel 2105 β wss 3898 ran crn 5621 βcfv 6479 Basecbs 17009 LSubSpclss 20299 HLchlt 37625 LHypclh 38260 DVecHcdvh 39354 DIsoHcdih 39504 ocHcoch 39623 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2707 ax-rep 5229 ax-sep 5243 ax-nul 5250 ax-pow 5308 ax-pr 5372 ax-un 7650 ax-cnex 11028 ax-resscn 11029 ax-1cn 11030 ax-icn 11031 ax-addcl 11032 ax-addrcl 11033 ax-mulcl 11034 ax-mulrcl 11035 ax-mulcom 11036 ax-addass 11037 ax-mulass 11038 ax-distr 11039 ax-i2m1 11040 ax-1ne0 11041 ax-1rid 11042 ax-rnegex 11043 ax-rrecex 11044 ax-cnre 11045 ax-pre-lttri 11046 ax-pre-lttrn 11047 ax-pre-ltadd 11048 ax-pre-mulgt0 11049 ax-riotaBAD 37228 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2886 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3349 df-reu 3350 df-rab 3404 df-v 3443 df-sbc 3728 df-csb 3844 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-pss 3917 df-nul 4270 df-if 4474 df-pw 4549 df-sn 4574 df-pr 4576 df-tp 4578 df-op 4580 df-uni 4853 df-int 4895 df-iun 4943 df-iin 4944 df-br 5093 df-opab 5155 df-mpt 5176 df-tr 5210 df-id 5518 df-eprel 5524 df-po 5532 df-so 5533 df-fr 5575 df-we 5577 df-xp 5626 df-rel 5627 df-cnv 5628 df-co 5629 df-dm 5630 df-rn 5631 df-res 5632 df-ima 5633 df-pred 6238 df-ord 6305 df-on 6306 df-lim 6307 df-suc 6308 df-iota 6431 df-fun 6481 df-fn 6482 df-f 6483 df-f1 6484 df-fo 6485 df-f1o 6486 df-fv 6487 df-riota 7293 df-ov 7340 df-oprab 7341 df-mpo 7342 df-om 7781 df-1st 7899 df-2nd 7900 df-tpos 8112 df-undef 8159 df-frecs 8167 df-wrecs 8198 df-recs 8272 df-rdg 8311 df-1o 8367 df-er 8569 df-map 8688 df-en 8805 df-dom 8806 df-sdom 8807 df-fin 8808 df-pnf 11112 df-mnf 11113 df-xr 11114 df-ltxr 11115 df-le 11116 df-sub 11308 df-neg 11309 df-nn 12075 df-2 12137 df-3 12138 df-4 12139 df-5 12140 df-6 12141 df-n0 12335 df-z 12421 df-uz 12684 df-fz 13341 df-struct 16945 df-sets 16962 df-slot 16980 df-ndx 16992 df-base 17010 df-ress 17039 df-plusg 17072 df-mulr 17073 df-sca 17075 df-vsca 17076 df-0g 17249 df-proset 18110 df-poset 18128 df-plt 18145 df-lub 18161 df-glb 18162 df-join 18163 df-meet 18164 df-p0 18240 df-p1 18241 df-lat 18247 df-clat 18314 df-mgm 18423 df-sgrp 18472 df-mnd 18483 df-submnd 18528 df-grp 18676 df-minusg 18677 df-sbg 18678 df-subg 18848 df-cntz 19019 df-lsm 19337 df-cmn 19483 df-abl 19484 df-mgp 19816 df-ur 19833 df-ring 19880 df-oppr 19957 df-dvdsr 19978 df-unit 19979 df-invr 20009 df-dvr 20020 df-drng 20095 df-lmod 20231 df-lss 20300 df-lsp 20340 df-lvec 20471 df-oposet 37451 df-ol 37453 df-oml 37454 df-covers 37541 df-ats 37542 df-atl 37573 df-cvlat 37597 df-hlat 37626 df-llines 37774 df-lplanes 37775 df-lvols 37776 df-lines 37777 df-psubsp 37779 df-pmap 37780 df-padd 38072 df-lhyp 38264 df-laut 38265 df-ldil 38380 df-ltrn 38381 df-trl 38435 df-tendo 39031 df-edring 39033 df-disoa 39305 df-dvech 39355 df-dib 39415 df-dic 39449 df-dih 39505 df-doch 39624 |
This theorem is referenced by: dochspocN 39656 dochsncom 39658 dochshpncl 39660 djhexmid 39687 dochsatshp 39727 dochsatshpb 39728 dochshpsat 39730 dochkrsat 39731 dochexmidlem2 39737 dochexmidlem5 39740 dochexmidlem7 39742 dochexmidlem8 39743 dochexmid 39744 dochfl1 39752 dochkr1 39754 dochkr1OLDN 39755 lcfl4N 39771 lclkrlem2a 39783 lclkrlem2o 39797 lclkrlem2v 39804 lclkrslem2 39814 lcfrlem5 39822 lcfrlem6 39823 lcfrlem19 39837 lcfrlem20 39838 lcfrlem23 39841 lcfrlem25 39843 lcfrlem26 39844 lcfrlem35 39853 lcfrlem36 39854 lcfr 39861 mapdrvallem2 39921 mapd0 39941 hgmapvvlem3 40201 hdmapglem7a 40203 hdmapoc 40207 |
Copyright terms: Public domain | W3C validator |