Theorem lssset 20110

Description: The set of all (not necessarily closed) linear subspaces of a left module or left vector space. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 15-Jul-2014.)

Hypotheses

Ref	Expression
lssset.f	⊢ 𝐹 = (Scalar‘𝑊)
lssset.b	⊢ 𝐵 = (Base‘𝐹)
lssset.v	⊢ 𝑉 = (Base‘𝑊)
lssset.p	⊢ + = (+g‘𝑊)
lssset.t	⊢ · = ( ·𝑠 ‘𝑊)
lssset.s	⊢ 𝑆 = (LSubSp‘𝑊)

Assertion

Ref	Expression
lssset	⊢ (𝑊 ∈ 𝑋 → 𝑆 = {𝑠 ∈ (𝒫 𝑉 ∖ {∅}) ∣ ∀𝑥 ∈ 𝐵 ∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥 · 𝑎) + 𝑏) ∈ 𝑠})

Distinct variable groups:   + ,𝑠   𝑥,𝑠,𝐵   𝑉,𝑠   𝑎,𝑏,𝑠,𝑥,𝑊   · ,𝑠

Allowed substitution hints:   𝐵(𝑎,𝑏)   + (𝑥,𝑎,𝑏)   𝑆(𝑥,𝑠,𝑎,𝑏)   · (𝑥,𝑎,𝑏)   𝐹(𝑥,𝑠,𝑎,𝑏)   𝑉(𝑥,𝑎,𝑏)   𝑋(𝑥,𝑠,𝑎,𝑏)

Proof of Theorem lssset

