Theorem lssset 19395

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 3455	. . 3 ⊢ (𝑊 ∈ 𝑋 → 𝑊 ∈ V)
3		fveq2 6538	. . . . . . . 8 ⊢ (𝑤 = 𝑊 → (Base‘𝑤) = (Base‘𝑊))
4		lssset.v	. . . . . . . 8 ⊢ 𝑉 = (Base‘𝑊)
5	3, 4	syl6eqr 2849	. . . . . . 7 ⊢ (𝑤 = 𝑊 → (Base‘𝑤) = 𝑉)
6	5	pweqd 4458	. . . . . 6 ⊢ (𝑤 = 𝑊 → 𝒫 (Base‘𝑤) = 𝒫 𝑉)
7	6	difeq1d 4019	. . . . 5 ⊢ (𝑤 = 𝑊 → (𝒫 (Base‘𝑤) ∖ {∅}) = (𝒫 𝑉 ∖ {∅}))
8		fveq2 6538	. . . . . . . . 9 ⊢ (𝑤 = 𝑊 → (Scalar‘𝑤) = (Scalar‘𝑊))
9		lssset.f	. . . . . . . . 9 ⊢ 𝐹 = (Scalar‘𝑊)
10	8, 9	syl6eqr 2849	. . . . . . . 8 ⊢ (𝑤 = 𝑊 → (Scalar‘𝑤) = 𝐹)
11	10	fveq2d 6542	. . . . . . 7 ⊢ (𝑤 = 𝑊 → (Base‘(Scalar‘𝑤)) = (Base‘𝐹))
12		lssset.b	. . . . . . 7 ⊢ 𝐵 = (Base‘𝐹)
13	11, 12	syl6eqr 2849	. . . . . 6 ⊢ (𝑤 = 𝑊 → (Base‘(Scalar‘𝑤)) = 𝐵)
14		fveq2 6538	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑊 → ( ·𝑠 ‘𝑤) = ( ·𝑠 ‘𝑊))
15		lssset.t	. . . . . . . . . . . 12 ⊢ · = ( ·𝑠 ‘𝑊)
16	14, 15	syl6eqr 2849	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑊 → ( ·𝑠 ‘𝑤) = · )
17	16	oveqd 7033	. . . . . . . . . 10 ⊢ (𝑤 = 𝑊 → (𝑥( ·𝑠 ‘𝑤)𝑎) = (𝑥 · 𝑎))
18	17	oveq1d 7031	. . . . . . . . 9 ⊢ (𝑤 = 𝑊 → ((𝑥( ·𝑠 ‘𝑤)𝑎)(+g‘𝑤)𝑏) = ((𝑥 · 𝑎)(+g‘𝑤)𝑏))
19		fveq2 6538	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑊 → (+g‘𝑤) = (+g‘𝑊))
20		lssset.p	. . . . . . . . . . 11 ⊢ + = (+g‘𝑊)
21	19, 20	syl6eqr 2849	. . . . . . . . . 10 ⊢ (𝑤 = 𝑊 → (+g‘𝑤) = + )
22	21	oveqd 7033	. . . . . . . . 9 ⊢ (𝑤 = 𝑊 → ((𝑥 · 𝑎)(+g‘𝑤)𝑏) = ((𝑥 · 𝑎) + 𝑏))
23	18, 22	eqtrd 2831	. . . . . . . 8 ⊢ (𝑤 = 𝑊 → ((𝑥( ·𝑠 ‘𝑤)𝑎)(+g‘𝑤)𝑏) = ((𝑥 · 𝑎) + 𝑏))
24	23	eleq1d 2867	. . . . . . 7 ⊢ (𝑤 = 𝑊 → (((𝑥( ·𝑠 ‘𝑤)𝑎)(+g‘𝑤)𝑏) ∈ 𝑠 ↔ ((𝑥 · 𝑎) + 𝑏) ∈ 𝑠))
25	24	2ralbidv 3166	. . . . . 6 ⊢ (𝑤 = 𝑊 → (∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥( ·𝑠 ‘𝑤)𝑎)(+g‘𝑤)𝑏) ∈ 𝑠 ↔ ∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥 · 𝑎) + 𝑏) ∈ 𝑠))
26	13, 25	raleqbidv 3361	. . . . 5 ⊢ (𝑤 = 𝑊 → (∀𝑥 ∈ (Base‘(Scalar‘𝑤))∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥( ·𝑠 ‘𝑤)𝑎)(+g‘𝑤)𝑏) ∈ 𝑠 ↔ ∀𝑥 ∈ 𝐵 ∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥 · 𝑎) + 𝑏) ∈ 𝑠))
27	7, 26	rabeqbidv 3430	. . . 4 ⊢ (𝑤 = 𝑊 → {𝑠 ∈ (𝒫 (Base‘𝑤) ∖ {∅}) ∣ ∀𝑥 ∈ (Base‘(Scalar‘𝑤))∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥( ·𝑠 ‘𝑤)𝑎)(+g‘𝑤)𝑏) ∈ 𝑠} = {𝑠 ∈ (𝒫 𝑉 ∖ {∅}) ∣ ∀𝑥 ∈ 𝐵 ∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥 · 𝑎) + 𝑏) ∈ 𝑠})
28		df-lss 19394	. . . 4 ⊢ LSubSp = (𝑤 ∈ V ↦ {𝑠 ∈ (𝒫 (Base‘𝑤) ∖ {∅}) ∣ ∀𝑥 ∈ (Base‘(Scalar‘𝑤))∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥( ·𝑠 ‘𝑤)𝑎)(+g‘𝑤)𝑏) ∈ 𝑠})
29	4	fvexi 6552	. . . . . . 7 ⊢ 𝑉 ∈ V
30	29	pwex 5172	. . . . . 6 ⊢ 𝒫 𝑉 ∈ V
31	30	difexi 5123	. . . . 5 ⊢ (𝒫 𝑉 ∖ {∅}) ∈ V
32	31	rabex 5126	. . . 4 ⊢ {𝑠 ∈ (𝒫 𝑉 ∖ {∅}) ∣ ∀𝑥 ∈ 𝐵 ∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥 · 𝑎) + 𝑏) ∈ 𝑠} ∈ V
33	27, 28, 32	fvmpt 6635	. . 3 ⊢ (𝑊 ∈ V → (LSubSp‘𝑊) = {𝑠 ∈ (𝒫 𝑉 ∖ {∅}) ∣ ∀𝑥 ∈ 𝐵 ∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥 · 𝑎) + 𝑏) ∈ 𝑠})
34	2, 33	syl 17	. 2 ⊢ (𝑊 ∈ 𝑋 → (LSubSp‘𝑊) = {𝑠 ∈ (𝒫 𝑉 ∖ {∅}) ∣ ∀𝑥 ∈ 𝐵 ∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥 · 𝑎) + 𝑏) ∈ 𝑠})
35	1, 34	syl5eq 2843	1 ⊢ (𝑊 ∈ 𝑋 → 𝑆 = {𝑠 ∈ (𝒫 𝑉 ∖ {∅}) ∣ ∀𝑥 ∈ 𝐵 ∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥 · 𝑎) + 𝑏) ∈ 𝑠})

Syntax hints:   → wi 4   = wceq 1522   ∈ wcel 2081  ∀wral 3105  {crab 3109  Vcvv 3437   ∖ cdif 3856  ∅c0 4211  𝒫 cpw 4453  {csn 4472  ‘cfv 6225  (class class class)co 7016  Basecbs 16312  +_gcplusg 16394  Scalarcsca 16397   ·_𝑠 cvsca 16398  LSubSpclss 19393

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-sep 5094  ax-nul 5101  ax-pow 5157  ax-pr 5221

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ral 3110  df-rex 3111  df-rab 3114  df-v 3439  df-sbc 3707  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-nul 4212  df-if 4382  df-pw 4455  df-sn 4473  df-pr 4475  df-op 4479  df-uni 4746  df-br 4963  df-opab 5025  df-mpt 5042  df-id 5348  df-xp 5449  df-rel 5450  df-cnv 5451  df-co 5452  df-dm 5453  df-iota 6189  df-fun 6227  df-fv 6233  df-ov 7019  df-lss 19394

This theorem is referenced by:  islss  19396