Theorem islss

Description: The predicate "is 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	lssset.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	lssset.b	⊢ 𝐵 = ( Base ‘ 𝐹 )
	lssset.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lssset.p	⊢ + = ( +g ‘ 𝑊 )
	lssset.t	⊢ · = ( ·𝑠 ‘ 𝑊 )
	lssset.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
Assertion	islss	⊢ ( 𝑈 ∈ 𝑆 ↔ ( 𝑈 ⊆ 𝑉 ∧ 𝑈 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑎 ∈ 𝑈 ∀ 𝑏 ∈ 𝑈 ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑈 ) )

Proof

Step	Hyp	Ref	Expression
1		lssset.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2		lssset.b	⊢ 𝐵 = ( Base ‘ 𝐹 )
3		lssset.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
4		lssset.p	⊢ + = ( +g ‘ 𝑊 )
5		lssset.t	⊢ · = ( ·𝑠 ‘ 𝑊 )
6		lssset.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
7		elfvex	⊢ ( 𝑈 ∈ ( LSubSp ‘ 𝑊 ) → 𝑊 ∈ V )
8	7 6	eleq2s	⊢ ( 𝑈 ∈ 𝑆 → 𝑊 ∈ V )
9		fvprc	⊢ ( ¬ 𝑊 ∈ V → ( Base ‘ 𝑊 ) = ∅ )
10	3 9	eqtrid	⊢ ( ¬ 𝑊 ∈ V → 𝑉 = ∅ )
11	10	sseq2d	⊢ ( ¬ 𝑊 ∈ V → ( 𝑈 ⊆ 𝑉 ↔ 𝑈 ⊆ ∅ ) )
12	11	biimpcd	⊢ ( 𝑈 ⊆ 𝑉 → ( ¬ 𝑊 ∈ V → 𝑈 ⊆ ∅ ) )
13		ss0	⊢ ( 𝑈 ⊆ ∅ → 𝑈 = ∅ )
14	12 13	syl6	⊢ ( 𝑈 ⊆ 𝑉 → ( ¬ 𝑊 ∈ V → 𝑈 = ∅ ) )
15	14	necon1ad	⊢ ( 𝑈 ⊆ 𝑉 → ( 𝑈 ≠ ∅ → 𝑊 ∈ V ) )
16	15	imp	⊢ ( ( 𝑈 ⊆ 𝑉 ∧ 𝑈 ≠ ∅ ) → 𝑊 ∈ V )
17	16	3adant3	⊢ ( ( 𝑈 ⊆ 𝑉 ∧ 𝑈 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑎 ∈ 𝑈 ∀ 𝑏 ∈ 𝑈 ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑈 ) → 𝑊 ∈ V )
18	1 2 3 4 5 6	lssset	⊢ ( 𝑊 ∈ V → 𝑆 = { 𝑠 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑠 } )
19	18	eleq2d	⊢ ( 𝑊 ∈ V → ( 𝑈 ∈ 𝑆 ↔ 𝑈 ∈ { 𝑠 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑠 } ) )
20		eldifsn	⊢ ( 𝑈 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ↔ ( 𝑈 ∈ 𝒫 𝑉 ∧ 𝑈 ≠ ∅ ) )
21	3	fvexi	⊢ 𝑉 ∈ V
22	21	elpw2	⊢ ( 𝑈 ∈ 𝒫 𝑉 ↔ 𝑈 ⊆ 𝑉 )
23	22	anbi1i	⊢ ( ( 𝑈 ∈ 𝒫 𝑉 ∧ 𝑈 ≠ ∅ ) ↔ ( 𝑈 ⊆ 𝑉 ∧ 𝑈 ≠ ∅ ) )
24	20 23	bitri	⊢ ( 𝑈 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ↔ ( 𝑈 ⊆ 𝑉 ∧ 𝑈 ≠ ∅ ) )
25	24	anbi1i	⊢ ( ( 𝑈 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑎 ∈ 𝑈 ∀ 𝑏 ∈ 𝑈 ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑈 ) ↔ ( ( 𝑈 ⊆ 𝑉 ∧ 𝑈 ≠ ∅ ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑎 ∈ 𝑈 ∀ 𝑏 ∈ 𝑈 ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑈 ) )
26		eleq2	⊢ ( 𝑠 = 𝑈 → ( ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑠 ↔ ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑈 ) )
27	26	raleqbi1dv	⊢ ( 𝑠 = 𝑈 → ( ∀ 𝑏 ∈ 𝑠 ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑠 ↔ ∀ 𝑏 ∈ 𝑈 ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑈 ) )
28	27	raleqbi1dv	⊢ ( 𝑠 = 𝑈 → ( ∀ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑠 ↔ ∀ 𝑎 ∈ 𝑈 ∀ 𝑏 ∈ 𝑈 ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑈 ) )
29	28	ralbidv	⊢ ( 𝑠 = 𝑈 → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑠 ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑎 ∈ 𝑈 ∀ 𝑏 ∈ 𝑈 ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑈 ) )
30	29	elrab	⊢ ( 𝑈 ∈ { 𝑠 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑠 } ↔ ( 𝑈 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑎 ∈ 𝑈 ∀ 𝑏 ∈ 𝑈 ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑈 ) )
31		df-3an	⊢ ( ( 𝑈 ⊆ 𝑉 ∧ 𝑈 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑎 ∈ 𝑈 ∀ 𝑏 ∈ 𝑈 ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑈 ) ↔ ( ( 𝑈 ⊆ 𝑉 ∧ 𝑈 ≠ ∅ ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑎 ∈ 𝑈 ∀ 𝑏 ∈ 𝑈 ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑈 ) )
32	25 30 31	3bitr4i	⊢ ( 𝑈 ∈ { 𝑠 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑠 } ↔ ( 𝑈 ⊆ 𝑉 ∧ 𝑈 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑎 ∈ 𝑈 ∀ 𝑏 ∈ 𝑈 ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑈 ) )
33	19 32	bitrdi	⊢ ( 𝑊 ∈ V → ( 𝑈 ∈ 𝑆 ↔ ( 𝑈 ⊆ 𝑉 ∧ 𝑈 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑎 ∈ 𝑈 ∀ 𝑏 ∈ 𝑈 ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑈 ) ) )
34	8 17 33	pm5.21nii	⊢ ( 𝑈 ∈ 𝑆 ↔ ( 𝑈 ⊆ 𝑉 ∧ 𝑈 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑎 ∈ 𝑈 ∀ 𝑏 ∈ 𝑈 ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑈 ) )