lclkrslem1 - Mathbox for Norm Megill

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

Theorem lclkrslem1 42026

Description: The set of functionals having closed kernels and majorizing the orthocomplement of a given subspace 𝑄 is closed under scalar product. (Contributed by NM, 27-Jan-2015.)

**Hypotheses**
Ref	Expression
lclkrslem1.h	⊢ 𝐻 = (LHyp‘𝐾)
lclkrslem1.o	⊢ ⊥ = ((ocH‘𝐾)‘𝑊)
lclkrslem1.u	⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
lclkrslem1.s	⊢ 𝑆 = (LSubSp‘𝑈)
lclkrslem1.f	⊢ 𝐹 = (LFnl‘𝑈)
lclkrslem1.l	⊢ 𝐿 = (LKer‘𝑈)
lclkrslem1.d	⊢ 𝐷 = (LDual‘𝑈)
lclkrslem1.r	⊢ 𝑅 = (Scalar‘𝑈)
lclkrslem1.b	⊢ 𝐵 = (Base‘𝑅)
lclkrslem1.t	⊢ · = ( ·_𝑠 ‘𝐷)
lclkrslem1.c	⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ (( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ ( ⊥ ‘(𝐿‘𝑓)) ⊆ 𝑄)}
lclkrslem1.k	⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
lclkrslem1.q	⊢ (𝜑 → 𝑄 ∈ 𝑆)
lclkrslem1.g	⊢ (𝜑 → 𝐺 ∈ 𝐶)
lclkrslem1.x	⊢ (𝜑 → 𝑋 ∈ 𝐵)

**Assertion**
Ref	Expression
lclkrslem1	⊢ (𝜑 → (𝑋 · 𝐺) ∈ 𝐶)

Distinct variable groups: ⊥ ,𝑓 𝑓,𝐹 𝑓,𝐺 𝑓,𝐿 𝑄,𝑓 · ,𝑓 𝑓,𝑋 Allowed substitution hints: 𝜑(𝑓) 𝐵(𝑓) 𝐶(𝑓) 𝐷(𝑓) 𝑅(𝑓) 𝑆(𝑓) 𝑈(𝑓) 𝐻(𝑓) 𝐾(𝑓) 𝑊(𝑓)

