Theorem djhcom

Description: Subspace join is commutative. (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	⊢ ( 𝜑 → ( 𝑋 ∨ 𝑌 ) = ( 𝑌 ∨ 𝑋 ) )