Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  mapdpglem3 Structured version   Visualization version   GIF version

Theorem mapdpglem3 38803
Description: Lemma for mapdpg 38834. Baer p. 45, line 3: "infer...the existence of a number g in G and of an element z in (Fy)* such that t = gx'-z." (We scope $d 𝑔𝑤𝑧𝜑 locally to avoid clashes with later substitutions into 𝜑.) (Contributed by NM, 18-Mar-2015.)
Hypotheses
Ref Expression
mapdpglem.h 𝐻 = (LHyp‘𝐾)
mapdpglem.m 𝑀 = ((mapd‘𝐾)‘𝑊)
mapdpglem.u 𝑈 = ((DVecH‘𝐾)‘𝑊)
mapdpglem.v 𝑉 = (Base‘𝑈)
mapdpglem.s = (-g𝑈)
mapdpglem.n 𝑁 = (LSpan‘𝑈)
mapdpglem.c 𝐶 = ((LCDual‘𝐾)‘𝑊)
mapdpglem.k (𝜑 → (𝐾 ∈ HL ∧ 𝑊𝐻))
mapdpglem.x (𝜑𝑋𝑉)
mapdpglem.y (𝜑𝑌𝑉)
mapdpglem1.p = (LSSum‘𝐶)
mapdpglem2.j 𝐽 = (LSpan‘𝐶)
mapdpglem3.f 𝐹 = (Base‘𝐶)
mapdpglem3.te (𝜑𝑡 ∈ ((𝑀‘(𝑁‘{𝑋})) (𝑀‘(𝑁‘{𝑌}))))
mapdpglem3.a 𝐴 = (Scalar‘𝑈)
mapdpglem3.b 𝐵 = (Base‘𝐴)
mapdpglem3.t · = ( ·𝑠𝐶)
mapdpglem3.r 𝑅 = (-g𝐶)
mapdpglem3.g (𝜑𝐺𝐹)
mapdpglem3.e (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺}))
Assertion
Ref Expression
mapdpglem3 (𝜑 → ∃𝑔𝐵𝑧 ∈ (𝑀‘(𝑁‘{𝑌}))𝑡 = ((𝑔 · 𝐺)𝑅𝑧))
Distinct variable groups:   𝑡,   𝑡,𝐶   𝑡,𝐽   𝑡,𝑀   𝑡,𝑁   𝑡,𝑋   𝑡,𝑌   𝐵,𝑔   𝑧,𝑔,𝐶   𝑔,𝐹   𝑔,𝐺,𝑧   𝑔,𝐽,𝑧   𝑔,𝑀,𝑧   𝑔,𝑁,𝑧   𝑅,𝑔,𝑧   · ,𝑔,𝑧   𝑔,𝑌,𝑧,𝑡   𝜑,𝑔,𝑧
Allowed substitution hints:   𝜑(𝑡)   𝐴(𝑧,𝑡,𝑔)   𝐵(𝑧,𝑡)   (𝑧,𝑡,𝑔)   𝑅(𝑡)   · (𝑡)   𝑈(𝑧,𝑡,𝑔)   𝐹(𝑧,𝑡)   𝐺(𝑡)   𝐻(𝑧,𝑡,𝑔)   𝐾(𝑧,𝑡,𝑔)   (𝑧,𝑔)   𝑉(𝑧,𝑡,𝑔)   𝑊(𝑧,𝑡,𝑔)   𝑋(𝑧,𝑔)

Proof of Theorem mapdpglem3
Dummy variable 𝑤 is distinct from all other variables.
StepHypRef Expression
1 mapdpglem3.te . . . 4 (𝜑𝑡 ∈ ((𝑀‘(𝑁‘{𝑋})) (𝑀‘(𝑁‘{𝑌}))))
2 mapdpglem3.e . . . . 5 (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺}))
32oveq1d 7163 . . . 4 (𝜑 → ((𝑀‘(𝑁‘{𝑋})) (𝑀‘(𝑁‘{𝑌}))) = ((𝐽‘{𝐺}) (𝑀‘(𝑁‘{𝑌}))))
41, 3eleqtrd 2913 . . 3 (𝜑𝑡 ∈ ((𝐽‘{𝐺}) (𝑀‘(𝑁‘{𝑌}))))
5 mapdpglem.h . . . . . . . . . . 11 𝐻 = (LHyp‘𝐾)
6 mapdpglem.c . . . . . . . . . . 11 𝐶 = ((LCDual‘𝐾)‘𝑊)
7 mapdpglem.k . . . . . . . . . . 11 (𝜑 → (𝐾 ∈ HL ∧ 𝑊𝐻))
85, 6, 7lcdlmod 38720 . . . . . . . . . 10 (𝜑𝐶 ∈ LMod)
9 mapdpglem3.g . . . . . . . . . 10 (𝜑𝐺𝐹)
10 eqid 2819 . . . . . . . . . . 11 (Scalar‘𝐶) = (Scalar‘𝐶)
11 eqid 2819 . . . . . . . . . . 11 (Base‘(Scalar‘𝐶)) = (Base‘(Scalar‘𝐶))
12 mapdpglem3.f . . . . . . . . . . 11 𝐹 = (Base‘𝐶)
13 mapdpglem3.t . . . . . . . . . . 11 · = ( ·𝑠𝐶)
14 mapdpglem2.j . . . . . . . . . . 11 𝐽 = (LSpan‘𝐶)
1510, 11, 12, 13, 14lspsnel 19767 . . . . . . . . . 10 ((𝐶 ∈ LMod ∧ 𝐺𝐹) → (𝑤 ∈ (𝐽‘{𝐺}) ↔ ∃𝑔 ∈ (Base‘(Scalar‘𝐶))𝑤 = (𝑔 · 𝐺)))
168, 9, 15syl2anc 586 . . . . . . . . 9 (𝜑 → (𝑤 ∈ (𝐽‘{𝐺}) ↔ ∃𝑔 ∈ (Base‘(Scalar‘𝐶))𝑤 = (𝑔 · 𝐺)))
17 mapdpglem.u . . . . . . . . . . 11 𝑈 = ((DVecH‘𝐾)‘𝑊)
18 mapdpglem3.a . . . . . . . . . . 11 𝐴 = (Scalar‘𝑈)
19 mapdpglem3.b . . . . . . . . . . 11 𝐵 = (Base‘𝐴)
205, 17, 18, 19, 6, 10, 11, 7lcdsbase 38728 . . . . . . . . . 10 (𝜑 → (Base‘(Scalar‘𝐶)) = 𝐵)
2120rexeqdv 3415 . . . . . . . . 9 (𝜑 → (∃𝑔 ∈ (Base‘(Scalar‘𝐶))𝑤 = (𝑔 · 𝐺) ↔ ∃𝑔𝐵 𝑤 = (𝑔 · 𝐺)))
2216, 21bitrd 281 . . . . . . . 8 (𝜑 → (𝑤 ∈ (𝐽‘{𝐺}) ↔ ∃𝑔𝐵 𝑤 = (𝑔 · 𝐺)))
2322anbi1d 631 . . . . . . 7 (𝜑 → ((𝑤 ∈ (𝐽‘{𝐺}) ∧ ∃𝑧 ∈ (𝑀‘(𝑁‘{𝑌}))𝑡 = (𝑤𝑅𝑧)) ↔ (∃𝑔𝐵 𝑤 = (𝑔 · 𝐺) ∧ ∃𝑧 ∈ (𝑀‘(𝑁‘{𝑌}))𝑡 = (𝑤𝑅𝑧))))
24 r19.41v 3345 . . . . . . 7 (∃𝑔𝐵 (𝑤 = (𝑔 · 𝐺) ∧ ∃𝑧 ∈ (𝑀‘(𝑁‘{𝑌}))𝑡 = (𝑤𝑅𝑧)) ↔ (∃𝑔𝐵 𝑤 = (𝑔 · 𝐺) ∧ ∃𝑧 ∈ (𝑀‘(𝑁‘{𝑌}))𝑡 = (𝑤𝑅𝑧)))
2523, 24syl6rbbr 292 . . . . . 6 (𝜑 → (∃𝑔𝐵 (𝑤 = (𝑔 · 𝐺) ∧ ∃𝑧 ∈ (𝑀‘(𝑁‘{𝑌}))𝑡 = (𝑤𝑅𝑧)) ↔ (𝑤 ∈ (𝐽‘{𝐺}) ∧ ∃𝑧 ∈ (𝑀‘(𝑁‘{𝑌}))𝑡 = (𝑤𝑅𝑧))))
2625exbidv 1916 . . . . 5 (𝜑 → (∃𝑤𝑔𝐵 (𝑤 = (𝑔 · 𝐺) ∧ ∃𝑧 ∈ (𝑀‘(𝑁‘{𝑌}))𝑡 = (𝑤𝑅𝑧)) ↔ ∃𝑤(𝑤 ∈ (𝐽‘{𝐺}) ∧ ∃𝑧 ∈ (𝑀‘(𝑁‘{𝑌}))𝑡 = (𝑤𝑅𝑧))))
27 df-rex 3142 . . . . 5 (∃𝑤 ∈ (𝐽‘{𝐺})∃𝑧 ∈ (𝑀‘(𝑁‘{𝑌}))𝑡 = (𝑤𝑅𝑧) ↔ ∃𝑤(𝑤 ∈ (𝐽‘{𝐺}) ∧ ∃𝑧 ∈ (𝑀‘(𝑁‘{𝑌}))𝑡 = (𝑤𝑅𝑧)))
2826, 27syl6bbr 291 . . . 4 (𝜑 → (∃𝑤𝑔𝐵 (𝑤 = (𝑔 · 𝐺) ∧ ∃𝑧 ∈ (𝑀‘(𝑁‘{𝑌}))𝑡 = (𝑤𝑅𝑧)) ↔ ∃𝑤 ∈ (𝐽‘{𝐺})∃𝑧 ∈ (𝑀‘(𝑁‘{𝑌}))𝑡 = (𝑤𝑅𝑧)))
29 mapdpglem3.r . . . . 5 𝑅 = (-g𝐶)
30 mapdpglem1.p . . . . 5 = (LSSum‘𝐶)
31 eqid 2819 . . . . . . . 8 (LSubSp‘𝐶) = (LSubSp‘𝐶)
3231lsssssubg 19722 . . . . . . 7 (𝐶 ∈ LMod → (LSubSp‘𝐶) ⊆ (SubGrp‘𝐶))
338, 32syl 17 . . . . . 6 (𝜑 → (LSubSp‘𝐶) ⊆ (SubGrp‘𝐶))
3412, 31, 14lspsncl 19741 . . . . . . 7 ((𝐶 ∈ LMod ∧ 𝐺𝐹) → (𝐽‘{𝐺}) ∈ (LSubSp‘𝐶))
358, 9, 34syl2anc 586 . . . . . 6 (𝜑 → (𝐽‘{𝐺}) ∈ (LSubSp‘𝐶))
3633, 35sseldd 3966 . . . . 5 (𝜑 → (𝐽‘{𝐺}) ∈ (SubGrp‘𝐶))
37 mapdpglem.m . . . . . . 7 𝑀 = ((mapd‘𝐾)‘𝑊)
38 eqid 2819 . . . . . . 7 (LSubSp‘𝑈) = (LSubSp‘𝑈)
395, 17, 7dvhlmod 38238 . . . . . . . 8 (𝜑𝑈 ∈ LMod)
40 mapdpglem.y . . . . . . . 8 (𝜑𝑌𝑉)
41 mapdpglem.v . . . . . . . . 9 𝑉 = (Base‘𝑈)
42 mapdpglem.n . . . . . . . . 9 𝑁 = (LSpan‘𝑈)
4341, 38, 42lspsncl 19741 . . . . . . . 8 ((𝑈 ∈ LMod ∧ 𝑌𝑉) → (𝑁‘{𝑌}) ∈ (LSubSp‘𝑈))
4439, 40, 43syl2anc 586 . . . . . . 7 (𝜑 → (𝑁‘{𝑌}) ∈ (LSubSp‘𝑈))
455, 37, 17, 38, 6, 31, 7, 44mapdcl2 38784 . . . . . 6 (𝜑 → (𝑀‘(𝑁‘{𝑌})) ∈ (LSubSp‘𝐶))
4633, 45sseldd 3966 . . . . 5 (𝜑 → (𝑀‘(𝑁‘{𝑌})) ∈ (SubGrp‘𝐶))
4729, 30, 36, 46lsmelvalm 18768 . . . 4 (𝜑 → (𝑡 ∈ ((𝐽‘{𝐺}) (𝑀‘(𝑁‘{𝑌}))) ↔ ∃𝑤 ∈ (𝐽‘{𝐺})∃𝑧 ∈ (𝑀‘(𝑁‘{𝑌}))𝑡 = (𝑤𝑅𝑧)))
4828, 47bitr4d 284 . . 3 (𝜑 → (∃𝑤𝑔𝐵 (𝑤 = (𝑔 · 𝐺) ∧ ∃𝑧 ∈ (𝑀‘(𝑁‘{𝑌}))𝑡 = (𝑤𝑅𝑧)) ↔ 𝑡 ∈ ((𝐽‘{𝐺}) (𝑀‘(𝑁‘{𝑌})))))
494, 48mpbird 259 . 2 (𝜑 → ∃𝑤𝑔𝐵 (𝑤 = (𝑔 · 𝐺) ∧ ∃𝑧 ∈ (𝑀‘(𝑁‘{𝑌}))𝑡 = (𝑤𝑅𝑧)))
50 ovex 7181 . . . . 5 (𝑔 · 𝐺) ∈ V
51 oveq1 7155 . . . . . . 7 (𝑤 = (𝑔 · 𝐺) → (𝑤𝑅𝑧) = ((𝑔 · 𝐺)𝑅𝑧))
5251eqeq2d 2830 . . . . . 6 (𝑤 = (𝑔 · 𝐺) → (𝑡 = (𝑤𝑅𝑧) ↔ 𝑡 = ((𝑔 · 𝐺)𝑅𝑧)))
5352rexbidv 3295 . . . . 5 (𝑤 = (𝑔 · 𝐺) → (∃𝑧 ∈ (𝑀‘(𝑁‘{𝑌}))𝑡 = (𝑤𝑅𝑧) ↔ ∃𝑧 ∈ (𝑀‘(𝑁‘{𝑌}))𝑡 = ((𝑔 · 𝐺)𝑅𝑧)))
5450, 53ceqsexv 3540 . . . 4 (∃𝑤(𝑤 = (𝑔 · 𝐺) ∧ ∃𝑧 ∈ (𝑀‘(𝑁‘{𝑌}))𝑡 = (𝑤𝑅𝑧)) ↔ ∃𝑧 ∈ (𝑀‘(𝑁‘{𝑌}))𝑡 = ((𝑔 · 𝐺)𝑅𝑧))
5554rexbii 3245 . . 3 (∃𝑔𝐵𝑤(𝑤 = (𝑔 · 𝐺) ∧ ∃𝑧 ∈ (𝑀‘(𝑁‘{𝑌}))𝑡 = (𝑤𝑅𝑧)) ↔ ∃𝑔𝐵𝑧 ∈ (𝑀‘(𝑁‘{𝑌}))𝑡 = ((𝑔 · 𝐺)𝑅𝑧))
56 rexcom4 3247 . . 3 (∃𝑔𝐵𝑤(𝑤 = (𝑔 · 𝐺) ∧ ∃𝑧 ∈ (𝑀‘(𝑁‘{𝑌}))𝑡 = (𝑤𝑅𝑧)) ↔ ∃𝑤𝑔𝐵 (𝑤 = (𝑔 · 𝐺) ∧ ∃𝑧 ∈ (𝑀‘(𝑁‘{𝑌}))𝑡 = (𝑤𝑅𝑧)))
5755, 56bitr3i 279 . 2 (∃𝑔𝐵𝑧 ∈ (𝑀‘(𝑁‘{𝑌}))𝑡 = ((𝑔 · 𝐺)𝑅𝑧) ↔ ∃𝑤𝑔𝐵 (𝑤 = (𝑔 · 𝐺) ∧ ∃𝑧 ∈ (𝑀‘(𝑁‘{𝑌}))𝑡 = (𝑤𝑅𝑧)))
5849, 57sylibr 236 1 (𝜑 → ∃𝑔𝐵𝑧 ∈ (𝑀‘(𝑁‘{𝑌}))𝑡 = ((𝑔 · 𝐺)𝑅𝑧))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208  wa 398   = wceq 1531  wex 1774  wcel 2108  wrex 3137  wss 3934  {csn 4559  cfv 6348  (class class class)co 7148  Basecbs 16475  Scalarcsca 16560   ·𝑠 cvsca 16561  -gcsg 18097  SubGrpcsubg 18265  LSSumclsm 18751  LModclmod 19626  LSubSpclss 19695  LSpanclspn 19735  HLchlt 36478  LHypclh 37112  DVecHcdvh 38206  LCDualclcd 38714  mapdcmpd 38752
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606  ax-riotaBAD 36081
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1083  df-3an 1084  df-tru 1534  df-fal 1544  df-ex 1775  df-nf 1779  df-sb 2064  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-nel 3122  df-ral 3141  df-rex 3142  df-reu 3143  df-rmo 3144  df-rab 3145  df-v 3495  df-sbc 3771  df-csb 3882  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-pss 3952  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4831  df-int 4868  df-iun 4912  df-iin 4913  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-riota 7106  df-ov 7151  df-oprab 7152  df-mpo 7153  df-of 7401  df-om 7573  df-1st 7681  df-2nd 7682  df-tpos 7884  df-undef 7931  df-wrecs 7939  df-recs 8000  df-rdg 8038  df-1o 8094  df-oadd 8098  df-er 8281  df-map 8400  df-en 8502  df-dom 8503  df-sdom 8504  df-fin 8505  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-nn 11631  df-2 11692  df-3 11693  df-4 11694  df-5 11695  df-6 11696  df-n0 11890  df-z 11974  df-uz 12236  df-fz 12885  df-struct 16477  df-ndx 16478  df-slot 16479  df-base 16481  df-sets 16482  df-ress 16483  df-plusg 16570  df-mulr 16571  df-sca 16573  df-vsca 16574  df-0g 16707  df-mre 16849  df-mrc 16850  df-acs 16852  df-proset 17530  df-poset 17548  df-plt 17560  df-lub 17576  df-glb 17577  df-join 17578  df-meet 17579  df-p0 17641  df-p1 17642  df-lat 17648  df-clat 17710  df-mgm 17844  df-sgrp 17893  df-mnd 17904  df-submnd 17949  df-grp 18098  df-minusg 18099  df-sbg 18100  df-subg 18268  df-cntz 18439  df-oppg 18466  df-lsm 18753  df-cmn 18900  df-abl 18901  df-mgp 19232  df-ur 19244  df-ring 19291  df-oppr 19365  df-dvdsr 19383  df-unit 19384  df-invr 19414  df-dvr 19425  df-drng 19496  df-lmod 19628  df-lss 19696  df-lsp 19736  df-lvec 19867  df-lsatoms 36104  df-lshyp 36105  df-lcv 36147  df-lfl 36186  df-lkr 36214  df-ldual 36252  df-oposet 36304  df-ol 36306  df-oml 36307  df-covers 36394  df-ats 36395  df-atl 36426  df-cvlat 36450  df-hlat 36479  df-llines 36626  df-lplanes 36627  df-lvols 36628  df-lines 36629  df-psubsp 36631  df-pmap 36632  df-padd 36924  df-lhyp 37116  df-laut 37117  df-ldil 37232  df-ltrn 37233  df-trl 37287  df-tgrp 37871  df-tendo 37883  df-edring 37885  df-dveca 38131  df-disoa 38157  df-dvech 38207  df-dib 38267  df-dic 38301  df-dih 38357  df-doch 38476  df-djh 38523  df-lcdual 38715  df-mapd 38753
This theorem is referenced by:  mapdpglem24  38832
  Copyright terms: Public domain W3C validator