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 ⊢ 𝐹 = ( 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 ⊢ ( ( 𝑈 ∈ 𝑆 ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) ) → ( ( 𝑍 · 𝑋 ) + 𝑌 ) ∈ 𝑈 )