Metamath Proof Explorer


Theorem djafvalN

Description: Subspace join for DVecA partial vector space. TODO: take out hypothesis .i, no longer used. (Contributed by NM, 6-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses djaval.h H = LHyp K
djaval.t T = LTrn K W
djaval.i I = DIsoA K W
djaval.n ˙ = ocA K W
djaval.j J = vA K W
Assertion djafvalN K V W H J = x 𝒫 T , y 𝒫 T ˙ ˙ x ˙ y

Proof

Step Hyp Ref Expression
1 djaval.h H = LHyp K
2 djaval.t T = LTrn K W
3 djaval.i I = DIsoA K W
4 djaval.n ˙ = ocA K W
5 djaval.j J = vA K W
6 1 djaffvalN K V vA K = w H x 𝒫 LTrn K w , y 𝒫 LTrn K w ocA K w ocA K w x ocA K w y
7 6 fveq1d K V vA K W = w H x 𝒫 LTrn K w , y 𝒫 LTrn K w ocA K w ocA K w x ocA K w y W
8 5 7 syl5eq K V J = w H x 𝒫 LTrn K w , y 𝒫 LTrn K w ocA K w ocA K w x ocA K w y W
9 fveq2 w = W LTrn K w = LTrn K W
10 9 2 eqtr4di w = W LTrn K w = T
11 10 pweqd w = W 𝒫 LTrn K w = 𝒫 T
12 fveq2 w = W ocA K w = ocA K W
13 12 4 eqtr4di w = W ocA K w = ˙
14 13 fveq1d w = W ocA K w x = ˙ x
15 13 fveq1d w = W ocA K w y = ˙ y
16 14 15 ineq12d w = W ocA K w x ocA K w y = ˙ x ˙ y
17 13 16 fveq12d w = W ocA K w ocA K w x ocA K w y = ˙ ˙ x ˙ y
18 11 11 17 mpoeq123dv w = W x 𝒫 LTrn K w , y 𝒫 LTrn K w ocA K w ocA K w x ocA K w y = x 𝒫 T , y 𝒫 T ˙ ˙ x ˙ y
19 eqid w H x 𝒫 LTrn K w , y 𝒫 LTrn K w ocA K w ocA K w x ocA K w y = w H x 𝒫 LTrn K w , y 𝒫 LTrn K w ocA K w ocA K w x ocA K w y
20 2 fvexi T V
21 20 pwex 𝒫 T V
22 21 21 mpoex x 𝒫 T , y 𝒫 T ˙ ˙ x ˙ y V
23 18 19 22 fvmpt W H w H x 𝒫 LTrn K w , y 𝒫 LTrn K w ocA K w ocA K w x ocA K w y W = x 𝒫 T , y 𝒫 T ˙ ˙ x ˙ y
24 8 23 sylan9eq K V W H J = x 𝒫 T , y 𝒫 T ˙ ˙ x ˙ y