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 43186. 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 42369 | . . . . 5 ⊢ (𝜑 → 𝑈 ∈ LVec) |
| 21 | 7 | lvecdrng 21413 | . . . . 5 ⊢ (𝑈 ∈ LVec → 𝑅 ∈ DivRing) |
| 22 | 20, 21 | syl 18 | . . . 4 ⊢ (𝜑 → 𝑅 ∈ DivRing) |
| 23 | 16 | eldifad 4054 | . . . . 5 ⊢ (𝜑 → 𝑋 ∈ 𝐵) |
| 24 | 1, 4, 7, 8, 14, 15, 23 | hgmapcl 43149 | . . . 4 ⊢ (𝜑 → (𝐺‘𝑋) ∈ 𝐵) |
| 25 | eldifsni 4753 | . . . . . 6 ⊢ (𝑋 ∈ (𝐵 ∖ { 0 }) → 𝑋 ≠ 0 ) | |
| 26 | 16, 25 | syl 18 | . . . . 5 ⊢ (𝜑 → 𝑋 ≠ 0 ) |
| 27 | 1, 4, 7, 8, 10, 14, 15, 23 | hgmapeq0 43164 | . . . . . 6 ⊢ (𝜑 → ((𝐺‘𝑋) = 0 ↔ 𝑋 = 0 )) |
| 28 | 27 | necon3bid 3003 | . . . . 5 ⊢ (𝜑 → ((𝐺‘𝑋) ≠ 0 ↔ 𝑋 ≠ 0 )) |
| 29 | 26, 28 | mpbird 260 | . . . 4 ⊢ (𝜑 → (𝐺‘𝑋) ≠ 0 ) |
| 30 | 8, 10, 12 | drnginvrcl 21044 | . . . 4 ⊢ ((𝑅 ∈ DivRing ∧ (𝐺‘𝑋) ∈ 𝐵 ∧ (𝐺‘𝑋) ≠ 0 ) → (𝑁‘(𝐺‘𝑋)) ∈ 𝐵) |
| 31 | 22, 24, 29, 30 | syl3anc 1399 | . . 3 ⊢ (𝜑 → (𝑁‘(𝐺‘𝑋)) ∈ 𝐵) |
| 32 | 8, 10, 12 | drnginvrn0 21045 | . . . 4 ⊢ ((𝑅 ∈ DivRing ∧ (𝐺‘𝑋) ∈ 𝐵 ∧ (𝐺‘𝑋) ≠ 0 ) → (𝑁‘(𝐺‘𝑋)) ≠ 0 ) |
| 33 | 22, 24, 29, 32 | syl3anc 1399 | . . 3 ⊢ (𝜑 → (𝑁‘(𝐺‘𝑋)) ≠ 0 ) |
| 34 | eldifsn 4748 | . . 3 ⊢ ((𝑁‘(𝐺‘𝑋)) ∈ (𝐵 ∖ { 0 }) ↔ ((𝑁‘(𝐺‘𝑋)) ∈ 𝐵 ∧ (𝑁‘(𝐺‘𝑋)) ≠ 0 )) | |
| 35 | 31, 33, 34 | sylanbrc 595 | . 2 ⊢ (𝜑 → (𝑁‘(𝐺‘𝑋)) ∈ (𝐵 ∖ { 0 })) |
| 36 | 8, 10, 9, 11, 12 | drnginvrl 21047 | . . 3 ⊢ ((𝑅 ∈ DivRing ∧ (𝐺‘𝑋) ∈ 𝐵 ∧ (𝐺‘𝑋) ≠ 0 ) → ((𝑁‘(𝐺‘𝑋)) × (𝐺‘𝑋)) = 1 ) |
| 37 | 22, 24, 29, 36 | syl3anc 1399 | . 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 43183 | 1 ⊢ (𝜑 → (𝐺‘(𝐺‘𝑋)) = 𝑋) |
| Colors of variables: wff setvar class |
| This proof depends on syntax axioms: → wi 4 ∧ wa 401 = wceq 1570 ∈ wcel 2147 ≠ wne 2959 ∖ cdif 4048 {csn 4588 ⟨cop 4838 I cid 5550 ↾ cres 5658 ‘cfv 6561 (class class class)co 7446 Basecbs 17419 .rcmulr 17461 Scalarcsca 17463 ·𝑠 cvsca 17464 0gc0g 17642 1rcur 20440 invrcinvr 20650 DivRingcdr 21013 LVecclvec 21410 HLchlt 40610 LHypclh 41244 LTrncltrn 41361 DVecHcdvh 42338 ocHcoch 42607 HDMapchdma 43052 HGMapchg 43143 |
| 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 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5236 ax-sep 5253 ax-nul 5264 ax-pow 5332 ax-pr 5396 ax-un 7778 ax-cnex 11286 ax-resscn 11287 ax-1cn 11288 ax-icn 11289 ax-addcl 11290 ax-addrcl 11291 ax-mulcl 11292 ax-mulrcl 11293 ax-mulcom 11294 ax-addass 11295 ax-mulass 11296 ax-distr 11297 ax-i2m1 11298 ax-1ne0 11299 ax-1rid 11300 ax-rnegex 11301 ax-rrecex 11302 ax-cnre 11303 ax-pre-lttri 11304 ax-pre-lttrn 11305 ax-pre-ltadd 11306 ax-pre-mulgt0 11307 ax-riotaBAD 40213 |
| 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 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4839 df-ot 4862 df-uni 4871 df-int 4911 df-iun 4956 df-iin 4957 df-br 5107 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5551 df-eprel 5556 df-po 5564 df-so 5565 df-fr 5609 df-we 5611 df-xp 5662 df-rel 5663 df-cnv 5664 df-co 5665 df-dm 5666 df-rn 5667 df-res 5668 df-ima 5669 df-pred 6325 df-ord 6386 df-on 6387 df-lim 6388 df-suc 6389 df-iota 6515 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-riota 7403 df-ov 7449 df-oprab 7450 df-mpo 7451 df-of 7720 df-om 7905 df-1st 8028 df-2nd 8029 df-tpos 8274 df-undef 8321 df-frecs 8330 df-wrecs 8361 df-recs 8410 df-rdg 8449 df-1o 8507 df-2o 8508 df-er 8748 df-map 8880 df-en 9005 df-dom 9006 df-sdom 9007 df-fin 9008 df-pnf 11375 df-mnf 11376 df-xr 11377 df-ltxr 11378 df-le 11379 df-sub 11573 df-neg 11574 df-nn 12366 df-2 12435 df-3 12436 df-4 12437 df-5 12438 df-6 12439 df-n0 12637 df-z 12724 df-uz 12996 df-fz 13670 df-struct 17357 df-sets 17374 df-slot 17392 df-ndx 17404 df-base 17420 df-ress 17441 df-plusg 17473 df-mulr 17474 df-sca 17476 df-vsca 17477 df-0g 17644 df-mre 17788 df-mrc 17789 df-acs 17791 df-proset 18500 df-poset 18519 df-plt 18534 df-lub 18550 df-glb 18551 df-join 18552 df-meet 18553 df-p0 18629 df-p1 18630 df-lat 18638 df-clat 18705 df-mgm 18848 df-sgrp 18940 df-mnd 18956 df-submnd 19011 df-grp 19179 df-minusg 19180 df-sbg 19181 df-subg 19365 df-cntz 19564 df-oppg 19593 df-lsm 19883 df-cmn 20029 df-abl 20030 df-mgp 20394 df-rng 20408 df-ur 20441 df-ring 20494 df-oppr 20600 df-dvdsr 20620 df-unit 20621 df-invr 20651 df-dvr 20664 df-nzr 20796 df-rlreg 20979 df-domn 20980 df-drng 21015 df-lmod 21170 df-lss 21240 df-lsp 21280 df-lvec 21411 df-lsatoms 40236 df-lshyp 40237 df-lcv 40279 df-lfl 40318 df-lkr 40346 df-ldual 40384 df-oposet 40436 df-ol 40438 df-oml 40439 df-covers 40526 df-ats 40527 df-atl 40558 df-cvlat 40582 df-hlat 40611 df-llines 40758 df-lplanes 40759 df-lvols 40760 df-lines 40761 df-psubsp 40763 df-pmap 40764 df-padd 41056 df-lhyp 41248 df-laut 41249 df-ldil 41364 df-ltrn 41365 df-trl 41419 df-tgrp 42003 df-tendo 42015 df-edring 42017 df-dveca 42263 df-disoa 42289 df-dvech 42339 df-dib 42399 df-dic 42433 df-dih 42489 df-doch 42608 df-djh 42655 df-lcdual 42847 df-mapd 42885 df-hvmap 43017 df-hdmap1 43053 df-hdmap 43054 df-hgmap 43144 |
| This theorem is used by: hgmapvvlem3 43185 |
| Copyright terms: Public domain | W3C validator |