Metamath Proof Explorer

Theorem djhval

Description: Subspace join for DVecH vector space. (Contributed by NM, 19-Jul-2014)

Ref Expression
Hypotheses djhval.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
djhval.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
djhval.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
djhval.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
djhval.j ⊢ ∨ = ( ( joinH ‘ 𝐾 ) ‘ 𝑊 )
Assertion djhval ( ( ( 𝐾 ∈ 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 djhfval ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∨ = ( 𝑥 ∈ 𝒫 𝑉 , 𝑦 ∈ 𝒫 𝑉 ↦ ( ⊥ ‘ ( ( ⊥ ‘ 𝑥 ) ∩ ( ⊥ ‘ 𝑦 ) ) ) ) )
7 6 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉 ) ) → ∨ = ( 𝑥 ∈ 𝒫 𝑉 , 𝑦 ∈ 𝒫 𝑉 ↦ ( ⊥ ‘ ( ( ⊥ ‘ 𝑥 ) ∩ ( ⊥ ‘ 𝑦 ) ) ) ) )
8 7 oveqd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉 ) ) → ( 𝑋 ∨ 𝑌 ) = ( 𝑋 ( 𝑥 ∈ 𝒫 𝑉 , 𝑦 ∈ 𝒫 𝑉 ↦ ( ⊥ ‘ ( ( ⊥ ‘ 𝑥 ) ∩ ( ⊥ ‘ 𝑦 ) ) ) ) 𝑌 ) )
9 3 fvexi ⊢ 𝑉 ∈ V
10 9 elpw2 ⊢ ( 𝑋 ∈ 𝒫 𝑉 ↔ 𝑋 ⊆ 𝑉 )
11 10 biimpri ⊢ ( 𝑋 ⊆ 𝑉 → 𝑋 ∈ 𝒫 𝑉 )
12 11 ad2antrl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉 ) ) → 𝑋 ∈ 𝒫 𝑉 )
13 9 elpw2 ⊢ ( 𝑌 ∈ 𝒫 𝑉 ↔ 𝑌 ⊆ 𝑉 )
14 13 biimpri ⊢ ( 𝑌 ⊆ 𝑉 → 𝑌 ∈ 𝒫 𝑉 )
15 14 ad2antll ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉 ) ) → 𝑌 ∈ 𝒫 𝑉 )
16 fvexd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉 ) ) → ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∩ ( ⊥ ‘ 𝑌 ) ) ) ∈ V )
17 fveq2 ⊢ ( 𝑥 = 𝑋 → ( ⊥ ‘ 𝑥 ) = ( ⊥ ‘ 𝑋 ) )
18 17 ineq1d ⊢ ( 𝑥 = 𝑋 → ( ( ⊥ ‘ 𝑥 ) ∩ ( ⊥ ‘ 𝑦 ) ) = ( ( ⊥ ‘ 𝑋 ) ∩ ( ⊥ ‘ 𝑦 ) ) )
19 18 fveq2d ⊢ ( 𝑥 = 𝑋 → ( ⊥ ‘ ( ( ⊥ ‘ 𝑥 ) ∩ ( ⊥ ‘ 𝑦 ) ) ) = ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∩ ( ⊥ ‘ 𝑦 ) ) ) )
20 fveq2 ⊢ ( 𝑦 = 𝑌 → ( ⊥ ‘ 𝑦 ) = ( ⊥ ‘ 𝑌 ) )
21 20 ineq2d ⊢ ( 𝑦 = 𝑌 → ( ( ⊥ ‘ 𝑋 ) ∩ ( ⊥ ‘ 𝑦 ) ) = ( ( ⊥ ‘ 𝑋 ) ∩ ( ⊥ ‘ 𝑌 ) ) )
22 21 fveq2d ⊢ ( 𝑦 = 𝑌 → ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∩ ( ⊥ ‘ 𝑦 ) ) ) = ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∩ ( ⊥ ‘ 𝑌 ) ) ) )
23 eqid ⊢ ( 𝑥 ∈ 𝒫 𝑉 , 𝑦 ∈ 𝒫 𝑉 ↦ ( ⊥ ‘ ( ( ⊥ ‘ 𝑥 ) ∩ ( ⊥ ‘ 𝑦 ) ) ) ) = ( 𝑥 ∈ 𝒫 𝑉 , 𝑦 ∈ 𝒫 𝑉 ↦ ( ⊥ ‘ ( ( ⊥ ‘ 𝑥 ) ∩ ( ⊥ ‘ 𝑦 ) ) ) )
24 19 22 23 ovmpog ⊢ ( ( 𝑋 ∈ 𝒫 𝑉 ∧ 𝑌 ∈ 𝒫 𝑉 ∧ ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∩ ( ⊥ ‘ 𝑌 ) ) ) ∈ V ) → ( 𝑋 ( 𝑥 ∈ 𝒫 𝑉 , 𝑦 ∈ 𝒫 𝑉 ↦ ( ⊥ ‘ ( ( ⊥ ‘ 𝑥 ) ∩ ( ⊥ ‘ 𝑦 ) ) ) ) 𝑌 ) = ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∩ ( ⊥ ‘ 𝑌 ) ) ) )
25 12 15 16 24 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉 ) ) → ( 𝑋 ( 𝑥 ∈ 𝒫 𝑉 , 𝑦 ∈ 𝒫 𝑉 ↦ ( ⊥ ‘ ( ( ⊥ ‘ 𝑥 ) ∩ ( ⊥ ‘ 𝑦 ) ) ) ) 𝑌 ) = ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∩ ( ⊥ ‘ 𝑌 ) ) ) )
26 8 25 eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉 ) ) → ( 𝑋 ∨ 𝑌 ) = ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∩ ( ⊥ ‘ 𝑌 ) ) ) )