shsval3i

Description: An alternate way to express subspace sum. (Contributed by NM, 25-Nov-2004) (New usage is discouraged.)

Step	Hyp	Ref	Expression
1		shlesb1.1	$⊢ A \in S_{ℋ}$
2		shlesb1.2	$⊢ B \in S_{ℋ}$
3	1 2	shsval2i	$⊢ A +_{ℋ} B = ⋂ \{x \in S_{ℋ} \| A \cup B \subseteq x\}$
4	1	shssii	$⊢ A \subseteq ℋ$
5	2	shssii	$⊢ B \subseteq ℋ$
6	4 5	unssi	$⊢ A \cup B \subseteq ℋ$
7		spanval	$⊢ A \cup B \subseteq ℋ \to span (A \cup B) = ⋂ \{x \in S_{ℋ} \| A \cup B \subseteq x\}$
8	6 7	ax-mp	$⊢ span (A \cup B) = ⋂ \{x \in S_{ℋ} \| A \cup B \subseteq x\}$
9	3 8	eqtr4i	$⊢ A +_{ℋ} B = span (A \cup B)$

Metamath Proof Explorer