Metamath Proof Explorer

Theorem islssd

Description: Properties that determine a subspace of a left module or left vector space. (Contributed by NM, 8-Dec-2013) (Revised by Mario Carneiro, 8-Jan-2015)

Ref Expression
Hypotheses islssd.f ⊢ ( 𝜑 → 𝐹 = ( Scalar ‘ 𝑊 ) )
islssd.b ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐹 ) )
islssd.v ⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑊 ) )
islssd.p ⊢ ( 𝜑 → + = ( +g ‘ 𝑊 ) )
islssd.t ⊢ ( 𝜑 → · = ( ·𝑠 ‘ 𝑊 ) )
islssd.s ⊢ ( 𝜑 → 𝑆 = ( LSubSp ‘ 𝑊 ) )
islssd.u ⊢ ( 𝜑 → 𝑈 ⊆ 𝑉 )
islssd.z ⊢ ( 𝜑 → 𝑈 ≠ ∅ )
islssd.c ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ) → ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑈 )
Assertion islssd ( 𝜑 → 𝑈 ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 islssd.f ⊢ ( 𝜑 → 𝐹 = ( Scalar ‘ 𝑊 ) )
2 islssd.b ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐹 ) )
3 islssd.v ⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑊 ) )
4 islssd.p ⊢ ( 𝜑 → + = ( +g ‘ 𝑊 ) )
5 islssd.t ⊢ ( 𝜑 → · = ( ·𝑠 ‘ 𝑊 ) )
6 islssd.s ⊢ ( 𝜑 → 𝑆 = ( LSubSp ‘ 𝑊 ) )
7 islssd.u ⊢ ( 𝜑 → 𝑈 ⊆ 𝑉 )
8 islssd.z ⊢ ( 𝜑 → 𝑈 ≠ ∅ )
9 islssd.c ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ) → ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑈 )
10 7 3 sseqtrd ⊢ ( 𝜑 → 𝑈 ⊆ ( Base ‘ 𝑊 ) )
11 9 3exp2 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 → ( 𝑎 ∈ 𝑈 → ( 𝑏 ∈ 𝑈 → ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑈 ) ) ) )
12 11 imp43 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ) → ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑈 )
13 12 ralrimivva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ∀ 𝑎 ∈ 𝑈 ∀ 𝑏 ∈ 𝑈 ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑈 )
14 13 ex ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 → ∀ 𝑎 ∈ 𝑈 ∀ 𝑏 ∈ 𝑈 ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑈 ) )
15 1 fveq2d ⊢ ( 𝜑 → ( Base ‘ 𝐹 ) = ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
16 2 15 eqtrd ⊢ ( 𝜑 → 𝐵 = ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
17 16 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↔ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) )
18 4 oveqd ⊢ ( 𝜑 → ( ( 𝑥 · 𝑎 ) + 𝑏 ) = ( ( 𝑥 · 𝑎 ) ( +g ‘ 𝑊 ) 𝑏 ) )
19 5 oveqd ⊢ ( 𝜑 → ( 𝑥 · 𝑎 ) = ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑎 ) )
20 19 oveq1d ⊢ ( 𝜑 → ( ( 𝑥 · 𝑎 ) ( +g ‘ 𝑊 ) 𝑏 ) = ( ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑎 ) ( +g ‘ 𝑊 ) 𝑏 ) )
21 18 20 eqtrd ⊢ ( 𝜑 → ( ( 𝑥 · 𝑎 ) + 𝑏 ) = ( ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑎 ) ( +g ‘ 𝑊 ) 𝑏 ) )
22 21 eleq1d ⊢ ( 𝜑 → ( ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑈 ↔ ( ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑎 ) ( +g ‘ 𝑊 ) 𝑏 ) ∈ 𝑈 ) )
23 22 2ralbidv ⊢ ( 𝜑 → ( ∀ 𝑎 ∈ 𝑈 ∀ 𝑏 ∈ 𝑈 ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑈 ↔ ∀ 𝑎 ∈ 𝑈 ∀ 𝑏 ∈ 𝑈 ( ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑎 ) ( +g ‘ 𝑊 ) 𝑏 ) ∈ 𝑈 ) )
24 14 17 23 3imtr3d ⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) → ∀ 𝑎 ∈ 𝑈 ∀ 𝑏 ∈ 𝑈 ( ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑎 ) ( +g ‘ 𝑊 ) 𝑏 ) ∈ 𝑈 ) )
25 24 ralrimiv ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑎 ∈ 𝑈 ∀ 𝑏 ∈ 𝑈 ( ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑎 ) ( +g ‘ 𝑊 ) 𝑏 ) ∈ 𝑈 )
26 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
27 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
28 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
29 eqid ⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
30 eqid ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
31 eqid ⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
32 26 27 28 29 30 31 islss ⊢ ( 𝑈 ∈ ( LSubSp ‘ 𝑊 ) ↔ ( 𝑈 ⊆ ( Base ‘ 𝑊 ) ∧ 𝑈 ≠ ∅ ∧ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑎 ∈ 𝑈 ∀ 𝑏 ∈ 𝑈 ( ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑎 ) ( +g ‘ 𝑊 ) 𝑏 ) ∈ 𝑈 ) )
33 10 8 25 32 syl3anbrc ⊢ ( 𝜑 → 𝑈 ∈ ( LSubSp ‘ 𝑊 ) )
34 33 6 eleqtrrd ⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )