Theorem djhcl

Description: Closure of subspace join for DVecH vector space. (Contributed by NM, 19-Jul-2014)

	Ref	Expression
Hypotheses	djhcl.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	djhcl.i	⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
	djhcl.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	djhcl.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	djhcl.j	⊢ ∨ = ( ( joinH ‘ 𝐾 ) ‘ 𝑊 )
Assertion	djhcl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉 ) ) → ( 𝑋 ∨ 𝑌 ) ∈ ran 𝐼 )

Proof

Step	Hyp	Ref	Expression
1		djhcl.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		djhcl.i	⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
3		djhcl.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4		djhcl.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
5		djhcl.j	⊢ ∨ = ( ( joinH ‘ 𝐾 ) ‘ 𝑊 )
6		eqid	⊢ ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
7	1 3 4 6 5	djhval	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉 ) ) → ( 𝑋 ∨ 𝑌 ) = ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) ∩ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑌 ) ) ) )
8		inss1	⊢ ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) ∩ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑌 ) ) ⊆ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 )
9	1 2 3 4 6	dochcl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑉 ) → ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) ∈ ran 𝐼 )
10	9	adantrr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉 ) ) → ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) ∈ ran 𝐼 )
11	1 3 2 4	dihrnss	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) ∈ ran 𝐼 ) → ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) ⊆ 𝑉 )
12	10 11	syldan	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉 ) ) → ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) ⊆ 𝑉 )
13	8 12	sstrid	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉 ) ) → ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) ∩ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑌 ) ) ⊆ 𝑉 )
14	1 2 3 4 6	dochcl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) ∩ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑌 ) ) ⊆ 𝑉 ) → ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) ∩ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑌 ) ) ) ∈ ran 𝐼 )
15	13 14	syldan	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉 ) ) → ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) ∩ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑌 ) ) ) ∈ ran 𝐼 )
16	7 15	eqeltrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉 ) ) → ( 𝑋 ∨ 𝑌 ) ∈ ran 𝐼 )