Metamath Proof Explorer


Theorem dsmmlss

Description: The finite hull of a product of modules is additionally closed under scalar multiplication and thus is a linear subspace of the product. (Contributed by Stefan O'Rear, 11-Jan-2015)

Ref Expression
Hypotheses dsmmlss.i โŠข ( ๐œ‘ โ†’ ๐ผ โˆˆ ๐‘Š )
dsmmlss.s โŠข ( ๐œ‘ โ†’ ๐‘† โˆˆ Ring )
dsmmlss.r โŠข ( ๐œ‘ โ†’ ๐‘… : ๐ผ โŸถ LMod )
dsmmlss.k โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ผ ) โ†’ ( Scalar โ€˜ ( ๐‘… โ€˜ ๐‘ฅ ) ) = ๐‘† )
dsmmlss.p โŠข ๐‘ƒ = ( ๐‘† Xs ๐‘… )
dsmmlss.u โŠข ๐‘ˆ = ( LSubSp โ€˜ ๐‘ƒ )
dsmmlss.h โŠข ๐ป = ( Base โ€˜ ( ๐‘† โŠ•m ๐‘… ) )
Assertion dsmmlss ( ๐œ‘ โ†’ ๐ป โˆˆ ๐‘ˆ )

Proof

Step Hyp Ref Expression
1 dsmmlss.i โŠข ( ๐œ‘ โ†’ ๐ผ โˆˆ ๐‘Š )
2 dsmmlss.s โŠข ( ๐œ‘ โ†’ ๐‘† โˆˆ Ring )
3 dsmmlss.r โŠข ( ๐œ‘ โ†’ ๐‘… : ๐ผ โŸถ LMod )
4 dsmmlss.k โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ผ ) โ†’ ( Scalar โ€˜ ( ๐‘… โ€˜ ๐‘ฅ ) ) = ๐‘† )
5 dsmmlss.p โŠข ๐‘ƒ = ( ๐‘† Xs ๐‘… )
6 dsmmlss.u โŠข ๐‘ˆ = ( LSubSp โ€˜ ๐‘ƒ )
7 dsmmlss.h โŠข ๐ป = ( Base โ€˜ ( ๐‘† โŠ•m ๐‘… ) )
8 lmodgrp โŠข ( ๐‘Ž โˆˆ LMod โ†’ ๐‘Ž โˆˆ Grp )
9 8 ssriv โŠข LMod โŠ† Grp
10 fss โŠข ( ( ๐‘… : ๐ผ โŸถ LMod โˆง LMod โŠ† Grp ) โ†’ ๐‘… : ๐ผ โŸถ Grp )
11 3 9 10 sylancl โŠข ( ๐œ‘ โ†’ ๐‘… : ๐ผ โŸถ Grp )
12 5 7 1 2 11 dsmmsubg โŠข ( ๐œ‘ โ†’ ๐ป โˆˆ ( SubGrp โ€˜ ๐‘ƒ ) )
13 5 2 1 3 4 prdslmodd โŠข ( ๐œ‘ โ†’ ๐‘ƒ โˆˆ LMod )
14 13 adantr โŠข ( ( ๐œ‘ โˆง ( ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘ƒ ) ) โˆง ๐‘ โˆˆ ๐ป ) ) โ†’ ๐‘ƒ โˆˆ LMod )
15 simprl โŠข ( ( ๐œ‘ โˆง ( ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘ƒ ) ) โˆง ๐‘ โˆˆ ๐ป ) ) โ†’ ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘ƒ ) ) )
16 simprr โŠข ( ( ๐œ‘ โˆง ( ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘ƒ ) ) โˆง ๐‘ โˆˆ ๐ป ) ) โ†’ ๐‘ โˆˆ ๐ป )
17 eqid โŠข ( ๐‘† โŠ•m ๐‘… ) = ( ๐‘† โŠ•m ๐‘… )
18 eqid โŠข ( Base โ€˜ ๐‘ƒ ) = ( Base โ€˜ ๐‘ƒ )
19 3 ffnd โŠข ( ๐œ‘ โ†’ ๐‘… Fn ๐ผ )
20 5 17 18 7 1 19 dsmmelbas โŠข ( ๐œ‘ โ†’ ( ๐‘ โˆˆ ๐ป โ†” ( ๐‘ โˆˆ ( Base โ€˜ ๐‘ƒ ) โˆง { ๐‘ฅ โˆˆ ๐ผ โˆฃ ( ๐‘ โ€˜ ๐‘ฅ ) โ‰  ( 0g โ€˜ ( ๐‘… โ€˜ ๐‘ฅ ) ) } โˆˆ Fin ) ) )
21 20 adantr โŠข ( ( ๐œ‘ โˆง ( ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘ƒ ) ) โˆง ๐‘ โˆˆ ๐ป ) ) โ†’ ( ๐‘ โˆˆ ๐ป โ†” ( ๐‘ โˆˆ ( Base โ€˜ ๐‘ƒ ) โˆง { ๐‘ฅ โˆˆ ๐ผ โˆฃ ( ๐‘ โ€˜ ๐‘ฅ ) โ‰  ( 0g โ€˜ ( ๐‘… โ€˜ ๐‘ฅ ) ) } โˆˆ Fin ) ) )
22 16 21 mpbid โŠข ( ( ๐œ‘ โˆง ( ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘ƒ ) ) โˆง ๐‘ โˆˆ ๐ป ) ) โ†’ ( ๐‘ โˆˆ ( Base โ€˜ ๐‘ƒ ) โˆง { ๐‘ฅ โˆˆ ๐ผ โˆฃ ( ๐‘ โ€˜ ๐‘ฅ ) โ‰  ( 0g โ€˜ ( ๐‘… โ€˜ ๐‘ฅ ) ) } โˆˆ Fin ) )
23 22 simpld โŠข ( ( ๐œ‘ โˆง ( ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘ƒ ) ) โˆง ๐‘ โˆˆ ๐ป ) ) โ†’ ๐‘ โˆˆ ( Base โ€˜ ๐‘ƒ ) )
24 eqid โŠข ( Scalar โ€˜ ๐‘ƒ ) = ( Scalar โ€˜ ๐‘ƒ )
25 eqid โŠข ( ยท๐‘  โ€˜ ๐‘ƒ ) = ( ยท๐‘  โ€˜ ๐‘ƒ )
26 eqid โŠข ( Base โ€˜ ( Scalar โ€˜ ๐‘ƒ ) ) = ( Base โ€˜ ( Scalar โ€˜ ๐‘ƒ ) )
27 18 24 25 26 lmodvscl โŠข ( ( ๐‘ƒ โˆˆ LMod โˆง ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘ƒ ) ) โˆง ๐‘ โˆˆ ( Base โ€˜ ๐‘ƒ ) ) โ†’ ( ๐‘Ž ( ยท๐‘  โ€˜ ๐‘ƒ ) ๐‘ ) โˆˆ ( Base โ€˜ ๐‘ƒ ) )
28 14 15 23 27 syl3anc โŠข ( ( ๐œ‘ โˆง ( ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘ƒ ) ) โˆง ๐‘ โˆˆ ๐ป ) ) โ†’ ( ๐‘Ž ( ยท๐‘  โ€˜ ๐‘ƒ ) ๐‘ ) โˆˆ ( Base โ€˜ ๐‘ƒ ) )
29 22 simprd โŠข ( ( ๐œ‘ โˆง ( ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘ƒ ) ) โˆง ๐‘ โˆˆ ๐ป ) ) โ†’ { ๐‘ฅ โˆˆ ๐ผ โˆฃ ( ๐‘ โ€˜ ๐‘ฅ ) โ‰  ( 0g โ€˜ ( ๐‘… โ€˜ ๐‘ฅ ) ) } โˆˆ Fin )
30 eqid โŠข ( Base โ€˜ ๐‘† ) = ( Base โ€˜ ๐‘† )
31 2 ad2antrr โŠข ( ( ( ๐œ‘ โˆง ( ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘ƒ ) ) โˆง ๐‘ โˆˆ ๐ป ) ) โˆง ๐‘ฅ โˆˆ ๐ผ ) โ†’ ๐‘† โˆˆ Ring )
32 1 ad2antrr โŠข ( ( ( ๐œ‘ โˆง ( ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘ƒ ) ) โˆง ๐‘ โˆˆ ๐ป ) ) โˆง ๐‘ฅ โˆˆ ๐ผ ) โ†’ ๐ผ โˆˆ ๐‘Š )
33 19 ad2antrr โŠข ( ( ( ๐œ‘ โˆง ( ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘ƒ ) ) โˆง ๐‘ โˆˆ ๐ป ) ) โˆง ๐‘ฅ โˆˆ ๐ผ ) โ†’ ๐‘… Fn ๐ผ )
34 3 1 fexd โŠข ( ๐œ‘ โ†’ ๐‘… โˆˆ V )
35 5 2 34 prdssca โŠข ( ๐œ‘ โ†’ ๐‘† = ( Scalar โ€˜ ๐‘ƒ ) )
36 35 fveq2d โŠข ( ๐œ‘ โ†’ ( Base โ€˜ ๐‘† ) = ( Base โ€˜ ( Scalar โ€˜ ๐‘ƒ ) ) )
37 36 eleq2d โŠข ( ๐œ‘ โ†’ ( ๐‘Ž โˆˆ ( Base โ€˜ ๐‘† ) โ†” ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘ƒ ) ) ) )
38 37 biimpar โŠข ( ( ๐œ‘ โˆง ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘ƒ ) ) ) โ†’ ๐‘Ž โˆˆ ( Base โ€˜ ๐‘† ) )
39 38 adantrr โŠข ( ( ๐œ‘ โˆง ( ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘ƒ ) ) โˆง ๐‘ โˆˆ ๐ป ) ) โ†’ ๐‘Ž โˆˆ ( Base โ€˜ ๐‘† ) )
40 39 adantr โŠข ( ( ( ๐œ‘ โˆง ( ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘ƒ ) ) โˆง ๐‘ โˆˆ ๐ป ) ) โˆง ๐‘ฅ โˆˆ ๐ผ ) โ†’ ๐‘Ž โˆˆ ( Base โ€˜ ๐‘† ) )
41 23 adantr โŠข ( ( ( ๐œ‘ โˆง ( ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘ƒ ) ) โˆง ๐‘ โˆˆ ๐ป ) ) โˆง ๐‘ฅ โˆˆ ๐ผ ) โ†’ ๐‘ โˆˆ ( Base โ€˜ ๐‘ƒ ) )
42 simpr โŠข ( ( ( ๐œ‘ โˆง ( ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘ƒ ) ) โˆง ๐‘ โˆˆ ๐ป ) ) โˆง ๐‘ฅ โˆˆ ๐ผ ) โ†’ ๐‘ฅ โˆˆ ๐ผ )
43 5 18 25 30 31 32 33 40 41 42 prdsvscafval โŠข ( ( ( ๐œ‘ โˆง ( ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘ƒ ) ) โˆง ๐‘ โˆˆ ๐ป ) ) โˆง ๐‘ฅ โˆˆ ๐ผ ) โ†’ ( ( ๐‘Ž ( ยท๐‘  โ€˜ ๐‘ƒ ) ๐‘ ) โ€˜ ๐‘ฅ ) = ( ๐‘Ž ( ยท๐‘  โ€˜ ( ๐‘… โ€˜ ๐‘ฅ ) ) ( ๐‘ โ€˜ ๐‘ฅ ) ) )
44 43 adantrr โŠข ( ( ( ๐œ‘ โˆง ( ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘ƒ ) ) โˆง ๐‘ โˆˆ ๐ป ) ) โˆง ( ๐‘ฅ โˆˆ ๐ผ โˆง ( ๐‘ โ€˜ ๐‘ฅ ) = ( 0g โ€˜ ( ๐‘… โ€˜ ๐‘ฅ ) ) ) ) โ†’ ( ( ๐‘Ž ( ยท๐‘  โ€˜ ๐‘ƒ ) ๐‘ ) โ€˜ ๐‘ฅ ) = ( ๐‘Ž ( ยท๐‘  โ€˜ ( ๐‘… โ€˜ ๐‘ฅ ) ) ( ๐‘ โ€˜ ๐‘ฅ ) ) )
45 3 ffvelrnda โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ผ ) โ†’ ( ๐‘… โ€˜ ๐‘ฅ ) โˆˆ LMod )
46 45 adantlr โŠข ( ( ( ๐œ‘ โˆง ( ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘ƒ ) ) โˆง ๐‘ โˆˆ ๐ป ) ) โˆง ๐‘ฅ โˆˆ ๐ผ ) โ†’ ( ๐‘… โ€˜ ๐‘ฅ ) โˆˆ LMod )
47 simplrl โŠข ( ( ( ๐œ‘ โˆง ( ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘ƒ ) ) โˆง ๐‘ โˆˆ ๐ป ) ) โˆง ๐‘ฅ โˆˆ ๐ผ ) โ†’ ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘ƒ ) ) )
48 35 adantr โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ผ ) โ†’ ๐‘† = ( Scalar โ€˜ ๐‘ƒ ) )
49 4 48 eqtrd โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ผ ) โ†’ ( Scalar โ€˜ ( ๐‘… โ€˜ ๐‘ฅ ) ) = ( Scalar โ€˜ ๐‘ƒ ) )
50 49 fveq2d โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ผ ) โ†’ ( Base โ€˜ ( Scalar โ€˜ ( ๐‘… โ€˜ ๐‘ฅ ) ) ) = ( Base โ€˜ ( Scalar โ€˜ ๐‘ƒ ) ) )
51 50 adantlr โŠข ( ( ( ๐œ‘ โˆง ( ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘ƒ ) ) โˆง ๐‘ โˆˆ ๐ป ) ) โˆง ๐‘ฅ โˆˆ ๐ผ ) โ†’ ( Base โ€˜ ( Scalar โ€˜ ( ๐‘… โ€˜ ๐‘ฅ ) ) ) = ( Base โ€˜ ( Scalar โ€˜ ๐‘ƒ ) ) )
52 47 51 eleqtrrd โŠข ( ( ( ๐œ‘ โˆง ( ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘ƒ ) ) โˆง ๐‘ โˆˆ ๐ป ) ) โˆง ๐‘ฅ โˆˆ ๐ผ ) โ†’ ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ( ๐‘… โ€˜ ๐‘ฅ ) ) ) )
53 eqid โŠข ( Scalar โ€˜ ( ๐‘… โ€˜ ๐‘ฅ ) ) = ( Scalar โ€˜ ( ๐‘… โ€˜ ๐‘ฅ ) )
54 eqid โŠข ( ยท๐‘  โ€˜ ( ๐‘… โ€˜ ๐‘ฅ ) ) = ( ยท๐‘  โ€˜ ( ๐‘… โ€˜ ๐‘ฅ ) )
55 eqid โŠข ( Base โ€˜ ( Scalar โ€˜ ( ๐‘… โ€˜ ๐‘ฅ ) ) ) = ( Base โ€˜ ( Scalar โ€˜ ( ๐‘… โ€˜ ๐‘ฅ ) ) )
56 eqid โŠข ( 0g โ€˜ ( ๐‘… โ€˜ ๐‘ฅ ) ) = ( 0g โ€˜ ( ๐‘… โ€˜ ๐‘ฅ ) )
57 53 54 55 56 lmodvs0 โŠข ( ( ( ๐‘… โ€˜ ๐‘ฅ ) โˆˆ LMod โˆง ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ( ๐‘… โ€˜ ๐‘ฅ ) ) ) ) โ†’ ( ๐‘Ž ( ยท๐‘  โ€˜ ( ๐‘… โ€˜ ๐‘ฅ ) ) ( 0g โ€˜ ( ๐‘… โ€˜ ๐‘ฅ ) ) ) = ( 0g โ€˜ ( ๐‘… โ€˜ ๐‘ฅ ) ) )
58 46 52 57 syl2anc โŠข ( ( ( ๐œ‘ โˆง ( ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘ƒ ) ) โˆง ๐‘ โˆˆ ๐ป ) ) โˆง ๐‘ฅ โˆˆ ๐ผ ) โ†’ ( ๐‘Ž ( ยท๐‘  โ€˜ ( ๐‘… โ€˜ ๐‘ฅ ) ) ( 0g โ€˜ ( ๐‘… โ€˜ ๐‘ฅ ) ) ) = ( 0g โ€˜ ( ๐‘… โ€˜ ๐‘ฅ ) ) )
59 oveq2 โŠข ( ( ๐‘ โ€˜ ๐‘ฅ ) = ( 0g โ€˜ ( ๐‘… โ€˜ ๐‘ฅ ) ) โ†’ ( ๐‘Ž ( ยท๐‘  โ€˜ ( ๐‘… โ€˜ ๐‘ฅ ) ) ( ๐‘ โ€˜ ๐‘ฅ ) ) = ( ๐‘Ž ( ยท๐‘  โ€˜ ( ๐‘… โ€˜ ๐‘ฅ ) ) ( 0g โ€˜ ( ๐‘… โ€˜ ๐‘ฅ ) ) ) )
60 59 eqeq1d โŠข ( ( ๐‘ โ€˜ ๐‘ฅ ) = ( 0g โ€˜ ( ๐‘… โ€˜ ๐‘ฅ ) ) โ†’ ( ( ๐‘Ž ( ยท๐‘  โ€˜ ( ๐‘… โ€˜ ๐‘ฅ ) ) ( ๐‘ โ€˜ ๐‘ฅ ) ) = ( 0g โ€˜ ( ๐‘… โ€˜ ๐‘ฅ ) ) โ†” ( ๐‘Ž ( ยท๐‘  โ€˜ ( ๐‘… โ€˜ ๐‘ฅ ) ) ( 0g โ€˜ ( ๐‘… โ€˜ ๐‘ฅ ) ) ) = ( 0g โ€˜ ( ๐‘… โ€˜ ๐‘ฅ ) ) ) )
61 58 60 syl5ibrcom โŠข ( ( ( ๐œ‘ โˆง ( ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘ƒ ) ) โˆง ๐‘ โˆˆ ๐ป ) ) โˆง ๐‘ฅ โˆˆ ๐ผ ) โ†’ ( ( ๐‘ โ€˜ ๐‘ฅ ) = ( 0g โ€˜ ( ๐‘… โ€˜ ๐‘ฅ ) ) โ†’ ( ๐‘Ž ( ยท๐‘  โ€˜ ( ๐‘… โ€˜ ๐‘ฅ ) ) ( ๐‘ โ€˜ ๐‘ฅ ) ) = ( 0g โ€˜ ( ๐‘… โ€˜ ๐‘ฅ ) ) ) )
62 61 impr โŠข ( ( ( ๐œ‘ โˆง ( ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘ƒ ) ) โˆง ๐‘ โˆˆ ๐ป ) ) โˆง ( ๐‘ฅ โˆˆ ๐ผ โˆง ( ๐‘ โ€˜ ๐‘ฅ ) = ( 0g โ€˜ ( ๐‘… โ€˜ ๐‘ฅ ) ) ) ) โ†’ ( ๐‘Ž ( ยท๐‘  โ€˜ ( ๐‘… โ€˜ ๐‘ฅ ) ) ( ๐‘ โ€˜ ๐‘ฅ ) ) = ( 0g โ€˜ ( ๐‘… โ€˜ ๐‘ฅ ) ) )
63 44 62 eqtrd โŠข ( ( ( ๐œ‘ โˆง ( ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘ƒ ) ) โˆง ๐‘ โˆˆ ๐ป ) ) โˆง ( ๐‘ฅ โˆˆ ๐ผ โˆง ( ๐‘ โ€˜ ๐‘ฅ ) = ( 0g โ€˜ ( ๐‘… โ€˜ ๐‘ฅ ) ) ) ) โ†’ ( ( ๐‘Ž ( ยท๐‘  โ€˜ ๐‘ƒ ) ๐‘ ) โ€˜ ๐‘ฅ ) = ( 0g โ€˜ ( ๐‘… โ€˜ ๐‘ฅ ) ) )
64 63 expr โŠข ( ( ( ๐œ‘ โˆง ( ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘ƒ ) ) โˆง ๐‘ โˆˆ ๐ป ) ) โˆง ๐‘ฅ โˆˆ ๐ผ ) โ†’ ( ( ๐‘ โ€˜ ๐‘ฅ ) = ( 0g โ€˜ ( ๐‘… โ€˜ ๐‘ฅ ) ) โ†’ ( ( ๐‘Ž ( ยท๐‘  โ€˜ ๐‘ƒ ) ๐‘ ) โ€˜ ๐‘ฅ ) = ( 0g โ€˜ ( ๐‘… โ€˜ ๐‘ฅ ) ) ) )
65 64 necon3d โŠข ( ( ( ๐œ‘ โˆง ( ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘ƒ ) ) โˆง ๐‘ โˆˆ ๐ป ) ) โˆง ๐‘ฅ โˆˆ ๐ผ ) โ†’ ( ( ( ๐‘Ž ( ยท๐‘  โ€˜ ๐‘ƒ ) ๐‘ ) โ€˜ ๐‘ฅ ) โ‰  ( 0g โ€˜ ( ๐‘… โ€˜ ๐‘ฅ ) ) โ†’ ( ๐‘ โ€˜ ๐‘ฅ ) โ‰  ( 0g โ€˜ ( ๐‘… โ€˜ ๐‘ฅ ) ) ) )
66 65 ss2rabdv โŠข ( ( ๐œ‘ โˆง ( ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘ƒ ) ) โˆง ๐‘ โˆˆ ๐ป ) ) โ†’ { ๐‘ฅ โˆˆ ๐ผ โˆฃ ( ( ๐‘Ž ( ยท๐‘  โ€˜ ๐‘ƒ ) ๐‘ ) โ€˜ ๐‘ฅ ) โ‰  ( 0g โ€˜ ( ๐‘… โ€˜ ๐‘ฅ ) ) } โŠ† { ๐‘ฅ โˆˆ ๐ผ โˆฃ ( ๐‘ โ€˜ ๐‘ฅ ) โ‰  ( 0g โ€˜ ( ๐‘… โ€˜ ๐‘ฅ ) ) } )
67 29 66 ssfid โŠข ( ( ๐œ‘ โˆง ( ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘ƒ ) ) โˆง ๐‘ โˆˆ ๐ป ) ) โ†’ { ๐‘ฅ โˆˆ ๐ผ โˆฃ ( ( ๐‘Ž ( ยท๐‘  โ€˜ ๐‘ƒ ) ๐‘ ) โ€˜ ๐‘ฅ ) โ‰  ( 0g โ€˜ ( ๐‘… โ€˜ ๐‘ฅ ) ) } โˆˆ Fin )
68 5 17 18 7 1 19 dsmmelbas โŠข ( ๐œ‘ โ†’ ( ( ๐‘Ž ( ยท๐‘  โ€˜ ๐‘ƒ ) ๐‘ ) โˆˆ ๐ป โ†” ( ( ๐‘Ž ( ยท๐‘  โ€˜ ๐‘ƒ ) ๐‘ ) โˆˆ ( Base โ€˜ ๐‘ƒ ) โˆง { ๐‘ฅ โˆˆ ๐ผ โˆฃ ( ( ๐‘Ž ( ยท๐‘  โ€˜ ๐‘ƒ ) ๐‘ ) โ€˜ ๐‘ฅ ) โ‰  ( 0g โ€˜ ( ๐‘… โ€˜ ๐‘ฅ ) ) } โˆˆ Fin ) ) )
69 68 adantr โŠข ( ( ๐œ‘ โˆง ( ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘ƒ ) ) โˆง ๐‘ โˆˆ ๐ป ) ) โ†’ ( ( ๐‘Ž ( ยท๐‘  โ€˜ ๐‘ƒ ) ๐‘ ) โˆˆ ๐ป โ†” ( ( ๐‘Ž ( ยท๐‘  โ€˜ ๐‘ƒ ) ๐‘ ) โˆˆ ( Base โ€˜ ๐‘ƒ ) โˆง { ๐‘ฅ โˆˆ ๐ผ โˆฃ ( ( ๐‘Ž ( ยท๐‘  โ€˜ ๐‘ƒ ) ๐‘ ) โ€˜ ๐‘ฅ ) โ‰  ( 0g โ€˜ ( ๐‘… โ€˜ ๐‘ฅ ) ) } โˆˆ Fin ) ) )
70 28 67 69 mpbir2and โŠข ( ( ๐œ‘ โˆง ( ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘ƒ ) ) โˆง ๐‘ โˆˆ ๐ป ) ) โ†’ ( ๐‘Ž ( ยท๐‘  โ€˜ ๐‘ƒ ) ๐‘ ) โˆˆ ๐ป )
71 70 ralrimivva โŠข ( ๐œ‘ โ†’ โˆ€ ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘ƒ ) ) โˆ€ ๐‘ โˆˆ ๐ป ( ๐‘Ž ( ยท๐‘  โ€˜ ๐‘ƒ ) ๐‘ ) โˆˆ ๐ป )
72 24 26 18 25 6 islss4 โŠข ( ๐‘ƒ โˆˆ LMod โ†’ ( ๐ป โˆˆ ๐‘ˆ โ†” ( ๐ป โˆˆ ( SubGrp โ€˜ ๐‘ƒ ) โˆง โˆ€ ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘ƒ ) ) โˆ€ ๐‘ โˆˆ ๐ป ( ๐‘Ž ( ยท๐‘  โ€˜ ๐‘ƒ ) ๐‘ ) โˆˆ ๐ป ) ) )
73 13 72 syl โŠข ( ๐œ‘ โ†’ ( ๐ป โˆˆ ๐‘ˆ โ†” ( ๐ป โˆˆ ( SubGrp โ€˜ ๐‘ƒ ) โˆง โˆ€ ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘ƒ ) ) โˆ€ ๐‘ โˆˆ ๐ป ( ๐‘Ž ( ยท๐‘  โ€˜ ๐‘ƒ ) ๐‘ ) โˆˆ ๐ป ) ) )
74 12 71 73 mpbir2and โŠข ( ๐œ‘ โ†’ ๐ป โˆˆ ๐‘ˆ )