Metamath Proof Explorer

Theorem djhcom

Description: Subspace join commutes. (Contributed by NM, 8-Aug-2014)

Ref Expression
Hypotheses djhcom.h ⊢ H = LHyp ⁡ K
djhcom.u ⊢ U = DVecH ⁡ K ⁡ W
djhcom.v ⊢ V = Base U
djhcom.j ⊢ ∨ ˙ = joinH ⁡ K ⁡ W
djhcom.k ⊢ φ → K ∈ HL ∧ W ∈ H
djhcom.x ⊢ φ → X ⊆ V
djhcom.y ⊢ φ → Y ⊆ V
Assertion djhcom ⊢ φ → X ∨ ˙ Y = Y ∨ ˙ X

Proof

Step Hyp Ref Expression
1 djhcom.h ⊢ H = LHyp ⁡ K
2 djhcom.u ⊢ U = DVecH ⁡ K ⁡ W
3 djhcom.v ⊢ V = Base U
4 djhcom.j ⊢ ∨ ˙ = joinH ⁡ K ⁡ W
5 djhcom.k ⊢ φ → K ∈ HL ∧ W ∈ H
6 djhcom.x ⊢ φ → X ⊆ V
7 djhcom.y ⊢ φ → Y ⊆ V
8 uncom ⊢ X ∪ Y = Y ∪ X
9 8 fveq2i ⊢ ocH ⁡ K ⁡ W ⁡ X ∪ Y = ocH ⁡ K ⁡ W ⁡ Y ∪ X
10 9 fveq2i ⊢ ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ X ∪ Y = ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ Y ∪ X
11 eqid ⊢ ocH ⁡ K ⁡ W = ocH ⁡ K ⁡ W
12 1 2 3 11 4 djhval2 ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V ∧ Y ⊆ V → X ∨ ˙ Y = ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ X ∪ Y
13 5 6 7 12 syl3anc ⊢ φ → X ∨ ˙ Y = ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ X ∪ Y
14 1 2 3 11 4 djhval2 ⊢ K ∈ HL ∧ W ∈ H ∧ Y ⊆ V ∧ X ⊆ V → Y ∨ ˙ X = ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ Y ∪ X
15 5 7 6 14 syl3anc ⊢ φ → Y ∨ ˙ X = ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ Y ∪ X
16 10 13 15 3eqtr4a ⊢ φ → X ∨ ˙ Y = Y ∨ ˙ X