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 𝒫 Base DVecH K w , y 𝒫 Base DVecH 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 Base DVecH k w = Base DVecH K w
8 7 pweqd k = K 𝒫 Base DVecH k w = 𝒫 Base DVecH 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 𝒫 Base DVecH k w , y 𝒫 Base DVecH k w ocH k w ocH k w x ocH k w y = x 𝒫 Base DVecH K w , y 𝒫 Base DVecH K w ocH K w ocH K w x ocH K w y
16 4 15 mpteq12dv k = K w LHyp k x 𝒫 Base DVecH k w , y 𝒫 Base DVecH k w ocH k w ocH k w x ocH k w y = w H x 𝒫 Base DVecH K w , y 𝒫 Base DVecH K w ocH K w ocH K w x ocH K w y
17 df-djh joinH = k V w LHyp k x 𝒫 Base DVecH k w , y 𝒫 Base DVecH 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 𝒫 Base DVecH K w , y 𝒫 Base DVecH K w ocH K w ocH K w x ocH K w y
19 2 18 syl K X joinH K = w H x 𝒫 Base DVecH K w , y 𝒫 Base DVecH K w ocH K w ocH K w x ocH K w y