Nearby theorems
|
|
Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
|
| Mirrors > Home > MPE Home > Th. List > Mathboxes > hdmapip1 | Structured version Visualization version GIF version | ||
| Description: Construct a proportional vector 𝑌 whose inner product with the original 𝑋 equals one. (Contributed by NM, 13-Jun-2015.) |
| Ref | Expression |
|---|---|
| hdmapip1.h | ⊢ 𝐻 = (LHyp‘𝐾) |
| hdmapip1.u | ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
| hdmapip1.v | ⊢ 𝑉 = (Base‘𝑈) |
| hdmapip1.t | ⊢ · = ( ·𝑠 ‘𝑈) |
| hdmapip1.o | ⊢ 0 = (0g‘𝑈) |
| hdmapip1.r | ⊢ 𝑅 = (Scalar‘𝑈) |
| hdmapip1.i | ⊢ 1 = (1r‘𝑅) |
| hdmapip1.n | ⊢ 𝑁 = (invr‘𝑅) |
| hdmapip1.s | ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) |
| hdmapip1.k | ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
| hdmapip1.x | ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) |
| hdmapip1.y | ⊢ 𝑌 = ((𝑁‘((𝑆‘𝑋)‘𝑋)) · 𝑋) |
| Ref | Expression |
|---|---|
| hdmapip1 | ⊢ (𝜑 → ((𝑆‘𝑋)‘𝑌) = 1 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | hdmapip1.y | . . 3 ⊢ 𝑌 = ((𝑁‘((𝑆‘𝑋)‘𝑋)) · 𝑋) | |
| 2 | 1 | fveq2i 6888 | . 2 ⊢ ((𝑆‘𝑋)‘𝑌) = ((𝑆‘𝑋)‘((𝑁‘((𝑆‘𝑋)‘𝑋)) · 𝑋)) |
| 3 | hdmapip1.h | . . . 4 ⊢ 𝐻 = (LHyp‘𝐾) | |
| 4 | hdmapip1.u | . . . 4 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) | |
| 5 | hdmapip1.v | . . . 4 ⊢ 𝑉 = (Base‘𝑈) | |
| 6 | hdmapip1.t | . . . 4 ⊢ · = ( ·𝑠 ‘𝑈) | |
| 7 | hdmapip1.r | . . . 4 ⊢ 𝑅 = (Scalar‘𝑈) | |
| 8 | eqid 2765 | . . . 4 ⊢ (Base‘𝑅) = (Base‘𝑅) | |
| 9 | eqid 2765 | . . . 4 ⊢ (.r‘𝑅) = (.r‘𝑅) | |
| 10 | hdmapip1.s | . . . 4 ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) | |
| 11 | hdmapip1.k | . . . 4 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) | |
| 12 | hdmapip1.x | . . . . 5 ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) | |
| 13 | 12 | eldifad 3918 | . . . 4 ⊢ (𝜑 → 𝑋 ∈ 𝑉) |
| 14 | 3, 4, 11 | dvhlvec 41943 | . . . . . 6 ⊢ (𝜑 → 𝑈 ∈ LVec) |
| 15 | 7 | lvecdrng 21278 | . . . . . 6 ⊢ (𝑈 ∈ LVec → 𝑅 ∈ DivRing) |
| 16 | 14, 15 | syl 18 | . . . . 5 ⊢ (𝜑 → 𝑅 ∈ DivRing) |
| 17 | 3, 4, 5, 7, 8, 10, 11, 13, 13 | hdmapipcl 42739 | . . . . 5 ⊢ (𝜑 → ((𝑆‘𝑋)‘𝑋) ∈ (Base‘𝑅)) |
| 18 | eldifsni 4760 | . . . . . . 7 ⊢ (𝑋 ∈ (𝑉 ∖ { 0 }) → 𝑋 ≠ 0 ) | |
| 19 | 12, 18 | syl 18 | . . . . . 6 ⊢ (𝜑 → 𝑋 ≠ 0 ) |
| 20 | hdmapip1.o | . . . . . . . 8 ⊢ 0 = (0g‘𝑈) | |
| 21 | eqid 2765 | . . . . . . . 8 ⊢ (0g‘𝑅) = (0g‘𝑅) | |
| 22 | 3, 4, 5, 20, 7, 21, 10, 11, 13 | hdmapip0 42749 | . . . . . . 7 ⊢ (𝜑 → (((𝑆‘𝑋)‘𝑋) = (0g‘𝑅) ↔ 𝑋 = 0 )) |
| 23 | 22 | necon3bid 3004 | . . . . . 6 ⊢ (𝜑 → (((𝑆‘𝑋)‘𝑋) ≠ (0g‘𝑅) ↔ 𝑋 ≠ 0 )) |
| 24 | 19, 23 | mpbird 260 | . . . . 5 ⊢ (𝜑 → ((𝑆‘𝑋)‘𝑋) ≠ (0g‘𝑅)) |
| 25 | hdmapip1.n | . . . . . 6 ⊢ 𝑁 = (invr‘𝑅) | |
| 26 | 8, 21, 25 | drnginvrcl 20909 | . . . . 5 ⊢ ((𝑅 ∈ DivRing ∧ ((𝑆‘𝑋)‘𝑋) ∈ (Base‘𝑅) ∧ ((𝑆‘𝑋)‘𝑋) ≠ (0g‘𝑅)) → (𝑁‘((𝑆‘𝑋)‘𝑋)) ∈ (Base‘𝑅)) |
| 27 | 16, 17, 24, 26 | syl3anc 1398 | . . . 4 ⊢ (𝜑 → (𝑁‘((𝑆‘𝑋)‘𝑋)) ∈ (Base‘𝑅)) |
| 28 | 3, 4, 5, 6, 7, 8, 9, 10, 11, 13, 13, 27 | hdmaplnm1 42743 | . . 3 ⊢ (𝜑 → ((𝑆‘𝑋)‘((𝑁‘((𝑆‘𝑋)‘𝑋)) · 𝑋)) = ((𝑁‘((𝑆‘𝑋)‘𝑋))(.r‘𝑅)((𝑆‘𝑋)‘𝑋))) |
| 29 | hdmapip1.i | . . . . 5 ⊢ 1 = (1r‘𝑅) | |
| 30 | 8, 21, 9, 29, 25 | drnginvrl 20912 | . . . 4 ⊢ ((𝑅 ∈ DivRing ∧ ((𝑆‘𝑋)‘𝑋) ∈ (Base‘𝑅) ∧ ((𝑆‘𝑋)‘𝑋) ≠ (0g‘𝑅)) → ((𝑁‘((𝑆‘𝑋)‘𝑋))(.r‘𝑅)((𝑆‘𝑋)‘𝑋)) = 1 ) |
| 31 | 16, 17, 24, 30 | syl3anc 1398 | . . 3 ⊢ (𝜑 → ((𝑁‘((𝑆‘𝑋)‘𝑋))(.r‘𝑅)((𝑆‘𝑋)‘𝑋)) = 1 ) |
| 32 | 28, 31 | eqtrd 2800 | . 2 ⊢ (𝜑 → ((𝑆‘𝑋)‘((𝑁‘((𝑆‘𝑋)‘𝑋)) · 𝑋)) = 1 ) |
| 33 | 2, 32 | eqtrid 2812 | 1 ⊢ (𝜑 → ((𝑆‘𝑋)‘𝑌) = 1 ) |
| Colors of variables: wff setvar class |
| This proof depends on syntax axioms: → wi 4 ∧ wa 401 = wceq 1570 ∈ wcel 2146 ≠ wne 2960 ∖ cdif 3903 {csn 4591 ‘cfv 6540 (class class class)co 7419 Basecbs 17293 .rcmulr 17335 Scalarcsca 17337 ·𝑠 cvsca 17338 0gc0g 17516 1rcur 20309 invrcinvr 20517 DivRingcdr 20879 LVecclvec 21275 HLchlt 40184 LHypclh 40818 DVecHcdvh 41912 HDMapchdma 42626 |
| This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2737 ax-rep 5240 ax-sep 5259 ax-nul 5271 ax-pow 5338 ax-pr 5406 ax-un 7742 ax-cnex 11173 ax-resscn 11174 ax-1cn 11175 ax-icn 11176 ax-addcl 11177 ax-addrcl 11178 ax-mulcl 11179 ax-mulrcl 11180 ax-mulcom 11181 ax-addass 11182 ax-mulass 11183 ax-distr 11184 ax-i2m1 11185 ax-1ne0 11186 ax-1rid 11187 ax-rnegex 11188 ax-rrecex 11189 ax-cnre 11190 ax-pre-lttri 11191 ax-pre-lttrn 11192 ax-pre-ltadd 11193 ax-pre-mulgt0 11194 ax-riotaBAD 39787 |
| This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3067 df-ral 3082 df-rex 3092 df-rmo 3371 df-reu 3372 df-rab 3419 df-v 3459 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4287 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-tp 4596 df-op 4598 df-ot 4600 df-uni 4875 df-int 4915 df-iun 4960 df-iin 4961 df-br 5112 df-opab 5176 df-mpt 5195 df-tr 5221 df-id 5558 df-eprel 5563 df-po 5571 df-so 5572 df-fr 5616 df-we 5618 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-pred 6306 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6496 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-riota 7376 df-ov 7422 df-oprab 7423 df-mpo 7424 df-of 7684 df-om 7869 df-1st 7992 df-2nd 7993 df-tpos 8228 df-undef 8275 df-frecs 8284 df-wrecs 8315 df-recs 8364 df-rdg 8403 df-1o 8459 df-2o 8460 df-er 8700 df-map 8832 df-en 8950 df-dom 8951 df-sdom 8952 df-fin 8953 df-pnf 11262 df-mnf 11263 df-xr 11264 df-ltxr 11265 df-le 11266 df-sub 11460 df-neg 11461 df-nn 12251 df-2 12320 df-3 12321 df-4 12322 df-5 12323 df-6 12324 df-n0 12522 df-z 12609 df-uz 12881 df-fz 13554 df-struct 17231 df-sets 17248 df-slot 17266 df-ndx 17278 df-base 17294 df-ress 17315 df-plusg 17347 df-mulr 17348 df-sca 17350 df-vsca 17351 df-0g 17518 df-mre 17662 df-mrc 17663 df-acs 17665 df-proset 18374 df-poset 18393 df-plt 18408 df-lub 18424 df-glb 18425 df-join 18426 df-meet 18427 df-p0 18503 df-p1 18504 df-lat 18512 df-clat 18579 df-mgm 18722 df-sgrp 18811 df-mnd 18827 df-submnd 18881 df-grp 19049 df-minusg 19050 df-sbg 19051 df-subg 19235 df-cntz 19433 df-oppg 19462 df-lsm 19752 df-cmn 19898 df-abl 19899 df-mgp 20263 df-rng 20277 df-ur 20310 df-ring 20363 df-oppr 20467 df-dvdsr 20487 df-unit 20488 df-invr 20518 df-dvr 20531 df-nzr 20662 df-rlreg 20845 df-domn 20846 df-drng 20881 df-lmod 21035 df-lss 21105 df-lsp 21145 df-lvec 21276 df-lsatoms 39810 df-lshyp 39811 df-lcv 39853 df-lfl 39892 df-lkr 39920 df-ldual 39958 df-oposet 40010 df-ol 40012 df-oml 40013 df-covers 40100 df-ats 40101 df-atl 40132 df-cvlat 40156 df-hlat 40185 df-llines 40332 df-lplanes 40333 df-lvols 40334 df-lines 40335 df-psubsp 40337 df-pmap 40338 df-padd 40630 df-lhyp 40822 df-laut 40823 df-ldil 40938 df-ltrn 40939 df-trl 40993 df-tgrp 41577 df-tendo 41589 df-edring 41591 df-dveca 41837 df-disoa 41863 df-dvech 41913 df-dib 41973 df-dic 42007 df-dih 42063 df-doch 42182 df-djh 42229 df-lcdual 42421 df-mapd 42459 df-hvmap 42591 df-hdmap1 42627 df-hdmap 42628 |
| This theorem is used by: hgmapvvlem3 42759 |
| Copyright terms: Public domain | W3C validator |