djavalN

Description: Subspace join for DVecA partial vector space. (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	djavalN	$⊢ ((K \in HL \land W \in H) \land (X \subseteq T \land Y \subseteq T)) \to X J Y = \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 2 3 4 5	djafvalN	$⊢ (K \in HL \land W \in H) \to J = (x \in 𝒫 T, y \in 𝒫 T ⟼ \underset{˙}{⊥} (\underset{˙}{⊥} (x) \cap \underset{˙}{⊥} (y)))$
7	6	adantr	$⊢ ((K \in HL \land W \in H) \land (X \subseteq T \land Y \subseteq T)) \to J = (x \in 𝒫 T, y \in 𝒫 T ⟼ \underset{˙}{⊥} (\underset{˙}{⊥} (x) \cap \underset{˙}{⊥} (y)))$
8	7	oveqd	$⊢ ((K \in HL \land W \in H) \land (X \subseteq T \land Y \subseteq T)) \to X J Y = X (x \in 𝒫 T, y \in 𝒫 T ⟼ \underset{˙}{⊥} (\underset{˙}{⊥} (x) \cap \underset{˙}{⊥} (y))) Y$
9	2	fvexi	$⊢ T \in V$
10	9	elpw2	$⊢ X \in 𝒫 T \leftrightarrow X \subseteq T$
11	10	biimpri	$⊢ X \subseteq T \to X \in 𝒫 T$
12	11	ad2antrl	$⊢ ((K \in HL \land W \in H) \land (X \subseteq T \land Y \subseteq T)) \to X \in 𝒫 T$
13	9	elpw2	$⊢ Y \in 𝒫 T \leftrightarrow Y \subseteq T$
14	13	biimpri	$⊢ Y \subseteq T \to Y \in 𝒫 T$
15	14	ad2antll	$⊢ ((K \in HL \land W \in H) \land (X \subseteq T \land Y \subseteq T)) \to Y \in 𝒫 T$
16		fvexd	$⊢ ((K \in HL \land W \in H) \land (X \subseteq T \land Y \subseteq T)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap \underset{˙}{⊥} (Y)) \in V$
17		fveq2	$⊢ x = X \to \underset{˙}{⊥} (x) = \underset{˙}{⊥} (X)$
18	17	ineq1d	$⊢ x = X \to \underset{˙}{⊥} (x) \cap \underset{˙}{⊥} (y) = \underset{˙}{⊥} (X) \cap \underset{˙}{⊥} (y)$
19	18	fveq2d	$⊢ x = X \to \underset{˙}{⊥} (\underset{˙}{⊥} (x) \cap \underset{˙}{⊥} (y)) = \underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap \underset{˙}{⊥} (y))$
20		fveq2	$⊢ y = Y \to \underset{˙}{⊥} (y) = \underset{˙}{⊥} (Y)$
21	20	ineq2d	$⊢ y = Y \to \underset{˙}{⊥} (X) \cap \underset{˙}{⊥} (y) = \underset{˙}{⊥} (X) \cap \underset{˙}{⊥} (Y)$
22	21	fveq2d	$⊢ y = Y \to \underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap \underset{˙}{⊥} (y)) = \underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap \underset{˙}{⊥} (Y))$
23		eqid	$⊢ (x \in 𝒫 T, y \in 𝒫 T ⟼ \underset{˙}{⊥} (\underset{˙}{⊥} (x) \cap \underset{˙}{⊥} (y))) = (x \in 𝒫 T, y \in 𝒫 T ⟼ \underset{˙}{⊥} (\underset{˙}{⊥} (x) \cap \underset{˙}{⊥} (y)))$
24	19 22 23	ovmpog	$⊢ (X \in 𝒫 T \land Y \in 𝒫 T \land \underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap \underset{˙}{⊥} (Y)) \in V) \to X (x \in 𝒫 T, y \in 𝒫 T ⟼ \underset{˙}{⊥} (\underset{˙}{⊥} (x) \cap \underset{˙}{⊥} (y))) Y = \underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap \underset{˙}{⊥} (Y))$
25	12 15 16 24	syl3anc	$⊢ ((K \in HL \land W \in H) \land (X \subseteq T \land Y \subseteq T)) \to X (x \in 𝒫 T, y \in 𝒫 T ⟼ \underset{˙}{⊥} (\underset{˙}{⊥} (x) \cap \underset{˙}{⊥} (y))) Y = \underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap \underset{˙}{⊥} (Y))$
26	8 25	eqtrd	$⊢ ((K \in HL \land W \in H) \land (X \subseteq T \land Y \subseteq T)) \to X J Y = \underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap \underset{˙}{⊥} (Y))$

Metamath Proof Explorer

Theorem djavalN

Proof