Nearby theorems
|
|
Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
|
| Mirrors > Home > MPE Home > Th. List > Mathboxes > hdmapglem5 | Structured version Visualization version GIF version | ||
| Description: Part 1.2 in [Baer] p. 110 line 34, f(u,v) alpha = f(v,u). (Contributed by NM, 12-Jun-2015.) |
| Ref | Expression |
|---|---|
| hdmapglem5.h | ⊢ 𝐻 = (LHyp‘𝐾) |
| hdmapglem5.e | ⊢ 𝐸 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩ |
| hdmapglem5.o | ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊) |
| hdmapglem5.u | ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
| hdmapglem5.v | ⊢ 𝑉 = (Base‘𝑈) |
| hdmapglem5.p | ⊢ + = (+g‘𝑈) |
| hdmapglem5.m | ⊢ − = (-g‘𝑈) |
| hdmapglem5.q | ⊢ · = ( ·𝑠 ‘𝑈) |
| hdmapglem5.r | ⊢ 𝑅 = (Scalar‘𝑈) |
| hdmapglem5.b | ⊢ 𝐵 = (Base‘𝑅) |
| hdmapglem5.t | ⊢ × = (.r‘𝑅) |
| hdmapglem5.z | ⊢ 0 = (0g‘𝑅) |
| hdmapglem5.s | ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) |
| hdmapglem5.g | ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊) |
| hdmapglem5.k | ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
| hdmapglem5.c | ⊢ (𝜑 → 𝐶 ∈ (𝑂‘{𝐸})) |
| hdmapglem5.d | ⊢ (𝜑 → 𝐷 ∈ (𝑂‘{𝐸})) |
| hdmapglem5.i | ⊢ (𝜑 → 𝐼 ∈ 𝐵) |
| hdmapglem5.j | ⊢ (𝜑 → 𝐽 ∈ 𝐵) |
| Ref | Expression |
|---|---|
| hdmapglem5 | ⊢ (𝜑 → (𝐺‘((𝑆‘𝐷)‘𝐶)) = ((𝑆‘𝐶)‘𝐷)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | hdmapglem5.h | . . . . 5 ⊢ 𝐻 = (LHyp‘𝐾) | |
| 2 | hdmapglem5.u | . . . . 5 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) | |
| 3 | hdmapglem5.k | . . . . 5 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) | |
| 4 | 1, 2, 3 | dvhlmod 41155 | . . . 4 ⊢ (𝜑 → 𝑈 ∈ LMod) |
| 5 | hdmapglem5.r | . . . . 5 ⊢ 𝑅 = (Scalar‘𝑈) | |
| 6 | 5 | lmodring 20802 | . . . 4 ⊢ (𝑈 ∈ LMod → 𝑅 ∈ Ring) |
| 7 | 4, 6 | syl 17 | . . 3 ⊢ (𝜑 → 𝑅 ∈ Ring) |
| 8 | hdmapglem5.b | . . . 4 ⊢ 𝐵 = (Base‘𝑅) | |
| 9 | hdmapglem5.g | . . . 4 ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊) | |
| 10 | hdmapglem5.v | . . . . 5 ⊢ 𝑉 = (Base‘𝑈) | |
| 11 | hdmapglem5.s | . . . . 5 ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) | |
| 12 | eqid 2731 | . . . . . . . . . 10 ⊢ (Base‘𝐾) = (Base‘𝐾) | |
| 13 | eqid 2731 | . . . . . . . . . 10 ⊢ ((LTrn‘𝐾)‘𝑊) = ((LTrn‘𝐾)‘𝑊) | |
| 14 | eqid 2731 | . . . . . . . . . 10 ⊢ (0g‘𝑈) = (0g‘𝑈) | |
| 15 | hdmapglem5.e | . . . . . . . . . 10 ⊢ 𝐸 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩ | |
| 16 | 1, 12, 13, 2, 10, 14, 15, 3 | dvheveccl 41157 | . . . . . . . . 9 ⊢ (𝜑 → 𝐸 ∈ (𝑉 ∖ {(0g‘𝑈)})) |
| 17 | 16 | eldifad 3914 | . . . . . . . 8 ⊢ (𝜑 → 𝐸 ∈ 𝑉) |
| 18 | 17 | snssd 4761 | . . . . . . 7 ⊢ (𝜑 → {𝐸} ⊆ 𝑉) |
| 19 | hdmapglem5.o | . . . . . . . 8 ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊) | |
| 20 | 1, 2, 10, 19 | dochssv 41400 | . . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ {𝐸} ⊆ 𝑉) → (𝑂‘{𝐸}) ⊆ 𝑉) |
| 21 | 3, 18, 20 | syl2anc 584 | . . . . . 6 ⊢ (𝜑 → (𝑂‘{𝐸}) ⊆ 𝑉) |
| 22 | hdmapglem5.c | . . . . . 6 ⊢ (𝜑 → 𝐶 ∈ (𝑂‘{𝐸})) | |
| 23 | 21, 22 | sseldd 3935 | . . . . 5 ⊢ (𝜑 → 𝐶 ∈ 𝑉) |
| 24 | hdmapglem5.d | . . . . . 6 ⊢ (𝜑 → 𝐷 ∈ (𝑂‘{𝐸})) | |
| 25 | 21, 24 | sseldd 3935 | . . . . 5 ⊢ (𝜑 → 𝐷 ∈ 𝑉) |
| 26 | 1, 2, 10, 5, 8, 11, 3, 23, 25 | hdmapipcl 41950 | . . . 4 ⊢ (𝜑 → ((𝑆‘𝐷)‘𝐶) ∈ 𝐵) |
| 27 | 1, 2, 5, 8, 9, 3, 26 | hgmapcl 41934 | . . 3 ⊢ (𝜑 → (𝐺‘((𝑆‘𝐷)‘𝐶)) ∈ 𝐵) |
| 28 | hdmapglem5.t | . . . 4 ⊢ × = (.r‘𝑅) | |
| 29 | eqid 2731 | . . . 4 ⊢ (1r‘𝑅) = (1r‘𝑅) | |
| 30 | 8, 28, 29 | ringlidm 20188 | . . 3 ⊢ ((𝑅 ∈ Ring ∧ (𝐺‘((𝑆‘𝐷)‘𝐶)) ∈ 𝐵) → ((1r‘𝑅) × (𝐺‘((𝑆‘𝐷)‘𝐶))) = (𝐺‘((𝑆‘𝐷)‘𝐶))) |
| 31 | 7, 27, 30 | syl2anc 584 | . 2 ⊢ (𝜑 → ((1r‘𝑅) × (𝐺‘((𝑆‘𝐷)‘𝐶))) = (𝐺‘((𝑆‘𝐷)‘𝐶))) |
| 32 | hdmapglem5.p | . . 3 ⊢ + = (+g‘𝑈) | |
| 33 | hdmapglem5.m | . . 3 ⊢ − = (-g‘𝑈) | |
| 34 | hdmapglem5.q | . . 3 ⊢ · = ( ·𝑠 ‘𝑈) | |
| 35 | hdmapglem5.z | . . 3 ⊢ 0 = (0g‘𝑅) | |
| 36 | 8, 29 | ringidcl 20184 | . . . 4 ⊢ (𝑅 ∈ Ring → (1r‘𝑅) ∈ 𝐵) |
| 37 | 7, 36 | syl 17 | . . 3 ⊢ (𝜑 → (1r‘𝑅) ∈ 𝐵) |
| 38 | 1, 2, 5, 29, 9, 3 | hgmapval1 41938 | . . . . 5 ⊢ (𝜑 → (𝐺‘(1r‘𝑅)) = (1r‘𝑅)) |
| 39 | 38 | oveq2d 7362 | . . . 4 ⊢ (𝜑 → (((𝑆‘𝐷)‘𝐶) × (𝐺‘(1r‘𝑅))) = (((𝑆‘𝐷)‘𝐶) × (1r‘𝑅))) |
| 40 | 8, 28, 29 | ringridm 20189 | . . . . 5 ⊢ ((𝑅 ∈ Ring ∧ ((𝑆‘𝐷)‘𝐶) ∈ 𝐵) → (((𝑆‘𝐷)‘𝐶) × (1r‘𝑅)) = ((𝑆‘𝐷)‘𝐶)) |
| 41 | 7, 26, 40 | syl2anc 584 | . . . 4 ⊢ (𝜑 → (((𝑆‘𝐷)‘𝐶) × (1r‘𝑅)) = ((𝑆‘𝐷)‘𝐶)) |
| 42 | 39, 41 | eqtrd 2766 | . . 3 ⊢ (𝜑 → (((𝑆‘𝐷)‘𝐶) × (𝐺‘(1r‘𝑅))) = ((𝑆‘𝐷)‘𝐶)) |
| 43 | 1, 15, 19, 2, 10, 32, 33, 34, 5, 8, 28, 35, 11, 9, 3, 22, 24, 26, 37, 42 | hdmapinvlem4 41966 | . 2 ⊢ (𝜑 → ((1r‘𝑅) × (𝐺‘((𝑆‘𝐷)‘𝐶))) = ((𝑆‘𝐶)‘𝐷)) |
| 44 | 31, 43 | eqtr3d 2768 | 1 ⊢ (𝜑 → (𝐺‘((𝑆‘𝐷)‘𝐶)) = ((𝑆‘𝐶)‘𝐷)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 = wceq 1541 ∈ wcel 2111 ⊆ wss 3902 {csn 4576 ⟨cop 4582 I cid 5510 ↾ cres 5618 ‘cfv 6481 (class class class)co 7346 Basecbs 17120 +gcplusg 17161 .rcmulr 17162 Scalarcsca 17164 ·𝑠 cvsca 17165 0gc0g 17343 -gcsg 18848 1rcur 20100 Ringcrg 20152 LModclmod 20794 HLchlt 39395 LHypclh 40029 LTrncltrn 40146 DVecHcdvh 41123 ocHcoch 41392 HDMapchdma 41837 HGMapchg 41928 |
| 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 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-rep 5217 ax-sep 5234 ax-nul 5244 ax-pow 5303 ax-pr 5370 ax-un 7668 ax-cnex 11062 ax-resscn 11063 ax-1cn 11064 ax-icn 11065 ax-addcl 11066 ax-addrcl 11067 ax-mulcl 11068 ax-mulrcl 11069 ax-mulcom 11070 ax-addass 11071 ax-mulass 11072 ax-distr 11073 ax-i2m1 11074 ax-1ne0 11075 ax-1rid 11076 ax-rnegex 11077 ax-rrecex 11078 ax-cnre 11079 ax-pre-lttri 11080 ax-pre-lttrn 11081 ax-pre-ltadd 11082 ax-pre-mulgt0 11083 ax-riotaBAD 38998 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-rmo 3346 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3742 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4284 df-if 4476 df-pw 4552 df-sn 4577 df-pr 4579 df-tp 4581 df-op 4583 df-ot 4585 df-uni 4860 df-int 4898 df-iun 4943 df-iin 4944 df-br 5092 df-opab 5154 df-mpt 5173 df-tr 5199 df-id 5511 df-eprel 5516 df-po 5524 df-so 5525 df-fr 5569 df-we 5571 df-xp 5622 df-rel 5623 df-cnv 5624 df-co 5625 df-dm 5626 df-rn 5627 df-res 5628 df-ima 5629 df-pred 6248 df-ord 6309 df-on 6310 df-lim 6311 df-suc 6312 df-iota 6437 df-fun 6483 df-fn 6484 df-f 6485 df-f1 6486 df-fo 6487 df-f1o 6488 df-fv 6489 df-riota 7303 df-ov 7349 df-oprab 7350 df-mpo 7351 df-of 7610 df-om 7797 df-1st 7921 df-2nd 7922 df-tpos 8156 df-undef 8203 df-frecs 8211 df-wrecs 8242 df-recs 8291 df-rdg 8329 df-1o 8385 df-2o 8386 df-er 8622 df-map 8752 df-en 8870 df-dom 8871 df-sdom 8872 df-fin 8873 df-pnf 11148 df-mnf 11149 df-xr 11150 df-ltxr 11151 df-le 11152 df-sub 11346 df-neg 11347 df-nn 12126 df-2 12188 df-3 12189 df-4 12190 df-5 12191 df-6 12192 df-n0 12382 df-z 12469 df-uz 12733 df-fz 13408 df-struct 17058 df-sets 17075 df-slot 17093 df-ndx 17105 df-base 17121 df-ress 17142 df-plusg 17174 df-mulr 17175 df-sca 17177 df-vsca 17178 df-0g 17345 df-mre 17488 df-mrc 17489 df-acs 17491 df-proset 18200 df-poset 18219 df-plt 18234 df-lub 18250 df-glb 18251 df-join 18252 df-meet 18253 df-p0 18329 df-p1 18330 df-lat 18338 df-clat 18405 df-mgm 18548 df-sgrp 18627 df-mnd 18643 df-submnd 18692 df-grp 18849 df-minusg 18850 df-sbg 18851 df-subg 19036 df-cntz 19230 df-oppg 19259 df-lsm 19549 df-cmn 19695 df-abl 19696 df-mgp 20060 df-rng 20072 df-ur 20101 df-ring 20154 df-oppr 20256 df-dvdsr 20276 df-unit 20277 df-invr 20307 df-dvr 20320 df-nzr 20429 df-rlreg 20610 df-domn 20611 df-drng 20647 df-lmod 20796 df-lss 20866 df-lsp 20906 df-lvec 21038 df-lsatoms 39021 df-lshyp 39022 df-lcv 39064 df-lfl 39103 df-lkr 39131 df-ldual 39169 df-oposet 39221 df-ol 39223 df-oml 39224 df-covers 39311 df-ats 39312 df-atl 39343 df-cvlat 39367 df-hlat 39396 df-llines 39543 df-lplanes 39544 df-lvols 39545 df-lines 39546 df-psubsp 39548 df-pmap 39549 df-padd 39841 df-lhyp 40033 df-laut 40034 df-ldil 40149 df-ltrn 40150 df-trl 40204 df-tgrp 40788 df-tendo 40800 df-edring 40802 df-dveca 41048 df-disoa 41074 df-dvech 41124 df-dib 41184 df-dic 41218 df-dih 41274 df-doch 41393 df-djh 41440 df-lcdual 41632 df-mapd 41670 df-hvmap 41802 df-hdmap1 41838 df-hdmap 41839 df-hgmap 41929 |
| This theorem is referenced by: hgmapvvlem1 41968 hdmapglem7 41974 |
| Copyright terms: Public domain | W3C validator |