Metamath Proof Explorer

Theorem islss4

Description: A linear subspace is a subgroup which respects scalar multiplication. (Contributed by Stefan O'Rear, 11-Dec-2014) (Revised by Mario Carneiro, 19-Apr-2016)

Ref Expression
Hypotheses islss4.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
islss4.b ⊢ 𝐵 = ( Base ‘ 𝐹 )
islss4.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
islss4.t ⊢ · = ( ·𝑠 ‘ 𝑊 )
islss4.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
Assertion islss4 ( 𝑊 ∈ LMod → ( 𝑈 ∈ 𝑆 ↔ ( 𝑈 ∈ ( SubGrp ‘ 𝑊 ) ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝑈 ( 𝑎 · 𝑏 ) ∈ 𝑈 ) ) )

Proof

Step Hyp Ref Expression
1 islss4.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2 islss4.b ⊢ 𝐵 = ( Base ‘ 𝐹 )
3 islss4.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
4 islss4.t ⊢ · = ( ·𝑠 ‘ 𝑊 )
5 islss4.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
6 5 lsssubg ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → 𝑈 ∈ ( SubGrp ‘ 𝑊 ) )
7 1 4 2 5 lssvscl ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝑈 ) ) → ( 𝑎 · 𝑏 ) ∈ 𝑈 )
8 7 ralrimivva ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝑈 ( 𝑎 · 𝑏 ) ∈ 𝑈 )
9 6 8 jca ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → ( 𝑈 ∈ ( SubGrp ‘ 𝑊 ) ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝑈 ( 𝑎 · 𝑏 ) ∈ 𝑈 ) )
10 3 subgss ⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝑊 ) → 𝑈 ⊆ 𝑉 )
11 10 ad2antrl ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑈 ∈ ( SubGrp ‘ 𝑊 ) ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝑈 ( 𝑎 · 𝑏 ) ∈ 𝑈 ) ) → 𝑈 ⊆ 𝑉 )
12 eqid ⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
13 12 subg0cl ⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝑊 ) → ( 0g ‘ 𝑊 ) ∈ 𝑈 )
14 13 ne0d ⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝑊 ) → 𝑈 ≠ ∅ )
15 14 ad2antrl ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑈 ∈ ( SubGrp ‘ 𝑊 ) ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝑈 ( 𝑎 · 𝑏 ) ∈ 𝑈 ) ) → 𝑈 ≠ ∅ )
16 eqid ⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
17 16 subgcl ⊢ ( ( 𝑈 ∈ ( SubGrp ‘ 𝑊 ) ∧ ( 𝑎 · 𝑏 ) ∈ 𝑈 ∧ 𝑐 ∈ 𝑈 ) → ( ( 𝑎 · 𝑏 ) ( +g ‘ 𝑊 ) 𝑐 ) ∈ 𝑈 )
18 17 3exp ⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝑊 ) → ( ( 𝑎 · 𝑏 ) ∈ 𝑈 → ( 𝑐 ∈ 𝑈 → ( ( 𝑎 · 𝑏 ) ( +g ‘ 𝑊 ) 𝑐 ) ∈ 𝑈 ) ) )
19 18 adantl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ ( SubGrp ‘ 𝑊 ) ) → ( ( 𝑎 · 𝑏 ) ∈ 𝑈 → ( 𝑐 ∈ 𝑈 → ( ( 𝑎 · 𝑏 ) ( +g ‘ 𝑊 ) 𝑐 ) ∈ 𝑈 ) ) )
20 19 ralrimdv ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ ( SubGrp ‘ 𝑊 ) ) → ( ( 𝑎 · 𝑏 ) ∈ 𝑈 → ∀ 𝑐 ∈ 𝑈 ( ( 𝑎 · 𝑏 ) ( +g ‘ 𝑊 ) 𝑐 ) ∈ 𝑈 ) )
21 20 ralimdv ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ ( SubGrp ‘ 𝑊 ) ) → ( ∀ 𝑏 ∈ 𝑈 ( 𝑎 · 𝑏 ) ∈ 𝑈 → ∀ 𝑏 ∈ 𝑈 ∀ 𝑐 ∈ 𝑈 ( ( 𝑎 · 𝑏 ) ( +g ‘ 𝑊 ) 𝑐 ) ∈ 𝑈 ) )
22 21 ralimdv ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ ( SubGrp ‘ 𝑊 ) ) → ( ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝑈 ( 𝑎 · 𝑏 ) ∈ 𝑈 → ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝑈 ∀ 𝑐 ∈ 𝑈 ( ( 𝑎 · 𝑏 ) ( +g ‘ 𝑊 ) 𝑐 ) ∈ 𝑈 ) )
23 22 impr ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑈 ∈ ( SubGrp ‘ 𝑊 ) ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝑈 ( 𝑎 · 𝑏 ) ∈ 𝑈 ) ) → ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝑈 ∀ 𝑐 ∈ 𝑈 ( ( 𝑎 · 𝑏 ) ( +g ‘ 𝑊 ) 𝑐 ) ∈ 𝑈 )
24 1 2 3 16 4 5 islss ⊢ ( 𝑈 ∈ 𝑆 ↔ ( 𝑈 ⊆ 𝑉 ∧ 𝑈 ≠ ∅ ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝑈 ∀ 𝑐 ∈ 𝑈 ( ( 𝑎 · 𝑏 ) ( +g ‘ 𝑊 ) 𝑐 ) ∈ 𝑈 ) )
25 11 15 23 24 syl3anbrc ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑈 ∈ ( SubGrp ‘ 𝑊 ) ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝑈 ( 𝑎 · 𝑏 ) ∈ 𝑈 ) ) → 𝑈 ∈ 𝑆 )
26 9 25 impbida ⊢ ( 𝑊 ∈ LMod → ( 𝑈 ∈ 𝑆 ↔ ( 𝑈 ∈ ( SubGrp ‘ 𝑊 ) ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝑈 ( 𝑎 · 𝑏 ) ∈ 𝑈 ) ) )