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 e. LMod -> S e. ( ACS ` B ) )

Proof

Step Hyp Ref Expression
1 lssacs.b 
 |-  B = ( Base ` W )
2 lssacs.s 
 |-  S = ( LSubSp ` W )
3 1 2 lssss 
 |-  ( a e. S -> a C_ B )
4 3 a1i 
 |-  ( W e. LMod -> ( a e. S -> a C_ B ) )
5 inss2 
 |-  ( ( SubGrp ` W ) i^i { b e. ~P B | A. x e. ( Base ` ( Scalar ` W ) ) A. y e. b ( x ( .s ` W ) y ) e. b } ) C_ { b e. ~P B | A. x e. ( Base ` ( Scalar ` W ) ) A. y e. b ( x ( .s ` W ) y ) e. b }
6 ssrab2 
 |-  { b e. ~P B | A. x e. ( Base ` ( Scalar ` W ) ) A. y e. b ( x ( .s ` W ) y ) e. b } C_ ~P B
7 5 6 sstri 
 |-  ( ( SubGrp ` W ) i^i { b e. ~P B | A. x e. ( Base ` ( Scalar ` W ) ) A. y e. b ( x ( .s ` W ) y ) e. b } ) C_ ~P B
8 7 sseli 
 |-  ( a e. ( ( SubGrp ` W ) i^i { b e. ~P B | A. x e. ( Base ` ( Scalar ` W ) ) A. y e. b ( x ( .s ` W ) y ) e. b } ) -> a e. ~P B )
9 8 elpwid 
 |-  ( a e. ( ( SubGrp ` W ) i^i { b e. ~P B | A. x e. ( Base ` ( Scalar ` W ) ) A. y e. b ( x ( .s ` W ) y ) e. b } ) -> a C_ B )
10 9 a1i 
 |-  ( W e. LMod -> ( a e. ( ( SubGrp ` W ) i^i { b e. ~P B | A. x e. ( Base ` ( Scalar ` W ) ) A. y e. b ( x ( .s ` W ) y ) e. b } ) -> a C_ B ) )
11 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
12 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
13 eqid 
 |-  ( .s ` W ) = ( .s ` W )
14 11 12 1 13 2 islss4 
 |-  ( W e. LMod -> ( a e. S <-> ( a e. ( SubGrp ` W ) /\ A. x e. ( Base ` ( Scalar ` W ) ) A. y e. a ( x ( .s ` W ) y ) e. a ) ) )
15 14 adantr 
 |-  ( ( W e. LMod /\ a C_ B ) -> ( a e. S <-> ( a e. ( SubGrp ` W ) /\ A. x e. ( Base ` ( Scalar ` W ) ) A. y e. a ( x ( .s ` W ) y ) e. a ) ) )
16 velpw 
 |-  ( a e. ~P B <-> a C_ B )
17 eleq2w 
 |-  ( b = a -> ( ( x ( .s ` W ) y ) e. b <-> ( x ( .s ` W ) y ) e. a ) )
18 17 raleqbi1dv 
 |-  ( b = a -> ( A. y e. b ( x ( .s ` W ) y ) e. b <-> A. y e. a ( x ( .s ` W ) y ) e. a ) )
19 18 ralbidv 
 |-  ( b = a -> ( A. x e. ( Base ` ( Scalar ` W ) ) A. y e. b ( x ( .s ` W ) y ) e. b <-> A. x e. ( Base ` ( Scalar ` W ) ) A. y e. a ( x ( .s ` W ) y ) e. a ) )
20 19 elrab3 
 |-  ( a e. ~P B -> ( a e. { b e. ~P B | A. x e. ( Base ` ( Scalar ` W ) ) A. y e. b ( x ( .s ` W ) y ) e. b } <-> A. x e. ( Base ` ( Scalar ` W ) ) A. y e. a ( x ( .s ` W ) y ) e. a ) )
21 16 20 sylbir 
 |-  ( a C_ B -> ( a e. { b e. ~P B | A. x e. ( Base ` ( Scalar ` W ) ) A. y e. b ( x ( .s ` W ) y ) e. b } <-> A. x e. ( Base ` ( Scalar ` W ) ) A. y e. a ( x ( .s ` W ) y ) e. a ) )
22 21 adantl 
 |-  ( ( W e. LMod /\ a C_ B ) -> ( a e. { b e. ~P B | A. x e. ( Base ` ( Scalar ` W ) ) A. y e. b ( x ( .s ` W ) y ) e. b } <-> A. x e. ( Base ` ( Scalar ` W ) ) A. y e. a ( x ( .s ` W ) y ) e. a ) )
23 22 anbi2d 
 |-  ( ( W e. LMod /\ a C_ B ) -> ( ( a e. ( SubGrp ` W ) /\ a e. { b e. ~P B | A. x e. ( Base ` ( Scalar ` W ) ) A. y e. b ( x ( .s ` W ) y ) e. b } ) <-> ( a e. ( SubGrp ` W ) /\ A. x e. ( Base ` ( Scalar ` W ) ) A. y e. a ( x ( .s ` W ) y ) e. a ) ) )
24 15 23 bitr4d 
 |-  ( ( W e. LMod /\ a C_ B ) -> ( a e. S <-> ( a e. ( SubGrp ` W ) /\ a e. { b e. ~P B | A. x e. ( Base ` ( Scalar ` W ) ) A. y e. b ( x ( .s ` W ) y ) e. b } ) ) )
25 elin 
 |-  ( a e. ( ( SubGrp ` W ) i^i { b e. ~P B | A. x e. ( Base ` ( Scalar ` W ) ) A. y e. b ( x ( .s ` W ) y ) e. b } ) <-> ( a e. ( SubGrp ` W ) /\ a e. { b e. ~P B | A. x e. ( Base ` ( Scalar ` W ) ) A. y e. b ( x ( .s ` W ) y ) e. b } ) )
26 24 25 bitr4di 
 |-  ( ( W e. LMod /\ a C_ B ) -> ( a e. S <-> a e. ( ( SubGrp ` W ) i^i { b e. ~P B | A. x e. ( Base ` ( Scalar ` W ) ) A. y e. b ( x ( .s ` W ) y ) e. b } ) ) )
27 26 ex 
 |-  ( W e. LMod -> ( a C_ B -> ( a e. S <-> a e. ( ( SubGrp ` W ) i^i { b e. ~P B | A. x e. ( Base ` ( Scalar ` W ) ) A. y e. b ( x ( .s ` W ) y ) e. b } ) ) ) )
28 4 10 27 pm5.21ndd 
 |-  ( W e. LMod -> ( a e. S <-> a e. ( ( SubGrp ` W ) i^i { b e. ~P B | A. x e. ( Base ` ( Scalar ` W ) ) A. y e. b ( x ( .s ` W ) y ) e. b } ) ) )
29 28 eqrdv 
 |-  ( W e. LMod -> S = ( ( SubGrp ` W ) i^i { b e. ~P B | A. x e. ( Base ` ( Scalar ` W ) ) A. y e. b ( x ( .s ` W ) y ) e. b } ) )
30 1 fvexi 
 |-  B e. _V
31 mreacs 
 |-  ( B e. _V -> ( ACS ` B ) e. ( Moore ` ~P B ) )
32 30 31 mp1i 
 |-  ( W e. LMod -> ( ACS ` B ) e. ( Moore ` ~P B ) )
33 lmodgrp 
 |-  ( W e. LMod -> W e. Grp )
34 1 subgacs 
 |-  ( W e. Grp -> ( SubGrp ` W ) e. ( ACS ` B ) )
35 33 34 syl 
 |-  ( W e. LMod -> ( SubGrp ` W ) e. ( ACS ` B ) )
36 1 11 13 12 lmodvscl 
 |-  ( ( W e. LMod /\ x e. ( Base ` ( Scalar ` W ) ) /\ y e. B ) -> ( x ( .s ` W ) y ) e. B )
37 36 3expb 
 |-  ( ( W e. LMod /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ y e. B ) ) -> ( x ( .s ` W ) y ) e. B )
38 37 ralrimivva 
 |-  ( W e. LMod -> A. x e. ( Base ` ( Scalar ` W ) ) A. y e. B ( x ( .s ` W ) y ) e. B )
39 acsfn1c 
 |-  ( ( B e. _V /\ A. x e. ( Base ` ( Scalar ` W ) ) A. y e. B ( x ( .s ` W ) y ) e. B ) -> { b e. ~P B | A. x e. ( Base ` ( Scalar ` W ) ) A. y e. b ( x ( .s ` W ) y ) e. b } e. ( ACS ` B ) )
40 30 38 39 sylancr 
 |-  ( W e. LMod -> { b e. ~P B | A. x e. ( Base ` ( Scalar ` W ) ) A. y e. b ( x ( .s ` W ) y ) e. b } e. ( ACS ` B ) )
41 mreincl 
 |-  ( ( ( ACS ` B ) e. ( Moore ` ~P B ) /\ ( SubGrp ` W ) e. ( ACS ` B ) /\ { b e. ~P B | A. x e. ( Base ` ( Scalar ` W ) ) A. y e. b ( x ( .s ` W ) y ) e. b } e. ( ACS ` B ) ) -> ( ( SubGrp ` W ) i^i { b e. ~P B | A. x e. ( Base ` ( Scalar ` W ) ) A. y e. b ( x ( .s ` W ) y ) e. b } ) e. ( ACS ` B ) )
42 32 35 40 41 syl3anc 
 |-  ( W e. LMod -> ( ( SubGrp ` W ) i^i { b e. ~P B | A. x e. ( Base ` ( Scalar ` W ) ) A. y e. b ( x ( .s ` W ) y ) e. b } ) e. ( ACS ` B ) )
43 29 42 eqeltrd 
 |-  ( W e. LMod -> S e. ( ACS ` B ) )