**Proof of Theorem lclkrslem1**
Step	Hyp	Ref	Expression
1		lclkrslem1.h	. . 3 ⊢ 𝐻 = (LHyp‘𝐾)
2		lclkrslem1.o	. . 3 ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)
3		lclkrslem1.u	. . 3 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
4		lclkrslem1.f	. . 3 ⊢ 𝐹 = (LFnl‘𝑈)
5		lclkrslem1.l	. . 3 ⊢ 𝐿 = (LKer‘𝑈)
6		lclkrslem1.d	. . 3 ⊢ 𝐷 = (LDual‘𝑈)
7		lclkrslem1.r	. . 3 ⊢ 𝑅 = (Scalar‘𝑈)
8		lclkrslem1.b	. . 3 ⊢ 𝐵 = (Base‘𝑅)
9		lclkrslem1.t	. . 3 ⊢ · = ( ·_𝑠 ‘𝐷)
10		eqid 2736	. . 3 ⊢ {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)}
11		lclkrslem1.k	. . 3 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
12		lclkrslem1.x	. . 3 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
13		lclkrslem1.g	. . . 4 ⊢ (𝜑 → 𝐺 ∈ 𝐶)
14		lclkrslem1.c	. . . . . 6 ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ (( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ ( ⊥ ‘(𝐿‘𝑓)) ⊆ 𝑄)}
15	14, 10	lcfls1c 42025	. . . . 5 ⊢ (𝐺 ∈ 𝐶 ↔ (𝐺 ∈ {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} ∧ ( ⊥ ‘(𝐿‘𝐺)) ⊆ 𝑄))
16	15	simplbi 497	. . . 4 ⊢ (𝐺 ∈ 𝐶 → 𝐺 ∈ {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)})
17	13, 16	syl 17	. . 3 ⊢ (𝜑 → 𝐺 ∈ {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)})
18	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 17	lclkrlem1 41995	. 2 ⊢ (𝜑 → (𝑋 · 𝐺) ∈ {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)})
19		eqid 2736	. . . . 5 ⊢ (Base‘𝑈) = (Base‘𝑈)
20	1, 3, 11	dvhlmod 41599	. . . . 5 ⊢ (𝜑 → 𝑈 ∈ LMod)
21	14	lcfls1lem 42023	. . . . . . . 8 ⊢ (𝐺 ∈ 𝐶 ↔ (𝐺 ∈ 𝐹 ∧ ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = (𝐿‘𝐺) ∧ ( ⊥ ‘(𝐿‘𝐺)) ⊆ 𝑄))
22	13, 21	sylib 219	. . . . . . 7 ⊢ (𝜑 → (𝐺 ∈ 𝐹 ∧ ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = (𝐿‘𝐺) ∧ ( ⊥ ‘(𝐿‘𝐺)) ⊆ 𝑄))
23	22	simp1d 1144	. . . . . 6 ⊢ (𝜑 → 𝐺 ∈ 𝐹)
24	4, 7, 8, 6, 9, 20, 12, 23	ldualvscl 39628	. . . . 5 ⊢ (𝜑 → (𝑋 · 𝐺) ∈ 𝐹)
25	19, 4, 5, 20, 24	lkrssv 39585	. . . 4 ⊢ (𝜑 → (𝐿‘(𝑋 · 𝐺)) ⊆ (Base‘𝑈))
26	1, 3, 11	dvhlvec 41598	. . . . 5 ⊢ (𝜑 → 𝑈 ∈ LVec)
27	7, 8, 4, 5, 6, 9, 26, 23, 12	lkrss 39657	. . . 4 ⊢ (𝜑 → (𝐿‘𝐺) ⊆ (𝐿‘(𝑋 · 𝐺)))
28	1, 3, 19, 2	dochss 41854	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐿‘(𝑋 · 𝐺)) ⊆ (Base‘𝑈) ∧ (𝐿‘𝐺) ⊆ (𝐿‘(𝑋 · 𝐺))) → ( ⊥ ‘(𝐿‘(𝑋 · 𝐺))) ⊆ ( ⊥ ‘(𝐿‘𝐺)))
29	11, 25, 27, 28	syl3anc 1375	. . 3 ⊢ (𝜑 → ( ⊥ ‘(𝐿‘(𝑋 · 𝐺))) ⊆ ( ⊥ ‘(𝐿‘𝐺)))
30	22	simp3d 1146	. . 3 ⊢ (𝜑 → ( ⊥ ‘(𝐿‘𝐺)) ⊆ 𝑄)
31	29, 30	sstrd 3928	. 2 ⊢ (𝜑 → ( ⊥ ‘(𝐿‘(𝑋 · 𝐺))) ⊆ 𝑄)
32	14, 10	lcfls1c 42025	. 2 ⊢ ((𝑋 · 𝐺) ∈ 𝐶 ↔ ((𝑋 · 𝐺) ∈ {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} ∧ ( ⊥ ‘(𝐿‘(𝑋 · 𝐺))) ⊆ 𝑄))
33	18, 31, 32	sylanbrc 585	1 ⊢ (𝜑 → (𝑋 · 𝐺) ∈ 𝐶)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1088 = wceq 1543 ∈ wcel 2115 {crab 3388 ⊆ wss 3886 ‘cfv 6488 (class class class)co 7359 Basecbs 17173 Scalarcsca 17217 ·_𝑠 cvsca 17218 LSubSpclss 20924 LFnlclfn 39546 LKerclk 39574 LDualcld 39612 HLchlt 39839 LHypclh 40473 DVecHcdvh 41567 ocHcoch 41836

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1970 ax-7 2011 ax-8 2117 ax-9 2125 ax-10 2148 ax-11 2164 ax-12 2185 ax-ext 2708 ax-rep 5202 ax-sep 5221 ax-nul 5231 ax-pow 5297 ax-pr 5365 ax-un 7681 ax-cnex 11088 ax-resscn 11089 ax-1cn 11090 ax-icn 11091 ax-addcl 11092 ax-addrcl 11093 ax-mulcl 11094 ax-mulrcl 11095 ax-mulcom 11096 ax-addass 11097 ax-mulass 11098 ax-distr 11099 ax-i2m1 11100 ax-1ne0 11101 ax-1rid 11102 ax-rnegex 11103 ax-rrecex 11104 ax-cnre 11105 ax-pre-lttri 11106 ax-pre-lttrn 11107 ax-pre-ltadd 11108 ax-pre-mulgt0 11109 ax-riotaBAD 39442

This theorem depends on definitions: df-bi 208 df-an 397 df-or 850 df-3or 1089 df-3an 1090 df-tru 1546 df-fal 1556 df-ex 1783 df-nf 1787 df-sb 2070 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2932 df-nel 3036 df-ral 3051 df-rex 3061 df-rmo 3341 df-reu 3342 df-rab 3389 df-v 3430 df-sbc 3727 df-csb 3835 df-dif 3889 df-un 3891 df-in 3893 df-ss 3903 df-pss 3906 df-nul 4265 df-if 4458 df-pw 4534 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4842 df-int 4881 df-iun 4926 df-iin 4927 df-br 5076 df-opab 5138 df-mpt 5157 df-tr 5183 df-id 5516 df-eprel 5521 df-po 5529 df-so 5530 df-fr 5574 df-we 5576 df-xp 5627 df-rel 5628 df-cnv 5629 df-co 5630 df-dm 5631 df-rn 5632 df-res 5633 df-ima 5634 df-pred 6255 df-ord 6316 df-on 6317 df-lim 6318 df-suc 6319 df-iota 6444 df-fun 6490 df-fn 6491 df-f 6492 df-f1 6493 df-fo 6494 df-f1o 6495 df-fv 6496 df-riota 7316 df-ov 7362 df-oprab 7363 df-mpo 7364 df-of 7623 df-om 7810 df-1st 7934 df-2nd 7935 df-tpos 8169 df-undef 8216 df-frecs 8224 df-wrecs 8255 df-recs 8304 df-rdg 8342 df-1o 8398 df-er 8636 df-map 8768 df-en 8887 df-dom 8888 df-sdom 8889 df-fin 8890 df-pnf 11175 df-mnf 11176 df-xr 11177 df-ltxr 11178 df-le 11179 df-sub 11373 df-neg 11374 df-nn 12169 df-2 12238 df-3 12239 df-4 12240 df-5 12241 df-6 12242 df-n0 12432 df-z 12519 df-uz 12783 df-fz 13456 df-struct 17111 df-sets 17128 df-slot 17146 df-ndx 17158 df-base 17174 df-ress 17195 df-plusg 17227 df-mulr 17228 df-sca 17230 df-vsca 17231 df-0g 17398 df-proset 18254 df-poset 18273 df-plt 18288 df-lub 18304 df-glb 18305 df-join 18306 df-meet 18307 df-p0 18383 df-p1 18384 df-lat 18392 df-clat 18459 df-mgm 18602 df-sgrp 18681 df-mnd 18697 df-submnd 18746 df-grp 18906 df-minusg 18907 df-sbg 18908 df-subg 19093 df-cntz 19286 df-lsm 19605 df-cmn 19751 df-abl 19752 df-mgp 20116 df-rng 20128 df-ur 20157 df-ring 20210 df-oppr 20311 df-dvdsr 20331 df-unit 20332 df-invr 20362 df-dvr 20375 df-nzr 20488 df-rlreg 20669 df-domn 20670 df-drng 20706 df-lmod 20855 df-lss 20925 df-lsp 20965 df-lvec 21096 df-lfl 39547 df-lkr 39575 df-ldual 39613 df-oposet 39665 df-ol 39667 df-oml 39668 df-covers 39755 df-ats 39756 df-atl 39787 df-cvlat 39811 df-hlat 39840 df-llines 39987 df-lplanes 39988 df-lvols 39989 df-lines 39990 df-psubsp 39992 df-pmap 39993 df-padd 40285 df-lhyp 40477 df-laut 40478 df-ldil 40593 df-ltrn 40594 df-trl 40648 df-tendo 41244 df-edring 41246 df-disoa 41518 df-dvech 41568 df-dib 41628 df-dic 41662 df-dih 41718 df-doch 41837

This theorem is referenced by: lclkrs 42028

W3C validator