Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > hgmapvv | Structured version Visualization version GIF version |
Description: Value of a double involution. Part 1.2 of [Baer] p. 110 line 37. (Contributed by NM, 13-Jun-2015.) |
Ref | Expression |
---|---|
hgmapvv.h | ⊢ 𝐻 = (LHyp‘𝐾) |
hgmapvv.u | ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
hgmapvv.r | ⊢ 𝑅 = (Scalar‘𝑈) |
hgmapvv.b | ⊢ 𝐵 = (Base‘𝑅) |
hgmapvv.g | ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊) |
hgmapvv.k | ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
hgmapvv.j | ⊢ (𝜑 → 𝑋 ∈ 𝐵) |
Ref | Expression |
---|---|
hgmapvv | ⊢ (𝜑 → (𝐺‘(𝐺‘𝑋)) = 𝑋) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2fveq3 6661 | . . 3 ⊢ (𝑋 = (0g‘𝑅) → (𝐺‘(𝐺‘𝑋)) = (𝐺‘(𝐺‘(0g‘𝑅)))) | |
2 | id 22 | . . 3 ⊢ (𝑋 = (0g‘𝑅) → 𝑋 = (0g‘𝑅)) | |
3 | 1, 2 | eqeq12d 2837 | . 2 ⊢ (𝑋 = (0g‘𝑅) → ((𝐺‘(𝐺‘𝑋)) = 𝑋 ↔ (𝐺‘(𝐺‘(0g‘𝑅))) = (0g‘𝑅))) |
4 | hgmapvv.h | . . 3 ⊢ 𝐻 = (LHyp‘𝐾) | |
5 | eqid 2821 | . . 3 ⊢ 〈( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))〉 = 〈( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))〉 | |
6 | eqid 2821 | . . 3 ⊢ ((ocH‘𝐾)‘𝑊) = ((ocH‘𝐾)‘𝑊) | |
7 | hgmapvv.u | . . 3 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) | |
8 | eqid 2821 | . . 3 ⊢ (Base‘𝑈) = (Base‘𝑈) | |
9 | eqid 2821 | . . 3 ⊢ ( ·𝑠 ‘𝑈) = ( ·𝑠 ‘𝑈) | |
10 | hgmapvv.r | . . 3 ⊢ 𝑅 = (Scalar‘𝑈) | |
11 | hgmapvv.b | . . 3 ⊢ 𝐵 = (Base‘𝑅) | |
12 | eqid 2821 | . . 3 ⊢ (.r‘𝑅) = (.r‘𝑅) | |
13 | eqid 2821 | . . 3 ⊢ (0g‘𝑅) = (0g‘𝑅) | |
14 | eqid 2821 | . . 3 ⊢ (1r‘𝑅) = (1r‘𝑅) | |
15 | eqid 2821 | . . 3 ⊢ (invr‘𝑅) = (invr‘𝑅) | |
16 | eqid 2821 | . . 3 ⊢ ((HDMap‘𝐾)‘𝑊) = ((HDMap‘𝐾)‘𝑊) | |
17 | hgmapvv.g | . . 3 ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊) | |
18 | hgmapvv.k | . . . 4 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) | |
19 | 18 | adantr 483 | . . 3 ⊢ ((𝜑 ∧ 𝑋 ≠ (0g‘𝑅)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
20 | hgmapvv.j | . . . . 5 ⊢ (𝜑 → 𝑋 ∈ 𝐵) | |
21 | 20 | anim1i 616 | . . . 4 ⊢ ((𝜑 ∧ 𝑋 ≠ (0g‘𝑅)) → (𝑋 ∈ 𝐵 ∧ 𝑋 ≠ (0g‘𝑅))) |
22 | eldifsn 4705 | . . . 4 ⊢ (𝑋 ∈ (𝐵 ∖ {(0g‘𝑅)}) ↔ (𝑋 ∈ 𝐵 ∧ 𝑋 ≠ (0g‘𝑅))) | |
23 | 21, 22 | sylibr 236 | . . 3 ⊢ ((𝜑 ∧ 𝑋 ≠ (0g‘𝑅)) → 𝑋 ∈ (𝐵 ∖ {(0g‘𝑅)})) |
24 | 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 19, 23 | hgmapvvlem3 39093 | . 2 ⊢ ((𝜑 ∧ 𝑋 ≠ (0g‘𝑅)) → (𝐺‘(𝐺‘𝑋)) = 𝑋) |
25 | 4, 7, 10, 13, 17, 18 | hgmapval0 39060 | . . . 4 ⊢ (𝜑 → (𝐺‘(0g‘𝑅)) = (0g‘𝑅)) |
26 | 25 | fveq2d 6660 | . . 3 ⊢ (𝜑 → (𝐺‘(𝐺‘(0g‘𝑅))) = (𝐺‘(0g‘𝑅))) |
27 | 26, 25 | eqtrd 2856 | . 2 ⊢ (𝜑 → (𝐺‘(𝐺‘(0g‘𝑅))) = (0g‘𝑅)) |
28 | 3, 24, 27 | pm2.61ne 3102 | 1 ⊢ (𝜑 → (𝐺‘(𝐺‘𝑋)) = 𝑋) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 = wceq 1537 ∈ wcel 2114 ≠ wne 3016 ∖ cdif 3921 {csn 4553 〈cop 4559 I cid 5445 ↾ cres 5543 ‘cfv 6341 Basecbs 16466 .rcmulr 16549 Scalarcsca 16551 ·𝑠 cvsca 16552 0gc0g 16696 1rcur 19234 invrcinvr 19404 HLchlt 36518 LHypclh 37152 LTrncltrn 37269 DVecHcdvh 38246 ocHcoch 38515 HDMapchdma 38960 HGMapchg 39051 |
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 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 ax-rep 5176 ax-sep 5189 ax-nul 5196 ax-pow 5252 ax-pr 5316 ax-un 7447 ax-cnex 10579 ax-resscn 10580 ax-1cn 10581 ax-icn 10582 ax-addcl 10583 ax-addrcl 10584 ax-mulcl 10585 ax-mulrcl 10586 ax-mulcom 10587 ax-addass 10588 ax-mulass 10589 ax-distr 10590 ax-i2m1 10591 ax-1ne0 10592 ax-1rid 10593 ax-rnegex 10594 ax-rrecex 10595 ax-cnre 10596 ax-pre-lttri 10597 ax-pre-lttrn 10598 ax-pre-ltadd 10599 ax-pre-mulgt0 10600 ax-riotaBAD 36121 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1540 df-fal 1550 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-nel 3124 df-ral 3143 df-rex 3144 df-reu 3145 df-rmo 3146 df-rab 3147 df-v 3488 df-sbc 3764 df-csb 3872 df-dif 3927 df-un 3929 df-in 3931 df-ss 3940 df-pss 3942 df-nul 4280 df-if 4454 df-pw 4527 df-sn 4554 df-pr 4556 df-tp 4558 df-op 4560 df-ot 4562 df-uni 4825 df-int 4863 df-iun 4907 df-iin 4908 df-br 5053 df-opab 5115 df-mpt 5133 df-tr 5159 df-id 5446 df-eprel 5451 df-po 5460 df-so 5461 df-fr 5500 df-we 5502 df-xp 5547 df-rel 5548 df-cnv 5549 df-co 5550 df-dm 5551 df-rn 5552 df-res 5553 df-ima 5554 df-pred 6134 df-ord 6180 df-on 6181 df-lim 6182 df-suc 6183 df-iota 6300 df-fun 6343 df-fn 6344 df-f 6345 df-f1 6346 df-fo 6347 df-f1o 6348 df-fv 6349 df-riota 7100 df-ov 7145 df-oprab 7146 df-mpo 7147 df-of 7395 df-om 7567 df-1st 7675 df-2nd 7676 df-tpos 7878 df-undef 7925 df-wrecs 7933 df-recs 7994 df-rdg 8032 df-1o 8088 df-oadd 8092 df-er 8275 df-map 8394 df-en 8496 df-dom 8497 df-sdom 8498 df-fin 8499 df-pnf 10663 df-mnf 10664 df-xr 10665 df-ltxr 10666 df-le 10667 df-sub 10858 df-neg 10859 df-nn 11625 df-2 11687 df-3 11688 df-4 11689 df-5 11690 df-6 11691 df-n0 11885 df-z 11969 df-uz 12231 df-fz 12883 df-struct 16468 df-ndx 16469 df-slot 16470 df-base 16472 df-sets 16473 df-ress 16474 df-plusg 16561 df-mulr 16562 df-sca 16564 df-vsca 16565 df-0g 16698 df-mre 16840 df-mrc 16841 df-acs 16843 df-proset 17521 df-poset 17539 df-plt 17551 df-lub 17567 df-glb 17568 df-join 17569 df-meet 17570 df-p0 17632 df-p1 17633 df-lat 17639 df-clat 17701 df-mgm 17835 df-sgrp 17884 df-mnd 17895 df-submnd 17940 df-grp 18089 df-minusg 18090 df-sbg 18091 df-subg 18259 df-cntz 18430 df-oppg 18457 df-lsm 18744 df-cmn 18891 df-abl 18892 df-mgp 19223 df-ur 19235 df-ring 19282 df-oppr 19356 df-dvdsr 19374 df-unit 19375 df-invr 19405 df-dvr 19416 df-drng 19487 df-lmod 19619 df-lss 19687 df-lsp 19727 df-lvec 19858 df-lsatoms 36144 df-lshyp 36145 df-lcv 36187 df-lfl 36226 df-lkr 36254 df-ldual 36292 df-oposet 36344 df-ol 36346 df-oml 36347 df-covers 36434 df-ats 36435 df-atl 36466 df-cvlat 36490 df-hlat 36519 df-llines 36666 df-lplanes 36667 df-lvols 36668 df-lines 36669 df-psubsp 36671 df-pmap 36672 df-padd 36964 df-lhyp 37156 df-laut 37157 df-ldil 37272 df-ltrn 37273 df-trl 37327 df-tgrp 37911 df-tendo 37923 df-edring 37925 df-dveca 38171 df-disoa 38197 df-dvech 38247 df-dib 38307 df-dic 38341 df-dih 38397 df-doch 38516 df-djh 38563 df-lcdual 38755 df-mapd 38793 df-hvmap 38925 df-hdmap1 38961 df-hdmap 38962 df-hgmap 39052 |
This theorem is referenced by: hdmapglem7 39097 hlhilsrnglem 39121 |
Copyright terms: Public domain | W3C validator |