Dummy variable 𝑤 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		lssset.s	. 2 ⊢ 𝑆 = (LSubSp‘𝑊)
2		elex 3440	. . 3 ⊢ (𝑊 ∈ 𝑋 → 𝑊 ∈ V)
3		fveq2 6756	. . . . . . . 8 ⊢ (𝑤 = 𝑊 → (Base‘𝑤) = (Base‘𝑊))
4		lssset.v	. . . . . . . 8 ⊢ 𝑉 = (Base‘𝑊)
5	3, 4	eqtr4di 2797	. . . . . . 7 ⊢ (𝑤 = 𝑊 → (Base‘𝑤) = 𝑉)
6	5	pweqd 4549	. . . . . 6 ⊢ (𝑤 = 𝑊 → 𝒫 (Base‘𝑤) = 𝒫 𝑉)
7	6	difeq1d 4052	. . . . 5 ⊢ (𝑤 = 𝑊 → (𝒫 (Base‘𝑤) ∖ {∅}) = (𝒫 𝑉 ∖ {∅}))
8		fveq2 6756	. . . . . . . . 9 ⊢ (𝑤 = 𝑊 → (Scalar‘𝑤) = (Scalar‘𝑊))
9		lssset.f	. . . . . . . . 9 ⊢ 𝐹 = (Scalar‘𝑊)
10	8, 9	eqtr4di 2797	. . . . . . . 8 ⊢ (𝑤 = 𝑊 → (Scalar‘𝑤) = 𝐹)
11	10	fveq2d 6760	. . . . . . 7 ⊢ (𝑤 = 𝑊 → (Base‘(Scalar‘𝑤)) = (Base‘𝐹))
12		lssset.b	. . . . . . 7 ⊢ 𝐵 = (Base‘𝐹)
13	11, 12	eqtr4di 2797	. . . . . 6 ⊢ (𝑤 = 𝑊 → (Base‘(Scalar‘𝑤)) = 𝐵)
14		fveq2 6756	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑊 → ( ·𝑠 ‘𝑤) = ( ·𝑠 ‘𝑊))
15		lssset.t	. . . . . . . . . . . 12 ⊢ · = ( ·𝑠 ‘𝑊)
16	14, 15	eqtr4di 2797	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑊 → ( ·𝑠 ‘𝑤) = · )
17	16	oveqd 7272	. . . . . . . . . 10 ⊢ (𝑤 = 𝑊 → (𝑥( ·𝑠 ‘𝑤)𝑎) = (𝑥 · 𝑎))
18	17	oveq1d 7270	. . . . . . . . 9 ⊢ (𝑤 = 𝑊 → ((𝑥( ·𝑠 ‘𝑤)𝑎)(+g‘𝑤)𝑏) = ((𝑥 · 𝑎)(+g‘𝑤)𝑏))
19		fveq2 6756	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑊 → (+g‘𝑤) = (+g‘𝑊))
20		lssset.p	. . . . . . . . . . 11 ⊢ + = (+g‘𝑊)
21	19, 20	eqtr4di 2797	. . . . . . . . . 10 ⊢ (𝑤 = 𝑊 → (+g‘𝑤) = + )
22	21	oveqd 7272	. . . . . . . . 9 ⊢ (𝑤 = 𝑊 → ((𝑥 · 𝑎)(+g‘𝑤)𝑏) = ((𝑥 · 𝑎) + 𝑏))
23	18, 22	eqtrd 2778	. . . . . . . 8 ⊢ (𝑤 = 𝑊 → ((𝑥( ·𝑠 ‘𝑤)𝑎)(+g‘𝑤)𝑏) = ((𝑥 · 𝑎) + 𝑏))
24	23	eleq1d 2823	. . . . . . 7 ⊢ (𝑤 = 𝑊 → (((𝑥( ·𝑠 ‘𝑤)𝑎)(+g‘𝑤)𝑏) ∈ 𝑠 ↔ ((𝑥 · 𝑎) + 𝑏) ∈ 𝑠))
25	24	2ralbidv 3122	. . . . . 6 ⊢ (𝑤 = 𝑊 → (∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥( ·𝑠 ‘𝑤)𝑎)(+g‘𝑤)𝑏) ∈ 𝑠 ↔ ∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥 · 𝑎) + 𝑏) ∈ 𝑠))
26	13, 25	raleqbidv 3327	. . . . 5 ⊢ (𝑤 = 𝑊 → (∀𝑥 ∈ (Base‘(Scalar‘𝑤))∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥( ·𝑠 ‘𝑤)𝑎)(+g‘𝑤)𝑏) ∈ 𝑠 ↔ ∀𝑥 ∈ 𝐵 ∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥 · 𝑎) + 𝑏) ∈ 𝑠))
27	7, 26	rabeqbidv 3410	. . . 4 ⊢ (𝑤 = 𝑊 → {𝑠 ∈ (𝒫 (Base‘𝑤) ∖ {∅}) ∣ ∀𝑥 ∈ (Base‘(Scalar‘𝑤))∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥( ·𝑠 ‘𝑤)𝑎)(+g‘𝑤)𝑏) ∈ 𝑠} = {𝑠 ∈ (𝒫 𝑉 ∖ {∅}) ∣ ∀𝑥 ∈ 𝐵 ∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥 · 𝑎) + 𝑏) ∈ 𝑠})
28		df-lss 20109	. . . 4 ⊢ LSubSp = (𝑤 ∈ V ↦ {𝑠 ∈ (𝒫 (Base‘𝑤) ∖ {∅}) ∣ ∀𝑥 ∈ (Base‘(Scalar‘𝑤))∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥( ·𝑠 ‘𝑤)𝑎)(+g‘𝑤)𝑏) ∈ 𝑠})
29	4	fvexi 6770	. . . . . . 7 ⊢ 𝑉 ∈ V
30	29	pwex 5298	. . . . . 6 ⊢ 𝒫 𝑉 ∈ V
31	30	difexi 5247	. . . . 5 ⊢ (𝒫 𝑉 ∖ {∅}) ∈ V
32	31	rabex 5251	. . . 4 ⊢ {𝑠 ∈ (𝒫 𝑉 ∖ {∅}) ∣ ∀𝑥 ∈ 𝐵 ∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥 · 𝑎) + 𝑏) ∈ 𝑠} ∈ V
33	27, 28, 32	fvmpt 6857	. . 3 ⊢ (𝑊 ∈ V → (LSubSp‘𝑊) = {𝑠 ∈ (𝒫 𝑉 ∖ {∅}) ∣ ∀𝑥 ∈ 𝐵 ∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥 · 𝑎) + 𝑏) ∈ 𝑠})
34	2, 33	syl 17	. 2 ⊢ (𝑊 ∈ 𝑋 → (LSubSp‘𝑊) = {𝑠 ∈ (𝒫 𝑉 ∖ {∅}) ∣ ∀𝑥 ∈ 𝐵 ∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥 · 𝑎) + 𝑏) ∈ 𝑠})
35	1, 34	eqtrid 2790	1 ⊢ (𝑊 ∈ 𝑋 → 𝑆 = {𝑠 ∈ (𝒫 𝑉 ∖ {∅}) ∣ ∀𝑥 ∈ 𝐵 ∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥 · 𝑎) + 𝑏) ∈ 𝑠})

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2108  ∀wral 3063  {crab 3067  Vcvv 3422   ∖ cdif 3880  ∅c0 4253  𝒫 cpw 4530  {csn 4558  ‘cfv 6418  (class class class)co 7255  Basecbs 16840  +_gcplusg 16888  Scalarcsca 16891   ·_𝑠 cvsca 16892  LSubSpclss 20108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-iota 6376  df-fun 6420  df-fv 6426  df-ov 7258  df-lss 20109

This theorem is referenced by:  islss  20111