Metamath Proof Explorer

Theorem lssacs

Description: Submodules are an algebraic closure system. (Contributed by Stefan O'Rear, 4-Apr-2015)

Ref Expression
Hypotheses lssacs.b ⊢B=BaseW
lssacs.s ⊢S=LSubSp⁡W
Assertion lssacs ⊢W∈LMod→S∈ACS⁡B

Proof

Step Hyp Ref Expression
1 lssacs.b ⊢B=BaseW
2 lssacs.s ⊢S=LSubSp⁡W
3 1 2 lssss ⊢a∈S→a⊆B
4 3 a1i ⊢W∈LMod→a∈S→a⊆B
5 inss2 ⊢SubGrp⁡W∩b∈𝒫B|∀x∈BaseScalar⁡W∀y∈bx⋅Wy∈b⊆b∈𝒫B|∀x∈BaseScalar⁡W∀y∈bx⋅Wy∈b
6 ssrab2 ⊢b∈𝒫B|∀x∈BaseScalar⁡W∀y∈bx⋅Wy∈b⊆𝒫B
7 5 6 sstri ⊢SubGrp⁡W∩b∈𝒫B|∀x∈BaseScalar⁡W∀y∈bx⋅Wy∈b⊆𝒫B
8 7 sseli ⊢a∈SubGrp⁡W∩b∈𝒫B|∀x∈BaseScalar⁡W∀y∈bx⋅Wy∈b→a∈𝒫B
9 8 elpwid ⊢a∈SubGrp⁡W∩b∈𝒫B|∀x∈BaseScalar⁡W∀y∈bx⋅Wy∈b→a⊆B
10 9 a1i ⊢W∈LMod→a∈SubGrp⁡W∩b∈𝒫B|∀x∈BaseScalar⁡W∀y∈bx⋅Wy∈b→a⊆B
11 eqid ⊢Scalar⁡W=Scalar⁡W
12 eqid ⊢BaseScalar⁡W=BaseScalar⁡W
13 eqid ⊢⋅W=⋅W
14 11 12 1 13 2 islss4 ⊢W∈LMod→a∈S↔a∈SubGrp⁡W∧∀x∈BaseScalar⁡W∀y∈ax⋅Wy∈a
15 14 adantr ⊢W∈LMod∧a⊆B→a∈S↔a∈SubGrp⁡W∧∀x∈BaseScalar⁡W∀y∈ax⋅Wy∈a
16 velpw ⊢a∈𝒫B↔a⊆B
17 eleq2w ⊢b=a→x⋅Wy∈b↔x⋅Wy∈a
18 17 raleqbi1dv ⊢b=a→∀y∈bx⋅Wy∈b↔∀y∈ax⋅Wy∈a
19 18 ralbidv ⊢b=a→∀x∈BaseScalar⁡W∀y∈bx⋅Wy∈b↔∀x∈BaseScalar⁡W∀y∈ax⋅Wy∈a
20 19 elrab3 ⊢a∈𝒫B→a∈b∈𝒫B|∀x∈BaseScalar⁡W∀y∈bx⋅Wy∈b↔∀x∈BaseScalar⁡W∀y∈ax⋅Wy∈a
21 16 20 sylbir ⊢a⊆B→a∈b∈𝒫B|∀x∈BaseScalar⁡W∀y∈bx⋅Wy∈b↔∀x∈BaseScalar⁡W∀y∈ax⋅Wy∈a
22 21 adantl ⊢W∈LMod∧a⊆B→a∈b∈𝒫B|∀x∈BaseScalar⁡W∀y∈bx⋅Wy∈b↔∀x∈BaseScalar⁡W∀y∈ax⋅Wy∈a
23 22 anbi2d ⊢W∈LMod∧a⊆B→a∈SubGrp⁡W∧a∈b∈𝒫B|∀x∈BaseScalar⁡W∀y∈bx⋅Wy∈b↔a∈SubGrp⁡W∧∀x∈BaseScalar⁡W∀y∈ax⋅Wy∈a
24 15 23 bitr4d ⊢W∈LMod∧a⊆B→a∈S↔a∈SubGrp⁡W∧a∈b∈𝒫B|∀x∈BaseScalar⁡W∀y∈bx⋅Wy∈b
25 elin ⊢a∈SubGrp⁡W∩b∈𝒫B|∀x∈BaseScalar⁡W∀y∈bx⋅Wy∈b↔a∈SubGrp⁡W∧a∈b∈𝒫B|∀x∈BaseScalar⁡W∀y∈bx⋅Wy∈b
26 24 25 bitr4di ⊢W∈LMod∧a⊆B→a∈S↔a∈SubGrp⁡W∩b∈𝒫B|∀x∈BaseScalar⁡W∀y∈bx⋅Wy∈b
27 26 ex ⊢W∈LMod→a⊆B→a∈S↔a∈SubGrp⁡W∩b∈𝒫B|∀x∈BaseScalar⁡W∀y∈bx⋅Wy∈b
28 4 10 27 pm5.21ndd ⊢W∈LMod→a∈S↔a∈SubGrp⁡W∩b∈𝒫B|∀x∈BaseScalar⁡W∀y∈bx⋅Wy∈b
29 28 eqrdv ⊢W∈LMod→S=SubGrp⁡W∩b∈𝒫B|∀x∈BaseScalar⁡W∀y∈bx⋅Wy∈b
30 1 fvexi ⊢B∈V
31 mreacs ⊢B∈V→ACS⁡B∈Moore⁡𝒫B
32 30 31 mp1i ⊢W∈LMod→ACS⁡B∈Moore⁡𝒫B
33 lmodgrp ⊢W∈LMod→W∈Grp
34 1 subgacs ⊢W∈Grp→SubGrp⁡W∈ACS⁡B
35 33 34 syl ⊢W∈LMod→SubGrp⁡W∈ACS⁡B
36 1 11 13 12 lmodvscl ⊢W∈LMod∧x∈BaseScalar⁡W∧y∈B→x⋅Wy∈B
37 36 3expb ⊢W∈LMod∧x∈BaseScalar⁡W∧y∈B→x⋅Wy∈B
38 37 ralrimivva ⊢W∈LMod→∀x∈BaseScalar⁡W∀y∈Bx⋅Wy∈B
39 acsfn1c ⊢B∈V∧∀x∈BaseScalar⁡W∀y∈Bx⋅Wy∈B→b∈𝒫B|∀x∈BaseScalar⁡W∀y∈bx⋅Wy∈b∈ACS⁡B
40 30 38 39 sylancr ⊢W∈LMod→b∈𝒫B|∀x∈BaseScalar⁡W∀y∈bx⋅Wy∈b∈ACS⁡B
41 mreincl ⊢ACS⁡B∈Moore⁡𝒫B∧SubGrp⁡W∈ACS⁡B∧b∈𝒫B|∀x∈BaseScalar⁡W∀y∈bx⋅Wy∈b∈ACS⁡B→SubGrp⁡W∩b∈𝒫B|∀x∈BaseScalar⁡W∀y∈bx⋅Wy∈b∈ACS⁡B
42 32 35 40 41 syl3anc ⊢W∈LMod→SubGrp⁡W∩b∈𝒫B|∀x∈BaseScalar⁡W∀y∈bx⋅Wy∈b∈ACS⁡B
43 29 42 eqeltrd ⊢W∈LMod→S∈ACS⁡B