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 \in X \to joinH (K) = (w \in H ⟼ (x \in 𝒫 {Base}_{DVecH (K) (w)}, y \in 𝒫 {Base}_{DVecH (K) (w)} ⟼ ocH (K) (w) (ocH (K) (w) (x) \cap ocH (K) (w) (y))))$

Proof

Step	Hyp	Ref	Expression
1		djhval.h	$⊢ H = LHyp (K)$
2		elex	$⊢ K \in X \to K \in V$
3		fveq2	$⊢ k = K \to LHyp (k) = LHyp (K)$
4	3 1	eqtr4di	$⊢ k = K \to LHyp (k) = H$
5		fveq2	$⊢ k = K \to DVecH (k) = DVecH (K)$
6	5	fveq1d	$⊢ k = K \to DVecH (k) (w) = DVecH (K) (w)$
7	6	fveq2d	$⊢ k = K \to {Base}_{DVecH (k) (w)} = {Base}_{DVecH (K) (w)}$
8	7	pweqd	$⊢ k = K \to 𝒫 {Base}_{DVecH (k) (w)} = 𝒫 {Base}_{DVecH (K) (w)}$
9		fveq2	$⊢ k = K \to ocH (k) = ocH (K)$
10	9	fveq1d	$⊢ k = K \to ocH (k) (w) = ocH (K) (w)$
11	10	fveq1d	$⊢ k = K \to ocH (k) (w) (x) = ocH (K) (w) (x)$
12	10	fveq1d	$⊢ k = K \to ocH (k) (w) (y) = ocH (K) (w) (y)$
13	11 12	ineq12d	$⊢ k = K \to ocH (k) (w) (x) \cap ocH (k) (w) (y) = ocH (K) (w) (x) \cap ocH (K) (w) (y)$
14	10 13	fveq12d	$⊢ k = K \to ocH (k) (w) (ocH (k) (w) (x) \cap ocH (k) (w) (y)) = ocH (K) (w) (ocH (K) (w) (x) \cap ocH (K) (w) (y))$
15	8 8 14	mpoeq123dv	$⊢ k = K \to (x \in 𝒫 {Base}_{DVecH (k) (w)}, y \in 𝒫 {Base}_{DVecH (k) (w)} ⟼ ocH (k) (w) (ocH (k) (w) (x) \cap ocH (k) (w) (y))) = (x \in 𝒫 {Base}_{DVecH (K) (w)}, y \in 𝒫 {Base}_{DVecH (K) (w)} ⟼ ocH (K) (w) (ocH (K) (w) (x) \cap ocH (K) (w) (y)))$
16	4 15	mpteq12dv	$⊢ k = K \to (w \in LHyp (k) ⟼ (x \in 𝒫 {Base}_{DVecH (k) (w)}, y \in 𝒫 {Base}_{DVecH (k) (w)} ⟼ ocH (k) (w) (ocH (k) (w) (x) \cap ocH (k) (w) (y)))) = (w \in H ⟼ (x \in 𝒫 {Base}_{DVecH (K) (w)}, y \in 𝒫 {Base}_{DVecH (K) (w)} ⟼ ocH (K) (w) (ocH (K) (w) (x) \cap ocH (K) (w) (y))))$
17		df-djh	$⊢ joinH = (k \in V ⟼ (w \in LHyp (k) ⟼ (x \in 𝒫 {Base}_{DVecH (k) (w)}, y \in 𝒫 {Base}_{DVecH (k) (w)} ⟼ ocH (k) (w) (ocH (k) (w) (x) \cap ocH (k) (w) (y)))))$
18	16 17 1	mptfvmpt	$⊢ K \in V \to joinH (K) = (w \in H ⟼ (x \in 𝒫 {Base}_{DVecH (K) (w)}, y \in 𝒫 {Base}_{DVecH (K) (w)} ⟼ ocH (K) (w) (ocH (K) (w) (x) \cap ocH (K) (w) (y))))$
19	2 18	syl	$⊢ K \in X \to joinH (K) = (w \in H ⟼ (x \in 𝒫 {Base}_{DVecH (K) (w)}, y \in 𝒫 {Base}_{DVecH (K) (w)} ⟼ ocH (K) (w) (ocH (K) (w) (x) \cap ocH (K) (w) (y))))$