This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐼 )