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

Theorem mapdval4N 36422
Description: Value of projectivity from vector space H to dual space. TODO: 1. This is shorter than others - make it the official def? (but is not as obvious that it is 𝐶) 2. The unneeded direction of lcfl8a 36293 has awkward - add another thm with only one direction of it? 3. Swap 𝑂‘{𝑣} and 𝐿𝑓? (Contributed by NM, 31-Jan-2015.) (New usage is discouraged.)
Hypotheses
Ref Expression
mapdval4.h 𝐻 = (LHyp‘𝐾)
mapdval4.u 𝑈 = ((DVecH‘𝐾)‘𝑊)
mapdval4.s 𝑆 = (LSubSp‘𝑈)
mapdval4.f 𝐹 = (LFnl‘𝑈)
mapdval4.l 𝐿 = (LKer‘𝑈)
mapdval4.o 𝑂 = ((ocH‘𝐾)‘𝑊)
mapdval4.m 𝑀 = ((mapd‘𝐾)‘𝑊)
mapdval4.k (𝜑 → (𝐾 ∈ HL ∧ 𝑊𝐻))
mapdval4.t (𝜑𝑇𝑆)
Assertion
Ref Expression
mapdval4N (𝜑 → (𝑀𝑇) = {𝑓𝐹 ∣ ∃𝑣𝑇 (𝑂‘{𝑣}) = (𝐿𝑓)})
Distinct variable groups:   𝑣,𝑓,𝐹   𝑓,𝐾   𝑣,𝐿   𝑣,𝑂   𝑇,𝑓,𝑣   𝑣,𝑈   𝑓,𝑊   𝜑,𝑓,𝑣
Allowed substitution hints:   𝑆(𝑣,𝑓)   𝑈(𝑓)   𝐻(𝑣,𝑓)   𝐾(𝑣)   𝐿(𝑓)   𝑀(𝑣,𝑓)   𝑂(𝑓)   𝑊(𝑣)

