lclkrlem2v - Mathbox for Norm Megill

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

Theorem lclkrlem2v 41637

Description: Lemma for lclkr 41642. When the hypotheses of lclkrlem2u 41636 and lclkrlem2u 41636 are negated, the functional sum must be zero, so the kernel is the vector space. We make use of the law of excluded middle, dochexmid 41577, which requires the orthomodular law dihoml4 41486 (Lemma 3.3 of [Holland95] p. 214). (Contributed by NM, 16-Jan-2015.)

**Hypotheses**
Ref	Expression
lclkrlem2m.v	⊢ 𝑉 = (Base‘𝑈)
lclkrlem2m.t	⊢ · = ( ·_𝑠 ‘𝑈)
lclkrlem2m.s	⊢ 𝑆 = (Scalar‘𝑈)
lclkrlem2m.q	⊢ × = (._r‘𝑆)
lclkrlem2m.z	⊢ 0 = (0_g‘𝑆)
lclkrlem2m.i	⊢ 𝐼 = (inv_r‘𝑆)
lclkrlem2m.m	⊢ − = (-_g‘𝑈)
lclkrlem2m.f	⊢ 𝐹 = (LFnl‘𝑈)
lclkrlem2m.d	⊢ 𝐷 = (LDual‘𝑈)
lclkrlem2m.p	⊢ + = (+_g‘𝐷)
lclkrlem2m.x	⊢ (𝜑 → 𝑋 ∈ 𝑉)
lclkrlem2m.y	⊢ (𝜑 → 𝑌 ∈ 𝑉)
lclkrlem2m.e	⊢ (𝜑 → 𝐸 ∈ 𝐹)
lclkrlem2m.g	⊢ (𝜑 → 𝐺 ∈ 𝐹)
lclkrlem2n.n	⊢ 𝑁 = (LSpan‘𝑈)
lclkrlem2n.l	⊢ 𝐿 = (LKer‘𝑈)
lclkrlem2o.h	⊢ 𝐻 = (LHyp‘𝐾)
lclkrlem2o.o	⊢ ⊥ = ((ocH‘𝐾)‘𝑊)
lclkrlem2o.u	⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
lclkrlem2o.a	⊢ ⊕ = (LSSum‘𝑈)
lclkrlem2o.k	⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
lclkrlem2q.le	⊢ (𝜑 → (𝐿‘𝐸) = ( ⊥ ‘{𝑋}))
lclkrlem2q.lg	⊢ (𝜑 → (𝐿‘𝐺) = ( ⊥ ‘{𝑌}))
lclkrlem2v.j	⊢ (𝜑 → ((𝐸 + 𝐺)‘𝑋) = 0 )
lclkrlem2v.k	⊢ (𝜑 → ((𝐸 + 𝐺)‘𝑌) = 0 )

**Assertion**
Ref	Expression
lclkrlem2v	⊢ (𝜑 → (𝐿‘(𝐸 + 𝐺)) = 𝑉)

