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	|- .+ = ( +g ` W )
	lsscl.t	|- .x. = ( .s ` W )
	lsscl.s	|- S = ( LSubSp ` W )
Assertion	lsscl	|- ( ( U e. S /\ ( Z e. B /\ X e. U /\ Y e. U ) ) -> ( ( Z .x. X ) .+ Y ) e. U )

Proof

Step	Hyp	Ref	Expression
1		lsscl.f	|- F = ( Scalar ` W )
2		lsscl.b	|- B = ( Base ` F )
3		lsscl.p	|- .+ = ( +g ` W )
4		lsscl.t	|- .x. = ( .s ` W )
5		lsscl.s	|- S = ( LSubSp ` W )
6		eqid	|- ( Base ` W ) = ( Base ` W )
7	1 2 6 3 4 5	islss	|- ( U e. S <-> ( U C_ ( Base ` W ) /\ U =/= (/) /\ A. x e. B A. a e. U A. b e. U ( ( x .x. a ) .+ b ) e. U ) )
8	7	simp3bi	|- ( U e. S -> A. x e. B A. a e. U A. b e. U ( ( x .x. a ) .+ b ) e. U )
9		oveq1	|- ( x = Z -> ( x .x. a ) = ( Z .x. a ) )
10	9	oveq1d	|- ( x = Z -> ( ( x .x. a ) .+ b ) = ( ( Z .x. a ) .+ b ) )
11	10	eleq1d	|- ( x = Z -> ( ( ( x .x. a ) .+ b ) e. U <-> ( ( Z .x. a ) .+ b ) e. U ) )
12		oveq2	|- ( a = X -> ( Z .x. a ) = ( Z .x. X ) )
13	12	oveq1d	|- ( a = X -> ( ( Z .x. a ) .+ b ) = ( ( Z .x. X ) .+ b ) )
14	13	eleq1d	|- ( a = X -> ( ( ( Z .x. a ) .+ b ) e. U <-> ( ( Z .x. X ) .+ b ) e. U ) )
15		oveq2	|- ( b = Y -> ( ( Z .x. X ) .+ b ) = ( ( Z .x. X ) .+ Y ) )
16	15	eleq1d	|- ( b = Y -> ( ( ( Z .x. X ) .+ b ) e. U <-> ( ( Z .x. X ) .+ Y ) e. U ) )
17	11 14 16	rspc3v	|- ( ( Z e. B /\ X e. U /\ Y e. U ) -> ( A. x e. B A. a e. U A. b e. U ( ( x .x. a ) .+ b ) e. U -> ( ( Z .x. X ) .+ Y ) e. U ) )
18	8 17	mpan9	|- ( ( U e. S /\ ( Z e. B /\ X e. U /\ Y e. U ) ) -> ( ( Z .x. X ) .+ Y ) e. U )