lclkrlem2f - Mathbox for Norm Megill

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

Theorem lclkrlem2f 41634

Description: Lemma for lclkr 41655. Construct a closed hyperplane under the kernel of the sum. (Contributed by NM, 16-Jan-2015.)

**Hypotheses**
Ref	Expression
lclkrlem2f.h	⊢ 𝐻 = (LHyp‘𝐾)
lclkrlem2f.o	⊢ ⊥ = ((ocH‘𝐾)‘𝑊)
lclkrlem2f.u	⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
lclkrlem2f.v	⊢ 𝑉 = (Base‘𝑈)
lclkrlem2f.s	⊢ 𝑆 = (Scalar‘𝑈)
lclkrlem2f.q	⊢ 𝑄 = (0_g‘𝑆)
lclkrlem2f.z	⊢ 0 = (0_g‘𝑈)
lclkrlem2f.a	⊢ ⊕ = (LSSum‘𝑈)
lclkrlem2f.n	⊢ 𝑁 = (LSpan‘𝑈)
lclkrlem2f.f	⊢ 𝐹 = (LFnl‘𝑈)
lclkrlem2f.j	⊢ 𝐽 = (LSHyp‘𝑈)
lclkrlem2f.l	⊢ 𝐿 = (LKer‘𝑈)
lclkrlem2f.d	⊢ 𝐷 = (LDual‘𝑈)
lclkrlem2f.p	⊢ + = (+_g‘𝐷)
lclkrlem2f.k	⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
lclkrlem2f.b	⊢ (𝜑 → 𝐵 ∈ (𝑉 ∖ { 0 }))
lclkrlem2f.e	⊢ (𝜑 → 𝐸 ∈ 𝐹)
lclkrlem2f.g	⊢ (𝜑 → 𝐺 ∈ 𝐹)
lclkrlem2f.le	⊢ (𝜑 → (𝐿‘𝐸) = ( ⊥ ‘{𝑋}))
lclkrlem2f.lg	⊢ (𝜑 → (𝐿‘𝐺) = ( ⊥ ‘{𝑌}))
lclkrlem2f.kb	⊢ (𝜑 → ((𝐸 + 𝐺)‘𝐵) = 𝑄)
lclkrlem2f.nx	⊢ (𝜑 → (¬ 𝑋 ∈ ( ⊥ ‘{𝐵}) ∨ ¬ 𝑌 ∈ ( ⊥ ‘{𝐵})))
lclkrlem2f.x	⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))
lclkrlem2f.y	⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))
lclkrlem2f.ne	⊢ (𝜑 → (𝐿‘𝐸) ≠ (𝐿‘𝐺))
lclkrlem2f.lp	⊢ (𝜑 → (𝐿‘(𝐸 + 𝐺)) ∈ 𝐽)

**Assertion**
Ref	Expression
lclkrlem2f	⊢ (𝜑 → (((𝐿‘𝐸) ∩ (𝐿‘𝐺)) ⊕ (𝑁‘{𝐵})) ⊆ (𝐿‘(𝐸 + 𝐺)))

