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

Metamath Proof Explorer

Theorem djhcom

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

Ref Expression
Hypotheses djhcom.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
djhcom.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
djhcom.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
djhcom.j ⊢ ∨ = ( ( joinH ‘ 𝐾 ) ‘ 𝑊 )
djhcom.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
djhcom.x ⊢ ( 𝜑 → 𝑋 ⊆ 𝑉 )
djhcom.y ⊢ ( 𝜑 → 𝑌 ⊆ 𝑉 )
Assertion djhcom ( 𝜑 → ( 𝑋 ∨ 𝑌 ) = ( 𝑌 ∨ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 djhcom.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 djhcom.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 djhcom.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
4 djhcom.j ⊢ ∨ = ( ( joinH ‘ 𝐾 ) ‘ 𝑊 )
5 djhcom.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
6 djhcom.x ⊢ ( 𝜑 → 𝑋 ⊆ 𝑉 )
7 djhcom.y ⊢ ( 𝜑 → 𝑌 ⊆ 𝑉 )
8 uncom ⊢ ( 𝑋 ∪ 𝑌 ) = ( 𝑌 ∪ 𝑋 )
9 8 fveq2i ⊢ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ∪ 𝑌 ) ) = ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑌 ∪ 𝑋 ) )
10 9 fveq2i ⊢ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ∪ 𝑌 ) ) ) = ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑌 ∪ 𝑋 ) ) )
11 eqid ⊢ ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
12 1 2 3 11 4 djhval2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉 ) → ( 𝑋 ∨ 𝑌 ) = ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ∪ 𝑌 ) ) ) )
13 5 6 7 12 syl3anc ⊢ ( 𝜑 → ( 𝑋 ∨ 𝑌 ) = ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ∪ 𝑌 ) ) ) )
14 1 2 3 11 4 djhval2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑌 ⊆ 𝑉 ∧ 𝑋 ⊆ 𝑉 ) → ( 𝑌 ∨ 𝑋 ) = ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑌 ∪ 𝑋 ) ) ) )
15 5 7 6 14 syl3anc ⊢ ( 𝜑 → ( 𝑌 ∨ 𝑋 ) = ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑌 ∪ 𝑋 ) ) ) )
16 10 13 15 3eqtr4a ⊢ ( 𝜑 → ( 𝑋 ∨ 𝑌 ) = ( 𝑌 ∨ 𝑋 ) )