djhsumss

Description: Subspace sum is a subset of subspace join. (Contributed by NM, 6-Aug-2014)

	Ref	Expression
Hypotheses	djhsumss.h	$⊢ H = LHyp (K)$
	djhsumss.u	$⊢ U = DVecH (K) (W)$
	djhsumss.v	$⊢ V = {Base}_{U}$
	djhsumss.p	$⊢ \underset{˙}{\oplus} = LSSum (U)$
	djhsumss.j	$⊢ \underset{˙}{\lor} = joinH (K) (W)$
	djhsumss.k	$⊢ φ \to (K \in HL \land W \in H)$
	djhsumss.x	$⊢ φ \to X \subseteq V$
	djhsumss.y	$⊢ φ \to Y \subseteq V$
Assertion	djhsumss	$⊢ φ \to X \underset{˙}{\oplus} Y \subseteq X \underset{˙}{\lor} Y$

Step	Hyp	Ref	Expression
1		djhsumss.h	$⊢ H = LHyp (K)$
2		djhsumss.u	$⊢ U = DVecH (K) (W)$
3		djhsumss.v	$⊢ V = {Base}_{U}$
4		djhsumss.p	$⊢ \underset{˙}{\oplus} = LSSum (U)$
5		djhsumss.j	$⊢ \underset{˙}{\lor} = joinH (K) (W)$
6		djhsumss.k	$⊢ φ \to (K \in HL \land W \in H)$
7		djhsumss.x	$⊢ φ \to X \subseteq V$
8		djhsumss.y	$⊢ φ \to Y \subseteq V$
9		eqid	$⊢ LSpan (U) = LSpan (U)$
10	1 2 6	dvhlmod	$⊢ φ \to U \in LMod$
11	3 9 4 7 8 10	lsmssspx	$⊢ φ \to X \underset{˙}{\oplus} Y \subseteq LSpan (U) (X \cup Y)$
12	1 2 3 9 5 6 7 8	djhspss	$⊢ φ \to LSpan (U) (X \cup Y) \subseteq X \underset{˙}{\lor} Y$
13	11 12	sstrd	$⊢ φ \to X \underset{˙}{\oplus} Y \subseteq X \underset{˙}{\lor} Y$

Metamath Proof Explorer