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 bitr4di 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