Theorem lssset 21123

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 3474	. . 3 ⊢ (𝑊 ∈ 𝑋 → 𝑊 ∈ V)
3		fveq2 6882	. . . . . . . 8 ⊢ (𝑤 = 𝑊 → (Base‘𝑤) = (Base‘𝑊))
4		lssset.v	. . . . . . . 8 ⊢ 𝑉 = (Base‘𝑊)
5	3, 4	eqtr4di 2815	. . . . . . 7 ⊢ (𝑤 = 𝑊 → (Base‘𝑤) = 𝑉)
6	5	pweqd 4577	. . . . . 6 ⊢ (𝑤 = 𝑊 → 𝒫 (Base‘𝑤) = 𝒫 𝑉)
7	6	difeq1d 4076	. . . . 5 ⊢ (𝑤 = 𝑊 → (𝒫 (Base‘𝑤) ∖ {∅}) = (𝒫 𝑉 ∖ {∅}))
8		fveq2 6882	. . . . . . . . 9 ⊢ (𝑤 = 𝑊 → (Scalar‘𝑤) = (Scalar‘𝑊))
9		lssset.f	. . . . . . . . 9 ⊢ 𝐹 = (Scalar‘𝑊)
10	8, 9	eqtr4di 2815	. . . . . . . 8 ⊢ (𝑤 = 𝑊 → (Scalar‘𝑤) = 𝐹)
11	10	fveq2d 6886	. . . . . . 7 ⊢ (𝑤 = 𝑊 → (Base‘(Scalar‘𝑤)) = (Base‘𝐹))
12		lssset.b	. . . . . . 7 ⊢ 𝐵 = (Base‘𝐹)
13	11, 12	eqtr4di 2815	. . . . . 6 ⊢ (𝑤 = 𝑊 → (Base‘(Scalar‘𝑤)) = 𝐵)
14		fveq2 6882	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑊 → ( ·𝑠 ‘𝑤) = ( ·𝑠 ‘𝑊))
15		lssset.t	. . . . . . . . . . . 12 ⊢ · = ( ·𝑠 ‘𝑊)
16	14, 15	eqtr4di 2815	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑊 → ( ·𝑠 ‘𝑤) = · )
17	16	oveqd 7434	. . . . . . . . . 10 ⊢ (𝑤 = 𝑊 → (𝑥( ·𝑠 ‘𝑤)𝑎) = (𝑥 · 𝑎))
18	17	oveq1d 7432	. . . . . . . . 9 ⊢ (𝑤 = 𝑊 → ((𝑥( ·𝑠 ‘𝑤)𝑎)(+g‘𝑤)𝑏) = ((𝑥 · 𝑎)(+g‘𝑤)𝑏))
19		fveq2 6882	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑊 → (+g‘𝑤) = (+g‘𝑊))
20		lssset.p	. . . . . . . . . . 11 ⊢ + = (+g‘𝑊)
21	19, 20	eqtr4di 2815	. . . . . . . . . 10 ⊢ (𝑤 = 𝑊 → (+g‘𝑤) = + )
22	21	oveqd 7434	. . . . . . . . 9 ⊢ (𝑤 = 𝑊 → ((𝑥 · 𝑎)(+g‘𝑤)𝑏) = ((𝑥 · 𝑎) + 𝑏))
23	18, 22	eqtrd 2797	. . . . . . . 8 ⊢ (𝑤 = 𝑊 → ((𝑥( ·𝑠 ‘𝑤)𝑎)(+g‘𝑤)𝑏) = ((𝑥 · 𝑎) + 𝑏))
24	23	eleq1d 2847	. . . . . . 7 ⊢ (𝑤 = 𝑊 → (((𝑥( ·𝑠 ‘𝑤)𝑎)(+g‘𝑤)𝑏) ∈ 𝑠 ↔ ((𝑥 · 𝑎) + 𝑏) ∈ 𝑠))
25	24	2ralbidv 3228	. . . . . 6 ⊢ (𝑤 = 𝑊 → (∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥( ·𝑠 ‘𝑤)𝑎)(+g‘𝑤)𝑏) ∈ 𝑠 ↔ ∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥 · 𝑎) + 𝑏) ∈ 𝑠))
26	13, 25	raleqbidv 3336	. . . . 5 ⊢ (𝑤 = 𝑊 → (∀𝑥 ∈ (Base‘(Scalar‘𝑤))∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥( ·𝑠 ‘𝑤)𝑎)(+g‘𝑤)𝑏) ∈ 𝑠 ↔ ∀𝑥 ∈ 𝐵 ∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥 · 𝑎) + 𝑏) ∈ 𝑠))
27	7, 26	rabeqbidv 3432	. . . 4 ⊢ (𝑤 = 𝑊 → {𝑠 ∈ (𝒫 (Base‘𝑤) ∖ {∅}) ∣ ∀𝑥 ∈ (Base‘(Scalar‘𝑤))∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥( ·𝑠 ‘𝑤)𝑎)(+g‘𝑤)𝑏) ∈ 𝑠} = {𝑠 ∈ (𝒫 𝑉 ∖ {∅}) ∣ ∀𝑥 ∈ 𝐵 ∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥 · 𝑎) + 𝑏) ∈ 𝑠})
28		df-lss 21122	. . . 4 ⊢ LSubSp = (𝑤 ∈ V ↦ {𝑠 ∈ (𝒫 (Base‘𝑤) ∖ {∅}) ∣ ∀𝑥 ∈ (Base‘(Scalar‘𝑤))∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥( ·𝑠 ‘𝑤)𝑎)(+g‘𝑤)𝑏) ∈ 𝑠})
29	4	fvexi 6896	. . . . . . 7 ⊢ 𝑉 ∈ V
30	29	pwex 5349	. . . . . 6 ⊢ 𝒫 𝑉 ∈ V
31	30	difexi 5299	. . . . 5 ⊢ (𝒫 𝑉 ∖ {∅}) ∈ V
32	31	rabex 5307	. . . 4 ⊢ {𝑠 ∈ (𝒫 𝑉 ∖ {∅}) ∣ ∀𝑥 ∈ 𝐵 ∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥 · 𝑎) + 𝑏) ∈ 𝑠} ∈ V
33	27, 28, 32	fvmpt 6990	. . 3 ⊢ (𝑊 ∈ V → (LSubSp‘𝑊) = {𝑠 ∈ (𝒫 𝑉 ∖ {∅}) ∣ ∀𝑥 ∈ 𝐵 ∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥 · 𝑎) + 𝑏) ∈ 𝑠})
34	2, 33	syl 18	. 2 ⊢ (𝑊 ∈ 𝑋 → (LSubSp‘𝑊) = {𝑠 ∈ (𝒫 𝑉 ∖ {∅}) ∣ ∀𝑥 ∈ 𝐵 ∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥 · 𝑎) + 𝑏) ∈ 𝑠})
35	1, 34	eqtrid 2809	1 ⊢ (𝑊 ∈ 𝑋 → 𝑆 = {𝑠 ∈ (𝒫 𝑉 ∖ {∅}) ∣ ∀𝑥 ∈ 𝐵 ∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥 · 𝑎) + 𝑏) ∈ 𝑠})

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  ∀wral 3078  {crab 3414  Vcvv 3453   ∖ cdif 3899  ∅c0 4282  𝒫 cpw 4560  {csn 4587  ‘cfv 6537  (class class class)co 7417  Basecbs 17307  +_gcplusg 17348  Scalarcsca 17351   ·_𝑠 cvsca 17352  LSubSpclss 21121

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-iota 6493  df-fun 6539  df-fv 6545  df-ov 7420  df-lss 21122

This theorem is used by:  islss  21124