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 ‘ 𝑊 ) ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝑈 ( 𝑎 · 𝑏 ) ∈ 𝑈 ) ) )