Metamath Proof Explorer

Theorem djaffvalN

Description: Subspace join for DVecA partial vector space. (Contributed by NM, 6-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypothesis djaval.h ⊢ H = LHyp ⁡ K
Assertion 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

Proof

Step Hyp Ref Expression
1 djaval.h ⊢ H = LHyp ⁡ K
2 elex ⊢ K ∈ V → K ∈ V
3 fveq2 ⊢ k = K → LHyp ⁡ k = LHyp ⁡ K
4 3 1 eqtr4di ⊢ k = K → LHyp ⁡ k = H
5 fveq2 ⊢ k = K → LTrn ⁡ k = LTrn ⁡ K
6 5 fveq1d ⊢ k = K → LTrn ⁡ k ⁡ w = LTrn ⁡ K ⁡ w
7 6 pweqd ⊢ k = K → 𝒫 LTrn ⁡ k ⁡ w = 𝒫 LTrn ⁡ K ⁡ w
8 fveq2 ⊢ k = K → ocA ⁡ k = ocA ⁡ K
9 8 fveq1d ⊢ k = K → ocA ⁡ k ⁡ w = ocA ⁡ K ⁡ w
10 9 fveq1d ⊢ k = K → ocA ⁡ k ⁡ w ⁡ x = ocA ⁡ K ⁡ w ⁡ x
11 9 fveq1d ⊢ k = K → ocA ⁡ k ⁡ w ⁡ y = ocA ⁡ K ⁡ w ⁡ y
12 10 11 ineq12d ⊢ k = K → ocA ⁡ k ⁡ w ⁡ x ∩ ocA ⁡ k ⁡ w ⁡ y = ocA ⁡ K ⁡ w ⁡ x ∩ ocA ⁡ K ⁡ w ⁡ y
13 9 12 fveq12d ⊢ k = K → ocA ⁡ k ⁡ w ⁡ ocA ⁡ k ⁡ w ⁡ x ∩ ocA ⁡ k ⁡ w ⁡ y = ocA ⁡ K ⁡ w ⁡ ocA ⁡ K ⁡ w ⁡ x ∩ ocA ⁡ K ⁡ w ⁡ y
14 7 7 13 mpoeq123dv ⊢ k = K → x ∈ 𝒫 LTrn ⁡ k ⁡ w , y ∈ 𝒫 LTrn ⁡ k ⁡ w ⟼ ocA ⁡ k ⁡ w ⁡ ocA ⁡ k ⁡ w ⁡ x ∩ ocA ⁡ k ⁡ w ⁡ y = x ∈ 𝒫 LTrn ⁡ K ⁡ w , y ∈ 𝒫 LTrn ⁡ K ⁡ w ⟼ ocA ⁡ K ⁡ w ⁡ ocA ⁡ K ⁡ w ⁡ x ∩ ocA ⁡ K ⁡ w ⁡ y
15 4 14 mpteq12dv ⊢ k = K → w ∈ LHyp ⁡ k ⟼ 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
16 df-djaN ⊢ vA = k ∈ V ⟼ w ∈ LHyp ⁡ k ⟼ x ∈ 𝒫 LTrn ⁡ k ⁡ w , y ∈ 𝒫 LTrn ⁡ k ⁡ w ⟼ ocA ⁡ k ⁡ w ⁡ ocA ⁡ k ⁡ w ⁡ x ∩ ocA ⁡ k ⁡ w ⁡ y
17 15 16 1 mptfvmpt ⊢ 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
18 2 17 syl ⊢ 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