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

Metamath Proof Explorer

Theorem djaclN

Description: Closure of subspace join for DVecA partial vector space. (Contributed by NM, 5-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses djacl.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
djacl.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
djacl.i ⊢ 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
djacl.j ⊢ 𝐽 = ( ( vA ‘ 𝐾 ) ‘ 𝑊 )
Assertion djaclN ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ⊆ 𝑇 ∧ 𝑌 ⊆ 𝑇 ) ) → ( 𝑋 𝐽 𝑌 ) ∈ ran 𝐼 )

Proof

Step Hyp Ref Expression
1 djacl.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 djacl.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
3 djacl.i ⊢ 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
4 djacl.j ⊢ 𝐽 = ( ( vA ‘ 𝐾 ) ‘ 𝑊 )
5 eqid ⊢ ( ( ocA ‘ 𝐾 ) ‘ 𝑊 ) = ( ( ocA ‘ 𝐾 ) ‘ 𝑊 )
6 1 2 3 5 4 djavalN ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ⊆ 𝑇 ∧ 𝑌 ⊆ 𝑇 ) ) → ( 𝑋 𝐽 𝑌 ) = ( ( ( ocA ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ( ocA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) ∩ ( ( ( ocA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑌 ) ) ) )
7 inss1 ⊢ ( ( ( ( ocA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) ∩ ( ( ( ocA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑌 ) ) ⊆ ( ( ( ocA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 )
8 1 2 3 5 docaclN ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑇 ) → ( ( ( ocA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) ∈ ran 𝐼 )
9 8 adantrr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ⊆ 𝑇 ∧ 𝑌 ⊆ 𝑇 ) ) → ( ( ( ocA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) ∈ ran 𝐼 )
10 1 2 3 diaelrnN ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( ( ocA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) ∈ ran 𝐼 ) → ( ( ( ocA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) ⊆ 𝑇 )
11 9 10 syldan ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ⊆ 𝑇 ∧ 𝑌 ⊆ 𝑇 ) ) → ( ( ( ocA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) ⊆ 𝑇 )
12 7 11 sstrid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ⊆ 𝑇 ∧ 𝑌 ⊆ 𝑇 ) ) → ( ( ( ( ocA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) ∩ ( ( ( ocA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑌 ) ) ⊆ 𝑇 )
13 1 2 3 5 docaclN ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( ( ( ocA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) ∩ ( ( ( ocA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑌 ) ) ⊆ 𝑇 ) → ( ( ( ocA ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ( ocA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) ∩ ( ( ( ocA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑌 ) ) ) ∈ ran 𝐼 )
14 12 13 syldan ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ⊆ 𝑇 ∧ 𝑌 ⊆ 𝑇 ) ) → ( ( ( ocA ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ( ocA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) ∩ ( ( ( ocA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑌 ) ) ) ∈ ran 𝐼 )
15 6 14 eqeltrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ⊆ 𝑇 ∧ 𝑌 ⊆ 𝑇 ) ) → ( 𝑋 𝐽 𝑌 ) ∈ ran 𝐼 )