Proof of Theorem mapdval4N
Dummy variables 𝑔 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mapdval4.h . . 3 𝐻 = (LHyp‘𝐾)
2 mapdval4.u . . 3 𝑈 = ((DVecH‘𝐾)‘𝑊)
3 mapdval4.s . . 3 𝑆 = (LSubSp‘𝑈)
4 eqid 2621 . . 3 (LSpan‘𝑈) = (LSpan‘𝑈)
5 mapdval4.f . . 3 𝐹 = (LFnl‘𝑈)
6 mapdval4.l . . 3 𝐿 = (LKer‘𝑈)
7 mapdval4.o . . 3 𝑂 = ((ocH‘𝐾)‘𝑊)
8 mapdval4.m . . 3 𝑀 = ((mapd‘𝐾)‘𝑊)
9 mapdval4.k . . 3 (𝜑 → (𝐾 ∈ HL ∧ 𝑊𝐻))
10 mapdval4.t . . 3 (𝜑𝑇𝑆)
11 eqid 2621 . . 3 {𝑔𝐹 ∣ (𝑂‘(𝑂‘(𝐿𝑔))) = (𝐿𝑔)} = {𝑔𝐹 ∣ (𝑂‘(𝑂‘(𝐿𝑔))) = (𝐿𝑔)}
121, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11mapdval2N 36420 . 2 (𝜑 → (𝑀𝑇) = {𝑓 ∈ {𝑔𝐹 ∣ (𝑂‘(𝑂‘(𝐿𝑔))) = (𝐿𝑔)} ∣ ∃𝑣𝑇 (𝑂‘(𝐿𝑓)) = ((LSpan‘𝑈)‘{𝑣})})
1311lcfl1lem 36281 . . . . . 6 (𝑓 ∈ {𝑔𝐹 ∣ (𝑂‘(𝑂‘(𝐿𝑔))) = (𝐿𝑔)} ↔ (𝑓𝐹 ∧ (𝑂‘(𝑂‘(𝐿𝑓))) = (𝐿𝑓)))
1413anbi1i 730 . . . . 5 ((𝑓 ∈ {𝑔𝐹 ∣ (𝑂‘(𝑂‘(𝐿𝑔))) = (𝐿𝑔)} ∧ ∃𝑣𝑇 (𝑂‘(𝐿𝑓)) = ((LSpan‘𝑈)‘{𝑣})) ↔ ((𝑓𝐹 ∧ (𝑂‘(𝑂‘(𝐿𝑓))) = (𝐿𝑓)) ∧ ∃𝑣𝑇 (𝑂‘(𝐿𝑓)) = ((LSpan‘𝑈)‘{𝑣})))
15 anass 680 . . . . 5 (((𝑓𝐹 ∧ (𝑂‘(𝑂‘(𝐿𝑓))) = (𝐿𝑓)) ∧ ∃𝑣𝑇 (𝑂‘(𝐿𝑓)) = ((LSpan‘𝑈)‘{𝑣})) ↔ (𝑓𝐹 ∧ ((𝑂‘(𝑂‘(𝐿𝑓))) = (𝐿𝑓) ∧ ∃𝑣𝑇 (𝑂‘(𝐿𝑓)) = ((LSpan‘𝑈)‘{𝑣}))))
1614, 15bitri 264 . . . 4 ((𝑓 ∈ {𝑔𝐹 ∣ (𝑂‘(𝑂‘(𝐿𝑔))) = (𝐿𝑔)} ∧ ∃𝑣𝑇 (𝑂‘(𝐿𝑓)) = ((LSpan‘𝑈)‘{𝑣})) ↔ (𝑓𝐹 ∧ ((𝑂‘(𝑂‘(𝐿𝑓))) = (𝐿𝑓) ∧ ∃𝑣𝑇 (𝑂‘(𝐿𝑓)) = ((LSpan‘𝑈)‘{𝑣}))))
17 r19.42v 3084 . . . . . 6 (∃𝑣𝑇 ((𝑂‘(𝑂‘(𝐿𝑓))) = (𝐿𝑓) ∧ (𝑂‘(𝐿𝑓)) = ((LSpan‘𝑈)‘{𝑣})) ↔ ((𝑂‘(𝑂‘(𝐿𝑓))) = (𝐿𝑓) ∧ ∃𝑣𝑇 (𝑂‘(𝐿𝑓)) = ((LSpan‘𝑈)‘{𝑣})))
18 simprr 795 . . . . . . . . . 10 ((((𝜑𝑓𝐹) ∧ 𝑣𝑇) ∧ ((𝑂‘(𝑂‘(𝐿𝑓))) = (𝐿𝑓) ∧ (𝑂‘(𝐿𝑓)) = ((LSpan‘𝑈)‘{𝑣}))) → (𝑂‘(𝐿𝑓)) = ((LSpan‘𝑈)‘{𝑣}))
1918fveq2d 6154 . . . . . . . . 9 ((((𝜑𝑓𝐹) ∧ 𝑣𝑇) ∧ ((𝑂‘(𝑂‘(𝐿𝑓))) = (𝐿𝑓) ∧ (𝑂‘(𝐿𝑓)) = ((LSpan‘𝑈)‘{𝑣}))) → (𝑂‘(𝑂‘(𝐿𝑓))) = (𝑂‘((LSpan‘𝑈)‘{𝑣})))
20 simprl 793 . . . . . . . . 9 ((((𝜑𝑓𝐹) ∧ 𝑣𝑇) ∧ ((𝑂‘(𝑂‘(𝐿𝑓))) = (𝐿𝑓) ∧ (𝑂‘(𝐿𝑓)) = ((LSpan‘𝑈)‘{𝑣}))) → (𝑂‘(𝑂‘(𝐿𝑓))) = (𝐿𝑓))
21 eqid 2621 . . . . . . . . . 10 (Base‘𝑈) = (Base‘𝑈)
229adantr 481 . . . . . . . . . . . 12 ((𝜑𝑓𝐹) → (𝐾 ∈ HL ∧ 𝑊𝐻))
2322adantr 481 . . . . . . . . . . 11 (((𝜑𝑓𝐹) ∧ 𝑣𝑇) → (𝐾 ∈ HL ∧ 𝑊𝐻))
2423adantr 481 . . . . . . . . . 10 ((((𝜑𝑓𝐹) ∧ 𝑣𝑇) ∧ ((𝑂‘(𝑂‘(𝐿𝑓))) = (𝐿𝑓) ∧ (𝑂‘(𝐿𝑓)) = ((LSpan‘𝑈)‘{𝑣}))) → (𝐾 ∈ HL ∧ 𝑊𝐻))
2510adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑓𝐹) → 𝑇𝑆)
2621, 3lssel 18860 . . . . . . . . . . . . 13 ((𝑇𝑆𝑣𝑇) → 𝑣 ∈ (Base‘𝑈))
2725, 26sylan 488 . . . . . . . . . . . 12 (((𝜑𝑓𝐹) ∧ 𝑣𝑇) → 𝑣 ∈ (Base‘𝑈))
2827snssd 4311 . . . . . . . . . . 11 (((𝜑𝑓𝐹) ∧ 𝑣𝑇) → {𝑣} ⊆ (Base‘𝑈))
2928adantr 481 . . . . . . . . . 10 ((((𝜑𝑓𝐹) ∧ 𝑣𝑇) ∧ ((𝑂‘(𝑂‘(𝐿𝑓))) = (𝐿𝑓) ∧ (𝑂‘(𝐿𝑓)) = ((LSpan‘𝑈)‘{𝑣}))) → {𝑣} ⊆ (Base‘𝑈))
301, 2, 7, 21, 4, 24, 29dochocsp 36169 . . . . . . . . 9 ((((𝜑𝑓𝐹) ∧ 𝑣𝑇) ∧ ((𝑂‘(𝑂‘(𝐿𝑓))) = (𝐿𝑓) ∧ (𝑂‘(𝐿𝑓)) = ((LSpan‘𝑈)‘{𝑣}))) → (𝑂‘((LSpan‘𝑈)‘{𝑣})) = (𝑂‘{𝑣}))
3119, 20, 303eqtr3rd 2664 . . . . . . . 8 ((((𝜑𝑓𝐹) ∧ 𝑣𝑇) ∧ ((𝑂‘(𝑂‘(𝐿𝑓))) = (𝐿𝑓) ∧ (𝑂‘(𝐿𝑓)) = ((LSpan‘𝑈)‘{𝑣}))) → (𝑂‘{𝑣}) = (𝐿𝑓))
3227adantr 481 . . . . . . . . . . 11 ((((𝜑𝑓𝐹) ∧ 𝑣𝑇) ∧ (𝑂‘{𝑣}) = (𝐿𝑓)) → 𝑣 ∈ (Base‘𝑈))
33 simpr 477 . . . . . . . . . . . 12 ((((𝜑𝑓𝐹) ∧ 𝑣𝑇) ∧ (𝑂‘{𝑣}) = (𝐿𝑓)) → (𝑂‘{𝑣}) = (𝐿𝑓))
3433eqcomd 2627 . . . . . . . . . . 11 ((((𝜑𝑓𝐹) ∧ 𝑣𝑇) ∧ (𝑂‘{𝑣}) = (𝐿𝑓)) → (𝐿𝑓) = (𝑂‘{𝑣}))
35 sneq 4160 . . . . . . . . . . . . . 14 (𝑤 = 𝑣 → {𝑤} = {𝑣})
3635fveq2d 6154 . . . . . . . . . . . . 13 (𝑤 = 𝑣 → (𝑂‘{𝑤}) = (𝑂‘{𝑣}))
3736eqeq2d 2631 . . . . . . . . . . . 12 (𝑤 = 𝑣 → ((𝐿𝑓) = (𝑂‘{𝑤}) ↔ (𝐿𝑓) = (𝑂‘{𝑣})))
3837rspcev 3295 . . . . . . . . . . 11 ((𝑣 ∈ (Base‘𝑈) ∧ (𝐿𝑓) = (𝑂‘{𝑣})) → ∃𝑤 ∈ (Base‘𝑈)(𝐿𝑓) = (𝑂‘{𝑤}))
3932, 34, 38syl2anc 692 . . . . . . . . . 10 ((((𝜑𝑓𝐹) ∧ 𝑣𝑇) ∧ (𝑂‘{𝑣}) = (𝐿𝑓)) → ∃𝑤 ∈ (Base‘𝑈)(𝐿𝑓) = (𝑂‘{𝑤}))
4023adantr 481 . . . . . . . . . . 11 ((((𝜑𝑓𝐹) ∧ 𝑣𝑇) ∧ (𝑂‘{𝑣}) = (𝐿𝑓)) → (𝐾 ∈ HL ∧ 𝑊𝐻))
41 simpllr 798 . . . . . . . . . . 11 ((((𝜑𝑓𝐹) ∧ 𝑣𝑇) ∧ (𝑂‘{𝑣}) = (𝐿𝑓)) → 𝑓𝐹)
421, 7, 2, 21, 5, 6, 40, 41lcfl8a 36293 . . . . . . . . . 10 ((((𝜑𝑓𝐹) ∧ 𝑣𝑇) ∧ (𝑂‘{𝑣}) = (𝐿𝑓)) → ((𝑂‘(𝑂‘(𝐿𝑓))) = (𝐿𝑓) ↔ ∃𝑤 ∈ (Base‘𝑈)(𝐿𝑓) = (𝑂‘{𝑤})))
4339, 42mpbird 247 . . . . . . . . 9 ((((𝜑𝑓𝐹) ∧ 𝑣𝑇) ∧ (𝑂‘{𝑣}) = (𝐿𝑓)) → (𝑂‘(𝑂‘(𝐿𝑓))) = (𝐿𝑓))
441, 2, 7, 21, 4, 23, 27dochocsn 36171 . . . . . . . . . . 11 (((𝜑𝑓𝐹) ∧ 𝑣𝑇) → (𝑂‘(𝑂‘{𝑣})) = ((LSpan‘𝑈)‘{𝑣}))
45 fveq2 6150 . . . . . . . . . . 11 ((𝑂‘{𝑣}) = (𝐿𝑓) → (𝑂‘(𝑂‘{𝑣})) = (𝑂‘(𝐿𝑓)))
4644, 45sylan9req 2676 . . . . . . . . . 10 ((((𝜑𝑓𝐹) ∧ 𝑣𝑇) ∧ (𝑂‘{𝑣}) = (𝐿𝑓)) → ((LSpan‘𝑈)‘{𝑣}) = (𝑂‘(𝐿𝑓)))
4746eqcomd 2627 . . . . . . . . 9 ((((𝜑𝑓𝐹) ∧ 𝑣𝑇) ∧ (𝑂‘{𝑣}) = (𝐿𝑓)) → (𝑂‘(𝐿𝑓)) = ((LSpan‘𝑈)‘{𝑣}))
4843, 47jca 554 . . . . . . . 8 ((((𝜑𝑓𝐹) ∧ 𝑣𝑇) ∧ (𝑂‘{𝑣}) = (𝐿𝑓)) → ((𝑂‘(𝑂‘(𝐿𝑓))) = (𝐿𝑓) ∧ (𝑂‘(𝐿𝑓)) = ((LSpan‘𝑈)‘{𝑣})))
4931, 48impbida 876 . . . . . . 7 (((𝜑𝑓𝐹) ∧ 𝑣𝑇) → (((𝑂‘(𝑂‘(𝐿𝑓))) = (𝐿𝑓) ∧ (𝑂‘(𝐿𝑓)) = ((LSpan‘𝑈)‘{𝑣})) ↔ (𝑂‘{𝑣}) = (𝐿𝑓)))
5049rexbidva 3042 . . . . . 6 ((𝜑𝑓𝐹) → (∃𝑣𝑇 ((𝑂‘(𝑂‘(𝐿𝑓))) = (𝐿𝑓) ∧ (𝑂‘(𝐿𝑓)) = ((LSpan‘𝑈)‘{𝑣})) ↔ ∃𝑣𝑇 (𝑂‘{𝑣}) = (𝐿𝑓)))
5117, 50syl5bbr 274 . . . . 5 ((𝜑𝑓𝐹) → (((𝑂‘(𝑂‘(𝐿𝑓))) = (𝐿𝑓) ∧ ∃𝑣𝑇 (𝑂‘(𝐿𝑓)) = ((LSpan‘𝑈)‘{𝑣})) ↔ ∃𝑣𝑇 (𝑂‘{𝑣}) = (𝐿𝑓)))
5251pm5.32da 672 . . . 4 (𝜑 → ((𝑓𝐹 ∧ ((𝑂‘(𝑂‘(𝐿𝑓))) = (𝐿𝑓) ∧ ∃𝑣𝑇 (𝑂‘(𝐿𝑓)) = ((LSpan‘𝑈)‘{𝑣}))) ↔ (𝑓𝐹 ∧ ∃𝑣𝑇 (𝑂‘{𝑣}) = (𝐿𝑓))))
5316, 52syl5bb 272 . . 3 (𝜑 → ((𝑓 ∈ {𝑔𝐹 ∣ (𝑂‘(𝑂‘(𝐿𝑔))) = (𝐿𝑔)} ∧ ∃𝑣𝑇 (𝑂‘(𝐿𝑓)) = ((LSpan‘𝑈)‘{𝑣})) ↔ (𝑓𝐹 ∧ ∃𝑣𝑇 (𝑂‘{𝑣}) = (𝐿𝑓))))
5453rabbidva2 3174 . 2 (𝜑 → {𝑓 ∈ {𝑔𝐹 ∣ (𝑂‘(𝑂‘(𝐿𝑔))) = (𝐿𝑔)} ∣ ∃𝑣𝑇 (𝑂‘(𝐿𝑓)) = ((LSpan‘𝑈)‘{𝑣})} = {𝑓𝐹 ∣ ∃𝑣𝑇 (𝑂‘{𝑣}) = (𝐿𝑓)})
5512, 54eqtrd 2655 1 (𝜑 → (𝑀𝑇) = {𝑓𝐹 ∣ ∃𝑣𝑇 (𝑂‘{𝑣}) = (𝐿𝑓)})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1480  wcel 1987  wrex 2908  {crab 2911  wss 3556  {csn 4150  cfv 5849  Basecbs 15784  LSubSpclss 18854  LSpanclspn 18893  LFnlclfn 33845  LKerclk 33873  HLchlt 34138  LHypclh 34771  DVecHcdvh 35868  ocHcoch 36137  mapdcmpd 36414
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4733  ax-sep 4743  ax-nul 4751  ax-pow 4805  ax-pr 4869  ax-un 6905  ax-cnex 9939  ax-resscn 9940  ax-1cn 9941  ax-icn 9942  ax-addcl 9943  ax-addrcl 9944  ax-mulcl 9945  ax-mulrcl 9946  ax-mulcom 9947  ax-addass 9948  ax-mulass 9949  ax-distr 9950  ax-i2m1 9951  ax-1ne0 9952  ax-1rid 9953  ax-rnegex 9954  ax-rrecex 9955  ax-cnre 9956  ax-pre-lttri 9957  ax-pre-lttrn 9958  ax-pre-ltadd 9959  ax-pre-mulgt0 9960  ax-riotaBAD 33740
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3419  df-csb 3516  df-dif 3559  df-un 3561  df-in 3563  df-ss 3570  df-pss 3572  df-nul 3894  df-if 4061  df-pw 4134  df-sn 4151  df-pr 4153  df-tp 4155  df-op 4157  df-uni 4405  df-int 4443  df-iun 4489  df-iin 4490  df-br 4616  df-opab 4676  df-mpt 4677  df-tr 4715  df-eprel 4987  df-id 4991  df-po 4997  df-so 4998  df-fr 5035  df-we 5037  df-xp 5082  df-rel 5083  df-cnv 5084  df-co 5085  df-dm 5086  df-rn 5087  df-res 5088  df-ima 5089  df-pred 5641  df-ord 5687  df-on 5688  df-lim 5689  df-suc 5690  df-iota 5812  df-fun 5851  df-fn 5852  df-f 5853  df-f1 5854  df-fo 5855  df-f1o 5856  df-fv 5857  df-riota 6568  df-ov 6610  df-oprab 6611  df-mpt2 6612  df-om 7016  df-1st 7116  df-2nd 7117  df-tpos 7300  df-undef 7347  df-wrecs 7355  df-recs 7416  df-rdg 7454  df-1o 7508  df-oadd 7512  df-er 7690  df-map 7807  df-en 7903  df-dom 7904  df-sdom 7905  df-fin 7906  df-pnf 10023  df-mnf 10024  df-xr 10025  df-ltxr 10026  df-le 10027  df-sub 10215  df-neg 10216  df-nn 10968  df-2 11026  df-3 11027  df-4 11028  df-5 11029  df-6 11030  df-n0 11240  df-z 11325  df-uz 11635  df-fz 12272  df-struct 15786  df-ndx 15787  df-slot 15788  df-base 15789  df-sets 15790  df-ress 15791  df-plusg 15878  df-mulr 15879  df-sca 15881  df-vsca 15882  df-0g 16026  df-preset 16852  df-poset 16870  df-plt 16882  df-lub 16898  df-glb 16899  df-join 16900  df-meet 16901  df-p0 16963  df-p1 16964  df-lat 16970  df-clat 17032  df-mgm 17166  df-sgrp 17208  df-mnd 17219  df-submnd 17260  df-grp 17349  df-minusg 17350  df-sbg 17351  df-subg 17515  df-cntz 17674  df-lsm 17975  df-cmn 18119  df-abl 18120  df-mgp 18414  df-ur 18426  df-ring 18473  df-oppr 18547  df-dvdsr 18565  df-unit 18566  df-invr 18596  df-dvr 18607  df-drng 18673  df-lmod 18789  df-lss 18855  df-lsp 18894  df-lvec 19025  df-lsatoms 33764  df-lshyp 33765  df-lfl 33846  df-lkr 33874  df-oposet 33964  df-ol 33966  df-oml 33967  df-covers 34054  df-ats 34055  df-atl 34086  df-cvlat 34110  df-hlat 34139  df-llines 34285  df-lplanes 34286  df-lvols 34287  df-lines 34288  df-psubsp 34290  df-pmap 34291  df-padd 34583  df-lhyp 34775  df-laut 34776  df-ldil 34891  df-ltrn 34892  df-trl 34947  df-tgrp 35532  df-tendo 35544  df-edring 35546  df-dveca 35792  df-disoa 35819  df-dvech 35869  df-dib 35929  df-dic 35963  df-dih 36019  df-doch 36138  df-djh 36185  df-mapd 36415
This theorem is referenced by:  mapdval5N  36423  mapd1dim2lem1N  36434
  Copyright terms: Public domain W3C validator