![]() |
Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > hdmaprnlem3N | Structured version Visualization version GIF version |
Description: Part of proof of part 12 in [Baer] p. 49 line 15, T ≠ P. Our (◡𝑀‘(𝐿‘{((𝑆‘𝑢) ✚ 𝑠)})) is Baer's P, where P* = G(u'+s). (Contributed by NM, 27-May-2015.) (New usage is discouraged.) |
Ref | Expression |
---|---|
hdmaprnlem1.h | ⊢ 𝐻 = (LHyp‘𝐾) |
hdmaprnlem1.u | ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
hdmaprnlem1.v | ⊢ 𝑉 = (Base‘𝑈) |
hdmaprnlem1.n | ⊢ 𝑁 = (LSpan‘𝑈) |
hdmaprnlem1.c | ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) |
hdmaprnlem1.l | ⊢ 𝐿 = (LSpan‘𝐶) |
hdmaprnlem1.m | ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) |
hdmaprnlem1.s | ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) |
hdmaprnlem1.k | ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
hdmaprnlem1.se | ⊢ (𝜑 → 𝑠 ∈ (𝐷 ∖ {𝑄})) |
hdmaprnlem1.ve | ⊢ (𝜑 → 𝑣 ∈ 𝑉) |
hdmaprnlem1.e | ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑣})) = (𝐿‘{𝑠})) |
hdmaprnlem1.ue | ⊢ (𝜑 → 𝑢 ∈ 𝑉) |
hdmaprnlem1.un | ⊢ (𝜑 → ¬ 𝑢 ∈ (𝑁‘{𝑣})) |
hdmaprnlem1.d | ⊢ 𝐷 = (Base‘𝐶) |
hdmaprnlem1.q | ⊢ 𝑄 = (0g‘𝐶) |
hdmaprnlem1.o | ⊢ 0 = (0g‘𝑈) |
hdmaprnlem1.a | ⊢ ✚ = (+g‘𝐶) |
Ref | Expression |
---|---|
hdmaprnlem3N | ⊢ (𝜑 → (𝑁‘{𝑣}) ≠ (◡𝑀‘(𝐿‘{((𝑆‘𝑢) ✚ 𝑠)}))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hdmaprnlem1.d | . . . . 5 ⊢ 𝐷 = (Base‘𝐶) | |
2 | hdmaprnlem1.l | . . . . 5 ⊢ 𝐿 = (LSpan‘𝐶) | |
3 | hdmaprnlem1.h | . . . . . 6 ⊢ 𝐻 = (LHyp‘𝐾) | |
4 | hdmaprnlem1.c | . . . . . 6 ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) | |
5 | hdmaprnlem1.k | . . . . . 6 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) | |
6 | 3, 4, 5 | lcdlmod 38173 | . . . . 5 ⊢ (𝜑 → 𝐶 ∈ LMod) |
7 | hdmaprnlem1.u | . . . . . . 7 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) | |
8 | hdmaprnlem1.v | . . . . . . 7 ⊢ 𝑉 = (Base‘𝑈) | |
9 | hdmaprnlem1.s | . . . . . . 7 ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) | |
10 | hdmaprnlem1.ue | . . . . . . 7 ⊢ (𝜑 → 𝑢 ∈ 𝑉) | |
11 | 3, 7, 8, 4, 1, 9, 5, 10 | hdmapcl 38411 | . . . . . 6 ⊢ (𝜑 → (𝑆‘𝑢) ∈ 𝐷) |
12 | hdmaprnlem1.se | . . . . . . 7 ⊢ (𝜑 → 𝑠 ∈ (𝐷 ∖ {𝑄})) | |
13 | 12 | eldifad 3843 | . . . . . 6 ⊢ (𝜑 → 𝑠 ∈ 𝐷) |
14 | hdmaprnlem1.a | . . . . . . 7 ⊢ ✚ = (+g‘𝐶) | |
15 | 1, 14 | lmodvacl 19373 | . . . . . 6 ⊢ ((𝐶 ∈ LMod ∧ (𝑆‘𝑢) ∈ 𝐷 ∧ 𝑠 ∈ 𝐷) → ((𝑆‘𝑢) ✚ 𝑠) ∈ 𝐷) |
16 | 6, 11, 13, 15 | syl3anc 1351 | . . . . 5 ⊢ (𝜑 → ((𝑆‘𝑢) ✚ 𝑠) ∈ 𝐷) |
17 | eqid 2778 | . . . . . 6 ⊢ (LSubSp‘𝐶) = (LSubSp‘𝐶) | |
18 | 1, 17, 2 | lspsncl 19474 | . . . . . . 7 ⊢ ((𝐶 ∈ LMod ∧ 𝑠 ∈ 𝐷) → (𝐿‘{𝑠}) ∈ (LSubSp‘𝐶)) |
19 | 6, 13, 18 | syl2anc 576 | . . . . . 6 ⊢ (𝜑 → (𝐿‘{𝑠}) ∈ (LSubSp‘𝐶)) |
20 | 1, 2 | lspsnid 19490 | . . . . . . 7 ⊢ ((𝐶 ∈ LMod ∧ 𝑠 ∈ 𝐷) → 𝑠 ∈ (𝐿‘{𝑠})) |
21 | 6, 13, 20 | syl2anc 576 | . . . . . 6 ⊢ (𝜑 → 𝑠 ∈ (𝐿‘{𝑠})) |
22 | hdmaprnlem1.q | . . . . . . 7 ⊢ 𝑄 = (0g‘𝐶) | |
23 | 3, 4, 5 | lcdlvec 38172 | . . . . . . 7 ⊢ (𝜑 → 𝐶 ∈ LVec) |
24 | hdmaprnlem1.o | . . . . . . . 8 ⊢ 0 = (0g‘𝑈) | |
25 | eqid 2778 | . . . . . . . . 9 ⊢ (LSubSp‘𝑈) = (LSubSp‘𝑈) | |
26 | 3, 7, 5 | dvhlmod 37691 | . . . . . . . . 9 ⊢ (𝜑 → 𝑈 ∈ LMod) |
27 | hdmaprnlem1.ve | . . . . . . . . . 10 ⊢ (𝜑 → 𝑣 ∈ 𝑉) | |
28 | hdmaprnlem1.n | . . . . . . . . . . 11 ⊢ 𝑁 = (LSpan‘𝑈) | |
29 | 8, 25, 28 | lspsncl 19474 | . . . . . . . . . 10 ⊢ ((𝑈 ∈ LMod ∧ 𝑣 ∈ 𝑉) → (𝑁‘{𝑣}) ∈ (LSubSp‘𝑈)) |
30 | 26, 27, 29 | syl2anc 576 | . . . . . . . . 9 ⊢ (𝜑 → (𝑁‘{𝑣}) ∈ (LSubSp‘𝑈)) |
31 | hdmaprnlem1.un | . . . . . . . . 9 ⊢ (𝜑 → ¬ 𝑢 ∈ (𝑁‘{𝑣})) | |
32 | 24, 25, 26, 30, 10, 31 | lssneln0 19449 | . . . . . . . 8 ⊢ (𝜑 → 𝑢 ∈ (𝑉 ∖ { 0 })) |
33 | 3, 7, 8, 24, 4, 22, 1, 9, 5, 32 | hdmapnzcl 38426 | . . . . . . 7 ⊢ (𝜑 → (𝑆‘𝑢) ∈ (𝐷 ∖ {𝑄})) |
34 | hdmaprnlem1.m | . . . . . . . 8 ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) | |
35 | hdmaprnlem1.e | . . . . . . . 8 ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑣})) = (𝐿‘{𝑠})) | |
36 | 3, 7, 8, 28, 4, 2, 34, 9, 5, 12, 27, 35, 10, 31 | hdmaprnlem1N 38430 | . . . . . . 7 ⊢ (𝜑 → (𝐿‘{(𝑆‘𝑢)}) ≠ (𝐿‘{𝑠})) |
37 | 1, 22, 2, 23, 33, 13, 36 | lspsnne1 19614 | . . . . . 6 ⊢ (𝜑 → ¬ (𝑆‘𝑢) ∈ (𝐿‘{𝑠})) |
38 | 1, 14, 17, 6, 19, 21, 11, 37 | lssvancl2 19442 | . . . . 5 ⊢ (𝜑 → ¬ ((𝑆‘𝑢) ✚ 𝑠) ∈ (𝐿‘{𝑠})) |
39 | 1, 2, 6, 16, 13, 38 | lspsnne2 19615 | . . . 4 ⊢ (𝜑 → (𝐿‘{((𝑆‘𝑢) ✚ 𝑠)}) ≠ (𝐿‘{𝑠})) |
40 | 39 | necomd 3022 | . . 3 ⊢ (𝜑 → (𝐿‘{𝑠}) ≠ (𝐿‘{((𝑆‘𝑢) ✚ 𝑠)})) |
41 | 1, 17, 2 | lspsncl 19474 | . . . . . 6 ⊢ ((𝐶 ∈ LMod ∧ ((𝑆‘𝑢) ✚ 𝑠) ∈ 𝐷) → (𝐿‘{((𝑆‘𝑢) ✚ 𝑠)}) ∈ (LSubSp‘𝐶)) |
42 | 6, 16, 41 | syl2anc 576 | . . . . 5 ⊢ (𝜑 → (𝐿‘{((𝑆‘𝑢) ✚ 𝑠)}) ∈ (LSubSp‘𝐶)) |
43 | 3, 34, 4, 17, 5 | mapdrn2 38232 | . . . . 5 ⊢ (𝜑 → ran 𝑀 = (LSubSp‘𝐶)) |
44 | 42, 43 | eleqtrrd 2869 | . . . 4 ⊢ (𝜑 → (𝐿‘{((𝑆‘𝑢) ✚ 𝑠)}) ∈ ran 𝑀) |
45 | 3, 34, 5, 44 | mapdcnvid2 38238 | . . 3 ⊢ (𝜑 → (𝑀‘(◡𝑀‘(𝐿‘{((𝑆‘𝑢) ✚ 𝑠)}))) = (𝐿‘{((𝑆‘𝑢) ✚ 𝑠)})) |
46 | 40, 35, 45 | 3netr4d 3044 | . 2 ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑣})) ≠ (𝑀‘(◡𝑀‘(𝐿‘{((𝑆‘𝑢) ✚ 𝑠)})))) |
47 | 3, 34, 7, 25, 5, 44 | mapdcnvcl 38233 | . . . 4 ⊢ (𝜑 → (◡𝑀‘(𝐿‘{((𝑆‘𝑢) ✚ 𝑠)})) ∈ (LSubSp‘𝑈)) |
48 | 3, 7, 25, 34, 5, 30, 47 | mapd11 38220 | . . 3 ⊢ (𝜑 → ((𝑀‘(𝑁‘{𝑣})) = (𝑀‘(◡𝑀‘(𝐿‘{((𝑆‘𝑢) ✚ 𝑠)}))) ↔ (𝑁‘{𝑣}) = (◡𝑀‘(𝐿‘{((𝑆‘𝑢) ✚ 𝑠)})))) |
49 | 48 | necon3bid 3011 | . 2 ⊢ (𝜑 → ((𝑀‘(𝑁‘{𝑣})) ≠ (𝑀‘(◡𝑀‘(𝐿‘{((𝑆‘𝑢) ✚ 𝑠)}))) ↔ (𝑁‘{𝑣}) ≠ (◡𝑀‘(𝐿‘{((𝑆‘𝑢) ✚ 𝑠)})))) |
50 | 46, 49 | mpbid 224 | 1 ⊢ (𝜑 → (𝑁‘{𝑣}) ≠ (◡𝑀‘(𝐿‘{((𝑆‘𝑢) ✚ 𝑠)}))) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 387 = wceq 1507 ∈ wcel 2050 ≠ wne 2967 ∖ cdif 3828 {csn 4442 ◡ccnv 5407 ran crn 5409 ‘cfv 6190 (class class class)co 6978 Basecbs 16342 +gcplusg 16424 0gc0g 16572 LModclmod 19359 LSubSpclss 19428 LSpanclspn 19468 HLchlt 35931 LHypclh 36565 DVecHcdvh 37659 LCDualclcd 38167 mapdcmpd 38205 HDMapchdma 38373 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-13 2301 ax-ext 2750 ax-rep 5050 ax-sep 5061 ax-nul 5068 ax-pow 5120 ax-pr 5187 ax-un 7281 ax-cnex 10393 ax-resscn 10394 ax-1cn 10395 ax-icn 10396 ax-addcl 10397 ax-addrcl 10398 ax-mulcl 10399 ax-mulrcl 10400 ax-mulcom 10401 ax-addass 10402 ax-mulass 10403 ax-distr 10404 ax-i2m1 10405 ax-1ne0 10406 ax-1rid 10407 ax-rnegex 10408 ax-rrecex 10409 ax-cnre 10410 ax-pre-lttri 10411 ax-pre-lttrn 10412 ax-pre-ltadd 10413 ax-pre-mulgt0 10414 ax-riotaBAD 35534 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3or 1069 df-3an 1070 df-tru 1510 df-fal 1520 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-eu 2583 df-clab 2759 df-cleq 2771 df-clel 2846 df-nfc 2918 df-ne 2968 df-nel 3074 df-ral 3093 df-rex 3094 df-reu 3095 df-rmo 3096 df-rab 3097 df-v 3417 df-sbc 3684 df-csb 3789 df-dif 3834 df-un 3836 df-in 3838 df-ss 3845 df-pss 3847 df-nul 4181 df-if 4352 df-pw 4425 df-sn 4443 df-pr 4445 df-tp 4447 df-op 4449 df-ot 4451 df-uni 4714 df-int 4751 df-iun 4795 df-iin 4796 df-br 4931 df-opab 4993 df-mpt 5010 df-tr 5032 df-id 5313 df-eprel 5318 df-po 5327 df-so 5328 df-fr 5367 df-we 5369 df-xp 5414 df-rel 5415 df-cnv 5416 df-co 5417 df-dm 5418 df-rn 5419 df-res 5420 df-ima 5421 df-pred 5988 df-ord 6034 df-on 6035 df-lim 6036 df-suc 6037 df-iota 6154 df-fun 6192 df-fn 6193 df-f 6194 df-f1 6195 df-fo 6196 df-f1o 6197 df-fv 6198 df-riota 6939 df-ov 6981 df-oprab 6982 df-mpo 6983 df-of 7229 df-om 7399 df-1st 7503 df-2nd 7504 df-tpos 7697 df-undef 7744 df-wrecs 7752 df-recs 7814 df-rdg 7852 df-1o 7907 df-oadd 7911 df-er 8091 df-map 8210 df-en 8309 df-dom 8310 df-sdom 8311 df-fin 8312 df-pnf 10478 df-mnf 10479 df-xr 10480 df-ltxr 10481 df-le 10482 df-sub 10674 df-neg 10675 df-nn 11442 df-2 11506 df-3 11507 df-4 11508 df-5 11509 df-6 11510 df-n0 11711 df-z 11797 df-uz 12062 df-fz 12712 df-struct 16344 df-ndx 16345 df-slot 16346 df-base 16348 df-sets 16349 df-ress 16350 df-plusg 16437 df-mulr 16438 df-sca 16440 df-vsca 16441 df-0g 16574 df-mre 16718 df-mrc 16719 df-acs 16721 df-proset 17399 df-poset 17417 df-plt 17429 df-lub 17445 df-glb 17446 df-join 17447 df-meet 17448 df-p0 17510 df-p1 17511 df-lat 17517 df-clat 17579 df-mgm 17713 df-sgrp 17755 df-mnd 17766 df-submnd 17807 df-grp 17897 df-minusg 17898 df-sbg 17899 df-subg 18063 df-cntz 18221 df-oppg 18248 df-lsm 18525 df-cmn 18671 df-abl 18672 df-mgp 18966 df-ur 18978 df-ring 19025 df-oppr 19099 df-dvdsr 19117 df-unit 19118 df-invr 19148 df-dvr 19159 df-drng 19230 df-lmod 19361 df-lss 19429 df-lsp 19469 df-lvec 19600 df-lsatoms 35557 df-lshyp 35558 df-lcv 35600 df-lfl 35639 df-lkr 35667 df-ldual 35705 df-oposet 35757 df-ol 35759 df-oml 35760 df-covers 35847 df-ats 35848 df-atl 35879 df-cvlat 35903 df-hlat 35932 df-llines 36079 df-lplanes 36080 df-lvols 36081 df-lines 36082 df-psubsp 36084 df-pmap 36085 df-padd 36377 df-lhyp 36569 df-laut 36570 df-ldil 36685 df-ltrn 36686 df-trl 36740 df-tgrp 37324 df-tendo 37336 df-edring 37338 df-dveca 37584 df-disoa 37610 df-dvech 37660 df-dib 37720 df-dic 37754 df-dih 37810 df-doch 37929 df-djh 37976 df-lcdual 38168 df-mapd 38206 df-hvmap 38338 df-hdmap1 38374 df-hdmap 38375 |
This theorem is referenced by: hdmaprnlem9N 38438 hdmaprnlem3eN 38439 |
Copyright terms: Public domain | W3C validator |