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 ⊢ H = LHyp ⁡ K
djhcl.i ⊢ I = DIsoH ⁡ K ⁡ W
djhcl.u ⊢ U = DVecH ⁡ K ⁡ W
djhcl.v ⊢ V = Base U
djhcl.j ⊢ ∨ ˙ = joinH ⁡ K ⁡ W
Assertion djhcl ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V ∧ Y ⊆ V → X ∨ ˙ Y ∈ ran ⁡ I

Proof

Step Hyp Ref Expression
1 djhcl.h ⊢ H = LHyp ⁡ K
2 djhcl.i ⊢ I = DIsoH ⁡ K ⁡ W
3 djhcl.u ⊢ U = DVecH ⁡ K ⁡ W
4 djhcl.v ⊢ V = Base U
5 djhcl.j ⊢ ∨ ˙ = joinH ⁡ K ⁡ W
6 eqid ⊢ ocH ⁡ K ⁡ W = ocH ⁡ K ⁡ W
7 1 3 4 6 5 djhval ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V ∧ Y ⊆ V → X ∨ ˙ Y = ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ X ∩ ocH ⁡ K ⁡ W ⁡ Y
8 inss1 ⊢ ocH ⁡ K ⁡ W ⁡ X ∩ ocH ⁡ K ⁡ W ⁡ Y ⊆ ocH ⁡ K ⁡ W ⁡ X
9 1 2 3 4 6 dochcl ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → ocH ⁡ K ⁡ W ⁡ X ∈ ran ⁡ I
10 9 adantrr ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V ∧ Y ⊆ V → ocH ⁡ K ⁡ W ⁡ X ∈ ran ⁡ I
11 1 3 2 4 dihrnss ⊢ K ∈ HL ∧ W ∈ H ∧ ocH ⁡ K ⁡ W ⁡ X ∈ ran ⁡ I → ocH ⁡ K ⁡ W ⁡ X ⊆ V
12 10 11 syldan ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V ∧ Y ⊆ V → ocH ⁡ K ⁡ W ⁡ X ⊆ V
13 8 12 sstrid ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V ∧ Y ⊆ V → ocH ⁡ K ⁡ W ⁡ X ∩ ocH ⁡ K ⁡ W ⁡ Y ⊆ V
14 1 2 3 4 6 dochcl ⊢ K ∈ HL ∧ W ∈ H ∧ ocH ⁡ K ⁡ W ⁡ X ∩ ocH ⁡ K ⁡ W ⁡ Y ⊆ V → ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ X ∩ ocH ⁡ K ⁡ W ⁡ Y ∈ ran ⁡ I
15 13 14 syldan ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V ∧ Y ⊆ V → ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ X ∩ ocH ⁡ K ⁡ W ⁡ Y ∈ ran ⁡ I
16 7 15 eqeltrd ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V ∧ Y ⊆ V → X ∨ ˙ Y ∈ ran ⁡ I