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