| Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > Mathboxes > dvheveccl | Structured version Visualization version GIF version | ||
| Description: Properties of a unit vector that we will use later as a convenient reference vector. This vector is called "e" in the remark after Lemma M of [Crawley] p. 121. line 17. See also dvhopN 41112 and dihpN 41332. (Contributed by NM, 27-Mar-2015.) |
| Ref | Expression |
|---|---|
| dvheveccl.h | ⊢ 𝐻 = (LHyp‘𝐾) |
| dvheveccl.b | ⊢ 𝐵 = (Base‘𝐾) |
| dvheveccl.t | ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
| dvheveccl.u | ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
| dvheveccl.v | ⊢ 𝑉 = (Base‘𝑈) |
| dvheveccl.z | ⊢ 0 = (0g‘𝑈) |
| dvheveccl.e | ⊢ 𝐸 = 〈( I ↾ 𝐵), ( I ↾ 𝑇)〉 |
| dvheveccl.k | ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
| Ref | Expression |
|---|---|
| dvheveccl | ⊢ (𝜑 → 𝐸 ∈ (𝑉 ∖ { 0 })) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dvheveccl.e | . 2 ⊢ 𝐸 = 〈( I ↾ 𝐵), ( I ↾ 𝑇)〉 | |
| 2 | dvheveccl.k | . . . 4 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) | |
| 3 | dvheveccl.b | . . . . . 6 ⊢ 𝐵 = (Base‘𝐾) | |
| 4 | dvheveccl.h | . . . . . 6 ⊢ 𝐻 = (LHyp‘𝐾) | |
| 5 | dvheveccl.t | . . . . . 6 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) | |
| 6 | 3, 4, 5 | idltrn 40146 | . . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ( I ↾ 𝐵) ∈ 𝑇) |
| 7 | 2, 6 | syl 17 | . . . 4 ⊢ (𝜑 → ( I ↾ 𝐵) ∈ 𝑇) |
| 8 | eqid 2729 | . . . . . 6 ⊢ ((TEndo‘𝐾)‘𝑊) = ((TEndo‘𝐾)‘𝑊) | |
| 9 | 4, 5, 8 | tendoidcl 40765 | . . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ( I ↾ 𝑇) ∈ ((TEndo‘𝐾)‘𝑊)) |
| 10 | 2, 9 | syl 17 | . . . 4 ⊢ (𝜑 → ( I ↾ 𝑇) ∈ ((TEndo‘𝐾)‘𝑊)) |
| 11 | dvheveccl.u | . . . . 5 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) | |
| 12 | dvheveccl.v | . . . . 5 ⊢ 𝑉 = (Base‘𝑈) | |
| 13 | 4, 5, 8, 11, 12 | dvhelvbasei 41084 | . . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (( I ↾ 𝐵) ∈ 𝑇 ∧ ( I ↾ 𝑇) ∈ ((TEndo‘𝐾)‘𝑊))) → 〈( I ↾ 𝐵), ( I ↾ 𝑇)〉 ∈ 𝑉) |
| 14 | 2, 7, 10, 13 | syl12anc 836 | . . 3 ⊢ (𝜑 → 〈( I ↾ 𝐵), ( I ↾ 𝑇)〉 ∈ 𝑉) |
| 15 | eqid 2729 | . . . . . 6 ⊢ (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵)) = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵)) | |
| 16 | 3, 4, 5, 8, 15 | tendo1ne0 40824 | . . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ( I ↾ 𝑇) ≠ (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵))) |
| 17 | 2, 16 | syl 17 | . . . 4 ⊢ (𝜑 → ( I ↾ 𝑇) ≠ (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵))) |
| 18 | dvheveccl.z | . . . . . . . 8 ⊢ 0 = (0g‘𝑈) | |
| 19 | 3, 4, 5, 11, 18, 15 | dvh0g 41107 | . . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 0 = 〈( I ↾ 𝐵), (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵))〉) |
| 20 | 2, 19 | syl 17 | . . . . . 6 ⊢ (𝜑 → 0 = 〈( I ↾ 𝐵), (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵))〉) |
| 21 | eqtr 2749 | . . . . . . 7 ⊢ ((〈( I ↾ 𝐵), ( I ↾ 𝑇)〉 = 0 ∧ 0 = 〈( I ↾ 𝐵), (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵))〉) → 〈( I ↾ 𝐵), ( I ↾ 𝑇)〉 = 〈( I ↾ 𝐵), (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵))〉) | |
| 22 | opthg 5414 | . . . . . . . . 9 ⊢ ((( I ↾ 𝐵) ∈ 𝑇 ∧ ( I ↾ 𝑇) ∈ ((TEndo‘𝐾)‘𝑊)) → (〈( I ↾ 𝐵), ( I ↾ 𝑇)〉 = 〈( I ↾ 𝐵), (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵))〉 ↔ (( I ↾ 𝐵) = ( I ↾ 𝐵) ∧ ( I ↾ 𝑇) = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵))))) | |
| 23 | 7, 10, 22 | syl2anc 584 | . . . . . . . 8 ⊢ (𝜑 → (〈( I ↾ 𝐵), ( I ↾ 𝑇)〉 = 〈( I ↾ 𝐵), (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵))〉 ↔ (( I ↾ 𝐵) = ( I ↾ 𝐵) ∧ ( I ↾ 𝑇) = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵))))) |
| 24 | simpr 484 | . . . . . . . 8 ⊢ ((( I ↾ 𝐵) = ( I ↾ 𝐵) ∧ ( I ↾ 𝑇) = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵))) → ( I ↾ 𝑇) = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵))) | |
| 25 | 23, 24 | biimtrdi 253 | . . . . . . 7 ⊢ (𝜑 → (〈( I ↾ 𝐵), ( I ↾ 𝑇)〉 = 〈( I ↾ 𝐵), (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵))〉 → ( I ↾ 𝑇) = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵)))) |
| 26 | 21, 25 | syl5 34 | . . . . . 6 ⊢ (𝜑 → ((〈( I ↾ 𝐵), ( I ↾ 𝑇)〉 = 0 ∧ 0 = 〈( I ↾ 𝐵), (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵))〉) → ( I ↾ 𝑇) = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵)))) |
| 27 | 20, 26 | mpan2d 694 | . . . . 5 ⊢ (𝜑 → (〈( I ↾ 𝐵), ( I ↾ 𝑇)〉 = 0 → ( I ↾ 𝑇) = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵)))) |
| 28 | 27 | necon3d 2946 | . . . 4 ⊢ (𝜑 → (( I ↾ 𝑇) ≠ (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵)) → 〈( I ↾ 𝐵), ( I ↾ 𝑇)〉 ≠ 0 )) |
| 29 | 17, 28 | mpd 15 | . . 3 ⊢ (𝜑 → 〈( I ↾ 𝐵), ( I ↾ 𝑇)〉 ≠ 0 ) |
| 30 | eldifsn 4735 | . . 3 ⊢ (〈( I ↾ 𝐵), ( I ↾ 𝑇)〉 ∈ (𝑉 ∖ { 0 }) ↔ (〈( I ↾ 𝐵), ( I ↾ 𝑇)〉 ∈ 𝑉 ∧ 〈( I ↾ 𝐵), ( I ↾ 𝑇)〉 ≠ 0 )) | |
| 31 | 14, 29, 30 | sylanbrc 583 | . 2 ⊢ (𝜑 → 〈( I ↾ 𝐵), ( I ↾ 𝑇)〉 ∈ (𝑉 ∖ { 0 })) |
| 32 | 1, 31 | eqeltrid 2832 | 1 ⊢ (𝜑 → 𝐸 ∈ (𝑉 ∖ { 0 })) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1540 ∈ wcel 2109 ≠ wne 2925 ∖ cdif 3896 {csn 4573 〈cop 4579 ↦ cmpt 5169 I cid 5507 ↾ cres 5615 ‘cfv 6476 Basecbs 17107 0gc0g 17330 HLchlt 39346 LHypclh 39980 LTrncltrn 40097 TEndoctendo 40748 DVecHcdvh 41074 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5214 ax-sep 5231 ax-nul 5241 ax-pow 5300 ax-pr 5367 ax-un 7662 ax-cnex 11053 ax-resscn 11054 ax-1cn 11055 ax-icn 11056 ax-addcl 11057 ax-addrcl 11058 ax-mulcl 11059 ax-mulrcl 11060 ax-mulcom 11061 ax-addass 11062 ax-mulass 11063 ax-distr 11064 ax-i2m1 11065 ax-1ne0 11066 ax-1rid 11067 ax-rnegex 11068 ax-rrecex 11069 ax-cnre 11070 ax-pre-lttri 11071 ax-pre-lttrn 11072 ax-pre-ltadd 11073 ax-pre-mulgt0 11074 ax-riotaBAD 38949 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3343 df-reu 3344 df-rab 3393 df-v 3435 df-sbc 3739 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4281 df-if 4473 df-pw 4549 df-sn 4574 df-pr 4576 df-tp 4578 df-op 4580 df-uni 4857 df-iun 4940 df-iin 4941 df-br 5089 df-opab 5151 df-mpt 5170 df-tr 5196 df-id 5508 df-eprel 5513 df-po 5521 df-so 5522 df-fr 5566 df-we 5568 df-xp 5619 df-rel 5620 df-cnv 5621 df-co 5622 df-dm 5623 df-rn 5624 df-res 5625 df-ima 5626 df-pred 6243 df-ord 6304 df-on 6305 df-lim 6306 df-suc 6307 df-iota 6432 df-fun 6478 df-fn 6479 df-f 6480 df-f1 6481 df-fo 6482 df-f1o 6483 df-fv 6484 df-riota 7297 df-ov 7343 df-oprab 7344 df-mpo 7345 df-om 7791 df-1st 7915 df-2nd 7916 df-tpos 8150 df-undef 8197 df-frecs 8205 df-wrecs 8236 df-recs 8285 df-rdg 8323 df-1o 8379 df-er 8616 df-map 8746 df-en 8864 df-dom 8865 df-sdom 8866 df-fin 8867 df-pnf 11139 df-mnf 11140 df-xr 11141 df-ltxr 11142 df-le 11143 df-sub 11337 df-neg 11338 df-nn 12117 df-2 12179 df-3 12180 df-4 12181 df-5 12182 df-6 12183 df-n0 12373 df-z 12460 df-uz 12724 df-fz 13399 df-struct 17045 df-sets 17062 df-slot 17080 df-ndx 17092 df-base 17108 df-ress 17129 df-plusg 17161 df-mulr 17162 df-sca 17164 df-vsca 17165 df-0g 17332 df-proset 18187 df-poset 18206 df-plt 18221 df-lub 18237 df-glb 18238 df-join 18239 df-meet 18240 df-p0 18316 df-p1 18317 df-lat 18325 df-clat 18392 df-mgm 18501 df-sgrp 18580 df-mnd 18596 df-grp 18802 df-minusg 18803 df-cmn 19648 df-abl 19649 df-mgp 20013 df-rng 20025 df-ur 20054 df-ring 20107 df-oppr 20209 df-dvdsr 20229 df-unit 20230 df-invr 20260 df-dvr 20273 df-drng 20600 df-lmod 20749 df-lvec 20991 df-oposet 39172 df-ol 39174 df-oml 39175 df-covers 39262 df-ats 39263 df-atl 39294 df-cvlat 39318 df-hlat 39347 df-llines 39494 df-lplanes 39495 df-lvols 39496 df-lines 39497 df-psubsp 39499 df-pmap 39500 df-padd 39792 df-lhyp 39984 df-laut 39985 df-ldil 40100 df-ltrn 40101 df-trl 40155 df-tendo 40751 df-edring 40753 df-dvech 41075 |
| This theorem is referenced by: hdmapcl 41826 hdmapval2lem 41827 hdmapval0 41829 hdmapeveclem 41830 hdmapevec 41831 hdmapevec2 41832 hdmapval3lemN 41833 hdmapval3N 41834 hdmap10lem 41835 hdmap11lem1 41837 hdmap11lem2 41838 hdmapinvlem1 41914 hdmapinvlem2 41915 hdmapinvlem3 41916 hdmapinvlem4 41917 hdmapglem5 41918 hgmapvvlem3 41921 hdmapglem7a 41923 hdmapglem7b 41924 hdmapglem7 41925 |
| Copyright terms: Public domain | W3C validator |