Metamath Proof Explorer

Theorem djhval2

Description: Value of subspace join for DVecH vector space. (Contributed by NM, 6-Aug-2014)

Ref Expression
Hypotheses djhval.h ⊢ H = LHyp ⁡ K
djhval.u ⊢ U = DVecH ⁡ K ⁡ W
djhval.v ⊢ V = Base U
djhval.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
djhval.j ⊢ ∨ ˙ = joinH ⁡ K ⁡ W
Assertion djhval2 ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V ∧ Y ⊆ V → X ∨ ˙ Y = ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ∪ Y

Proof

Step Hyp Ref Expression
1 djhval.h ⊢ H = LHyp ⁡ K
2 djhval.u ⊢ U = DVecH ⁡ K ⁡ W
3 djhval.v ⊢ V = Base U
4 djhval.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
5 djhval.j ⊢ ∨ ˙ = joinH ⁡ K ⁡ W
6 1 2 3 4 5 djhval ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V ∧ Y ⊆ V → X ∨ ˙ Y = ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ∩ ⊥ ˙ ⁡ Y
7 6 3impb ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V ∧ Y ⊆ V → X ∨ ˙ Y = ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ∩ ⊥ ˙ ⁡ Y
8 1 2 3 4 dochdmj1 ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V ∧ Y ⊆ V → ⊥ ˙ ⁡ X ∪ Y = ⊥ ˙ ⁡ X ∩ ⊥ ˙ ⁡ Y
9 8 fveq2d ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V ∧ Y ⊆ V → ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ∪ Y = ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ∩ ⊥ ˙ ⁡ Y
10 7 9 eqtr4d ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V ∧ Y ⊆ V → X ∨ ˙ Y = ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ∪ Y