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	$⊢ \underset{˙}{⊥} = ocA (K) (W)$
	djaval.j	$⊢ J = vA (K) (W)$
Assertion	djafvalN	$⊢ (K \in V \land W \in H) \to J = (x \in 𝒫 T, y \in 𝒫 T ⟼ \underset{˙}{⊥} (\underset{˙}{⊥} (x) \cap \underset{˙}{⊥} (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	$⊢ \underset{˙}{⊥} = ocA (K) (W)$
5		djaval.j	$⊢ J = vA (K) (W)$
6	1	djaffvalN	$⊢ K \in V \to vA (K) = (w \in H ⟼ (x \in 𝒫 LTrn (K) (w), y \in 𝒫 LTrn (K) (w) ⟼ ocA (K) (w) (ocA (K) (w) (x) \cap ocA (K) (w) (y))))$
7	6	fveq1d	$⊢ K \in V \to vA (K) (W) = (w \in H ⟼ (x \in 𝒫 LTrn (K) (w), y \in 𝒫 LTrn (K) (w) ⟼ ocA (K) (w) (ocA (K) (w) (x) \cap ocA (K) (w) (y)))) (W)$
8	5 7	syl5eq	$⊢ K \in V \to J = (w \in H ⟼ (x \in 𝒫 LTrn (K) (w), y \in 𝒫 LTrn (K) (w) ⟼ ocA (K) (w) (ocA (K) (w) (x) \cap ocA (K) (w) (y)))) (W)$
9		fveq2	$⊢ w = W \to LTrn (K) (w) = LTrn (K) (W)$
10	9 2	eqtr4di	$⊢ w = W \to LTrn (K) (w) = T$
11	10	pweqd	$⊢ w = W \to 𝒫 LTrn (K) (w) = 𝒫 T$
12		fveq2	$⊢ w = W \to ocA (K) (w) = ocA (K) (W)$
13	12 4	eqtr4di	$⊢ w = W \to ocA (K) (w) = \underset{˙}{⊥}$
14	13	fveq1d	$⊢ w = W \to ocA (K) (w) (x) = \underset{˙}{⊥} (x)$
15	13	fveq1d	$⊢ w = W \to ocA (K) (w) (y) = \underset{˙}{⊥} (y)$
16	14 15	ineq12d	$⊢ w = W \to ocA (K) (w) (x) \cap ocA (K) (w) (y) = \underset{˙}{⊥} (x) \cap \underset{˙}{⊥} (y)$
17	13 16	fveq12d	$⊢ w = W \to ocA (K) (w) (ocA (K) (w) (x) \cap ocA (K) (w) (y)) = \underset{˙}{⊥} (\underset{˙}{⊥} (x) \cap \underset{˙}{⊥} (y))$
18	11 11 17	mpoeq123dv	$⊢ w = W \to (x \in 𝒫 LTrn (K) (w), y \in 𝒫 LTrn (K) (w) ⟼ ocA (K) (w) (ocA (K) (w) (x) \cap ocA (K) (w) (y))) = (x \in 𝒫 T, y \in 𝒫 T ⟼ \underset{˙}{⊥} (\underset{˙}{⊥} (x) \cap \underset{˙}{⊥} (y)))$
19		eqid	$⊢ (w \in H ⟼ (x \in 𝒫 LTrn (K) (w), y \in 𝒫 LTrn (K) (w) ⟼ ocA (K) (w) (ocA (K) (w) (x) \cap ocA (K) (w) (y)))) = (w \in H ⟼ (x \in 𝒫 LTrn (K) (w), y \in 𝒫 LTrn (K) (w) ⟼ ocA (K) (w) (ocA (K) (w) (x) \cap ocA (K) (w) (y))))$
20	2	fvexi	$⊢ T \in V$
21	20	pwex	$⊢ 𝒫 T \in V$
22	21 21	mpoex	$⊢ (x \in 𝒫 T, y \in 𝒫 T ⟼ \underset{˙}{⊥} (\underset{˙}{⊥} (x) \cap \underset{˙}{⊥} (y))) \in V$
23	18 19 22	fvmpt	$⊢ W \in H \to (w \in H ⟼ (x \in 𝒫 LTrn (K) (w), y \in 𝒫 LTrn (K) (w) ⟼ ocA (K) (w) (ocA (K) (w) (x) \cap ocA (K) (w) (y)))) (W) = (x \in 𝒫 T, y \in 𝒫 T ⟼ \underset{˙}{⊥} (\underset{˙}{⊥} (x) \cap \underset{˙}{⊥} (y)))$
24	8 23	sylan9eq	$⊢ (K \in V \land W \in H) \to J = (x \in 𝒫 T, y \in 𝒫 T ⟼ \underset{˙}{⊥} (\underset{˙}{⊥} (x) \cap \underset{˙}{⊥} (y)))$

Metamath Proof Explorer

Theorem djafvalN

Proof