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	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	lsscl.b	⊢ 𝐵 = ( Base ‘ 𝐹 )
	lsscl.p	⊢ + = ( +g ‘ 𝑊 )
	lsscl.t	⊢ · = ( ·𝑠 ‘ 𝑊 )
	lsscl.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
Assertion	lsscl	⊢ ( ( 𝑈 ∈ 𝑆 ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) ) → ( ( 𝑍 · 𝑋 ) + 𝑌 ) ∈ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		lsscl.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2		lsscl.b	⊢ 𝐵 = ( Base ‘ 𝐹 )
3		lsscl.p	⊢ + = ( +g ‘ 𝑊 )
4		lsscl.t	⊢ · = ( ·𝑠 ‘ 𝑊 )
5		lsscl.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
6		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
7	1 2 6 3 4 5	islss	⊢ ( 𝑈 ∈ 𝑆 ↔ ( 𝑈 ⊆ ( Base ‘ 𝑊 ) ∧ 𝑈 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑎 ∈ 𝑈 ∀ 𝑏 ∈ 𝑈 ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑈 ) )
8	7	simp3bi	⊢ ( 𝑈 ∈ 𝑆 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑎 ∈ 𝑈 ∀ 𝑏 ∈ 𝑈 ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑈 )
9		oveq1	⊢ ( 𝑥 = 𝑍 → ( 𝑥 · 𝑎 ) = ( 𝑍 · 𝑎 ) )
10	9	oveq1d	⊢ ( 𝑥 = 𝑍 → ( ( 𝑥 · 𝑎 ) + 𝑏 ) = ( ( 𝑍 · 𝑎 ) + 𝑏 ) )
11	10	eleq1d	⊢ ( 𝑥 = 𝑍 → ( ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑈 ↔ ( ( 𝑍 · 𝑎 ) + 𝑏 ) ∈ 𝑈 ) )
12		oveq2	⊢ ( 𝑎 = 𝑋 → ( 𝑍 · 𝑎 ) = ( 𝑍 · 𝑋 ) )
13	12	oveq1d	⊢ ( 𝑎 = 𝑋 → ( ( 𝑍 · 𝑎 ) + 𝑏 ) = ( ( 𝑍 · 𝑋 ) + 𝑏 ) )
14	13	eleq1d	⊢ ( 𝑎 = 𝑋 → ( ( ( 𝑍 · 𝑎 ) + 𝑏 ) ∈ 𝑈 ↔ ( ( 𝑍 · 𝑋 ) + 𝑏 ) ∈ 𝑈 ) )
15		oveq2	⊢ ( 𝑏 = 𝑌 → ( ( 𝑍 · 𝑋 ) + 𝑏 ) = ( ( 𝑍 · 𝑋 ) + 𝑌 ) )
16	15	eleq1d	⊢ ( 𝑏 = 𝑌 → ( ( ( 𝑍 · 𝑋 ) + 𝑏 ) ∈ 𝑈 ↔ ( ( 𝑍 · 𝑋 ) + 𝑌 ) ∈ 𝑈 ) )
17	11 14 16	rspc3v	⊢ ( ( 𝑍 ∈ 𝐵 ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑎 ∈ 𝑈 ∀ 𝑏 ∈ 𝑈 ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑈 → ( ( 𝑍 · 𝑋 ) + 𝑌 ) ∈ 𝑈 ) )
18	8 17	mpan9	⊢ ( ( 𝑈 ∈ 𝑆 ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) ) → ( ( 𝑍 · 𝑋 ) + 𝑌 ) ∈ 𝑈 )