Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > lcfrlem26 | Structured version Visualization version GIF version |
Description: Lemma for lcfr 39902. Special case of lcfrlem36 39895 when ((𝐽‘𝑌)‘𝐼) is zero. (Contributed by NM, 11-Mar-2015.) |
Ref | Expression |
---|---|
lcfrlem17.h | ⊢ 𝐻 = (LHyp‘𝐾) |
lcfrlem17.o | ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) |
lcfrlem17.u | ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
lcfrlem17.v | ⊢ 𝑉 = (Base‘𝑈) |
lcfrlem17.p | ⊢ + = (+g‘𝑈) |
lcfrlem17.z | ⊢ 0 = (0g‘𝑈) |
lcfrlem17.n | ⊢ 𝑁 = (LSpan‘𝑈) |
lcfrlem17.a | ⊢ 𝐴 = (LSAtoms‘𝑈) |
lcfrlem17.k | ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
lcfrlem17.x | ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) |
lcfrlem17.y | ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) |
lcfrlem17.ne | ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) |
lcfrlem22.b | ⊢ 𝐵 = ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) |
lcfrlem24.t | ⊢ · = ( ·𝑠 ‘𝑈) |
lcfrlem24.s | ⊢ 𝑆 = (Scalar‘𝑈) |
lcfrlem24.q | ⊢ 𝑄 = (0g‘𝑆) |
lcfrlem24.r | ⊢ 𝑅 = (Base‘𝑆) |
lcfrlem24.j | ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) |
lcfrlem24.ib | ⊢ (𝜑 → 𝐼 ∈ 𝐵) |
lcfrlem24.l | ⊢ 𝐿 = (LKer‘𝑈) |
lcfrlem25.d | ⊢ 𝐷 = (LDual‘𝑈) |
lcfrlem25.jz | ⊢ (𝜑 → ((𝐽‘𝑌)‘𝐼) = 𝑄) |
lcfrlem25.in | ⊢ (𝜑 → 𝐼 ≠ 0 ) |
Ref | Expression |
---|---|
lcfrlem26 | ⊢ (𝜑 → (𝑋 + 𝑌) ∈ ( ⊥ ‘(𝐿‘(𝐽‘𝑌)))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lcfrlem17.h | . . . . 5 ⊢ 𝐻 = (LHyp‘𝐾) | |
2 | lcfrlem17.u | . . . . 5 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) | |
3 | lcfrlem17.o | . . . . 5 ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) | |
4 | lcfrlem17.v | . . . . 5 ⊢ 𝑉 = (Base‘𝑈) | |
5 | lcfrlem17.n | . . . . 5 ⊢ 𝑁 = (LSpan‘𝑈) | |
6 | lcfrlem17.k | . . . . 5 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) | |
7 | lcfrlem17.p | . . . . . . 7 ⊢ + = (+g‘𝑈) | |
8 | lcfrlem17.z | . . . . . . 7 ⊢ 0 = (0g‘𝑈) | |
9 | lcfrlem17.a | . . . . . . 7 ⊢ 𝐴 = (LSAtoms‘𝑈) | |
10 | lcfrlem17.x | . . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) | |
11 | lcfrlem17.y | . . . . . . 7 ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) | |
12 | lcfrlem17.ne | . . . . . . 7 ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) | |
13 | 1, 3, 2, 4, 7, 8, 5, 9, 6, 10, 11, 12 | lcfrlem17 39876 | . . . . . 6 ⊢ (𝜑 → (𝑋 + 𝑌) ∈ (𝑉 ∖ { 0 })) |
14 | 13 | eldifad 3914 | . . . . 5 ⊢ (𝜑 → (𝑋 + 𝑌) ∈ 𝑉) |
15 | 1, 2, 3, 4, 5, 6, 14 | dochocsn 39698 | . . . 4 ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘{(𝑋 + 𝑌)})) = (𝑁‘{(𝑋 + 𝑌)})) |
16 | lcfrlem22.b | . . . . . 6 ⊢ 𝐵 = ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) | |
17 | lcfrlem24.t | . . . . . 6 ⊢ · = ( ·𝑠 ‘𝑈) | |
18 | lcfrlem24.s | . . . . . 6 ⊢ 𝑆 = (Scalar‘𝑈) | |
19 | lcfrlem24.q | . . . . . 6 ⊢ 𝑄 = (0g‘𝑆) | |
20 | lcfrlem24.r | . . . . . 6 ⊢ 𝑅 = (Base‘𝑆) | |
21 | lcfrlem24.j | . . . . . 6 ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) | |
22 | lcfrlem24.ib | . . . . . 6 ⊢ (𝜑 → 𝐼 ∈ 𝐵) | |
23 | lcfrlem24.l | . . . . . 6 ⊢ 𝐿 = (LKer‘𝑈) | |
24 | lcfrlem25.d | . . . . . 6 ⊢ 𝐷 = (LDual‘𝑈) | |
25 | lcfrlem25.jz | . . . . . 6 ⊢ (𝜑 → ((𝐽‘𝑌)‘𝐼) = 𝑄) | |
26 | lcfrlem25.in | . . . . . 6 ⊢ (𝜑 → 𝐼 ≠ 0 ) | |
27 | 1, 3, 2, 4, 7, 8, 5, 9, 6, 10, 11, 12, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26 | lcfrlem25 39884 | . . . . 5 ⊢ (𝜑 → ( ⊥ ‘{(𝑋 + 𝑌)}) = (𝐿‘(𝐽‘𝑌))) |
28 | 27 | fveq2d 6834 | . . . 4 ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘{(𝑋 + 𝑌)})) = ( ⊥ ‘(𝐿‘(𝐽‘𝑌)))) |
29 | 15, 28 | eqtr3d 2779 | . . 3 ⊢ (𝜑 → (𝑁‘{(𝑋 + 𝑌)}) = ( ⊥ ‘(𝐿‘(𝐽‘𝑌)))) |
30 | eqimss 3992 | . . 3 ⊢ ((𝑁‘{(𝑋 + 𝑌)}) = ( ⊥ ‘(𝐿‘(𝐽‘𝑌))) → (𝑁‘{(𝑋 + 𝑌)}) ⊆ ( ⊥ ‘(𝐿‘(𝐽‘𝑌)))) | |
31 | 29, 30 | syl 17 | . 2 ⊢ (𝜑 → (𝑁‘{(𝑋 + 𝑌)}) ⊆ ( ⊥ ‘(𝐿‘(𝐽‘𝑌)))) |
32 | eqid 2737 | . . 3 ⊢ (LSubSp‘𝑈) = (LSubSp‘𝑈) | |
33 | 1, 2, 6 | dvhlmod 39427 | . . 3 ⊢ (𝜑 → 𝑈 ∈ LMod) |
34 | eqid 2737 | . . . . 5 ⊢ (LFnl‘𝑈) = (LFnl‘𝑈) | |
35 | eqid 2737 | . . . . . 6 ⊢ (0g‘𝐷) = (0g‘𝐷) | |
36 | eqid 2737 | . . . . . 6 ⊢ {𝑓 ∈ (LFnl‘𝑈) ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} = {𝑓 ∈ (LFnl‘𝑈) ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} | |
37 | 1, 3, 2, 4, 7, 17, 18, 20, 8, 34, 23, 24, 35, 36, 21, 6, 11 | lcfrlem10 39869 | . . . . 5 ⊢ (𝜑 → (𝐽‘𝑌) ∈ (LFnl‘𝑈)) |
38 | 4, 34, 23, 33, 37 | lkrssv 37412 | . . . 4 ⊢ (𝜑 → (𝐿‘(𝐽‘𝑌)) ⊆ 𝑉) |
39 | 1, 2, 4, 32, 3 | dochlss 39671 | . . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐿‘(𝐽‘𝑌)) ⊆ 𝑉) → ( ⊥ ‘(𝐿‘(𝐽‘𝑌))) ∈ (LSubSp‘𝑈)) |
40 | 6, 38, 39 | syl2anc 585 | . . 3 ⊢ (𝜑 → ( ⊥ ‘(𝐿‘(𝐽‘𝑌))) ∈ (LSubSp‘𝑈)) |
41 | 4, 32, 5, 33, 40, 14 | lspsnel5 20363 | . 2 ⊢ (𝜑 → ((𝑋 + 𝑌) ∈ ( ⊥ ‘(𝐿‘(𝐽‘𝑌))) ↔ (𝑁‘{(𝑋 + 𝑌)}) ⊆ ( ⊥ ‘(𝐿‘(𝐽‘𝑌))))) |
42 | 31, 41 | mpbird 257 | 1 ⊢ (𝜑 → (𝑋 + 𝑌) ∈ ( ⊥ ‘(𝐿‘(𝐽‘𝑌)))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 = wceq 1541 ∈ wcel 2106 ≠ wne 2941 ∃wrex 3071 {crab 3404 ∖ cdif 3899 ∩ cin 3901 ⊆ wss 3902 {csn 4578 {cpr 4580 ↦ cmpt 5180 ‘cfv 6484 ℩crio 7297 (class class class)co 7342 Basecbs 17010 +gcplusg 17060 Scalarcsca 17063 ·𝑠 cvsca 17064 0gc0g 17248 LSubSpclss 20299 LSpanclspn 20339 LSAtomsclsa 37290 LFnlclfn 37373 LKerclk 37401 LDualcld 37439 HLchlt 37666 LHypclh 38301 DVecHcdvh 39395 ocHcoch 39664 |
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 2708 ax-rep 5234 ax-sep 5248 ax-nul 5255 ax-pow 5313 ax-pr 5377 ax-un 7655 ax-cnex 11033 ax-resscn 11034 ax-1cn 11035 ax-icn 11036 ax-addcl 11037 ax-addrcl 11038 ax-mulcl 11039 ax-mulrcl 11040 ax-mulcom 11041 ax-addass 11042 ax-mulass 11043 ax-distr 11044 ax-i2m1 11045 ax-1ne0 11046 ax-1rid 11047 ax-rnegex 11048 ax-rrecex 11049 ax-cnre 11050 ax-pre-lttri 11051 ax-pre-lttrn 11052 ax-pre-ltadd 11053 ax-pre-mulgt0 11054 ax-riotaBAD 37269 |
This theorem depends on definitions: df-bi 206 df-an 398 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 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2815 df-nfc 2887 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rmo 3350 df-reu 3351 df-rab 3405 df-v 3444 df-sbc 3732 df-csb 3848 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3921 df-nul 4275 df-if 4479 df-pw 4554 df-sn 4579 df-pr 4581 df-tp 4583 df-op 4585 df-uni 4858 df-int 4900 df-iun 4948 df-iin 4949 df-br 5098 df-opab 5160 df-mpt 5181 df-tr 5215 df-id 5523 df-eprel 5529 df-po 5537 df-so 5538 df-fr 5580 df-we 5582 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-res 5637 df-ima 5638 df-pred 6243 df-ord 6310 df-on 6311 df-lim 6312 df-suc 6313 df-iota 6436 df-fun 6486 df-fn 6487 df-f 6488 df-f1 6489 df-fo 6490 df-f1o 6491 df-fv 6492 df-riota 7298 df-ov 7345 df-oprab 7346 df-mpo 7347 df-of 7600 df-om 7786 df-1st 7904 df-2nd 7905 df-tpos 8117 df-undef 8164 df-frecs 8172 df-wrecs 8203 df-recs 8277 df-rdg 8316 df-1o 8372 df-er 8574 df-map 8693 df-en 8810 df-dom 8811 df-sdom 8812 df-fin 8813 df-pnf 11117 df-mnf 11118 df-xr 11119 df-ltxr 11120 df-le 11121 df-sub 11313 df-neg 11314 df-nn 12080 df-2 12142 df-3 12143 df-4 12144 df-5 12145 df-6 12146 df-n0 12340 df-z 12426 df-uz 12689 df-fz 13346 df-struct 16946 df-sets 16963 df-slot 16981 df-ndx 16993 df-base 17011 df-ress 17040 df-plusg 17073 df-mulr 17074 df-sca 17076 df-vsca 17077 df-0g 17250 df-mre 17393 df-mrc 17394 df-acs 17396 df-proset 18111 df-poset 18129 df-plt 18146 df-lub 18162 df-glb 18163 df-join 18164 df-meet 18165 df-p0 18241 df-p1 18242 df-lat 18248 df-clat 18315 df-mgm 18424 df-sgrp 18473 df-mnd 18484 df-submnd 18529 df-grp 18677 df-minusg 18678 df-sbg 18679 df-subg 18849 df-cntz 19020 df-oppg 19047 df-lsm 19338 df-cmn 19484 df-abl 19485 df-mgp 19816 df-ur 19833 df-ring 19880 df-oppr 19957 df-dvdsr 19978 df-unit 19979 df-invr 20009 df-dvr 20020 df-drng 20095 df-lmod 20231 df-lss 20300 df-lsp 20340 df-lvec 20471 df-lsatoms 37292 df-lshyp 37293 df-lcv 37335 df-lfl 37374 df-lkr 37402 df-ldual 37440 df-oposet 37492 df-ol 37494 df-oml 37495 df-covers 37582 df-ats 37583 df-atl 37614 df-cvlat 37638 df-hlat 37667 df-llines 37815 df-lplanes 37816 df-lvols 37817 df-lines 37818 df-psubsp 37820 df-pmap 37821 df-padd 38113 df-lhyp 38305 df-laut 38306 df-ldil 38421 df-ltrn 38422 df-trl 38476 df-tgrp 39060 df-tendo 39072 df-edring 39074 df-dveca 39320 df-disoa 39346 df-dvech 39396 df-dib 39456 df-dic 39490 df-dih 39546 df-doch 39665 df-djh 39712 |
This theorem is referenced by: lcfrlem27 39886 |
Copyright terms: Public domain | W3C validator |