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 ( 𝜑 → ( 𝑋 𝑌 ) = ( 𝑌 𝑋 ) )