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

Metamath Proof Explorer

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 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉 ) → ( 𝑋 ∨ 𝑌 ) = ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 ∪ 𝑌 ) ) ) )