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	⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )