Metamath Proof Explorer

Theorem djhffval

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

Ref Expression
Hypothesis djhval.h ⊢H=LHyp⁡K
Assertion djhffval ⊢K∈X→joinH⁡K=w∈H⟼x∈𝒫BaseDVecH⁡K⁡w,y∈𝒫BaseDVecH⁡K⁡w⟼ocH⁡K⁡w⁡ocH⁡K⁡w⁡x∩ocH⁡K⁡w⁡y

Proof

Step Hyp Ref Expression
1 djhval.h ⊢H=LHyp⁡K
2 elex ⊢K∈X→K∈V
3 fveq2 ⊢k=K→LHyp⁡k=LHyp⁡K
4 3 1 eqtr4di ⊢k=K→LHyp⁡k=H
5 fveq2 ⊢k=K→DVecH⁡k=DVecH⁡K
6 5 fveq1d ⊢k=K→DVecH⁡k⁡w=DVecH⁡K⁡w
7 6 fveq2d ⊢k=K→BaseDVecH⁡k⁡w=BaseDVecH⁡K⁡w
8 7 pweqd ⊢k=K→𝒫BaseDVecH⁡k⁡w=𝒫BaseDVecH⁡K⁡w
9 fveq2 ⊢k=K→ocH⁡k=ocH⁡K
10 9 fveq1d ⊢k=K→ocH⁡k⁡w=ocH⁡K⁡w
11 10 fveq1d ⊢k=K→ocH⁡k⁡w⁡x=ocH⁡K⁡w⁡x
12 10 fveq1d ⊢k=K→ocH⁡k⁡w⁡y=ocH⁡K⁡w⁡y
13 11 12 ineq12d ⊢k=K→ocH⁡k⁡w⁡x∩ocH⁡k⁡w⁡y=ocH⁡K⁡w⁡x∩ocH⁡K⁡w⁡y
14 10 13 fveq12d ⊢k=K→ocH⁡k⁡w⁡ocH⁡k⁡w⁡x∩ocH⁡k⁡w⁡y=ocH⁡K⁡w⁡ocH⁡K⁡w⁡x∩ocH⁡K⁡w⁡y
15 8 8 14 mpoeq123dv ⊢k=K→x∈𝒫BaseDVecH⁡k⁡w,y∈𝒫BaseDVecH⁡k⁡w⟼ocH⁡k⁡w⁡ocH⁡k⁡w⁡x∩ocH⁡k⁡w⁡y=x∈𝒫BaseDVecH⁡K⁡w,y∈𝒫BaseDVecH⁡K⁡w⟼ocH⁡K⁡w⁡ocH⁡K⁡w⁡x∩ocH⁡K⁡w⁡y
16 4 15 mpteq12dv ⊢k=K→w∈LHyp⁡k⟼x∈𝒫BaseDVecH⁡k⁡w,y∈𝒫BaseDVecH⁡k⁡w⟼ocH⁡k⁡w⁡ocH⁡k⁡w⁡x∩ocH⁡k⁡w⁡y=w∈H⟼x∈𝒫BaseDVecH⁡K⁡w,y∈𝒫BaseDVecH⁡K⁡w⟼ocH⁡K⁡w⁡ocH⁡K⁡w⁡x∩ocH⁡K⁡w⁡y
17 df-djh ⊢joinH=k∈V⟼w∈LHyp⁡k⟼x∈𝒫BaseDVecH⁡k⁡w,y∈𝒫BaseDVecH⁡k⁡w⟼ocH⁡k⁡w⁡ocH⁡k⁡w⁡x∩ocH⁡k⁡w⁡y
18 16 17 1 mptfvmpt ⊢K∈V→joinH⁡K=w∈H⟼x∈𝒫BaseDVecH⁡K⁡w,y∈𝒫BaseDVecH⁡K⁡w⟼ocH⁡K⁡w⁡ocH⁡K⁡w⁡x∩ocH⁡K⁡w⁡y
19 2 18 syl ⊢K∈X→joinH⁡K=w∈H⟼x∈𝒫BaseDVecH⁡K⁡w,y∈𝒫BaseDVecH⁡K⁡w⟼ocH⁡K⁡w⁡ocH⁡K⁡w⁡x∩ocH⁡K⁡w⁡y