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 = Base W
lssacs.s ⊢ S = LSubSp ⁡ W
Assertion lssacs ⊢ W ∈ LMod → S ∈ ACS ⁡ B

Proof

Step Hyp Ref Expression
1 lssacs.b ⊢ B = Base W
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 ∈ Base Scalar ⁡ W ∀ y ∈ b x ⋅ W y ∈ b ⊆ b ∈ 𝒫 B | ∀ x ∈ Base Scalar ⁡ W ∀ y ∈ b x ⋅ W y ∈ b
6 ssrab2 ⊢ b ∈ 𝒫 B | ∀ x ∈ Base Scalar ⁡ W ∀ y ∈ b x ⋅ W y ∈ b ⊆ 𝒫 B
7 5 6 sstri ⊢ SubGrp ⁡ W ∩ b ∈ 𝒫 B | ∀ x ∈ Base Scalar ⁡ W ∀ y ∈ b x ⋅ W y ∈ b ⊆ 𝒫 B
8 7 sseli ⊢ a ∈ SubGrp ⁡ W ∩ b ∈ 𝒫 B | ∀ x ∈ Base Scalar ⁡ W ∀ y ∈ b x ⋅ W y ∈ b → a ∈ 𝒫 B
9 8 elpwid ⊢ a ∈ SubGrp ⁡ W ∩ b ∈ 𝒫 B | ∀ x ∈ Base Scalar ⁡ W ∀ y ∈ b x ⋅ W y ∈ b → a ⊆ B
10 9 a1i ⊢ W ∈ LMod → a ∈ SubGrp ⁡ W ∩ b ∈ 𝒫 B | ∀ x ∈ Base Scalar ⁡ W ∀ y ∈ b x ⋅ W y ∈ b → a ⊆ B
11 eqid ⊢ Scalar ⁡ W = Scalar ⁡ W
12 eqid ⊢ Base Scalar ⁡ W = Base Scalar ⁡ W
13 eqid ⊢ ⋅ W = ⋅ W
14 11 12 1 13 2 islss4 ⊢ W ∈ LMod → a ∈ S ↔ a ∈ SubGrp ⁡ W ∧ ∀ x ∈ Base Scalar ⁡ W ∀ y ∈ a x ⋅ W y ∈ a
15 14 adantr ⊢ W ∈ LMod ∧ a ⊆ B → a ∈ S ↔ a ∈ SubGrp ⁡ W ∧ ∀ x ∈ Base Scalar ⁡ W ∀ y ∈ a x ⋅ W y ∈ a
16 velpw ⊢ a ∈ 𝒫 B ↔ a ⊆ B
17 eleq2w ⊢ b = a → x ⋅ W y ∈ b ↔ x ⋅ W y ∈ a
18 17 raleqbi1dv ⊢ b = a → ∀ y ∈ b x ⋅ W y ∈ b ↔ ∀ y ∈ a x ⋅ W y ∈ a
19 18 ralbidv ⊢ b = a → ∀ x ∈ Base Scalar ⁡ W ∀ y ∈ b x ⋅ W y ∈ b ↔ ∀ x ∈ Base Scalar ⁡ W ∀ y ∈ a x ⋅ W y ∈ a
20 19 elrab3 ⊢ a ∈ 𝒫 B → a ∈ b ∈ 𝒫 B | ∀ x ∈ Base Scalar ⁡ W ∀ y ∈ b x ⋅ W y ∈ b ↔ ∀ x ∈ Base Scalar ⁡ W ∀ y ∈ a x ⋅ W y ∈ a
21 16 20 sylbir ⊢ a ⊆ B → a ∈ b ∈ 𝒫 B | ∀ x ∈ Base Scalar ⁡ W ∀ y ∈ b x ⋅ W y ∈ b ↔ ∀ x ∈ Base Scalar ⁡ W ∀ y ∈ a x ⋅ W y ∈ a
22 21 adantl ⊢ W ∈ LMod ∧ a ⊆ B → a ∈ b ∈ 𝒫 B | ∀ x ∈ Base Scalar ⁡ W ∀ y ∈ b x ⋅ W y ∈ b ↔ ∀ x ∈ Base Scalar ⁡ W ∀ y ∈ a x ⋅ W y ∈ a
23 22 anbi2d ⊢ W ∈ LMod ∧ a ⊆ B → a ∈ SubGrp ⁡ W ∧ a ∈ b ∈ 𝒫 B | ∀ x ∈ Base Scalar ⁡ W ∀ y ∈ b x ⋅ W y ∈ b ↔ a ∈ SubGrp ⁡ W ∧ ∀ x ∈ Base Scalar ⁡ W ∀ y ∈ a x ⋅ W y ∈ a
24 15 23 bitr4d ⊢ W ∈ LMod ∧ a ⊆ B → a ∈ S ↔ a ∈ SubGrp ⁡ W ∧ a ∈ b ∈ 𝒫 B | ∀ x ∈ Base Scalar ⁡ W ∀ y ∈ b x ⋅ W y ∈ b
25 elin ⊢ a ∈ SubGrp ⁡ W ∩ b ∈ 𝒫 B | ∀ x ∈ Base Scalar ⁡ W ∀ y ∈ b x ⋅ W y ∈ b ↔ a ∈ SubGrp ⁡ W ∧ a ∈ b ∈ 𝒫 B | ∀ x ∈ Base Scalar ⁡ W ∀ y ∈ b x ⋅ W y ∈ b
26 24 25 syl6bbr ⊢ W ∈ LMod ∧ a ⊆ B → a ∈ S ↔ a ∈ SubGrp ⁡ W ∩ b ∈ 𝒫 B | ∀ x ∈ Base Scalar ⁡ W ∀ y ∈ b x ⋅ W y ∈ b
27 26 ex ⊢ W ∈ LMod → a ⊆ B → a ∈ S ↔ a ∈ SubGrp ⁡ W ∩ b ∈ 𝒫 B | ∀ x ∈ Base Scalar ⁡ W ∀ y ∈ b x ⋅ W y ∈ b
28 4 10 27 pm5.21ndd ⊢ W ∈ LMod → a ∈ S ↔ a ∈ SubGrp ⁡ W ∩ b ∈ 𝒫 B | ∀ x ∈ Base Scalar ⁡ W ∀ y ∈ b x ⋅ W y ∈ b
29 28 eqrdv ⊢ W ∈ LMod → S = SubGrp ⁡ W ∩ b ∈ 𝒫 B | ∀ x ∈ Base Scalar ⁡ W ∀ y ∈ b x ⋅ W y ∈ 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 ∈ Base Scalar ⁡ W ∧ y ∈ B → x ⋅ W y ∈ B
37 36 3expb ⊢ W ∈ LMod ∧ x ∈ Base Scalar ⁡ W ∧ y ∈ B → x ⋅ W y ∈ B
38 37 ralrimivva ⊢ W ∈ LMod → ∀ x ∈ Base Scalar ⁡ W ∀ y ∈ B x ⋅ W y ∈ B
39 acsfn1c ⊢ B ∈ V ∧ ∀ x ∈ Base Scalar ⁡ W ∀ y ∈ B x ⋅ W y ∈ B → b ∈ 𝒫 B | ∀ x ∈ Base Scalar ⁡ W ∀ y ∈ b x ⋅ W y ∈ b ∈ ACS ⁡ B
40 30 38 39 sylancr ⊢ W ∈ LMod → b ∈ 𝒫 B | ∀ x ∈ Base Scalar ⁡ W ∀ y ∈ b x ⋅ W y ∈ b ∈ ACS ⁡ B
41 mreincl ⊢ ACS ⁡ B ∈ Moore ⁡ 𝒫 B ∧ SubGrp ⁡ W ∈ ACS ⁡ B ∧ b ∈ 𝒫 B | ∀ x ∈ Base Scalar ⁡ W ∀ y ∈ b x ⋅ W y ∈ b ∈ ACS ⁡ B → SubGrp ⁡ W ∩ b ∈ 𝒫 B | ∀ x ∈ Base Scalar ⁡ W ∀ y ∈ b x ⋅ W y ∈ b ∈ ACS ⁡ B
42 32 35 40 41 syl3anc ⊢ W ∈ LMod → SubGrp ⁡ W ∩ b ∈ 𝒫 B | ∀ x ∈ Base Scalar ⁡ W ∀ y ∈ b x ⋅ W y ∈ b ∈ ACS ⁡ B
43 29 42 eqeltrd ⊢ W ∈ LMod → S ∈ ACS ⁡ B