This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lsscl

Description: Closure property of a subspace. (Contributed by NM, 8-Dec-2013) (Revised by Mario Carneiro, 8-Jan-2015)

		Ref	Expression
	Hypotheses	lsscl.f	$⊢ F = Scalar (W)$
		lsscl.b	$⊢ B = {Base}_{F}$
		lsscl.p	$⊢ \underset{˙}{+} = +_{W}$
		lsscl.t	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
		lsscl.s	$⊢ S = LSubSp (W)$
	Assertion	lsscl	$⊢ (U \in S \land (Z \in B \land X \in U \land Y \in U)) \to (Z \underset{˙}{\cdot} X) \underset{˙}{+} Y \in U$

Proof

Step	Hyp	Ref	Expression
1		lsscl.f	$⊢ F = Scalar (W)$
2		lsscl.b	$⊢ B = {Base}_{F}$
3		lsscl.p	$⊢ \underset{˙}{+} = +_{W}$
4		lsscl.t	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
5		lsscl.s	$⊢ S = LSubSp (W)$
6		eqid	$⊢ {Base}_{W} = {Base}_{W}$
7	1 2 6 3 4 5	islss	$⊢ U \in S \leftrightarrow (U \subseteq {Base}_{W} \land U \neq \emptyset \land \forall x \in B \forall a \in U \forall b \in U (x \underset{˙}{\cdot} a) \underset{˙}{+} b \in U)$
8	7	simp3bi	$⊢ U \in S \to \forall x \in B \forall a \in U \forall b \in U (x \underset{˙}{\cdot} a) \underset{˙}{+} b \in U$
9		oveq1	$⊢ x = Z \to x \underset{˙}{\cdot} a = Z \underset{˙}{\cdot} a$
10	9	oveq1d	$⊢ x = Z \to (x \underset{˙}{\cdot} a) \underset{˙}{+} b = (Z \underset{˙}{\cdot} a) \underset{˙}{+} b$
11	10	eleq1d	$⊢ x = Z \to ((x \underset{˙}{\cdot} a) \underset{˙}{+} b \in U \leftrightarrow (Z \underset{˙}{\cdot} a) \underset{˙}{+} b \in U)$
12		oveq2	$⊢ a = X \to Z \underset{˙}{\cdot} a = Z \underset{˙}{\cdot} X$
13	12	oveq1d	$⊢ a = X \to (Z \underset{˙}{\cdot} a) \underset{˙}{+} b = (Z \underset{˙}{\cdot} X) \underset{˙}{+} b$
14	13	eleq1d	$⊢ a = X \to ((Z \underset{˙}{\cdot} a) \underset{˙}{+} b \in U \leftrightarrow (Z \underset{˙}{\cdot} X) \underset{˙}{+} b \in U)$
15		oveq2	$⊢ b = Y \to (Z \underset{˙}{\cdot} X) \underset{˙}{+} b = (Z \underset{˙}{\cdot} X) \underset{˙}{+} Y$
16	15	eleq1d	$⊢ b = Y \to ((Z \underset{˙}{\cdot} X) \underset{˙}{+} b \in U \leftrightarrow (Z \underset{˙}{\cdot} X) \underset{˙}{+} Y \in U)$
17	11 14 16	rspc3v	$⊢ (Z \in B \land X \in U \land Y \in U) \to (\forall x \in B \forall a \in U \forall b \in U (x \underset{˙}{\cdot} a) \underset{˙}{+} b \in U \to (Z \underset{˙}{\cdot} X) \underset{˙}{+} Y \in U)$
18	8 17	mpan9	$⊢ (U \in S \land (Z \in B \land X \in U \land Y \in U)) \to (Z \underset{˙}{\cdot} X) \underset{˙}{+} Y \in U$