Metamath Proof Explorer

Theorem djhfval

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 djhfval ( ( 𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻 ) → ∨ = ( 𝑥 ∈ 𝒫 𝑉 , 𝑦 ∈ 𝒫 𝑉 ↦ ( ⊥ ‘ ( ( ⊥ ‘ 𝑥 ) ∩ ( ⊥ ‘ 𝑦 ) ) ) ) )

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 djhffval ⊢ ( 𝐾 ∈ 𝑋 → ( joinH ‘ 𝐾 ) = ( 𝑤 ∈ 𝐻 ↦ ( 𝑥 ∈ 𝒫 ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) , 𝑦 ∈ 𝒫 ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ↦ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑥 ) ∩ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑦 ) ) ) ) ) )
7 6 fveq1d ⊢ ( 𝐾 ∈ 𝑋 → ( ( joinH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( 𝑤 ∈ 𝐻 ↦ ( 𝑥 ∈ 𝒫 ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) , 𝑦 ∈ 𝒫 ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ↦ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑥 ) ∩ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑦 ) ) ) ) ) ‘ 𝑊 ) )
8 5 7 syl5eq ⊢ ( 𝐾 ∈ 𝑋 → ∨ = ( ( 𝑤 ∈ 𝐻 ↦ ( 𝑥 ∈ 𝒫 ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) , 𝑦 ∈ 𝒫 ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ↦ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑥 ) ∩ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑦 ) ) ) ) ) ‘ 𝑊 ) )
9 2fveq3 ⊢ ( 𝑤 = 𝑊 → ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) = ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) )
10 2 fveq2i ⊢ ( Base ‘ 𝑈 ) = ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) )
11 3 10 eqtri ⊢ 𝑉 = ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) )
12 9 11 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) = 𝑉 )
13 12 pweqd ⊢ ( 𝑤 = 𝑊 → 𝒫 ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) = 𝒫 𝑉 )
14 fveq2 ⊢ ( 𝑤 = 𝑊 → ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) )
15 14 4 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) = ⊥ )
16 15 fveq1d ⊢ ( 𝑤 = 𝑊 → ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑥 ) = ( ⊥ ‘ 𝑥 ) )
17 15 fveq1d ⊢ ( 𝑤 = 𝑊 → ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑦 ) = ( ⊥ ‘ 𝑦 ) )
18 16 17 ineq12d ⊢ ( 𝑤 = 𝑊 → ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑥 ) ∩ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑦 ) ) = ( ( ⊥ ‘ 𝑥 ) ∩ ( ⊥ ‘ 𝑦 ) ) )
19 15 18 fveq12d ⊢ ( 𝑤 = 𝑊 → ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑥 ) ∩ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑦 ) ) ) = ( ⊥ ‘ ( ( ⊥ ‘ 𝑥 ) ∩ ( ⊥ ‘ 𝑦 ) ) ) )
20 13 13 19 mpoeq123dv ⊢ ( 𝑤 = 𝑊 → ( 𝑥 ∈ 𝒫 ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) , 𝑦 ∈ 𝒫 ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ↦ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑥 ) ∩ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑦 ) ) ) ) = ( 𝑥 ∈ 𝒫 𝑉 , 𝑦 ∈ 𝒫 𝑉 ↦ ( ⊥ ‘ ( ( ⊥ ‘ 𝑥 ) ∩ ( ⊥ ‘ 𝑦 ) ) ) ) )
21 eqid ⊢ ( 𝑤 ∈ 𝐻 ↦ ( 𝑥 ∈ 𝒫 ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) , 𝑦 ∈ 𝒫 ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ↦ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑥 ) ∩ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑦 ) ) ) ) ) = ( 𝑤 ∈ 𝐻 ↦ ( 𝑥 ∈ 𝒫 ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) , 𝑦 ∈ 𝒫 ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ↦ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑥 ) ∩ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑦 ) ) ) ) )
22 3 fvexi ⊢ 𝑉 ∈ V
23 22 pwex ⊢ 𝒫 𝑉 ∈ V
24 23 23 mpoex ⊢ ( 𝑥 ∈ 𝒫 𝑉 , 𝑦 ∈ 𝒫 𝑉 ↦ ( ⊥ ‘ ( ( ⊥ ‘ 𝑥 ) ∩ ( ⊥ ‘ 𝑦 ) ) ) ) ∈ V
25 20 21 24 fvmpt ⊢ ( 𝑊 ∈ 𝐻 → ( ( 𝑤 ∈ 𝐻 ↦ ( 𝑥 ∈ 𝒫 ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) , 𝑦 ∈ 𝒫 ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ↦ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑥 ) ∩ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑦 ) ) ) ) ) ‘ 𝑊 ) = ( 𝑥 ∈ 𝒫 𝑉 , 𝑦 ∈ 𝒫 𝑉 ↦ ( ⊥ ‘ ( ( ⊥ ‘ 𝑥 ) ∩ ( ⊥ ‘ 𝑦 ) ) ) ) )
26 8 25 sylan9eq ⊢ ( ( 𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻 ) → ∨ = ( 𝑥 ∈ 𝒫 𝑉 , 𝑦 ∈ 𝒫 𝑉 ↦ ( ⊥ ‘ ( ( ⊥ ‘ 𝑥 ) ∩ ( ⊥ ‘ 𝑦 ) ) ) ) )