Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > lcfrlem35 | Structured version Visualization version GIF version |
Description: Lemma for lcfr 39293. (Contributed by NM, 2-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‘𝑈) |
lcfrlem28.jn | ⊢ (𝜑 → ((𝐽‘𝑌)‘𝐼) ≠ 𝑄) |
lcfrlem29.i | ⊢ 𝐹 = (invr‘𝑆) |
lcfrlem30.m | ⊢ − = (-g‘𝐷) |
lcfrlem30.c | ⊢ 𝐶 = ((𝐽‘𝑋) − (((𝐹‘((𝐽‘𝑌)‘𝐼))(.r‘𝑆)((𝐽‘𝑋)‘𝐼))( ·𝑠 ‘𝐷)(𝐽‘𝑌))) |
Ref | Expression |
---|---|
lcfrlem35 | ⊢ (𝜑 → ( ⊥ ‘{(𝑋 + 𝑌)}) = (𝐿‘𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lcfrlem17.h | . . . 4 ⊢ 𝐻 = (LHyp‘𝐾) | |
2 | lcfrlem17.o | . . . 4 ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) | |
3 | lcfrlem17.u | . . . 4 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) | |
4 | lcfrlem17.v | . . . 4 ⊢ 𝑉 = (Base‘𝑈) | |
5 | lcfrlem17.p | . . . 4 ⊢ + = (+g‘𝑈) | |
6 | lcfrlem17.z | . . . 4 ⊢ 0 = (0g‘𝑈) | |
7 | lcfrlem17.n | . . . 4 ⊢ 𝑁 = (LSpan‘𝑈) | |
8 | lcfrlem17.a | . . . 4 ⊢ 𝐴 = (LSAtoms‘𝑈) | |
9 | lcfrlem17.k | . . . 4 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) | |
10 | lcfrlem17.x | . . . 4 ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) | |
11 | lcfrlem17.y | . . . 4 ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) | |
12 | lcfrlem17.ne | . . . 4 ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) | |
13 | lcfrlem22.b | . . . 4 ⊢ 𝐵 = ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) | |
14 | eqid 2734 | . . . 4 ⊢ (LSSum‘𝑈) = (LSSum‘𝑈) | |
15 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14 | lcfrlem23 39273 | . . 3 ⊢ (𝜑 → (( ⊥ ‘{𝑋, 𝑌})(LSSum‘𝑈)𝐵) = ( ⊥ ‘{(𝑋 + 𝑌)})) |
16 | lcfrlem24.t | . . . . . 6 ⊢ · = ( ·𝑠 ‘𝑈) | |
17 | lcfrlem24.s | . . . . . 6 ⊢ 𝑆 = (Scalar‘𝑈) | |
18 | lcfrlem24.q | . . . . . 6 ⊢ 𝑄 = (0g‘𝑆) | |
19 | lcfrlem24.r | . . . . . 6 ⊢ 𝑅 = (Base‘𝑆) | |
20 | lcfrlem24.j | . . . . . 6 ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) | |
21 | lcfrlem24.ib | . . . . . 6 ⊢ (𝜑 → 𝐼 ∈ 𝐵) | |
22 | lcfrlem24.l | . . . . . 6 ⊢ 𝐿 = (LKer‘𝑈) | |
23 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 16, 17, 18, 19, 20, 21, 22 | lcfrlem24 39274 | . . . . 5 ⊢ (𝜑 → ( ⊥ ‘{𝑋, 𝑌}) = ((𝐿‘(𝐽‘𝑋)) ∩ (𝐿‘(𝐽‘𝑌)))) |
24 | eqid 2734 | . . . . . 6 ⊢ (.r‘𝑆) = (.r‘𝑆) | |
25 | lcfrlem29.i | . . . . . 6 ⊢ 𝐹 = (invr‘𝑆) | |
26 | eqid 2734 | . . . . . 6 ⊢ (LFnl‘𝑈) = (LFnl‘𝑈) | |
27 | lcfrlem25.d | . . . . . 6 ⊢ 𝐷 = (LDual‘𝑈) | |
28 | eqid 2734 | . . . . . 6 ⊢ ( ·𝑠 ‘𝐷) = ( ·𝑠 ‘𝐷) | |
29 | lcfrlem30.m | . . . . . 6 ⊢ − = (-g‘𝐷) | |
30 | 1, 3, 9 | dvhlvec 38817 | . . . . . 6 ⊢ (𝜑 → 𝑈 ∈ LVec) |
31 | eqid 2734 | . . . . . . 7 ⊢ (0g‘𝐷) = (0g‘𝐷) | |
32 | eqid 2734 | . . . . . . 7 ⊢ {𝑓 ∈ (LFnl‘𝑈) ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} = {𝑓 ∈ (LFnl‘𝑈) ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} | |
33 | 1, 2, 3, 4, 5, 16, 17, 19, 6, 26, 22, 27, 31, 32, 20, 9, 10 | lcfrlem10 39260 | . . . . . 6 ⊢ (𝜑 → (𝐽‘𝑋) ∈ (LFnl‘𝑈)) |
34 | 1, 2, 3, 4, 5, 16, 17, 19, 6, 26, 22, 27, 31, 32, 20, 9, 11 | lcfrlem10 39260 | . . . . . 6 ⊢ (𝜑 → (𝐽‘𝑌) ∈ (LFnl‘𝑈)) |
35 | eqid 2734 | . . . . . . . 8 ⊢ (LSubSp‘𝑈) = (LSubSp‘𝑈) | |
36 | 1, 3, 9 | dvhlmod 38818 | . . . . . . . 8 ⊢ (𝜑 → 𝑈 ∈ LMod) |
37 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13 | lcfrlem22 39272 | . . . . . . . 8 ⊢ (𝜑 → 𝐵 ∈ 𝐴) |
38 | 35, 8, 36, 37 | lsatlssel 36705 | . . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ (LSubSp‘𝑈)) |
39 | 4, 35 | lssel 19946 | . . . . . . 7 ⊢ ((𝐵 ∈ (LSubSp‘𝑈) ∧ 𝐼 ∈ 𝐵) → 𝐼 ∈ 𝑉) |
40 | 38, 21, 39 | syl2anc 587 | . . . . . 6 ⊢ (𝜑 → 𝐼 ∈ 𝑉) |
41 | lcfrlem28.jn | . . . . . 6 ⊢ (𝜑 → ((𝐽‘𝑌)‘𝐼) ≠ 𝑄) | |
42 | lcfrlem30.c | . . . . . 6 ⊢ 𝐶 = ((𝐽‘𝑋) − (((𝐹‘((𝐽‘𝑌)‘𝐼))(.r‘𝑆)((𝐽‘𝑋)‘𝐼))( ·𝑠 ‘𝐷)(𝐽‘𝑌))) | |
43 | 4, 17, 24, 18, 25, 26, 27, 28, 29, 30, 33, 34, 40, 41, 42, 22 | lcfrlem2 39251 | . . . . 5 ⊢ (𝜑 → ((𝐿‘(𝐽‘𝑋)) ∩ (𝐿‘(𝐽‘𝑌))) ⊆ (𝐿‘𝐶)) |
44 | 23, 43 | eqsstrd 3929 | . . . 4 ⊢ (𝜑 → ( ⊥ ‘{𝑋, 𝑌}) ⊆ (𝐿‘𝐶)) |
45 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 16, 17, 18, 19, 20, 21, 22, 27, 41 | lcfrlem28 39278 | . . . . . 6 ⊢ (𝜑 → 𝐼 ≠ 0 ) |
46 | 6, 7, 8, 30, 37, 21, 45 | lsatel 36713 | . . . . 5 ⊢ (𝜑 → 𝐵 = (𝑁‘{𝐼})) |
47 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 16, 17, 18, 19, 20, 21, 22, 27, 41, 25, 29, 42 | lcfrlem30 39280 | . . . . . . 7 ⊢ (𝜑 → 𝐶 ∈ (LFnl‘𝑈)) |
48 | 26, 22, 35 | lkrlss 36803 | . . . . . . 7 ⊢ ((𝑈 ∈ LMod ∧ 𝐶 ∈ (LFnl‘𝑈)) → (𝐿‘𝐶) ∈ (LSubSp‘𝑈)) |
49 | 36, 47, 48 | syl2anc 587 | . . . . . 6 ⊢ (𝜑 → (𝐿‘𝐶) ∈ (LSubSp‘𝑈)) |
50 | 4, 17, 24, 18, 25, 26, 27, 28, 29, 30, 33, 34, 40, 41, 42, 22 | lcfrlem3 39252 | . . . . . 6 ⊢ (𝜑 → 𝐼 ∈ (𝐿‘𝐶)) |
51 | 35, 7, 36, 49, 50 | lspsnel5a 20005 | . . . . 5 ⊢ (𝜑 → (𝑁‘{𝐼}) ⊆ (𝐿‘𝐶)) |
52 | 46, 51 | eqsstrd 3929 | . . . 4 ⊢ (𝜑 → 𝐵 ⊆ (𝐿‘𝐶)) |
53 | 35 | lsssssubg 19967 | . . . . . . 7 ⊢ (𝑈 ∈ LMod → (LSubSp‘𝑈) ⊆ (SubGrp‘𝑈)) |
54 | 36, 53 | syl 17 | . . . . . 6 ⊢ (𝜑 → (LSubSp‘𝑈) ⊆ (SubGrp‘𝑈)) |
55 | 10 | eldifad 3869 | . . . . . . . 8 ⊢ (𝜑 → 𝑋 ∈ 𝑉) |
56 | 11 | eldifad 3869 | . . . . . . . 8 ⊢ (𝜑 → 𝑌 ∈ 𝑉) |
57 | prssi 4724 | . . . . . . . 8 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → {𝑋, 𝑌} ⊆ 𝑉) | |
58 | 55, 56, 57 | syl2anc 587 | . . . . . . 7 ⊢ (𝜑 → {𝑋, 𝑌} ⊆ 𝑉) |
59 | 1, 3, 4, 35, 2 | dochlss 39062 | . . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ {𝑋, 𝑌} ⊆ 𝑉) → ( ⊥ ‘{𝑋, 𝑌}) ∈ (LSubSp‘𝑈)) |
60 | 9, 58, 59 | syl2anc 587 | . . . . . 6 ⊢ (𝜑 → ( ⊥ ‘{𝑋, 𝑌}) ∈ (LSubSp‘𝑈)) |
61 | 54, 60 | sseldd 3892 | . . . . 5 ⊢ (𝜑 → ( ⊥ ‘{𝑋, 𝑌}) ∈ (SubGrp‘𝑈)) |
62 | 54, 38 | sseldd 3892 | . . . . 5 ⊢ (𝜑 → 𝐵 ∈ (SubGrp‘𝑈)) |
63 | 54, 49 | sseldd 3892 | . . . . 5 ⊢ (𝜑 → (𝐿‘𝐶) ∈ (SubGrp‘𝑈)) |
64 | 14 | lsmlub 19026 | . . . . 5 ⊢ ((( ⊥ ‘{𝑋, 𝑌}) ∈ (SubGrp‘𝑈) ∧ 𝐵 ∈ (SubGrp‘𝑈) ∧ (𝐿‘𝐶) ∈ (SubGrp‘𝑈)) → ((( ⊥ ‘{𝑋, 𝑌}) ⊆ (𝐿‘𝐶) ∧ 𝐵 ⊆ (𝐿‘𝐶)) ↔ (( ⊥ ‘{𝑋, 𝑌})(LSSum‘𝑈)𝐵) ⊆ (𝐿‘𝐶))) |
65 | 61, 62, 63, 64 | syl3anc 1373 | . . . 4 ⊢ (𝜑 → ((( ⊥ ‘{𝑋, 𝑌}) ⊆ (𝐿‘𝐶) ∧ 𝐵 ⊆ (𝐿‘𝐶)) ↔ (( ⊥ ‘{𝑋, 𝑌})(LSSum‘𝑈)𝐵) ⊆ (𝐿‘𝐶))) |
66 | 44, 52, 65 | mpbi2and 712 | . . 3 ⊢ (𝜑 → (( ⊥ ‘{𝑋, 𝑌})(LSSum‘𝑈)𝐵) ⊆ (𝐿‘𝐶)) |
67 | 15, 66 | eqsstrrd 3930 | . 2 ⊢ (𝜑 → ( ⊥ ‘{(𝑋 + 𝑌)}) ⊆ (𝐿‘𝐶)) |
68 | eqid 2734 | . . 3 ⊢ (LSHyp‘𝑈) = (LSHyp‘𝑈) | |
69 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12 | lcfrlem17 39267 | . . . 4 ⊢ (𝜑 → (𝑋 + 𝑌) ∈ (𝑉 ∖ { 0 })) |
70 | 1, 2, 3, 4, 6, 68, 9, 69 | dochsnshp 39161 | . . 3 ⊢ (𝜑 → ( ⊥ ‘{(𝑋 + 𝑌)}) ∈ (LSHyp‘𝑈)) |
71 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 16, 17, 18, 19, 20, 21, 22, 27, 41, 25, 29, 42 | lcfrlem34 39284 | . . . 4 ⊢ (𝜑 → 𝐶 ≠ (0g‘𝐷)) |
72 | 68, 26, 22, 27, 31, 30, 47 | lduallkr3 36870 | . . . 4 ⊢ (𝜑 → ((𝐿‘𝐶) ∈ (LSHyp‘𝑈) ↔ 𝐶 ≠ (0g‘𝐷))) |
73 | 71, 72 | mpbird 260 | . . 3 ⊢ (𝜑 → (𝐿‘𝐶) ∈ (LSHyp‘𝑈)) |
74 | 68, 30, 70, 73 | lshpcmp 36696 | . 2 ⊢ (𝜑 → (( ⊥ ‘{(𝑋 + 𝑌)}) ⊆ (𝐿‘𝐶) ↔ ( ⊥ ‘{(𝑋 + 𝑌)}) = (𝐿‘𝐶))) |
75 | 67, 74 | mpbid 235 | 1 ⊢ (𝜑 → ( ⊥ ‘{(𝑋 + 𝑌)}) = (𝐿‘𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 = wceq 1543 ∈ wcel 2110 ≠ wne 2935 ∃wrex 3055 {crab 3058 ∖ cdif 3854 ∩ cin 3856 ⊆ wss 3857 {csn 4531 {cpr 4533 ↦ cmpt 5124 ‘cfv 6369 ℩crio 7158 (class class class)co 7202 Basecbs 16684 +gcplusg 16767 .rcmulr 16768 Scalarcsca 16770 ·𝑠 cvsca 16771 0gc0g 16916 -gcsg 18339 SubGrpcsubg 18509 LSSumclsm 18995 invrcinvr 19661 LModclmod 19871 LSubSpclss 19940 LSpanclspn 19980 LSAtomsclsa 36682 LSHypclsh 36683 LFnlclfn 36765 LKerclk 36793 LDualcld 36831 HLchlt 37058 LHypclh 37692 DVecHcdvh 38786 ocHcoch 39055 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2158 ax-12 2175 ax-ext 2706 ax-rep 5168 ax-sep 5181 ax-nul 5188 ax-pow 5247 ax-pr 5311 ax-un 7512 ax-cnex 10768 ax-resscn 10769 ax-1cn 10770 ax-icn 10771 ax-addcl 10772 ax-addrcl 10773 ax-mulcl 10774 ax-mulrcl 10775 ax-mulcom 10776 ax-addass 10777 ax-mulass 10778 ax-distr 10779 ax-i2m1 10780 ax-1ne0 10781 ax-1rid 10782 ax-rnegex 10783 ax-rrecex 10784 ax-cnre 10785 ax-pre-lttri 10786 ax-pre-lttrn 10787 ax-pre-ltadd 10788 ax-pre-mulgt0 10789 ax-riotaBAD 36661 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3or 1090 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2071 df-mo 2537 df-eu 2566 df-clab 2713 df-cleq 2726 df-clel 2812 df-nfc 2882 df-ne 2936 df-nel 3040 df-ral 3059 df-rex 3060 df-reu 3061 df-rmo 3062 df-rab 3063 df-v 3403 df-sbc 3688 df-csb 3803 df-dif 3860 df-un 3862 df-in 3864 df-ss 3874 df-pss 3876 df-nul 4228 df-if 4430 df-pw 4505 df-sn 4532 df-pr 4534 df-tp 4536 df-op 4538 df-uni 4810 df-int 4850 df-iun 4896 df-iin 4897 df-br 5044 df-opab 5106 df-mpt 5125 df-tr 5151 df-id 5444 df-eprel 5449 df-po 5457 df-so 5458 df-fr 5498 df-we 5500 df-xp 5546 df-rel 5547 df-cnv 5548 df-co 5549 df-dm 5550 df-rn 5551 df-res 5552 df-ima 5553 df-pred 6149 df-ord 6205 df-on 6206 df-lim 6207 df-suc 6208 df-iota 6327 df-fun 6371 df-fn 6372 df-f 6373 df-f1 6374 df-fo 6375 df-f1o 6376 df-fv 6377 df-riota 7159 df-ov 7205 df-oprab 7206 df-mpo 7207 df-of 7458 df-om 7634 df-1st 7750 df-2nd 7751 df-tpos 7957 df-undef 8004 df-wrecs 8036 df-recs 8097 df-rdg 8135 df-1o 8191 df-er 8380 df-map 8499 df-en 8616 df-dom 8617 df-sdom 8618 df-fin 8619 df-pnf 10852 df-mnf 10853 df-xr 10854 df-ltxr 10855 df-le 10856 df-sub 11047 df-neg 11048 df-nn 11814 df-2 11876 df-3 11877 df-4 11878 df-5 11879 df-6 11880 df-n0 12074 df-z 12160 df-uz 12422 df-fz 13079 df-struct 16686 df-ndx 16687 df-slot 16688 df-base 16690 df-sets 16691 df-ress 16692 df-plusg 16780 df-mulr 16781 df-sca 16783 df-vsca 16784 df-0g 16918 df-mre 17061 df-mrc 17062 df-acs 17064 df-proset 17774 df-poset 17792 df-plt 17808 df-lub 17824 df-glb 17825 df-join 17826 df-meet 17827 df-p0 17903 df-p1 17904 df-lat 17910 df-clat 17977 df-mgm 18086 df-sgrp 18135 df-mnd 18146 df-submnd 18191 df-grp 18340 df-minusg 18341 df-sbg 18342 df-subg 18512 df-cntz 18683 df-oppg 18710 df-lsm 18997 df-cmn 19144 df-abl 19145 df-mgp 19477 df-ur 19489 df-ring 19536 df-oppr 19613 df-dvdsr 19631 df-unit 19632 df-invr 19662 df-dvr 19673 df-drng 19741 df-lmod 19873 df-lss 19941 df-lsp 19981 df-lvec 20112 df-lsatoms 36684 df-lshyp 36685 df-lcv 36727 df-lfl 36766 df-lkr 36794 df-ldual 36832 df-oposet 36884 df-ol 36886 df-oml 36887 df-covers 36974 df-ats 36975 df-atl 37006 df-cvlat 37030 df-hlat 37059 df-llines 37206 df-lplanes 37207 df-lvols 37208 df-lines 37209 df-psubsp 37211 df-pmap 37212 df-padd 37504 df-lhyp 37696 df-laut 37697 df-ldil 37812 df-ltrn 37813 df-trl 37867 df-tgrp 38451 df-tendo 38463 df-edring 38465 df-dveca 38711 df-disoa 38737 df-dvech 38787 df-dib 38847 df-dic 38881 df-dih 38937 df-doch 39056 df-djh 39103 |
This theorem is referenced by: lcfrlem36 39286 |
Copyright terms: Public domain | W3C validator |