**Proof of Theorem lclkrlem2f**
Step	Hyp	Ref	Expression
1		lclkrlem2f.f	. . 3 ⊢ 𝐹 = (LFnl‘𝑈)
2		lclkrlem2f.l	. . 3 ⊢ 𝐿 = (LKer‘𝑈)
3		lclkrlem2f.d	. . 3 ⊢ 𝐷 = (LDual‘𝑈)
4		lclkrlem2f.p	. . 3 ⊢ + = (+_g‘𝐷)
5		lclkrlem2f.h	. . . 4 ⊢ 𝐻 = (LHyp‘𝐾)
6		lclkrlem2f.u	. . . 4 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
7		lclkrlem2f.k	. . . 4 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
8	5, 6, 7	dvhlmod 41232	. . 3 ⊢ (𝜑 → 𝑈 ∈ LMod)
9		lclkrlem2f.e	. . 3 ⊢ (𝜑 → 𝐸 ∈ 𝐹)
10		lclkrlem2f.g	. . 3 ⊢ (𝜑 → 𝐺 ∈ 𝐹)
11	1, 2, 3, 4, 8, 9, 10	lkrin 39286	. 2 ⊢ (𝜑 → ((𝐿‘𝐸) ∩ (𝐿‘𝐺)) ⊆ (𝐿‘(𝐸 + 𝐺)))
12		eqid 2733	. . 3 ⊢ (LSubSp‘𝑈) = (LSubSp‘𝑈)
13		lclkrlem2f.n	. . 3 ⊢ 𝑁 = (LSpan‘𝑈)
14		lclkrlem2f.j	. . . 4 ⊢ 𝐽 = (LSHyp‘𝑈)
15		lclkrlem2f.lp	. . . 4 ⊢ (𝜑 → (𝐿‘(𝐸 + 𝐺)) ∈ 𝐽)
16	12, 14, 8, 15	lshplss 39103	. . 3 ⊢ (𝜑 → (𝐿‘(𝐸 + 𝐺)) ∈ (LSubSp‘𝑈))
17		lclkrlem2f.kb	. . . 4 ⊢ (𝜑 → ((𝐸 + 𝐺)‘𝐵) = 𝑄)
18		lclkrlem2f.v	. . . . 5 ⊢ 𝑉 = (Base‘𝑈)
19		lclkrlem2f.s	. . . . 5 ⊢ 𝑆 = (Scalar‘𝑈)
20		lclkrlem2f.q	. . . . 5 ⊢ 𝑄 = (0_g‘𝑆)
21	1, 3, 4, 8, 9, 10	ldualvaddcl 39252	. . . . 5 ⊢ (𝜑 → (𝐸 + 𝐺) ∈ 𝐹)
22		lclkrlem2f.b	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ (𝑉 ∖ { 0 }))
23	22	eldifad 3910	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ 𝑉)
24	18, 19, 20, 1, 2, 8, 21, 23	ellkr2 39213	. . . 4 ⊢ (𝜑 → (𝐵 ∈ (𝐿‘(𝐸 + 𝐺)) ↔ ((𝐸 + 𝐺)‘𝐵) = 𝑄))
25	17, 24	mpbird 257	. . 3 ⊢ (𝜑 → 𝐵 ∈ (𝐿‘(𝐸 + 𝐺)))
26	12, 13, 8, 16, 25	ellspsn5 20933	. 2 ⊢ (𝜑 → (𝑁‘{𝐵}) ⊆ (𝐿‘(𝐸 + 𝐺)))
27	12	lsssssubg 20895	. . . . 5 ⊢ (𝑈 ∈ LMod → (LSubSp‘𝑈) ⊆ (SubGrp‘𝑈))
28	8, 27	syl 17	. . . 4 ⊢ (𝜑 → (LSubSp‘𝑈) ⊆ (SubGrp‘𝑈))
29	1, 2, 12	lkrlss 39217	. . . . . 6 ⊢ ((𝑈 ∈ LMod ∧ 𝐸 ∈ 𝐹) → (𝐿‘𝐸) ∈ (LSubSp‘𝑈))
30	8, 9, 29	syl2anc 584	. . . . 5 ⊢ (𝜑 → (𝐿‘𝐸) ∈ (LSubSp‘𝑈))
31	1, 2, 12	lkrlss 39217	. . . . . 6 ⊢ ((𝑈 ∈ LMod ∧ 𝐺 ∈ 𝐹) → (𝐿‘𝐺) ∈ (LSubSp‘𝑈))
32	8, 10, 31	syl2anc 584	. . . . 5 ⊢ (𝜑 → (𝐿‘𝐺) ∈ (LSubSp‘𝑈))
33	12	lssincl 20902	. . . . 5 ⊢ ((𝑈 ∈ LMod ∧ (𝐿‘𝐸) ∈ (LSubSp‘𝑈) ∧ (𝐿‘𝐺) ∈ (LSubSp‘𝑈)) → ((𝐿‘𝐸) ∩ (𝐿‘𝐺)) ∈ (LSubSp‘𝑈))
34	8, 30, 32, 33	syl3anc 1373	. . . 4 ⊢ (𝜑 → ((𝐿‘𝐸) ∩ (𝐿‘𝐺)) ∈ (LSubSp‘𝑈))
35	28, 34	sseldd 3931	. . 3 ⊢ (𝜑 → ((𝐿‘𝐸) ∩ (𝐿‘𝐺)) ∈ (SubGrp‘𝑈))
36	18, 12, 13	lspsncl 20914	. . . . 5 ⊢ ((𝑈 ∈ LMod ∧ 𝐵 ∈ 𝑉) → (𝑁‘{𝐵}) ∈ (LSubSp‘𝑈))
37	8, 23, 36	syl2anc 584	. . . 4 ⊢ (𝜑 → (𝑁‘{𝐵}) ∈ (LSubSp‘𝑈))
38	28, 37	sseldd 3931	. . 3 ⊢ (𝜑 → (𝑁‘{𝐵}) ∈ (SubGrp‘𝑈))
39	28, 16	sseldd 3931	. . 3 ⊢ (𝜑 → (𝐿‘(𝐸 + 𝐺)) ∈ (SubGrp‘𝑈))
40		lclkrlem2f.a	. . . 4 ⊢ ⊕ = (LSSum‘𝑈)
41	40	lsmlub 19580	. . 3 ⊢ ((((𝐿‘𝐸) ∩ (𝐿‘𝐺)) ∈ (SubGrp‘𝑈) ∧ (𝑁‘{𝐵}) ∈ (SubGrp‘𝑈) ∧ (𝐿‘(𝐸 + 𝐺)) ∈ (SubGrp‘𝑈)) → ((((𝐿‘𝐸) ∩ (𝐿‘𝐺)) ⊆ (𝐿‘(𝐸 + 𝐺)) ∧ (𝑁‘{𝐵}) ⊆ (𝐿‘(𝐸 + 𝐺))) ↔ (((𝐿‘𝐸) ∩ (𝐿‘𝐺)) ⊕ (𝑁‘{𝐵})) ⊆ (𝐿‘(𝐸 + 𝐺))))
42	35, 38, 39, 41	syl3anc 1373	. 2 ⊢ (𝜑 → ((((𝐿‘𝐸) ∩ (𝐿‘𝐺)) ⊆ (𝐿‘(𝐸 + 𝐺)) ∧ (𝑁‘{𝐵}) ⊆ (𝐿‘(𝐸 + 𝐺))) ↔ (((𝐿‘𝐸) ∩ (𝐿‘𝐺)) ⊕ (𝑁‘{𝐵})) ⊆ (𝐿‘(𝐸 + 𝐺))))
43	11, 26, 42	mpbi2and 712	1 ⊢ (𝜑 → (((𝐿‘𝐸) ∩ (𝐿‘𝐺)) ⊕ (𝑁‘{𝐵})) ⊆ (𝐿‘(𝐸 + 𝐺)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 847 = wceq 1541 ∈ wcel 2113 ≠ wne 2929 ∖ cdif 3895 ∩ cin 3897 ⊆ wss 3898 {csn 4577 ‘cfv 6488 (class class class)co 7354 Basecbs 17124 +_gcplusg 17165 Scalarcsca 17168 0_gc0g 17347 SubGrpcsubg 19037 LSSumclsm 19550 LModclmod 20797 LSubSpclss 20868 LSpanclspn 20908 LSHypclsh 39097 LFnlclfn 39179 LKerclk 39207 LDualcld 39245 HLchlt 39472 LHypclh 40106 DVecHcdvh 41200 ocHcoch 41469

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2182 ax-ext 2705 ax-rep 5221 ax-sep 5238 ax-nul 5248 ax-pow 5307 ax-pr 5374 ax-un 7676 ax-cnex 11071 ax-resscn 11072 ax-1cn 11073 ax-icn 11074 ax-addcl 11075 ax-addrcl 11076 ax-mulcl 11077 ax-mulrcl 11078 ax-mulcom 11079 ax-addass 11080 ax-mulass 11081 ax-distr 11082 ax-i2m1 11083 ax-1ne0 11084 ax-1rid 11085 ax-rnegex 11086 ax-rrecex 11087 ax-cnre 11088 ax-pre-lttri 11089 ax-pre-lttrn 11090 ax-pre-ltadd 11091 ax-pre-mulgt0 11092 ax-riotaBAD 39075

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2725 df-clel 2808 df-nfc 2882 df-ne 2930 df-nel 3034 df-ral 3049 df-rex 3058 df-rmo 3347 df-reu 3348 df-rab 3397 df-v 3439 df-sbc 3738 df-csb 3847 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-pss 3918 df-nul 4283 df-if 4477 df-pw 4553 df-sn 4578 df-pr 4580 df-tp 4582 df-op 4584 df-uni 4861 df-int 4900 df-iun 4945 df-iin 4946 df-br 5096 df-opab 5158 df-mpt 5177 df-tr 5203 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 7311 df-ov 7357 df-oprab 7358 df-mpo 7359 df-of 7618 df-om 7805 df-1st 7929 df-2nd 7930 df-tpos 8164 df-undef 8211 df-frecs 8219 df-wrecs 8250 df-recs 8299 df-rdg 8337 df-1o 8393 df-er 8630 df-map 8760 df-en 8878 df-dom 8879 df-sdom 8880 df-fin 8881 df-pnf 11157 df-mnf 11158 df-xr 11159 df-ltxr 11160 df-le 11161 df-sub 11355 df-neg 11356 df-nn 12135 df-2 12197 df-3 12198 df-4 12199 df-5 12200 df-6 12201 df-n0 12391 df-z 12478 df-uz 12741 df-fz 13412 df-struct 17062 df-sets 17079 df-slot 17097 df-ndx 17109 df-base 17125 df-ress 17146 df-plusg 17178 df-mulr 17179 df-sca 17181 df-vsca 17182 df-0g 17349 df-proset 18204 df-poset 18223 df-plt 18238 df-lub 18254 df-glb 18255 df-join 18256 df-meet 18257 df-p0 18333 df-p1 18334 df-lat 18342 df-clat 18409 df-mgm 18552 df-sgrp 18631 df-mnd 18647 df-submnd 18696 df-grp 18853 df-minusg 18854 df-sbg 18855 df-subg 19040 df-lsm 19552 df-cmn 19698 df-abl 19699 df-mgp 20063 df-rng 20075 df-ur 20104 df-ring 20157 df-oppr 20259 df-dvdsr 20279 df-unit 20280 df-invr 20310 df-dvr 20323 df-drng 20650 df-lmod 20799 df-lss 20869 df-lsp 20909 df-lvec 21041 df-lshyp 39099 df-lfl 39180 df-lkr 39208 df-ldual 39246 df-oposet 39298 df-ol 39300 df-oml 39301 df-covers 39388 df-ats 39389 df-atl 39420 df-cvlat 39444 df-hlat 39473 df-llines 39620 df-lplanes 39621 df-lvols 39622 df-lines 39623 df-psubsp 39625 df-pmap 39626 df-padd 39918 df-lhyp 40110 df-laut 40111 df-ldil 40226 df-ltrn 40227 df-trl 40281 df-tendo 40877 df-edring 40879 df-dvech 41201

This theorem is referenced by: lclkrlem2g 41635

W3C validator