djhval2

Description: Value of subspace join for DVecH vector space. (Contributed by NM, 6-Aug-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	djhval2	$⊢ ((K \in HL \land W \in H) \land X \subseteq V \land Y \subseteq V) \to X \underset{˙}{\lor} Y = \underset{˙}{⊥} (\underset{˙}{⊥} (X \cup Y))$

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	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))$
7	6	3impb	$⊢ ((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))$
8	1 2 3 4	dochdmj1	$⊢ ((K \in HL \land W \in H) \land X \subseteq V \land Y \subseteq V) \to \underset{˙}{⊥} (X \cup Y) = \underset{˙}{⊥} (X) \cap \underset{˙}{⊥} (Y)$
9	8	fveq2d	$⊢ ((K \in HL \land W \in H) \land X \subseteq V \land Y \subseteq V) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X \cup Y)) = \underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap \underset{˙}{⊥} (Y))$
10	7 9	eqtr4d	$⊢ ((K \in HL \land W \in H) \land X \subseteq V \land Y \subseteq V) \to X \underset{˙}{\lor} Y = \underset{˙}{⊥} (\underset{˙}{⊥} (X \cup Y))$

Metamath Proof Explorer