Theorem djhval2

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

	Ref	Expression
Hypotheses	djhval.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	djhval.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	djhval.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	djhval.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
	djhval.j	⊢ ∨ = ( ( joinH ‘ 𝐾 ) ‘ 𝑊 )
Assertion	djhval2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉 ) → ( 𝑋 ∨ 𝑌 ) = ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 ∪ 𝑌 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		djhval.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		djhval.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3		djhval.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
4		djhval.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
5		djhval.j	⊢ ∨ = ( ( joinH ‘ 𝐾 ) ‘ 𝑊 )
6	1 2 3 4 5	djhval	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉 ) ) → ( 𝑋 ∨ 𝑌 ) = ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∩ ( ⊥ ‘ 𝑌 ) ) ) )
7	6	3impb	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉 ) → ( 𝑋 ∨ 𝑌 ) = ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∩ ( ⊥ ‘ 𝑌 ) ) ) )
8	1 2 3 4	dochdmj1	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉 ) → ( ⊥ ‘ ( 𝑋 ∪ 𝑌 ) ) = ( ( ⊥ ‘ 𝑋 ) ∩ ( ⊥ ‘ 𝑌 ) ) )
9	8	fveq2d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉 ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 ∪ 𝑌 ) ) ) = ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∩ ( ⊥ ‘ 𝑌 ) ) ) )
10	7 9	eqtr4d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉 ) → ( 𝑋 ∨ 𝑌 ) = ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 ∪ 𝑌 ) ) ) )