Theorem djhlsmcl

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

	Ref	Expression
Hypotheses	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	djhlsmcl	⊢ ( 𝜑 → ( ( 𝑋 ⊕ 𝑌 ) ∈ ran 𝐼 ↔ ( 𝑋 ⊕ 𝑌 ) = ( 𝑋 ∨ 𝑌 ) ) )

Proof

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