Nearby theorems
|
|
Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
|
| Mirrors > Home > MPE Home > Th. List > Mathboxes > hgmapvvlem2 | Structured version Visualization version GIF version | ||
| Description: Lemma for hgmapvv 42646. Eliminate 𝑌 (Baer's s). (Contributed by NM, 13-Jun-2015.) |
| Ref | Expression |
|---|---|
| hdmapglem6.h | ⊢ 𝐻 = (LHyp‘𝐾) |
| hdmapglem6.e | ⊢ 𝐸 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩ |
| hdmapglem6.o | ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊) |
| hdmapglem6.u | ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
| hdmapglem6.v | ⊢ 𝑉 = (Base‘𝑈) |
| hdmapglem6.q | ⊢ · = ( ·𝑠 ‘𝑈) |
| hdmapglem6.r | ⊢ 𝑅 = (Scalar‘𝑈) |
| hdmapglem6.b | ⊢ 𝐵 = (Base‘𝑅) |
| hdmapglem6.t | ⊢ × = (.r‘𝑅) |
| hdmapglem6.z | ⊢ 0 = (0g‘𝑅) |
| hdmapglem6.i | ⊢ 1 = (1r‘𝑅) |
| hdmapglem6.n | ⊢ 𝑁 = (invr‘𝑅) |
| hdmapglem6.s | ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) |
| hdmapglem6.g | ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊) |
| hdmapglem6.k | ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
| hdmapglem6.x | ⊢ (𝜑 → 𝑋 ∈ (𝐵 ∖ { 0 })) |
| hdmapglem6.c | ⊢ (𝜑 → 𝐶 ∈ (𝑂‘{𝐸})) |
| hdmapglem6.d | ⊢ (𝜑 → 𝐷 ∈ (𝑂‘{𝐸})) |
| hdmapglem6.cd | ⊢ (𝜑 → ((𝑆‘𝐷)‘𝐶) = 1 ) |
| Ref | Expression |
|---|---|
| hgmapvvlem2 | ⊢ (𝜑 → (𝐺‘(𝐺‘𝑋)) = 𝑋) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | hdmapglem6.h | . 2 ⊢ 𝐻 = (LHyp‘𝐾) | |
| 2 | hdmapglem6.e | . 2 ⊢ 𝐸 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩ | |
| 3 | hdmapglem6.o | . 2 ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊) | |
| 4 | hdmapglem6.u | . 2 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) | |
| 5 | hdmapglem6.v | . 2 ⊢ 𝑉 = (Base‘𝑈) | |
| 6 | hdmapglem6.q | . 2 ⊢ · = ( ·𝑠 ‘𝑈) | |
| 7 | hdmapglem6.r | . 2 ⊢ 𝑅 = (Scalar‘𝑈) | |
| 8 | hdmapglem6.b | . 2 ⊢ 𝐵 = (Base‘𝑅) | |
| 9 | hdmapglem6.t | . 2 ⊢ × = (.r‘𝑅) | |
| 10 | hdmapglem6.z | . 2 ⊢ 0 = (0g‘𝑅) | |
| 11 | hdmapglem6.i | . 2 ⊢ 1 = (1r‘𝑅) | |
| 12 | hdmapglem6.n | . 2 ⊢ 𝑁 = (invr‘𝑅) | |
| 13 | hdmapglem6.s | . 2 ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) | |
| 14 | hdmapglem6.g | . 2 ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊) | |
| 15 | hdmapglem6.k | . 2 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) | |
| 16 | hdmapglem6.x | . 2 ⊢ (𝜑 → 𝑋 ∈ (𝐵 ∖ { 0 })) | |
| 17 | hdmapglem6.c | . 2 ⊢ (𝜑 → 𝐶 ∈ (𝑂‘{𝐸})) | |
| 18 | hdmapglem6.d | . 2 ⊢ (𝜑 → 𝐷 ∈ (𝑂‘{𝐸})) | |
| 19 | hdmapglem6.cd | . 2 ⊢ (𝜑 → ((𝑆‘𝐷)‘𝐶) = 1 ) | |
| 20 | 1, 4, 15 | dvhlvec 41829 | . . . . 5 ⊢ (𝜑 → 𝑈 ∈ LVec) |
| 21 | 7 | lvecdrng 21205 | . . . . 5 ⊢ (𝑈 ∈ LVec → 𝑅 ∈ DivRing) |
| 22 | 20, 21 | syl 18 | . . . 4 ⊢ (𝜑 → 𝑅 ∈ DivRing) |
| 23 | 16 | eldifad 3916 | . . . . 5 ⊢ (𝜑 → 𝑋 ∈ 𝐵) |
| 24 | 1, 4, 7, 8, 14, 15, 23 | hgmapcl 42609 | . . . 4 ⊢ (𝜑 → (𝐺‘𝑋) ∈ 𝐵) |
| 25 | eldifsni 4757 | . . . . . 6 ⊢ (𝑋 ∈ (𝐵 ∖ { 0 }) → 𝑋 ≠ 0 ) | |
| 26 | 16, 25 | syl 18 | . . . . 5 ⊢ (𝜑 → 𝑋 ≠ 0 ) |
| 27 | 1, 4, 7, 8, 10, 14, 15, 23 | hgmapeq0 42624 | . . . . . 6 ⊢ (𝜑 → ((𝐺‘𝑋) = 0 ↔ 𝑋 = 0 )) |
| 28 | 27 | necon3bid 3000 | . . . . 5 ⊢ (𝜑 → ((𝐺‘𝑋) ≠ 0 ↔ 𝑋 ≠ 0 )) |
| 29 | 26, 28 | mpbird 260 | . . . 4 ⊢ (𝜑 → (𝐺‘𝑋) ≠ 0 ) |
| 30 | 8, 10, 12 | drnginvrcl 20837 | . . . 4 ⊢ ((𝑅 ∈ DivRing ∧ (𝐺‘𝑋) ∈ 𝐵 ∧ (𝐺‘𝑋) ≠ 0 ) → (𝑁‘(𝐺‘𝑋)) ∈ 𝐵) |
| 31 | 22, 24, 29, 30 | syl3anc 1396 | . . 3 ⊢ (𝜑 → (𝑁‘(𝐺‘𝑋)) ∈ 𝐵) |
| 32 | 8, 10, 12 | drnginvrn0 20838 | . . . 4 ⊢ ((𝑅 ∈ DivRing ∧ (𝐺‘𝑋) ∈ 𝐵 ∧ (𝐺‘𝑋) ≠ 0 ) → (𝑁‘(𝐺‘𝑋)) ≠ 0 ) |
| 33 | 22, 24, 29, 32 | syl3anc 1396 | . . 3 ⊢ (𝜑 → (𝑁‘(𝐺‘𝑋)) ≠ 0 ) |
| 34 | eldifsn 4752 | . . 3 ⊢ ((𝑁‘(𝐺‘𝑋)) ∈ (𝐵 ∖ { 0 }) ↔ ((𝑁‘(𝐺‘𝑋)) ∈ 𝐵 ∧ (𝑁‘(𝐺‘𝑋)) ≠ 0 )) | |
| 35 | 31, 33, 34 | sylanbrc 594 | . 2 ⊢ (𝜑 → (𝑁‘(𝐺‘𝑋)) ∈ (𝐵 ∖ { 0 })) |
| 36 | 8, 10, 9, 11, 12 | drnginvrl 20840 | . . 3 ⊢ ((𝑅 ∈ DivRing ∧ (𝐺‘𝑋) ∈ 𝐵 ∧ (𝐺‘𝑋) ≠ 0 ) → ((𝑁‘(𝐺‘𝑋)) × (𝐺‘𝑋)) = 1 ) |
| 37 | 22, 24, 29, 36 | syl3anc 1396 | . 2 ⊢ (𝜑 → ((𝑁‘(𝐺‘𝑋)) × (𝐺‘𝑋)) = 1 ) |
| 38 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 35, 37 | hgmapvvlem1 42643 | 1 ⊢ (𝜑 → (𝐺‘(𝐺‘𝑋)) = 𝑋) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 400 = wceq 1568 ∈ wcel 2141 ≠ wne 2956 ∖ cdif 3901 {csn 4588 ⟨cop 4594 I cid 5555 ↾ cres 5663 ‘cfv 6536 (class class class)co 7410 Basecbs 17268 .rcmulr 17310 Scalarcsca 17312 ·𝑠 cvsca 17313 0gc0g 17491 1rcur 20262 invrcinvr 20468 DivRingcdr 20812 LVecclvec 21202 HLchlt 40070 LHypclh 40704 LTrncltrn 40821 DVecHcdvh 41798 ocHcoch 42067 HDMapchdma 42512 HGMapchg 42603 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1823 ax-4 1837 ax-5 1938 ax-6 1995 ax-7 2036 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-rep 5237 ax-sep 5256 ax-nul 5268 ax-pow 5336 ax-pr 5404 ax-un 7732 ax-cnex 11155 ax-resscn 11156 ax-1cn 11157 ax-icn 11158 ax-addcl 11159 ax-addrcl 11160 ax-mulcl 11161 ax-mulrcl 11162 ax-mulcom 11163 ax-addass 11164 ax-mulass 11165 ax-distr 11166 ax-i2m1 11167 ax-1ne0 11168 ax-1rid 11169 ax-rnegex 11170 ax-rrecex 11171 ax-cnre 11172 ax-pre-lttri 11173 ax-pre-lttrn 11174 ax-pre-ltadd 11175 ax-pre-mulgt0 11176 ax-riotaBAD 39673 |
| This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1571 df-fal 1581 df-ex 1808 df-nf 1812 df-sb 2095 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3744 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4487 df-pw 4563 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4595 df-ot 4597 df-uni 4872 df-int 4912 df-iun 4957 df-iin 4958 df-br 5109 df-opab 5173 df-mpt 5192 df-tr 5218 df-id 5556 df-eprel 5561 df-po 5569 df-so 5570 df-fr 5614 df-we 5616 df-xp 5667 df-rel 5668 df-cnv 5669 df-co 5670 df-dm 5671 df-rn 5672 df-res 5673 df-ima 5674 df-pred 6302 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-of 7674 df-om 7862 df-1st 7985 df-2nd 7986 df-tpos 8221 df-undef 8268 df-frecs 8277 df-wrecs 8308 df-recs 8357 df-rdg 8396 df-1o 8452 df-2o 8453 df-er 8693 df-map 8825 df-en 8943 df-dom 8944 df-sdom 8945 df-fin 8946 df-pnf 11244 df-mnf 11245 df-xr 11246 df-ltxr 11247 df-le 11248 df-sub 11442 df-neg 11443 df-nn 12233 df-2 12302 df-3 12303 df-4 12304 df-5 12305 df-6 12306 df-n0 12504 df-z 12591 df-uz 12862 df-fz 13535 df-struct 17206 df-sets 17223 df-slot 17241 df-ndx 17253 df-base 17269 df-ress 17290 df-plusg 17322 df-mulr 17323 df-sca 17325 df-vsca 17326 df-0g 17493 df-mre 17637 df-mrc 17638 df-acs 17640 df-proset 18349 df-poset 18368 df-plt 18383 df-lub 18399 df-glb 18400 df-join 18401 df-meet 18402 df-p0 18478 df-p1 18479 df-lat 18487 df-clat 18554 df-mgm 18697 df-sgrp 18776 df-mnd 18792 df-submnd 18841 df-grp 19002 df-minusg 19003 df-sbg 19004 df-subg 19188 df-cntz 19386 df-oppg 19415 df-lsm 19705 df-cmn 19851 df-abl 19852 df-mgp 20216 df-rng 20230 df-ur 20263 df-ring 20316 df-oppr 20418 df-dvdsr 20438 df-unit 20439 df-invr 20469 df-dvr 20482 df-nzr 20595 df-rlreg 20778 df-domn 20779 df-drng 20814 df-lmod 20962 df-lss 21032 df-lsp 21072 df-lvec 21203 df-lsatoms 39696 df-lshyp 39697 df-lcv 39739 df-lfl 39778 df-lkr 39806 df-ldual 39844 df-oposet 39896 df-ol 39898 df-oml 39899 df-covers 39986 df-ats 39987 df-atl 40018 df-cvlat 40042 df-hlat 40071 df-llines 40218 df-lplanes 40219 df-lvols 40220 df-lines 40221 df-psubsp 40223 df-pmap 40224 df-padd 40516 df-lhyp 40708 df-laut 40709 df-ldil 40824 df-ltrn 40825 df-trl 40879 df-tgrp 41463 df-tendo 41475 df-edring 41477 df-dveca 41723 df-disoa 41749 df-dvech 41799 df-dib 41859 df-dic 41893 df-dih 41949 df-doch 42068 df-djh 42115 df-lcdual 42307 df-mapd 42345 df-hvmap 42477 df-hdmap1 42513 df-hdmap 42514 df-hgmap 42604 |
| This theorem is referenced by: hgmapvvlem3 42645 |
| Copyright terms: Public domain | W3C validator |