djhval

Description: Subspace join for DVecH vector space. (Contributed by NM, 19-Jul-2014)

	Ref	Expression
Hypotheses	djhval.h	$⊢ H = LHyp (K)$
	djhval.u	$⊢ U = DVecH (K) (W)$
	djhval.v	$⊢ V = {Base}_{U}$
	djhval.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
	djhval.j	$⊢ \underset{˙}{\lor} = joinH (K) (W)$
Assertion	djhval	$⊢ ((K \in HL \land W \in H) \land (X \subseteq V \land Y \subseteq V)) \to X \underset{˙}{\lor} Y = \underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap \underset{˙}{⊥} (Y))$

Proof

Step	Hyp	Ref	Expression
1		djhval.h	$⊢ H = LHyp (K)$
2		djhval.u	$⊢ U = DVecH (K) (W)$
3		djhval.v	$⊢ V = {Base}_{U}$
4		djhval.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
5		djhval.j	$⊢ \underset{˙}{\lor} = joinH (K) (W)$
6	1 2 3 4 5	djhfval	$⊢ (K \in HL \land W \in H) \to \underset{˙}{\lor} = (x \in 𝒫 V, y \in 𝒫 V ⟼ \underset{˙}{⊥} (\underset{˙}{⊥} (x) \cap \underset{˙}{⊥} (y)))$
7	6	adantr	$⊢ ((K \in HL \land W \in H) \land (X \subseteq V \land Y \subseteq V)) \to \underset{˙}{\lor} = (x \in 𝒫 V, y \in 𝒫 V ⟼ \underset{˙}{⊥} (\underset{˙}{⊥} (x) \cap \underset{˙}{⊥} (y)))$
8	7	oveqd	$⊢ ((K \in HL \land W \in H) \land (X \subseteq V \land Y \subseteq V)) \to X \underset{˙}{\lor} Y = X (x \in 𝒫 V, y \in 𝒫 V ⟼ \underset{˙}{⊥} (\underset{˙}{⊥} (x) \cap \underset{˙}{⊥} (y))) Y$
9	3	fvexi	$⊢ V \in V$
10	9	elpw2	$⊢ X \in 𝒫 V \leftrightarrow X \subseteq V$
11	10	biimpri	$⊢ X \subseteq V \to X \in 𝒫 V$
12	11	ad2antrl	$⊢ ((K \in HL \land W \in H) \land (X \subseteq V \land Y \subseteq V)) \to X \in 𝒫 V$
13	9	elpw2	$⊢ Y \in 𝒫 V \leftrightarrow Y \subseteq V$
14	13	biimpri	$⊢ Y \subseteq V \to Y \in 𝒫 V$
15	14	ad2antll	$⊢ ((K \in HL \land W \in H) \land (X \subseteq V \land Y \subseteq V)) \to Y \in 𝒫 V$
16		fvexd	$⊢ ((K \in HL \land W \in H) \land (X \subseteq V \land Y \subseteq V)) \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 𝒫 V, y \in 𝒫 V ⟼ \underset{˙}{⊥} (\underset{˙}{⊥} (x) \cap \underset{˙}{⊥} (y))) = (x \in 𝒫 V, y \in 𝒫 V ⟼ \underset{˙}{⊥} (\underset{˙}{⊥} (x) \cap \underset{˙}{⊥} (y)))$
24	19 22 23	ovmpog	$⊢ (X \in 𝒫 V \land Y \in 𝒫 V \land \underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap \underset{˙}{⊥} (Y)) \in V) \to X (x \in 𝒫 V, y \in 𝒫 V ⟼ \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 V \land Y \subseteq V)) \to X (x \in 𝒫 V, y \in 𝒫 V ⟼ \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 V \land Y \subseteq V)) \to X \underset{˙}{\lor} Y = \underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap \underset{˙}{⊥} (Y))$

Metamath Proof Explorer

Theorem djhval

Proof