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 42149

Description: Lemma for lclkr 42154. When the hypotheses of lclkrlem2u 42148 and lclkrlem2u 42148 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 42089, which requires the orthomodular law dihoml4 41998 (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 41731	. . 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 39751	. . 3 ⊢ (𝜑 → (𝐸 + 𝐺) ∈ 𝐹)
13	1, 2, 3, 7, 12	lkrssv 39717	. 2 ⊢ (𝜑 → (𝐿‘(𝐸 + 𝐺)) ⊆ 𝑉)
14		lclkrlem2o.o	. . . 4 ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)
15		eqid 2762	. . . 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 21042	. . . 4 ⊢ (𝜑 → (𝑁‘{𝑋, 𝑌}) ∈ (LSubSp‘𝑈))
21		eqid 2762	. . . . . 6 ⊢ ((DIsoH‘𝐾)‘𝑊) = ((DIsoH‘𝐾)‘𝑊)
22	4, 5, 1, 17, 21, 6, 18, 19	dihprrn 42047	. . . . 5 ⊢ (𝜑 → (𝑁‘{𝑋, 𝑌}) ∈ ran ((DIsoH‘𝐾)‘𝑊))
23	1, 15	lssss 21000	. . . . . . 7 ⊢ ((𝑁‘{𝑋, 𝑌}) ∈ (LSubSp‘𝑈) → (𝑁‘{𝑋, 𝑌}) ⊆ 𝑉)
24	20, 23	syl 17	. . . . . 6 ⊢ (𝜑 → (𝑁‘{𝑋, 𝑌}) ⊆ 𝑉)
25	4, 21, 5, 1, 14, 6, 24	dochoccl 41990	. . . . 5 ⊢ (𝜑 → ((𝑁‘{𝑋, 𝑌}) ∈ ran ((DIsoH‘𝐾)‘𝑊) ↔ ( ⊥ ‘( ⊥ ‘(𝑁‘{𝑋, 𝑌}))) = (𝑁‘{𝑋, 𝑌})))
26	22, 25	mpbid 234	. . . 4 ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘(𝑁‘{𝑋, 𝑌}))) = (𝑁‘{𝑋, 𝑌}))
27	4, 14, 5, 1, 15, 16, 6, 20, 26	dochexmid 42089	. . 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 41730	. . . . 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 42141	. . . 4 ⊢ (𝜑 → (𝑁‘{𝑋, 𝑌}) ⊆ (𝐿‘(𝐸 + 𝐺)))
38	18	snssd 4745	. . . . . . 7 ⊢ (𝜑 → {𝑋} ⊆ 𝑉)
39	19	snssd 4745	. . . . . . 7 ⊢ (𝜑 → {𝑌} ⊆ 𝑉)
40	4, 5, 1, 14	dochdmj1 42011	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ {𝑋} ⊆ 𝑉 ∧ {𝑌} ⊆ 𝑉) → ( ⊥ ‘({𝑋} ∪ {𝑌})) = (( ⊥ ‘{𝑋}) ∩ ( ⊥ ‘{𝑌})))
41	6, 38, 39, 40	syl3anc 1390	. . . . . 6 ⊢ (𝜑 → ( ⊥ ‘({𝑋} ∪ {𝑌})) = (( ⊥ ‘{𝑋}) ∩ ( ⊥ ‘{𝑌})))
42		df-pr 4585	. . . . . . . . 9 ⊢ {𝑋, 𝑌} = ({𝑋} ∪ {𝑌})
43	42	fveq2i 6870	. . . . . . . 8 ⊢ (𝑁‘{𝑋, 𝑌}) = (𝑁‘({𝑋} ∪ {𝑌}))
44	43	fveq2i 6870	. . . . . . 7 ⊢ ( ⊥ ‘(𝑁‘{𝑋, 𝑌})) = ( ⊥ ‘(𝑁‘({𝑋} ∪ {𝑌})))
45	38, 39	unssd 4144	. . . . . . . 8 ⊢ (𝜑 → ({𝑋} ∪ {𝑌}) ⊆ 𝑉)
46	4, 5, 14, 1, 17, 6, 45	dochocsp 42000	. . . . . . 7 ⊢ (𝜑 → ( ⊥ ‘(𝑁‘({𝑋} ∪ {𝑌}))) = ( ⊥ ‘({𝑋} ∪ {𝑌})))
47	44, 46	eqtrid 2809	. . . . . 6 ⊢ (𝜑 → ( ⊥ ‘(𝑁‘{𝑋, 𝑌})) = ( ⊥ ‘({𝑋} ∪ {𝑌})))
48		lclkrlem2q.le	. . . . . . 7 ⊢ (𝜑 → (𝐿‘𝐸) = ( ⊥ ‘{𝑋}))
49		lclkrlem2q.lg	. . . . . . 7 ⊢ (𝜑 → (𝐿‘𝐺) = ( ⊥ ‘{𝑌}))
50	48, 49	ineq12d 4173	. . . . . 6 ⊢ (𝜑 → ((𝐿‘𝐸) ∩ (𝐿‘𝐺)) = (( ⊥ ‘{𝑋}) ∩ ( ⊥ ‘{𝑌})))
51	41, 47, 50	3eqtr4d 2807	. . . . 5 ⊢ (𝜑 → ( ⊥ ‘(𝑁‘{𝑋, 𝑌})) = ((𝐿‘𝐸) ∩ (𝐿‘𝐺)))
52	2, 3, 8, 9, 7, 10, 11	lkrin 39785	. . . . 5 ⊢ (𝜑 → ((𝐿‘𝐸) ∩ (𝐿‘𝐺)) ⊆ (𝐿‘(𝐸 + 𝐺)))
53	51, 52	eqsstrd 3970	. . . 4 ⊢ (𝜑 → ( ⊥ ‘(𝑁‘{𝑋, 𝑌})) ⊆ (𝐿‘(𝐸 + 𝐺)))
54	15	lsssssubg 21022	. . . . . . 7 ⊢ (𝑈 ∈ LMod → (LSubSp‘𝑈) ⊆ (SubGrp‘𝑈))
55	7, 54	syl 17	. . . . . 6 ⊢ (𝜑 → (LSubSp‘𝑈) ⊆ (SubGrp‘𝑈))
56	55, 20	sseldd 3937	. . . . 5 ⊢ (𝜑 → (𝑁‘{𝑋, 𝑌}) ∈ (SubGrp‘𝑈))
57	4, 5, 1, 15, 14	dochlss 41975	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑁‘{𝑋, 𝑌}) ⊆ 𝑉) → ( ⊥ ‘(𝑁‘{𝑋, 𝑌})) ∈ (LSubSp‘𝑈))
58	6, 24, 57	syl2anc 593	. . . . . 6 ⊢ (𝜑 → ( ⊥ ‘(𝑁‘{𝑋, 𝑌})) ∈ (LSubSp‘𝑈))
59	55, 58	sseldd 3937	. . . . 5 ⊢ (𝜑 → ( ⊥ ‘(𝑁‘{𝑋, 𝑌})) ∈ (SubGrp‘𝑈))
60	2, 3, 15	lkrlss 39716	. . . . . . 7 ⊢ ((𝑈 ∈ LMod ∧ (𝐸 + 𝐺) ∈ 𝐹) → (𝐿‘(𝐸 + 𝐺)) ∈ (LSubSp‘𝑈))
61	7, 12, 60	syl2anc 593	. . . . . 6 ⊢ (𝜑 → (𝐿‘(𝐸 + 𝐺)) ∈ (LSubSp‘𝑈))
62	55, 61	sseldd 3937	. . . . 5 ⊢ (𝜑 → (𝐿‘(𝐸 + 𝐺)) ∈ (SubGrp‘𝑈))
63	16	lsmlub 19704	. . . . 5 ⊢ (((𝑁‘{𝑋, 𝑌}) ∈ (SubGrp‘𝑈) ∧ ( ⊥ ‘(𝑁‘{𝑋, 𝑌})) ∈ (SubGrp‘𝑈) ∧ (𝐿‘(𝐸 + 𝐺)) ∈ (SubGrp‘𝑈)) → (((𝑁‘{𝑋, 𝑌}) ⊆ (𝐿‘(𝐸 + 𝐺)) ∧ ( ⊥ ‘(𝑁‘{𝑋, 𝑌})) ⊆ (𝐿‘(𝐸 + 𝐺))) ↔ ((𝑁‘{𝑋, 𝑌}) ⊕ ( ⊥ ‘(𝑁‘{𝑋, 𝑌}))) ⊆ (𝐿‘(𝐸 + 𝐺))))
64	56, 59, 62, 63	syl3anc 1390	. . . 4 ⊢ (𝜑 → (((𝑁‘{𝑋, 𝑌}) ⊆ (𝐿‘(𝐸 + 𝐺)) ∧ ( ⊥ ‘(𝑁‘{𝑋, 𝑌})) ⊆ (𝐿‘(𝐸 + 𝐺))) ↔ ((𝑁‘{𝑋, 𝑌}) ⊕ ( ⊥ ‘(𝑁‘{𝑋, 𝑌}))) ⊆ (𝐿‘(𝐸 + 𝐺))))
65	37, 53, 64	mpbi2and 722	. . 3 ⊢ (𝜑 → ((𝑁‘{𝑋, 𝑌}) ⊕ ( ⊥ ‘(𝑁‘{𝑋, 𝑌}))) ⊆ (𝐿‘(𝐸 + 𝐺)))
66	27, 65	eqsstrrd 3971	. 2 ⊢ (𝜑 → 𝑉 ⊆ (𝐿‘(𝐸 + 𝐺)))
67	13, 66	eqssd 3953	1 ⊢ (𝜑 → (𝐿‘(𝐸 + 𝐺)) = 𝑉)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 399 = wceq 1560 ∈ wcel 2142 ∪ cun 3902 ∩ cin 3903 ⊆ wss 3904 {csn 4582 {cpr 4584 ran crn 5648 ‘cfv 6521 (class class class)co 7396 Basecbs 17245 +_gcplusg 17286 ._rcmulr 17287 Scalarcsca 17289 ·_𝑠 cvsca 17290 0_gc0g 17468 -_gcsg 18977 SubGrpcsubg 19162 LSSumclsm 19674 inv_rcinvr 20432 LModclmod 20924 LSubSpclss 20995 LSpanclspn 21035 LFnlclfn 39678 LKerclk 39706 LDualcld 39744 HLchlt 39971 LHypclh 40605 DVecHcdvh 41699 DIsoHcdih 41849 ocHcoch 41968

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1815 ax-4 1829 ax-5 1930 ax-6 1987 ax-7 2028 ax-8 2144 ax-9 2152 ax-10 2175 ax-11 2191 ax-12 2212 ax-ext 2734 ax-rep 5227 ax-sep 5246 ax-nul 5256 ax-pow 5322 ax-pr 5390 ax-un 7718 ax-cnex 11129 ax-resscn 11130 ax-1cn 11131 ax-icn 11132 ax-addcl 11133 ax-addrcl 11134 ax-mulcl 11135 ax-mulrcl 11136 ax-mulcom 11137 ax-addass 11138 ax-mulass 11139 ax-distr 11140 ax-i2m1 11141 ax-1ne0 11142 ax-1rid 11143 ax-rnegex 11144 ax-rrecex 11145 ax-cnre 11146 ax-pre-lttri 11147 ax-pre-lttrn 11148 ax-pre-ltadd 11149 ax-pre-mulgt0 11150 ax-riotaBAD 39574

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1099 df-3an 1100 df-tru 1563 df-fal 1573 df-ex 1800 df-nf 1804 df-sb 2091 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3456 df-sbc 3745 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4481 df-pw 4557 df-sn 4583 df-pr 4585 df-tp 4587 df-op 4589 df-uni 4866 df-int 4906 df-iun 4951 df-iin 4952 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5542 df-eprel 5547 df-po 5555 df-so 5556 df-fr 5600 df-we 5602 df-xp 5653 df-rel 5654 df-cnv 5655 df-co 5656 df-dm 5657 df-rn 5658 df-res 5659 df-ima 5660 df-pred 6288 df-ord 6349 df-on 6350 df-lim 6351 df-suc 6352 df-iota 6477 df-fun 6523 df-fn 6524 df-f 6525 df-f1 6526 df-fo 6527 df-f1o 6528 df-fv 6529 df-riota 7353 df-ov 7399 df-oprab 7400 df-mpo 7401 df-of 7660 df-om 7847 df-1st 7970 df-2nd 7971 df-tpos 8206 df-undef 8253 df-frecs 8262 df-wrecs 8293 df-recs 8342 df-rdg 8381 df-1o 8437 df-2o 8438 df-er 8678 df-map 8810 df-en 8928 df-dom 8929 df-sdom 8930 df-fin 8931 df-pnf 11218 df-mnf 11219 df-xr 11220 df-ltxr 11221 df-le 11222 df-sub 11416 df-neg 11417 df-nn 12211 df-2 12280 df-3 12281 df-4 12282 df-5 12283 df-6 12284 df-n0 12482 df-z 12569 df-uz 12840 df-fz 13513 df-struct 17183 df-sets 17200 df-slot 17218 df-ndx 17230 df-base 17246 df-ress 17267 df-plusg 17299 df-mulr 17300 df-sca 17302 df-vsca 17303 df-0g 17470 df-mre 17614 df-mrc 17615 df-acs 17617 df-proset 18326 df-poset 18345 df-plt 18360 df-lub 18376 df-glb 18377 df-join 18378 df-meet 18379 df-p0 18455 df-p1 18456 df-lat 18464 df-clat 18531 df-mgm 18674 df-sgrp 18753 df-mnd 18769 df-submnd 18818 df-grp 18978 df-minusg 18979 df-sbg 18980 df-subg 19165 df-cntz 19357 df-oppg 19386 df-lsm 19676 df-cmn 19822 df-abl 19823 df-mgp 20187 df-rng 20199 df-ur 20228 df-ring 20281 df-oppr 20382 df-dvdsr 20402 df-unit 20403 df-invr 20433 df-dvr 20446 df-drng 20777 df-lmod 20926 df-lss 20996 df-lsp 21036 df-lvec 21167 df-lsatoms 39597 df-lcv 39640 df-lfl 39679 df-lkr 39707 df-ldual 39745 df-oposet 39797 df-ol 39799 df-oml 39800 df-covers 39887 df-ats 39888 df-atl 39919 df-cvlat 39943 df-hlat 39972 df-llines 40119 df-lplanes 40120 df-lvols 40121 df-lines 40122 df-psubsp 40124 df-pmap 40125 df-padd 40417 df-lhyp 40609 df-laut 40610 df-ldil 40725 df-ltrn 40726 df-trl 40780 df-tgrp 41364 df-tendo 41376 df-edring 41378 df-dveca 41624 df-disoa 41650 df-dvech 41700 df-dib 41760 df-dic 41794 df-dih 41850 df-doch 41969 df-djh 42016

This theorem is referenced by: lclkrlem2w 42150

W3C validator