**Proof of Theorem lclkrlem2v**
Step	Hyp	Ref	Expression
1		lclkrlem2m.v	. . 3 ⊢ 𝑉 = (Base‘𝑈)
2		lclkrlem2m.f	. . 3 ⊢ 𝐹 = (LFnl‘𝑈)
3		lclkrlem2n.l	. . 3 ⊢ 𝐿 = (LKer‘𝑈)
4		lclkrlem2o.h	. . . 4 ⊢ 𝐻 = (LHyp‘𝐾)
5		lclkrlem2o.u	. . . 4 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
6		lclkrlem2o.k	. . . 4 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
7	4, 5, 6	dvhlmod 41219	. . 3 ⊢ (𝜑 → 𝑈 ∈ LMod)
8		lclkrlem2m.d	. . . 4 ⊢ 𝐷 = (LDual‘𝑈)
9		lclkrlem2m.p	. . . 4 ⊢ + = (+_g‘𝐷)
10		lclkrlem2m.e	. . . 4 ⊢ (𝜑 → 𝐸 ∈ 𝐹)
11		lclkrlem2m.g	. . . 4 ⊢ (𝜑 → 𝐺 ∈ 𝐹)
12	2, 8, 9, 7, 10, 11	ldualvaddcl 39239	. . 3 ⊢ (𝜑 → (𝐸 + 𝐺) ∈ 𝐹)
13	1, 2, 3, 7, 12	lkrssv 39205	. 2 ⊢ (𝜑 → (𝐿‘(𝐸 + 𝐺)) ⊆ 𝑉)
14		lclkrlem2o.o	. . . 4 ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)
15		eqid 2731	. . . 4 ⊢ (LSubSp‘𝑈) = (LSubSp‘𝑈)
16		lclkrlem2o.a	. . . 4 ⊢ ⊕ = (LSSum‘𝑈)
17		lclkrlem2n.n	. . . . 5 ⊢ 𝑁 = (LSpan‘𝑈)
18		lclkrlem2m.x	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ 𝑉)
19		lclkrlem2m.y	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ 𝑉)
20	1, 15, 17, 7, 18, 19	lspprcl 20911	. . . 4 ⊢ (𝜑 → (𝑁‘{𝑋, 𝑌}) ∈ (LSubSp‘𝑈))
21		eqid 2731	. . . . . 6 ⊢ ((DIsoH‘𝐾)‘𝑊) = ((DIsoH‘𝐾)‘𝑊)
22	4, 5, 1, 17, 21, 6, 18, 19	dihprrn 41535	. . . . 5 ⊢ (𝜑 → (𝑁‘{𝑋, 𝑌}) ∈ ran ((DIsoH‘𝐾)‘𝑊))
23	1, 15	lssss 20869	. . . . . . 7 ⊢ ((𝑁‘{𝑋, 𝑌}) ∈ (LSubSp‘𝑈) → (𝑁‘{𝑋, 𝑌}) ⊆ 𝑉)
24	20, 23	syl 17	. . . . . 6 ⊢ (𝜑 → (𝑁‘{𝑋, 𝑌}) ⊆ 𝑉)
25	4, 21, 5, 1, 14, 6, 24	dochoccl 41478	. . . . 5 ⊢ (𝜑 → ((𝑁‘{𝑋, 𝑌}) ∈ ran ((DIsoH‘𝐾)‘𝑊) ↔ ( ⊥ ‘( ⊥ ‘(𝑁‘{𝑋, 𝑌}))) = (𝑁‘{𝑋, 𝑌})))
26	22, 25	mpbid 232	. . . 4 ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘(𝑁‘{𝑋, 𝑌}))) = (𝑁‘{𝑋, 𝑌}))
27	4, 14, 5, 1, 15, 16, 6, 20, 26	dochexmid 41577	. . 3 ⊢ (𝜑 → ((𝑁‘{𝑋, 𝑌}) ⊕ ( ⊥ ‘(𝑁‘{𝑋, 𝑌}))) = 𝑉)
28		lclkrlem2m.t	. . . . 5 ⊢ · = ( ·_𝑠 ‘𝑈)
29		lclkrlem2m.s	. . . . 5 ⊢ 𝑆 = (Scalar‘𝑈)
30		lclkrlem2m.q	. . . . 5 ⊢ × = (._r‘𝑆)
31		lclkrlem2m.z	. . . . 5 ⊢ 0 = (0_g‘𝑆)
32		lclkrlem2m.i	. . . . 5 ⊢ 𝐼 = (inv_r‘𝑆)
33		lclkrlem2m.m	. . . . 5 ⊢ − = (-_g‘𝑈)
34	4, 5, 6	dvhlvec 41218	. . . . 5 ⊢ (𝜑 → 𝑈 ∈ LVec)
35		lclkrlem2v.j	. . . . 5 ⊢ (𝜑 → ((𝐸 + 𝐺)‘𝑋) = 0 )
36		lclkrlem2v.k	. . . . 5 ⊢ (𝜑 → ((𝐸 + 𝐺)‘𝑌) = 0 )
37	1, 28, 29, 30, 31, 32, 33, 2, 8, 9, 18, 19, 10, 11, 17, 3, 34, 35, 36	lclkrlem2n 41629	. . . 4 ⊢ (𝜑 → (𝑁‘{𝑋, 𝑌}) ⊆ (𝐿‘(𝐸 + 𝐺)))
38	18	snssd 4758	. . . . . . 7 ⊢ (𝜑 → {𝑋} ⊆ 𝑉)
39	19	snssd 4758	. . . . . . 7 ⊢ (𝜑 → {𝑌} ⊆ 𝑉)
40	4, 5, 1, 14	dochdmj1 41499	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ {𝑋} ⊆ 𝑉 ∧ {𝑌} ⊆ 𝑉) → ( ⊥ ‘({𝑋} ∪ {𝑌})) = (( ⊥ ‘{𝑋}) ∩ ( ⊥ ‘{𝑌})))
41	6, 38, 39, 40	syl3anc 1373	. . . . . 6 ⊢ (𝜑 → ( ⊥ ‘({𝑋} ∪ {𝑌})) = (( ⊥ ‘{𝑋}) ∩ ( ⊥ ‘{𝑌})))
42		df-pr 4576	. . . . . . . . 9 ⊢ {𝑋, 𝑌} = ({𝑋} ∪ {𝑌})
43	42	fveq2i 6825	. . . . . . . 8 ⊢ (𝑁‘{𝑋, 𝑌}) = (𝑁‘({𝑋} ∪ {𝑌}))
44	43	fveq2i 6825	. . . . . . 7 ⊢ ( ⊥ ‘(𝑁‘{𝑋, 𝑌})) = ( ⊥ ‘(𝑁‘({𝑋} ∪ {𝑌})))
45	38, 39	unssd 4139	. . . . . . . 8 ⊢ (𝜑 → ({𝑋} ∪ {𝑌}) ⊆ 𝑉)
46	4, 5, 14, 1, 17, 6, 45	dochocsp 41488	. . . . . . 7 ⊢ (𝜑 → ( ⊥ ‘(𝑁‘({𝑋} ∪ {𝑌}))) = ( ⊥ ‘({𝑋} ∪ {𝑌})))
47	44, 46	eqtrid 2778	. . . . . 6 ⊢ (𝜑 → ( ⊥ ‘(𝑁‘{𝑋, 𝑌})) = ( ⊥ ‘({𝑋} ∪ {𝑌})))
48		lclkrlem2q.le	. . . . . . 7 ⊢ (𝜑 → (𝐿‘𝐸) = ( ⊥ ‘{𝑋}))
49		lclkrlem2q.lg	. . . . . . 7 ⊢ (𝜑 → (𝐿‘𝐺) = ( ⊥ ‘{𝑌}))
50	48, 49	ineq12d 4168	. . . . . 6 ⊢ (𝜑 → ((𝐿‘𝐸) ∩ (𝐿‘𝐺)) = (( ⊥ ‘{𝑋}) ∩ ( ⊥ ‘{𝑌})))
51	41, 47, 50	3eqtr4d 2776	. . . . 5 ⊢ (𝜑 → ( ⊥ ‘(𝑁‘{𝑋, 𝑌})) = ((𝐿‘𝐸) ∩ (𝐿‘𝐺)))
52	2, 3, 8, 9, 7, 10, 11	lkrin 39273	. . . . 5 ⊢ (𝜑 → ((𝐿‘𝐸) ∩ (𝐿‘𝐺)) ⊆ (𝐿‘(𝐸 + 𝐺)))
53	51, 52	eqsstrd 3964	. . . 4 ⊢ (𝜑 → ( ⊥ ‘(𝑁‘{𝑋, 𝑌})) ⊆ (𝐿‘(𝐸 + 𝐺)))
54	15	lsssssubg 20891	. . . . . . 7 ⊢ (𝑈 ∈ LMod → (LSubSp‘𝑈) ⊆ (SubGrp‘𝑈))
55	7, 54	syl 17	. . . . . 6 ⊢ (𝜑 → (LSubSp‘𝑈) ⊆ (SubGrp‘𝑈))
56	55, 20	sseldd 3930	. . . . 5 ⊢ (𝜑 → (𝑁‘{𝑋, 𝑌}) ∈ (SubGrp‘𝑈))
57	4, 5, 1, 15, 14	dochlss 41463	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑁‘{𝑋, 𝑌}) ⊆ 𝑉) → ( ⊥ ‘(𝑁‘{𝑋, 𝑌})) ∈ (LSubSp‘𝑈))
58	6, 24, 57	syl2anc 584	. . . . . 6 ⊢ (𝜑 → ( ⊥ ‘(𝑁‘{𝑋, 𝑌})) ∈ (LSubSp‘𝑈))
59	55, 58	sseldd 3930	. . . . 5 ⊢ (𝜑 → ( ⊥ ‘(𝑁‘{𝑋, 𝑌})) ∈ (SubGrp‘𝑈))
60	2, 3, 15	lkrlss 39204	. . . . . . 7 ⊢ ((𝑈 ∈ LMod ∧ (𝐸 + 𝐺) ∈ 𝐹) → (𝐿‘(𝐸 + 𝐺)) ∈ (LSubSp‘𝑈))
61	7, 12, 60	syl2anc 584	. . . . . 6 ⊢ (𝜑 → (𝐿‘(𝐸 + 𝐺)) ∈ (LSubSp‘𝑈))
62	55, 61	sseldd 3930	. . . . 5 ⊢ (𝜑 → (𝐿‘(𝐸 + 𝐺)) ∈ (SubGrp‘𝑈))
63	16	lsmlub 19576	. . . . 5 ⊢ (((𝑁‘{𝑋, 𝑌}) ∈ (SubGrp‘𝑈) ∧ ( ⊥ ‘(𝑁‘{𝑋, 𝑌})) ∈ (SubGrp‘𝑈) ∧ (𝐿‘(𝐸 + 𝐺)) ∈ (SubGrp‘𝑈)) → (((𝑁‘{𝑋, 𝑌}) ⊆ (𝐿‘(𝐸 + 𝐺)) ∧ ( ⊥ ‘(𝑁‘{𝑋, 𝑌})) ⊆ (𝐿‘(𝐸 + 𝐺))) ↔ ((𝑁‘{𝑋, 𝑌}) ⊕ ( ⊥ ‘(𝑁‘{𝑋, 𝑌}))) ⊆ (𝐿‘(𝐸 + 𝐺))))
64	56, 59, 62, 63	syl3anc 1373	. . . 4 ⊢ (𝜑 → (((𝑁‘{𝑋, 𝑌}) ⊆ (𝐿‘(𝐸 + 𝐺)) ∧ ( ⊥ ‘(𝑁‘{𝑋, 𝑌})) ⊆ (𝐿‘(𝐸 + 𝐺))) ↔ ((𝑁‘{𝑋, 𝑌}) ⊕ ( ⊥ ‘(𝑁‘{𝑋, 𝑌}))) ⊆ (𝐿‘(𝐸 + 𝐺))))
65	37, 53, 64	mpbi2and 712	. . 3 ⊢ (𝜑 → ((𝑁‘{𝑋, 𝑌}) ⊕ ( ⊥ ‘(𝑁‘{𝑋, 𝑌}))) ⊆ (𝐿‘(𝐸 + 𝐺)))
66	27, 65	eqsstrrd 3965	. 2 ⊢ (𝜑 → 𝑉 ⊆ (𝐿‘(𝐸 + 𝐺)))
67	13, 66	eqssd 3947	1 ⊢ (𝜑 → (𝐿‘(𝐸 + 𝐺)) = 𝑉)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1541 ∈ wcel 2111 ∪ cun 3895 ∩ cin 3896 ⊆ wss 3897 {csn 4573 {cpr 4575 ran crn 5615 ‘cfv 6481 (class class class)co 7346 Basecbs 17120 +_gcplusg 17161 ._rcmulr 17162 Scalarcsca 17164 ·_𝑠 cvsca 17165 0_gc0g 17343 -_gcsg 18848 SubGrpcsubg 19033 LSSumclsm 19546 inv_rcinvr 20305 LModclmod 20793 LSubSpclss 20864 LSpanclspn 20904 LFnlclfn 39166 LKerclk 39194 LDualcld 39232 HLchlt 39459 LHypclh 40093 DVecHcdvh 41187 DIsoHcdih 41337 ocHcoch 41456

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 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-rep 5215 ax-sep 5232 ax-nul 5242 ax-pow 5301 ax-pr 5368 ax-un 7668 ax-cnex 11062 ax-resscn 11063 ax-1cn 11064 ax-icn 11065 ax-addcl 11066 ax-addrcl 11067 ax-mulcl 11068 ax-mulrcl 11069 ax-mulcom 11070 ax-addass 11071 ax-mulass 11072 ax-distr 11073 ax-i2m1 11074 ax-1ne0 11075 ax-1rid 11076 ax-rnegex 11077 ax-rrecex 11078 ax-cnre 11079 ax-pre-lttri 11080 ax-pre-lttrn 11081 ax-pre-ltadd 11082 ax-pre-mulgt0 11083 ax-riotaBAD 39062

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 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-rmo 3346 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3737 df-csb 3846 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-pss 3917 df-nul 4281 df-if 4473 df-pw 4549 df-sn 4574 df-pr 4576 df-tp 4578 df-op 4580 df-uni 4857 df-int 4896 df-iun 4941 df-iin 4942 df-br 5090 df-opab 5152 df-mpt 5171 df-tr 5197 df-id 5509 df-eprel 5514 df-po 5522 df-so 5523 df-fr 5567 df-we 5569 df-xp 5620 df-rel 5621 df-cnv 5622 df-co 5623 df-dm 5624 df-rn 5625 df-res 5626 df-ima 5627 df-pred 6248 df-ord 6309 df-on 6310 df-lim 6311 df-suc 6312 df-iota 6437 df-fun 6483 df-fn 6484 df-f 6485 df-f1 6486 df-fo 6487 df-f1o 6488 df-fv 6489 df-riota 7303 df-ov 7349 df-oprab 7350 df-mpo 7351 df-of 7610 df-om 7797 df-1st 7921 df-2nd 7922 df-tpos 8156 df-undef 8203 df-frecs 8211 df-wrecs 8242 df-recs 8291 df-rdg 8329 df-1o 8385 df-2o 8386 df-er 8622 df-map 8752 df-en 8870 df-dom 8871 df-sdom 8872 df-fin 8873 df-pnf 11148 df-mnf 11149 df-xr 11150 df-ltxr 11151 df-le 11152 df-sub 11346 df-neg 11347 df-nn 12126 df-2 12188 df-3 12189 df-4 12190 df-5 12191 df-6 12192 df-n0 12382 df-z 12469 df-uz 12733 df-fz 13408 df-struct 17058 df-sets 17075 df-slot 17093 df-ndx 17105 df-base 17121 df-ress 17142 df-plusg 17174 df-mulr 17175 df-sca 17177 df-vsca 17178 df-0g 17345 df-mre 17488 df-mrc 17489 df-acs 17491 df-proset 18200 df-poset 18219 df-plt 18234 df-lub 18250 df-glb 18251 df-join 18252 df-meet 18253 df-p0 18329 df-p1 18330 df-lat 18338 df-clat 18405 df-mgm 18548 df-sgrp 18627 df-mnd 18643 df-submnd 18692 df-grp 18849 df-minusg 18850 df-sbg 18851 df-subg 19036 df-cntz 19229 df-oppg 19258 df-lsm 19548 df-cmn 19694 df-abl 19695 df-mgp 20059 df-rng 20071 df-ur 20100 df-ring 20153 df-oppr 20255 df-dvdsr 20275 df-unit 20276 df-invr 20306 df-dvr 20319 df-drng 20646 df-lmod 20795 df-lss 20865 df-lsp 20905 df-lvec 21037 df-lsatoms 39085 df-lcv 39128 df-lfl 39167 df-lkr 39195 df-ldual 39233 df-oposet 39285 df-ol 39287 df-oml 39288 df-covers 39375 df-ats 39376 df-atl 39407 df-cvlat 39431 df-hlat 39460 df-llines 39607 df-lplanes 39608 df-lvols 39609 df-lines 39610 df-psubsp 39612 df-pmap 39613 df-padd 39905 df-lhyp 40097 df-laut 40098 df-ldil 40213 df-ltrn 40214 df-trl 40268 df-tgrp 40852 df-tendo 40864 df-edring 40866 df-dveca 41112 df-disoa 41138 df-dvech 41188 df-dib 41248 df-dic 41282 df-dih 41338 df-doch 41457 df-djh 41504

This theorem is referenced by: lclkrlem2w 41638

W3C validator