This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐵 = ( Base ‘ 𝑊 )
lssacs.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
Assertion lssacs ( 𝑊 ∈ LMod → 𝑆 ∈ ( ACS ‘ 𝐵 ) )

Proof

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 ‘ 𝐵 ) )