djhlsmcl - Mathbox for Norm Megill

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

Theorem djhlsmcl 42113

Description: A closed subspace sum equals subspace join. (shjshseli 31786 analog.) (Contributed by NM, 13-Aug-2014.)

**Hypotheses**
Ref	Expression
djhlsmcl.h	⊢ 𝐻 = (LHyp‘𝐾)
djhlsmcl.u	⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
djhlsmcl.v	⊢ 𝑉 = (Base‘𝑈)
djhlsmcl.s	⊢ 𝑆 = (LSubSp‘𝑈)
djhlsmcl.p	⊢ ⊕ = (LSSum‘𝑈)
djhlsmcl.i	⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)
djhlsmcl.j	⊢ ∨ = ((joinH‘𝐾)‘𝑊)
djhlsmcl.k	⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
djhlsmcl.x	⊢ (𝜑 → 𝑋 ∈ 𝑆)
djhlsmcl.y	⊢ (𝜑 → 𝑌 ∈ 𝑆)

**Assertion**
Ref	Expression
djhlsmcl	⊢ (𝜑 → ((𝑋 ⊕ 𝑌) ∈ ran 𝐼 ↔ (𝑋 ⊕ 𝑌) = (𝑋 ∨ 𝑌)))

**Proof of Theorem djhlsmcl**
Step	Hyp	Ref	Expression
1		djhlsmcl.k	. . . . . 6 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
2	1	adantr 485	. . . . 5 ⊢ ((𝜑 ∧ (𝑋 ⊕ 𝑌) ∈ ran 𝐼) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
3		djhlsmcl.x	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ 𝑆)
4		djhlsmcl.v	. . . . . . . 8 ⊢ 𝑉 = (Base‘𝑈)
5		djhlsmcl.s	. . . . . . . 8 ⊢ 𝑆 = (LSubSp‘𝑈)
6	4, 5	lssss 21035	. . . . . . 7 ⊢ (𝑋 ∈ 𝑆 → 𝑋 ⊆ 𝑉)
7	3, 6	syl 18	. . . . . 6 ⊢ (𝜑 → 𝑋 ⊆ 𝑉)
8	7	adantr 485	. . . . 5 ⊢ ((𝜑 ∧ (𝑋 ⊕ 𝑌) ∈ ran 𝐼) → 𝑋 ⊆ 𝑉)
9		djhlsmcl.y	. . . . . . 7 ⊢ (𝜑 → 𝑌 ∈ 𝑆)
10	4, 5	lssss 21035	. . . . . . 7 ⊢ (𝑌 ∈ 𝑆 → 𝑌 ⊆ 𝑉)
11	9, 10	syl 18	. . . . . 6 ⊢ (𝜑 → 𝑌 ⊆ 𝑉)
12	11	adantr 485	. . . . 5 ⊢ ((𝜑 ∧ (𝑋 ⊕ 𝑌) ∈ ran 𝐼) → 𝑌 ⊆ 𝑉)
13		djhlsmcl.h	. . . . . 6 ⊢ 𝐻 = (LHyp‘𝐾)
14		djhlsmcl.u	. . . . . 6 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
15		eqid 2769	. . . . . 6 ⊢ ((ocH‘𝐾)‘𝑊) = ((ocH‘𝐾)‘𝑊)
16		djhlsmcl.j	. . . . . 6 ⊢ ∨ = ((joinH‘𝐾)‘𝑊)
17	13, 14, 4, 15, 16	djhval2 42098	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉) → (𝑋 ∨ 𝑌) = (((ocH‘𝐾)‘𝑊)‘(((ocH‘𝐾)‘𝑊)‘(𝑋 ∪ 𝑌))))
18	2, 8, 12, 17	syl3anc 1396	. . . 4 ⊢ ((𝜑 ∧ (𝑋 ⊕ 𝑌) ∈ ran 𝐼) → (𝑋 ∨ 𝑌) = (((ocH‘𝐾)‘𝑊)‘(((ocH‘𝐾)‘𝑊)‘(𝑋 ∪ 𝑌))))
19	13, 14, 1	dvhlmod 41809	. . . . . . . . 9 ⊢ (𝜑 → 𝑈 ∈ LMod)
20	19	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑋 ⊕ 𝑌) ∈ ran 𝐼) → 𝑈 ∈ LMod)
21	3	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑋 ⊕ 𝑌) ∈ ran 𝐼) → 𝑋 ∈ 𝑆)
22	9	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑋 ⊕ 𝑌) ∈ ran 𝐼) → 𝑌 ∈ 𝑆)
23		eqid 2769	. . . . . . . . 9 ⊢ (LSpan‘𝑈) = (LSpan‘𝑈)
24		djhlsmcl.p	. . . . . . . . 9 ⊢ ⊕ = (LSSum‘𝑈)
25	5, 23, 24	lsmsp 21185	. . . . . . . 8 ⊢ ((𝑈 ∈ LMod ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) → (𝑋 ⊕ 𝑌) = ((LSpan‘𝑈)‘(𝑋 ∪ 𝑌)))
26	20, 21, 22, 25	syl3anc 1396	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑋 ⊕ 𝑌) ∈ ran 𝐼) → (𝑋 ⊕ 𝑌) = ((LSpan‘𝑈)‘(𝑋 ∪ 𝑌)))
27	26	fveq2d 6886	. . . . . 6 ⊢ ((𝜑 ∧ (𝑋 ⊕ 𝑌) ∈ ran 𝐼) → (((ocH‘𝐾)‘𝑊)‘(𝑋 ⊕ 𝑌)) = (((ocH‘𝐾)‘𝑊)‘((LSpan‘𝑈)‘(𝑋 ∪ 𝑌))))
28	7, 11	unssd 4151	. . . . . . . 8 ⊢ (𝜑 → (𝑋 ∪ 𝑌) ⊆ 𝑉)
29	28	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑋 ⊕ 𝑌) ∈ ran 𝐼) → (𝑋 ∪ 𝑌) ⊆ 𝑉)
30	13, 14, 15, 4, 23, 2, 29	dochocsp 42078	. . . . . 6 ⊢ ((𝜑 ∧ (𝑋 ⊕ 𝑌) ∈ ran 𝐼) → (((ocH‘𝐾)‘𝑊)‘((LSpan‘𝑈)‘(𝑋 ∪ 𝑌))) = (((ocH‘𝐾)‘𝑊)‘(𝑋 ∪ 𝑌)))
31	27, 30	eqtrd 2804	. . . . 5 ⊢ ((𝜑 ∧ (𝑋 ⊕ 𝑌) ∈ ran 𝐼) → (((ocH‘𝐾)‘𝑊)‘(𝑋 ⊕ 𝑌)) = (((ocH‘𝐾)‘𝑊)‘(𝑋 ∪ 𝑌)))
32	31	fveq2d 6886	. . . 4 ⊢ ((𝜑 ∧ (𝑋 ⊕ 𝑌) ∈ ran 𝐼) → (((ocH‘𝐾)‘𝑊)‘(((ocH‘𝐾)‘𝑊)‘(𝑋 ⊕ 𝑌))) = (((ocH‘𝐾)‘𝑊)‘(((ocH‘𝐾)‘𝑊)‘(𝑋 ∪ 𝑌))))
33		djhlsmcl.i	. . . . . 6 ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)
34	13, 33, 15	dochoc 42066	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ⊕ 𝑌) ∈ ran 𝐼) → (((ocH‘𝐾)‘𝑊)‘(((ocH‘𝐾)‘𝑊)‘(𝑋 ⊕ 𝑌))) = (𝑋 ⊕ 𝑌))
35	1, 34	sylan 591	. . . 4 ⊢ ((𝜑 ∧ (𝑋 ⊕ 𝑌) ∈ ran 𝐼) → (((ocH‘𝐾)‘𝑊)‘(((ocH‘𝐾)‘𝑊)‘(𝑋 ⊕ 𝑌))) = (𝑋 ⊕ 𝑌))
36	18, 32, 35	3eqtr2rd 2811	. . 3 ⊢ ((𝜑 ∧ (𝑋 ⊕ 𝑌) ∈ ran 𝐼) → (𝑋 ⊕ 𝑌) = (𝑋 ∨ 𝑌))
37	36	ex 417	. 2 ⊢ (𝜑 → ((𝑋 ⊕ 𝑌) ∈ ran 𝐼 → (𝑋 ⊕ 𝑌) = (𝑋 ∨ 𝑌)))
38	13, 33, 14, 4, 16	djhcl 42099	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉)) → (𝑋 ∨ 𝑌) ∈ ran 𝐼)
39	1, 7, 11, 38	syl12anc 849	. . 3 ⊢ (𝜑 → (𝑋 ∨ 𝑌) ∈ ran 𝐼)
40		eleq1a 2864	. . 3 ⊢ ((𝑋 ∨ 𝑌) ∈ ran 𝐼 → ((𝑋 ⊕ 𝑌) = (𝑋 ∨ 𝑌) → (𝑋 ⊕ 𝑌) ∈ ran 𝐼))
41	39, 40	syl 18	. 2 ⊢ (𝜑 → ((𝑋 ⊕ 𝑌) = (𝑋 ∨ 𝑌) → (𝑋 ⊕ 𝑌) ∈ ran 𝐼))
42	37, 41	impbid 215	1 ⊢ (𝜑 → ((𝑋 ⊕ 𝑌) ∈ ran 𝐼 ↔ (𝑋 ⊕ 𝑌) = (𝑋 ∨ 𝑌)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 400 = wceq 1567 ∈ wcel 2149 ∪ cun 3909 ⊆ wss 3911 ran crn 5663 ‘cfv 6537 (class class class)co 7411 Basecbs 17269 LSSumclsm 19704 LModclmod 20959 LSubSpclss 21030 LSpanclspn 21070 HLchlt 40049 LHypclh 40683 DVecHcdvh 41777 DIsoHcdih 41927 ocHcoch 42046 joinHcdjh 42093

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-rep 5240 ax-sep 5259 ax-nul 5271 ax-pow 5337 ax-pr 5405 ax-un 7733 ax-cnex 11156 ax-resscn 11157 ax-1cn 11158 ax-icn 11159 ax-addcl 11160 ax-addrcl 11161 ax-mulcl 11162 ax-mulrcl 11163 ax-mulcom 11164 ax-addass 11165 ax-mulass 11166 ax-distr 11167 ax-i2m1 11168 ax-1ne0 11169 ax-1rid 11170 ax-rnegex 11171 ax-rrecex 11172 ax-cnre 11173 ax-pre-lttri 11174 ax-pre-lttrn 11175 ax-pre-ltadd 11176 ax-pre-mulgt0 11177 ax-riotaBAD 39652

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-nel 3071 df-ral 3086 df-rex 3096 df-rmo 3375 df-reu 3376 df-rab 3423 df-v 3463 df-sbc 3752 df-csb 3860 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-pss 3931 df-nul 4293 df-if 4491 df-pw 4567 df-sn 4593 df-pr 4595 df-tp 4597 df-op 4599 df-uni 4875 df-int 4915 df-iun 4960 df-iin 4961 df-br 5112 df-opab 5176 df-mpt 5195 df-tr 5221 df-id 5557 df-eprel 5562 df-po 5570 df-so 5571 df-fr 5615 df-we 5617 df-xp 5668 df-rel 5669 df-cnv 5670 df-co 5671 df-dm 5672 df-rn 5673 df-res 5674 df-ima 5675 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7368 df-ov 7414 df-oprab 7415 df-mpo 7416 df-om 7863 df-1st 7986 df-2nd 7987 df-tpos 8222 df-undef 8269 df-frecs 8278 df-wrecs 8309 df-recs 8358 df-rdg 8397 df-1o 8453 df-er 8694 df-map 8826 df-en 8944 df-dom 8945 df-sdom 8946 df-fin 8947 df-pnf 11245 df-mnf 11246 df-xr 11247 df-ltxr 11248 df-le 11249 df-sub 11443 df-neg 11444 df-nn 12234 df-2 12303 df-3 12304 df-4 12305 df-5 12306 df-6 12307 df-n0 12505 df-z 12592 df-uz 12863 df-fz 13536 df-struct 17207 df-sets 17224 df-slot 17242 df-ndx 17254 df-base 17270 df-ress 17291 df-plusg 17323 df-mulr 17324 df-sca 17326 df-vsca 17327 df-0g 17494 df-proset 18350 df-poset 18369 df-plt 18384 df-lub 18400 df-glb 18401 df-join 18402 df-meet 18403 df-p0 18479 df-p1 18480 df-lat 18488 df-clat 18555 df-mgm 18698 df-sgrp 18777 df-mnd 18793 df-submnd 18842 df-grp 19003 df-minusg 19004 df-sbg 19005 df-subg 19189 df-cntz 19387 df-lsm 19706 df-cmn 19852 df-abl 19853 df-mgp 20217 df-rng 20231 df-ur 20264 df-ring 20317 df-oppr 20419 df-dvdsr 20439 df-unit 20440 df-invr 20470 df-dvr 20483 df-drng 20815 df-lmod 20961 df-lss 21031 df-lsp 21071 df-lvec 21202 df-lsatoms 39675 df-oposet 39875 df-ol 39877 df-oml 39878 df-covers 39965 df-ats 39966 df-atl 39997 df-cvlat 40021 df-hlat 40050 df-llines 40197 df-lplanes 40198 df-lvols 40199 df-lines 40200 df-psubsp 40202 df-pmap 40203 df-padd 40495 df-lhyp 40687 df-laut 40688 df-ldil 40803 df-ltrn 40804 df-trl 40858 df-tendo 41454 df-edring 41456 df-disoa 41728 df-dvech 41778 df-dib 41838 df-dic 41872 df-dih 41928 df-doch 42047 df-djh 42094

This theorem is referenced by: djhlsmat 42126 dihsmatrn 42135 lclkrslem2 42237

W3C validator