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