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 39733

Description: A closed subspace sum equals subspace join. (shjshseli 30142 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 482	. . . . 5 ⊢ ((𝜑 ∧ (𝑋 ⊕ 𝑌) ∈ ran 𝐼) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
3		djhlsmcl.x	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ 𝑆)
4		djhlsmcl.v	. . . . . . . 8 ⊢ 𝑉 = (Base‘𝑈)
5		djhlsmcl.s	. . . . . . . 8 ⊢ 𝑆 = (LSubSp‘𝑈)
6	4, 5	lssss 20303	. . . . . . 7 ⊢ (𝑋 ∈ 𝑆 → 𝑋 ⊆ 𝑉)
7	3, 6	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑋 ⊆ 𝑉)
8	7	adantr 482	. . . . 5 ⊢ ((𝜑 ∧ (𝑋 ⊕ 𝑌) ∈ ran 𝐼) → 𝑋 ⊆ 𝑉)
9		djhlsmcl.y	. . . . . . 7 ⊢ (𝜑 → 𝑌 ∈ 𝑆)
10	4, 5	lssss 20303	. . . . . . 7 ⊢ (𝑌 ∈ 𝑆 → 𝑌 ⊆ 𝑉)
11	9, 10	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑌 ⊆ 𝑉)
12	11	adantr 482	. . . . 5 ⊢ ((𝜑 ∧ (𝑋 ⊕ 𝑌) ∈ ran 𝐼) → 𝑌 ⊆ 𝑉)
13		djhlsmcl.h	. . . . . 6 ⊢ 𝐻 = (LHyp‘𝐾)
14		djhlsmcl.u	. . . . . 6 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
15		eqid 2737	. . . . . 6 ⊢ ((ocH‘𝐾)‘𝑊) = ((ocH‘𝐾)‘𝑊)
16		djhlsmcl.j	. . . . . 6 ⊢ ∨ = ((joinH‘𝐾)‘𝑊)
17	13, 14, 4, 15, 16	djhval2 39718	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉) → (𝑋 ∨ 𝑌) = (((ocH‘𝐾)‘𝑊)‘(((ocH‘𝐾)‘𝑊)‘(𝑋 ∪ 𝑌))))
18	2, 8, 12, 17	syl3anc 1371	. . . 4 ⊢ ((𝜑 ∧ (𝑋 ⊕ 𝑌) ∈ ran 𝐼) → (𝑋 ∨ 𝑌) = (((ocH‘𝐾)‘𝑊)‘(((ocH‘𝐾)‘𝑊)‘(𝑋 ∪ 𝑌))))
19	13, 14, 1	dvhlmod 39429	. . . . . . . . 9 ⊢ (𝜑 → 𝑈 ∈ LMod)
20	19	adantr 482	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑋 ⊕ 𝑌) ∈ ran 𝐼) → 𝑈 ∈ LMod)
21	3	adantr 482	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑋 ⊕ 𝑌) ∈ ran 𝐼) → 𝑋 ∈ 𝑆)
22	9	adantr 482	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑋 ⊕ 𝑌) ∈ ran 𝐼) → 𝑌 ∈ 𝑆)
23		eqid 2737	. . . . . . . . 9 ⊢ (LSpan‘𝑈) = (LSpan‘𝑈)
24		djhlsmcl.p	. . . . . . . . 9 ⊢ ⊕ = (LSSum‘𝑈)
25	5, 23, 24	lsmsp 20453	. . . . . . . 8 ⊢ ((𝑈 ∈ LMod ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) → (𝑋 ⊕ 𝑌) = ((LSpan‘𝑈)‘(𝑋 ∪ 𝑌)))
26	20, 21, 22, 25	syl3anc 1371	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑋 ⊕ 𝑌) ∈ ran 𝐼) → (𝑋 ⊕ 𝑌) = ((LSpan‘𝑈)‘(𝑋 ∪ 𝑌)))
27	26	fveq2d 6833	. . . . . 6 ⊢ ((𝜑 ∧ (𝑋 ⊕ 𝑌) ∈ ran 𝐼) → (((ocH‘𝐾)‘𝑊)‘(𝑋 ⊕ 𝑌)) = (((ocH‘𝐾)‘𝑊)‘((LSpan‘𝑈)‘(𝑋 ∪ 𝑌))))
28	7, 11	unssd 4137	. . . . . . . 8 ⊢ (𝜑 → (𝑋 ∪ 𝑌) ⊆ 𝑉)
29	28	adantr 482	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑋 ⊕ 𝑌) ∈ ran 𝐼) → (𝑋 ∪ 𝑌) ⊆ 𝑉)
30	13, 14, 15, 4, 23, 2, 29	dochocsp 39698	. . . . . 6 ⊢ ((𝜑 ∧ (𝑋 ⊕ 𝑌) ∈ ran 𝐼) → (((ocH‘𝐾)‘𝑊)‘((LSpan‘𝑈)‘(𝑋 ∪ 𝑌))) = (((ocH‘𝐾)‘𝑊)‘(𝑋 ∪ 𝑌)))
31	27, 30	eqtrd 2777	. . . . 5 ⊢ ((𝜑 ∧ (𝑋 ⊕ 𝑌) ∈ ran 𝐼) → (((ocH‘𝐾)‘𝑊)‘(𝑋 ⊕ 𝑌)) = (((ocH‘𝐾)‘𝑊)‘(𝑋 ∪ 𝑌)))
32	31	fveq2d 6833	. . . 4 ⊢ ((𝜑 ∧ (𝑋 ⊕ 𝑌) ∈ ran 𝐼) → (((ocH‘𝐾)‘𝑊)‘(((ocH‘𝐾)‘𝑊)‘(𝑋 ⊕ 𝑌))) = (((ocH‘𝐾)‘𝑊)‘(((ocH‘𝐾)‘𝑊)‘(𝑋 ∪ 𝑌))))
33		djhlsmcl.i	. . . . . 6 ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)
34	13, 33, 15	dochoc 39686	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ⊕ 𝑌) ∈ ran 𝐼) → (((ocH‘𝐾)‘𝑊)‘(((ocH‘𝐾)‘𝑊)‘(𝑋 ⊕ 𝑌))) = (𝑋 ⊕ 𝑌))
35	1, 34	sylan 581	. . . 4 ⊢ ((𝜑 ∧ (𝑋 ⊕ 𝑌) ∈ ran 𝐼) → (((ocH‘𝐾)‘𝑊)‘(((ocH‘𝐾)‘𝑊)‘(𝑋 ⊕ 𝑌))) = (𝑋 ⊕ 𝑌))
36	18, 32, 35	3eqtr2rd 2784	. . 3 ⊢ ((𝜑 ∧ (𝑋 ⊕ 𝑌) ∈ ran 𝐼) → (𝑋 ⊕ 𝑌) = (𝑋 ∨ 𝑌))
37	36	ex 414	. 2 ⊢ (𝜑 → ((𝑋 ⊕ 𝑌) ∈ ran 𝐼 → (𝑋 ⊕ 𝑌) = (𝑋 ∨ 𝑌)))
38	13, 33, 14, 4, 16	djhcl 39719	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉)) → (𝑋 ∨ 𝑌) ∈ ran 𝐼)
39	1, 7, 11, 38	syl12anc 835	. . 3 ⊢ (𝜑 → (𝑋 ∨ 𝑌) ∈ ran 𝐼)
40		eleq1a 2833	. . 3 ⊢ ((𝑋 ∨ 𝑌) ∈ ran 𝐼 → ((𝑋 ⊕ 𝑌) = (𝑋 ∨ 𝑌) → (𝑋 ⊕ 𝑌) ∈ ran 𝐼))
41	39, 40	syl 17	. 2 ⊢ (𝜑 → ((𝑋 ⊕ 𝑌) = (𝑋 ∨ 𝑌) → (𝑋 ⊕ 𝑌) ∈ ran 𝐼))
42	37, 41	impbid 211	1 ⊢ (𝜑 → ((𝑋 ⊕ 𝑌) ∈ ran 𝐼 ↔ (𝑋 ⊕ 𝑌) = (𝑋 ∨ 𝑌)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 = wceq 1541 ∈ wcel 2106 ∪ cun 3899 ⊆ wss 3901 ran crn 5625 ‘cfv 6483 (class class class)co 7341 Basecbs 17009 LSSumclsm 19335 LModclmod 20228 LSubSpclss 20298 LSpanclspn 20338 HLchlt 37668 LHypclh 38303 DVecHcdvh 39397 DIsoHcdih 39547 ocHcoch 39666 joinHcdjh 39713

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2708 ax-rep 5233 ax-sep 5247 ax-nul 5254 ax-pow 5312 ax-pr 5376 ax-un 7654 ax-cnex 11032 ax-resscn 11033 ax-1cn 11034 ax-icn 11035 ax-addcl 11036 ax-addrcl 11037 ax-mulcl 11038 ax-mulrcl 11039 ax-mulcom 11040 ax-addass 11041 ax-mulass 11042 ax-distr 11043 ax-i2m1 11044 ax-1ne0 11045 ax-1rid 11046 ax-rnegex 11047 ax-rrecex 11048 ax-cnre 11049 ax-pre-lttri 11050 ax-pre-lttrn 11051 ax-pre-ltadd 11052 ax-pre-mulgt0 11053 ax-riotaBAD 37271

This theorem depends on definitions: df-bi 206 df-an 398 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2815 df-nfc 2887 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rmo 3350 df-reu 3351 df-rab 3405 df-v 3444 df-sbc 3731 df-csb 3847 df-dif 3904 df-un 3906 df-in 3908 df-ss 3918 df-pss 3920 df-nul 4274 df-if 4478 df-pw 4553 df-sn 4578 df-pr 4580 df-tp 4582 df-op 4584 df-uni 4857 df-int 4899 df-iun 4947 df-iin 4948 df-br 5097 df-opab 5159 df-mpt 5180 df-tr 5214 df-id 5522 df-eprel 5528 df-po 5536 df-so 5537 df-fr 5579 df-we 5581 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-pred 6242 df-ord 6309 df-on 6310 df-lim 6311 df-suc 6312 df-iota 6435 df-fun 6485 df-fn 6486 df-f 6487 df-f1 6488 df-fo 6489 df-f1o 6490 df-fv 6491 df-riota 7297 df-ov 7344 df-oprab 7345 df-mpo 7346 df-om 7785 df-1st 7903 df-2nd 7904 df-tpos 8116 df-undef 8163 df-frecs 8171 df-wrecs 8202 df-recs 8276 df-rdg 8315 df-1o 8371 df-er 8573 df-map 8692 df-en 8809 df-dom 8810 df-sdom 8811 df-fin 8812 df-pnf 11116 df-mnf 11117 df-xr 11118 df-ltxr 11119 df-le 11120 df-sub 11312 df-neg 11313 df-nn 12079 df-2 12141 df-3 12142 df-4 12143 df-5 12144 df-6 12145 df-n0 12339 df-z 12425 df-uz 12688 df-fz 13345 df-struct 16945 df-sets 16962 df-slot 16980 df-ndx 16992 df-base 17010 df-ress 17039 df-plusg 17072 df-mulr 17073 df-sca 17075 df-vsca 17076 df-0g 17249 df-proset 18110 df-poset 18128 df-plt 18145 df-lub 18161 df-glb 18162 df-join 18163 df-meet 18164 df-p0 18240 df-p1 18241 df-lat 18247 df-clat 18314 df-mgm 18423 df-sgrp 18472 df-mnd 18483 df-submnd 18528 df-grp 18676 df-minusg 18677 df-sbg 18678 df-subg 18848 df-cntz 19019 df-lsm 19337 df-cmn 19483 df-abl 19484 df-mgp 19815 df-ur 19832 df-ring 19879 df-oppr 19956 df-dvdsr 19977 df-unit 19978 df-invr 20008 df-dvr 20019 df-drng 20094 df-lmod 20230 df-lss 20299 df-lsp 20339 df-lvec 20470 df-lsatoms 37294 df-oposet 37494 df-ol 37496 df-oml 37497 df-covers 37584 df-ats 37585 df-atl 37616 df-cvlat 37640 df-hlat 37669 df-llines 37817 df-lplanes 37818 df-lvols 37819 df-lines 37820 df-psubsp 37822 df-pmap 37823 df-padd 38115 df-lhyp 38307 df-laut 38308 df-ldil 38423 df-ltrn 38424 df-trl 38478 df-tendo 39074 df-edring 39076 df-disoa 39348 df-dvech 39398 df-dib 39458 df-dic 39492 df-dih 39548 df-doch 39667 df-djh 39714

This theorem is referenced by: djhlsmat 39746 dihsmatrn 39755 lclkrslem2 39857

W3C validator