lssvscl

Description: Closure of scalar product in a subspace. (Contributed by NM, 11-Jan-2014) (Revised by Mario Carneiro, 19-Jun-2014)

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

Proof

Step	Hyp	Ref	Expression
1		lssvscl.f	$⊢ F = Scalar (W)$
2		lssvscl.t	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
3		lssvscl.b	$⊢ B = {Base}_{F}$
4		lssvscl.s	$⊢ S = LSubSp (W)$
5		simpll	$⊢ ((W \in LMod \land U \in S) \land (X \in B \land Y \in U)) \to W \in LMod$
6		simprl	$⊢ ((W \in LMod \land U \in S) \land (X \in B \land Y \in U)) \to X \in B$
7		eqid	$⊢ {Base}_{W} = {Base}_{W}$
8	7 4	lssel	$⊢ (U \in S \land Y \in U) \to Y \in {Base}_{W}$
9	8	ad2ant2l	$⊢ ((W \in LMod \land U \in S) \land (X \in B \land Y \in U)) \to Y \in {Base}_{W}$
10	7 1 2 3	lmodvscl	$⊢ (W \in LMod \land X \in B \land Y \in {Base}_{W}) \to X \underset{˙}{\cdot} Y \in {Base}_{W}$
11	5 6 9 10	syl3anc	$⊢ ((W \in LMod \land U \in S) \land (X \in B \land Y \in U)) \to X \underset{˙}{\cdot} Y \in {Base}_{W}$
12		eqid	$⊢ +_{W} = +_{W}$
13		eqid	$⊢ 0_{W} = 0_{W}$
14	7 12 13	lmod0vrid	$⊢ (W \in LMod \land X \underset{˙}{\cdot} Y \in {Base}_{W}) \to (X \underset{˙}{\cdot} Y) +_{W} 0_{W} = X \underset{˙}{\cdot} Y$
15	5 11 14	syl2anc	$⊢ ((W \in LMod \land U \in S) \land (X \in B \land Y \in U)) \to (X \underset{˙}{\cdot} Y) +_{W} 0_{W} = X \underset{˙}{\cdot} Y$
16		simplr	$⊢ ((W \in LMod \land U \in S) \land (X \in B \land Y \in U)) \to U \in S$
17		simprr	$⊢ ((W \in LMod \land U \in S) \land (X \in B \land Y \in U)) \to Y \in U$
18	13 4	lss0cl	$⊢ (W \in LMod \land U \in S) \to 0_{W} \in U$
19	18	adantr	$⊢ ((W \in LMod \land U \in S) \land (X \in B \land Y \in U)) \to 0_{W} \in U$
20	1 3 12 2 4	lsscl	$⊢ (U \in S \land (X \in B \land Y \in U \land 0_{W} \in U)) \to (X \underset{˙}{\cdot} Y) +_{W} 0_{W} \in U$
21	16 6 17 19 20	syl13anc	$⊢ ((W \in LMod \land U \in S) \land (X \in B \land Y \in U)) \to (X \underset{˙}{\cdot} Y) +_{W} 0_{W} \in U$
22	15 21	eqeltrrd	$⊢ ((W \in LMod \land U \in S) \land (X \in B \land Y \in U)) \to X \underset{˙}{\cdot} Y \in U$

Metamath Proof Explorer

Theorem lssvscl

Proof