Step |
Hyp |
Ref |
Expression |
1 |
|
lssacs.b |
⊢ 𝐵 = ( Base ‘ 𝑊 ) |
2 |
|
lssacs.s |
⊢ 𝑆 = ( LSubSp ‘ 𝑊 ) |
3 |
1 2
|
lssss |
⊢ ( 𝑎 ∈ 𝑆 → 𝑎 ⊆ 𝐵 ) |
4 |
3
|
a1i |
⊢ ( 𝑊 ∈ LMod → ( 𝑎 ∈ 𝑆 → 𝑎 ⊆ 𝐵 ) ) |
5 |
|
inss2 |
⊢ ( ( SubGrp ‘ 𝑊 ) ∩ { 𝑏 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑏 } ) ⊆ { 𝑏 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑏 } |
6 |
|
ssrab2 |
⊢ { 𝑏 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑏 } ⊆ 𝒫 𝐵 |
7 |
5 6
|
sstri |
⊢ ( ( SubGrp ‘ 𝑊 ) ∩ { 𝑏 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑏 } ) ⊆ 𝒫 𝐵 |
8 |
7
|
sseli |
⊢ ( 𝑎 ∈ ( ( SubGrp ‘ 𝑊 ) ∩ { 𝑏 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑏 } ) → 𝑎 ∈ 𝒫 𝐵 ) |
9 |
8
|
elpwid |
⊢ ( 𝑎 ∈ ( ( SubGrp ‘ 𝑊 ) ∩ { 𝑏 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑏 } ) → 𝑎 ⊆ 𝐵 ) |
10 |
9
|
a1i |
⊢ ( 𝑊 ∈ LMod → ( 𝑎 ∈ ( ( SubGrp ‘ 𝑊 ) ∩ { 𝑏 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑏 } ) → 𝑎 ⊆ 𝐵 ) ) |
11 |
|
eqid |
⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 ) |
12 |
|
eqid |
⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) ) |
13 |
|
eqid |
⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 ) |
14 |
11 12 1 13 2
|
islss4 |
⊢ ( 𝑊 ∈ LMod → ( 𝑎 ∈ 𝑆 ↔ ( 𝑎 ∈ ( SubGrp ‘ 𝑊 ) ∧ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑎 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑎 ) ) ) |
15 |
14
|
adantr |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑎 ⊆ 𝐵 ) → ( 𝑎 ∈ 𝑆 ↔ ( 𝑎 ∈ ( SubGrp ‘ 𝑊 ) ∧ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑎 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑎 ) ) ) |
16 |
|
velpw |
⊢ ( 𝑎 ∈ 𝒫 𝐵 ↔ 𝑎 ⊆ 𝐵 ) |
17 |
|
eleq2w |
⊢ ( 𝑏 = 𝑎 → ( ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑏 ↔ ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑎 ) ) |
18 |
17
|
raleqbi1dv |
⊢ ( 𝑏 = 𝑎 → ( ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑏 ↔ ∀ 𝑦 ∈ 𝑎 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑎 ) ) |
19 |
18
|
ralbidv |
⊢ ( 𝑏 = 𝑎 → ( ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑏 ↔ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑎 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑎 ) ) |
20 |
19
|
elrab3 |
⊢ ( 𝑎 ∈ 𝒫 𝐵 → ( 𝑎 ∈ { 𝑏 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑏 } ↔ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑎 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑎 ) ) |
21 |
16 20
|
sylbir |
⊢ ( 𝑎 ⊆ 𝐵 → ( 𝑎 ∈ { 𝑏 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑏 } ↔ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑎 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑎 ) ) |
22 |
21
|
adantl |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑎 ⊆ 𝐵 ) → ( 𝑎 ∈ { 𝑏 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑏 } ↔ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑎 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑎 ) ) |
23 |
22
|
anbi2d |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑎 ⊆ 𝐵 ) → ( ( 𝑎 ∈ ( SubGrp ‘ 𝑊 ) ∧ 𝑎 ∈ { 𝑏 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑏 } ) ↔ ( 𝑎 ∈ ( SubGrp ‘ 𝑊 ) ∧ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑎 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑎 ) ) ) |
24 |
15 23
|
bitr4d |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑎 ⊆ 𝐵 ) → ( 𝑎 ∈ 𝑆 ↔ ( 𝑎 ∈ ( SubGrp ‘ 𝑊 ) ∧ 𝑎 ∈ { 𝑏 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑏 } ) ) ) |
25 |
|
elin |
⊢ ( 𝑎 ∈ ( ( SubGrp ‘ 𝑊 ) ∩ { 𝑏 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑏 } ) ↔ ( 𝑎 ∈ ( SubGrp ‘ 𝑊 ) ∧ 𝑎 ∈ { 𝑏 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑏 } ) ) |
26 |
24 25
|
bitr4di |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑎 ⊆ 𝐵 ) → ( 𝑎 ∈ 𝑆 ↔ 𝑎 ∈ ( ( SubGrp ‘ 𝑊 ) ∩ { 𝑏 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑏 } ) ) ) |
27 |
26
|
ex |
⊢ ( 𝑊 ∈ LMod → ( 𝑎 ⊆ 𝐵 → ( 𝑎 ∈ 𝑆 ↔ 𝑎 ∈ ( ( SubGrp ‘ 𝑊 ) ∩ { 𝑏 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑏 } ) ) ) ) |
28 |
4 10 27
|
pm5.21ndd |
⊢ ( 𝑊 ∈ LMod → ( 𝑎 ∈ 𝑆 ↔ 𝑎 ∈ ( ( SubGrp ‘ 𝑊 ) ∩ { 𝑏 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑏 } ) ) ) |
29 |
28
|
eqrdv |
⊢ ( 𝑊 ∈ LMod → 𝑆 = ( ( SubGrp ‘ 𝑊 ) ∩ { 𝑏 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑏 } ) ) |
30 |
1
|
fvexi |
⊢ 𝐵 ∈ V |
31 |
|
mreacs |
⊢ ( 𝐵 ∈ V → ( ACS ‘ 𝐵 ) ∈ ( Moore ‘ 𝒫 𝐵 ) ) |
32 |
30 31
|
mp1i |
⊢ ( 𝑊 ∈ LMod → ( ACS ‘ 𝐵 ) ∈ ( Moore ‘ 𝒫 𝐵 ) ) |
33 |
|
lmodgrp |
⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Grp ) |
34 |
1
|
subgacs |
⊢ ( 𝑊 ∈ Grp → ( SubGrp ‘ 𝑊 ) ∈ ( ACS ‘ 𝐵 ) ) |
35 |
33 34
|
syl |
⊢ ( 𝑊 ∈ LMod → ( SubGrp ‘ 𝑊 ) ∈ ( ACS ‘ 𝐵 ) ) |
36 |
1 11 13 12
|
lmodvscl |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝐵 ) |
37 |
36
|
3expb |
⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝐵 ) |
38 |
37
|
ralrimivva |
⊢ ( 𝑊 ∈ LMod → ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝐵 ) |
39 |
|
acsfn1c |
⊢ ( ( 𝐵 ∈ V ∧ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝐵 ) → { 𝑏 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑏 } ∈ ( ACS ‘ 𝐵 ) ) |
40 |
30 38 39
|
sylancr |
⊢ ( 𝑊 ∈ LMod → { 𝑏 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑏 } ∈ ( ACS ‘ 𝐵 ) ) |
41 |
|
mreincl |
⊢ ( ( ( ACS ‘ 𝐵 ) ∈ ( Moore ‘ 𝒫 𝐵 ) ∧ ( SubGrp ‘ 𝑊 ) ∈ ( ACS ‘ 𝐵 ) ∧ { 𝑏 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑏 } ∈ ( ACS ‘ 𝐵 ) ) → ( ( SubGrp ‘ 𝑊 ) ∩ { 𝑏 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑏 } ) ∈ ( ACS ‘ 𝐵 ) ) |
42 |
32 35 40 41
|
syl3anc |
⊢ ( 𝑊 ∈ LMod → ( ( SubGrp ‘ 𝑊 ) ∩ { 𝑏 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑏 } ) ∈ ( ACS ‘ 𝐵 ) ) |
43 |
29 42
|
eqeltrd |
⊢ ( 𝑊 ∈ LMod → 𝑆 ∈ ( ACS ‘ 𝐵 ) ) |