![]() |
Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > hgmaprnlem2N | Structured version Visualization version GIF version |
Description: Lemma for hgmaprnN 40641. Part 15 of [Baer] p. 50 line 20. We only require a subset relation, rather than equality, so that the case of zero 𝑧 is taken care of automatically. (Contributed by NM, 7-Jun-2015.) (New usage is discouraged.) |
Ref | Expression |
---|---|
hgmaprnlem1.h | ⊢ 𝐻 = (LHyp‘𝐾) |
hgmaprnlem1.u | ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
hgmaprnlem1.v | ⊢ 𝑉 = (Base‘𝑈) |
hgmaprnlem1.r | ⊢ 𝑅 = (Scalar‘𝑈) |
hgmaprnlem1.b | ⊢ 𝐵 = (Base‘𝑅) |
hgmaprnlem1.t | ⊢ · = ( ·𝑠 ‘𝑈) |
hgmaprnlem1.o | ⊢ 0 = (0g‘𝑈) |
hgmaprnlem1.c | ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) |
hgmaprnlem1.d | ⊢ 𝐷 = (Base‘𝐶) |
hgmaprnlem1.p | ⊢ 𝑃 = (Scalar‘𝐶) |
hgmaprnlem1.a | ⊢ 𝐴 = (Base‘𝑃) |
hgmaprnlem1.e | ⊢ ∙ = ( ·𝑠 ‘𝐶) |
hgmaprnlem1.q | ⊢ 𝑄 = (0g‘𝐶) |
hgmaprnlem1.s | ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) |
hgmaprnlem1.g | ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊) |
hgmaprnlem1.k | ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
hgmaprnlem1.z | ⊢ (𝜑 → 𝑧 ∈ 𝐴) |
hgmaprnlem1.t2 | ⊢ (𝜑 → 𝑡 ∈ (𝑉 ∖ { 0 })) |
hgmaprnlem1.s2 | ⊢ (𝜑 → 𝑠 ∈ 𝑉) |
hgmaprnlem1.sz | ⊢ (𝜑 → (𝑆‘𝑠) = (𝑧 ∙ (𝑆‘𝑡))) |
hgmaprnlem1.m | ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) |
hgmaprnlem1.n | ⊢ 𝑁 = (LSpan‘𝑈) |
hgmaprnlem1.l | ⊢ 𝐿 = (LSpan‘𝐶) |
Ref | Expression |
---|---|
hgmaprnlem2N | ⊢ (𝜑 → (𝑁‘{𝑠}) ⊆ (𝑁‘{𝑡})) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hgmaprnlem1.h | . . . . 5 ⊢ 𝐻 = (LHyp‘𝐾) | |
2 | hgmaprnlem1.c | . . . . 5 ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) | |
3 | hgmaprnlem1.k | . . . . 5 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) | |
4 | 1, 2, 3 | lcdlmod 40332 | . . . 4 ⊢ (𝜑 → 𝐶 ∈ LMod) |
5 | hgmaprnlem1.z | . . . 4 ⊢ (𝜑 → 𝑧 ∈ 𝐴) | |
6 | hgmaprnlem1.u | . . . . 5 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) | |
7 | hgmaprnlem1.v | . . . . 5 ⊢ 𝑉 = (Base‘𝑈) | |
8 | hgmaprnlem1.d | . . . . 5 ⊢ 𝐷 = (Base‘𝐶) | |
9 | hgmaprnlem1.s | . . . . 5 ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) | |
10 | hgmaprnlem1.t2 | . . . . . 6 ⊢ (𝜑 → 𝑡 ∈ (𝑉 ∖ { 0 })) | |
11 | 10 | eldifad 3957 | . . . . 5 ⊢ (𝜑 → 𝑡 ∈ 𝑉) |
12 | 1, 6, 7, 2, 8, 9, 3, 11 | hdmapcl 40570 | . . . 4 ⊢ (𝜑 → (𝑆‘𝑡) ∈ 𝐷) |
13 | hgmaprnlem1.p | . . . . 5 ⊢ 𝑃 = (Scalar‘𝐶) | |
14 | hgmaprnlem1.a | . . . . 5 ⊢ 𝐴 = (Base‘𝑃) | |
15 | hgmaprnlem1.e | . . . . 5 ⊢ ∙ = ( ·𝑠 ‘𝐶) | |
16 | hgmaprnlem1.l | . . . . 5 ⊢ 𝐿 = (LSpan‘𝐶) | |
17 | 13, 14, 8, 15, 16 | lspsnvsi 20566 | . . . 4 ⊢ ((𝐶 ∈ LMod ∧ 𝑧 ∈ 𝐴 ∧ (𝑆‘𝑡) ∈ 𝐷) → (𝐿‘{(𝑧 ∙ (𝑆‘𝑡))}) ⊆ (𝐿‘{(𝑆‘𝑡)})) |
18 | 4, 5, 12, 17 | syl3anc 1371 | . . 3 ⊢ (𝜑 → (𝐿‘{(𝑧 ∙ (𝑆‘𝑡))}) ⊆ (𝐿‘{(𝑆‘𝑡)})) |
19 | hgmaprnlem1.n | . . . . 5 ⊢ 𝑁 = (LSpan‘𝑈) | |
20 | hgmaprnlem1.m | . . . . 5 ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) | |
21 | hgmaprnlem1.s2 | . . . . 5 ⊢ (𝜑 → 𝑠 ∈ 𝑉) | |
22 | 1, 6, 7, 19, 2, 16, 20, 9, 3, 21 | hdmap10 40580 | . . . 4 ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑠})) = (𝐿‘{(𝑆‘𝑠)})) |
23 | hgmaprnlem1.sz | . . . . . 6 ⊢ (𝜑 → (𝑆‘𝑠) = (𝑧 ∙ (𝑆‘𝑡))) | |
24 | 23 | sneqd 4635 | . . . . 5 ⊢ (𝜑 → {(𝑆‘𝑠)} = {(𝑧 ∙ (𝑆‘𝑡))}) |
25 | 24 | fveq2d 6883 | . . . 4 ⊢ (𝜑 → (𝐿‘{(𝑆‘𝑠)}) = (𝐿‘{(𝑧 ∙ (𝑆‘𝑡))})) |
26 | 22, 25 | eqtrd 2772 | . . 3 ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑠})) = (𝐿‘{(𝑧 ∙ (𝑆‘𝑡))})) |
27 | 1, 6, 7, 19, 2, 16, 20, 9, 3, 11 | hdmap10 40580 | . . 3 ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑡})) = (𝐿‘{(𝑆‘𝑡)})) |
28 | 18, 26, 27 | 3sstr4d 4026 | . 2 ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑠})) ⊆ (𝑀‘(𝑁‘{𝑡}))) |
29 | eqid 2732 | . . 3 ⊢ (LSubSp‘𝑈) = (LSubSp‘𝑈) | |
30 | 1, 6, 3 | dvhlmod 39850 | . . . 4 ⊢ (𝜑 → 𝑈 ∈ LMod) |
31 | 7, 29, 19 | lspsncl 20539 | . . . 4 ⊢ ((𝑈 ∈ LMod ∧ 𝑠 ∈ 𝑉) → (𝑁‘{𝑠}) ∈ (LSubSp‘𝑈)) |
32 | 30, 21, 31 | syl2anc 584 | . . 3 ⊢ (𝜑 → (𝑁‘{𝑠}) ∈ (LSubSp‘𝑈)) |
33 | 7, 29, 19 | lspsncl 20539 | . . . 4 ⊢ ((𝑈 ∈ LMod ∧ 𝑡 ∈ 𝑉) → (𝑁‘{𝑡}) ∈ (LSubSp‘𝑈)) |
34 | 30, 11, 33 | syl2anc 584 | . . 3 ⊢ (𝜑 → (𝑁‘{𝑡}) ∈ (LSubSp‘𝑈)) |
35 | 1, 6, 29, 20, 3, 32, 34 | mapdord 40378 | . 2 ⊢ (𝜑 → ((𝑀‘(𝑁‘{𝑠})) ⊆ (𝑀‘(𝑁‘{𝑡})) ↔ (𝑁‘{𝑠}) ⊆ (𝑁‘{𝑡}))) |
36 | 28, 35 | mpbid 231 | 1 ⊢ (𝜑 → (𝑁‘{𝑠}) ⊆ (𝑁‘{𝑡})) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1541 ∈ wcel 2106 ∖ cdif 3942 ⊆ wss 3945 {csn 4623 ‘cfv 6533 (class class class)co 7394 Basecbs 17128 Scalarcsca 17184 ·𝑠 cvsca 17185 0gc0g 17369 LModclmod 20422 LSubSpclss 20493 LSpanclspn 20533 HLchlt 38089 LHypclh 38724 DVecHcdvh 39818 LCDualclcd 40326 mapdcmpd 40364 HDMapchdma 40532 HGMapchg 40623 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 ax-rep 5279 ax-sep 5293 ax-nul 5300 ax-pow 5357 ax-pr 5421 ax-un 7709 ax-cnex 11150 ax-resscn 11151 ax-1cn 11152 ax-icn 11153 ax-addcl 11154 ax-addrcl 11155 ax-mulcl 11156 ax-mulrcl 11157 ax-mulcom 11158 ax-addass 11159 ax-mulass 11160 ax-distr 11161 ax-i2m1 11162 ax-1ne0 11163 ax-1rid 11164 ax-rnegex 11165 ax-rrecex 11166 ax-cnre 11167 ax-pre-lttri 11168 ax-pre-lttrn 11169 ax-pre-ltadd 11170 ax-pre-mulgt0 11171 ax-riotaBAD 37692 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3376 df-reu 3377 df-rab 3433 df-v 3476 df-sbc 3775 df-csb 3891 df-dif 3948 df-un 3950 df-in 3952 df-ss 3962 df-pss 3964 df-nul 4320 df-if 4524 df-pw 4599 df-sn 4624 df-pr 4626 df-tp 4628 df-op 4630 df-ot 4632 df-uni 4903 df-int 4945 df-iun 4993 df-iin 4994 df-br 5143 df-opab 5205 df-mpt 5226 df-tr 5260 df-id 5568 df-eprel 5574 df-po 5582 df-so 5583 df-fr 5625 df-we 5627 df-xp 5676 df-rel 5677 df-cnv 5678 df-co 5679 df-dm 5680 df-rn 5681 df-res 5682 df-ima 5683 df-pred 6290 df-ord 6357 df-on 6358 df-lim 6359 df-suc 6360 df-iota 6485 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-riota 7350 df-ov 7397 df-oprab 7398 df-mpo 7399 df-of 7654 df-om 7840 df-1st 7959 df-2nd 7960 df-tpos 8195 df-undef 8242 df-frecs 8250 df-wrecs 8281 df-recs 8355 df-rdg 8394 df-1o 8450 df-er 8688 df-map 8807 df-en 8925 df-dom 8926 df-sdom 8927 df-fin 8928 df-pnf 11234 df-mnf 11235 df-xr 11236 df-ltxr 11237 df-le 11238 df-sub 11430 df-neg 11431 df-nn 12197 df-2 12259 df-3 12260 df-4 12261 df-5 12262 df-6 12263 df-n0 12457 df-z 12543 df-uz 12807 df-fz 13469 df-struct 17064 df-sets 17081 df-slot 17099 df-ndx 17111 df-base 17129 df-ress 17158 df-plusg 17194 df-mulr 17195 df-sca 17197 df-vsca 17198 df-0g 17371 df-mre 17514 df-mrc 17515 df-acs 17517 df-proset 18232 df-poset 18250 df-plt 18267 df-lub 18283 df-glb 18284 df-join 18285 df-meet 18286 df-p0 18362 df-p1 18363 df-lat 18369 df-clat 18436 df-mgm 18545 df-sgrp 18594 df-mnd 18605 df-submnd 18650 df-grp 18799 df-minusg 18800 df-sbg 18801 df-subg 18977 df-cntz 19149 df-oppg 19176 df-lsm 19470 df-cmn 19616 df-abl 19617 df-mgp 19949 df-ur 19966 df-ring 20018 df-oppr 20104 df-dvdsr 20125 df-unit 20126 df-invr 20156 df-dvr 20167 df-drng 20269 df-lmod 20424 df-lss 20494 df-lsp 20534 df-lvec 20665 df-lsatoms 37715 df-lshyp 37716 df-lcv 37758 df-lfl 37797 df-lkr 37825 df-ldual 37863 df-oposet 37915 df-ol 37917 df-oml 37918 df-covers 38005 df-ats 38006 df-atl 38037 df-cvlat 38061 df-hlat 38090 df-llines 38238 df-lplanes 38239 df-lvols 38240 df-lines 38241 df-psubsp 38243 df-pmap 38244 df-padd 38536 df-lhyp 38728 df-laut 38729 df-ldil 38844 df-ltrn 38845 df-trl 38899 df-tgrp 39483 df-tendo 39495 df-edring 39497 df-dveca 39743 df-disoa 39769 df-dvech 39819 df-dib 39879 df-dic 39913 df-dih 39969 df-doch 40088 df-djh 40135 df-lcdual 40327 df-mapd 40365 df-hvmap 40497 df-hdmap1 40533 df-hdmap 40534 |
This theorem is referenced by: hgmaprnlem3N 40638 |
Copyright terms: Public domain | W3C validator |