Metamath Proof Explorer


Theorem lsmcl

Description: The sum of two subspaces is a subspace. (Contributed by NM, 4-Feb-2014) (Revised by Mario Carneiro, 19-Apr-2016)

Ref Expression
Hypotheses lsmcl.s โŠข ๐‘† = ( LSubSp โ€˜ ๐‘Š )
lsmcl.p โŠข โŠ• = ( LSSum โ€˜ ๐‘Š )
Assertion lsmcl ( ( ๐‘Š โˆˆ LMod โˆง ๐‘‡ โˆˆ ๐‘† โˆง ๐‘ˆ โˆˆ ๐‘† ) โ†’ ( ๐‘‡ โŠ• ๐‘ˆ ) โˆˆ ๐‘† )

Proof

Step Hyp Ref Expression
1 lsmcl.s โŠข ๐‘† = ( LSubSp โ€˜ ๐‘Š )
2 lsmcl.p โŠข โŠ• = ( LSSum โ€˜ ๐‘Š )
3 lmodabl โŠข ( ๐‘Š โˆˆ LMod โ†’ ๐‘Š โˆˆ Abel )
4 3 3ad2ant1 โŠข ( ( ๐‘Š โˆˆ LMod โˆง ๐‘‡ โˆˆ ๐‘† โˆง ๐‘ˆ โˆˆ ๐‘† ) โ†’ ๐‘Š โˆˆ Abel )
5 1 lsssubg โŠข ( ( ๐‘Š โˆˆ LMod โˆง ๐‘‡ โˆˆ ๐‘† ) โ†’ ๐‘‡ โˆˆ ( SubGrp โ€˜ ๐‘Š ) )
6 5 3adant3 โŠข ( ( ๐‘Š โˆˆ LMod โˆง ๐‘‡ โˆˆ ๐‘† โˆง ๐‘ˆ โˆˆ ๐‘† ) โ†’ ๐‘‡ โˆˆ ( SubGrp โ€˜ ๐‘Š ) )
7 1 lsssubg โŠข ( ( ๐‘Š โˆˆ LMod โˆง ๐‘ˆ โˆˆ ๐‘† ) โ†’ ๐‘ˆ โˆˆ ( SubGrp โ€˜ ๐‘Š ) )
8 7 3adant2 โŠข ( ( ๐‘Š โˆˆ LMod โˆง ๐‘‡ โˆˆ ๐‘† โˆง ๐‘ˆ โˆˆ ๐‘† ) โ†’ ๐‘ˆ โˆˆ ( SubGrp โ€˜ ๐‘Š ) )
9 2 lsmsubg2 โŠข ( ( ๐‘Š โˆˆ Abel โˆง ๐‘‡ โˆˆ ( SubGrp โ€˜ ๐‘Š ) โˆง ๐‘ˆ โˆˆ ( SubGrp โ€˜ ๐‘Š ) ) โ†’ ( ๐‘‡ โŠ• ๐‘ˆ ) โˆˆ ( SubGrp โ€˜ ๐‘Š ) )
10 4 6 8 9 syl3anc โŠข ( ( ๐‘Š โˆˆ LMod โˆง ๐‘‡ โˆˆ ๐‘† โˆง ๐‘ˆ โˆˆ ๐‘† ) โ†’ ( ๐‘‡ โŠ• ๐‘ˆ ) โˆˆ ( SubGrp โ€˜ ๐‘Š ) )
11 eqid โŠข ( +g โ€˜ ๐‘Š ) = ( +g โ€˜ ๐‘Š )
12 11 2 lsmelval โŠข ( ( ๐‘‡ โˆˆ ( SubGrp โ€˜ ๐‘Š ) โˆง ๐‘ˆ โˆˆ ( SubGrp โ€˜ ๐‘Š ) ) โ†’ ( ๐‘ข โˆˆ ( ๐‘‡ โŠ• ๐‘ˆ ) โ†” โˆƒ ๐‘‘ โˆˆ ๐‘‡ โˆƒ ๐‘’ โˆˆ ๐‘ˆ ๐‘ข = ( ๐‘‘ ( +g โ€˜ ๐‘Š ) ๐‘’ ) ) )
13 6 8 12 syl2anc โŠข ( ( ๐‘Š โˆˆ LMod โˆง ๐‘‡ โˆˆ ๐‘† โˆง ๐‘ˆ โˆˆ ๐‘† ) โ†’ ( ๐‘ข โˆˆ ( ๐‘‡ โŠ• ๐‘ˆ ) โ†” โˆƒ ๐‘‘ โˆˆ ๐‘‡ โˆƒ ๐‘’ โˆˆ ๐‘ˆ ๐‘ข = ( ๐‘‘ ( +g โ€˜ ๐‘Š ) ๐‘’ ) ) )
14 13 adantr โŠข ( ( ( ๐‘Š โˆˆ LMod โˆง ๐‘‡ โˆˆ ๐‘† โˆง ๐‘ˆ โˆˆ ๐‘† ) โˆง ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) ) โ†’ ( ๐‘ข โˆˆ ( ๐‘‡ โŠ• ๐‘ˆ ) โ†” โˆƒ ๐‘‘ โˆˆ ๐‘‡ โˆƒ ๐‘’ โˆˆ ๐‘ˆ ๐‘ข = ( ๐‘‘ ( +g โ€˜ ๐‘Š ) ๐‘’ ) ) )
15 simpll1 โŠข ( ( ( ( ๐‘Š โˆˆ LMod โˆง ๐‘‡ โˆˆ ๐‘† โˆง ๐‘ˆ โˆˆ ๐‘† ) โˆง ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) ) โˆง ( ๐‘‘ โˆˆ ๐‘‡ โˆง ๐‘’ โˆˆ ๐‘ˆ ) ) โ†’ ๐‘Š โˆˆ LMod )
16 simplr โŠข ( ( ( ( ๐‘Š โˆˆ LMod โˆง ๐‘‡ โˆˆ ๐‘† โˆง ๐‘ˆ โˆˆ ๐‘† ) โˆง ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) ) โˆง ( ๐‘‘ โˆˆ ๐‘‡ โˆง ๐‘’ โˆˆ ๐‘ˆ ) ) โ†’ ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) )
17 simpll2 โŠข ( ( ( ( ๐‘Š โˆˆ LMod โˆง ๐‘‡ โˆˆ ๐‘† โˆง ๐‘ˆ โˆˆ ๐‘† ) โˆง ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) ) โˆง ( ๐‘‘ โˆˆ ๐‘‡ โˆง ๐‘’ โˆˆ ๐‘ˆ ) ) โ†’ ๐‘‡ โˆˆ ๐‘† )
18 simprl โŠข ( ( ( ( ๐‘Š โˆˆ LMod โˆง ๐‘‡ โˆˆ ๐‘† โˆง ๐‘ˆ โˆˆ ๐‘† ) โˆง ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) ) โˆง ( ๐‘‘ โˆˆ ๐‘‡ โˆง ๐‘’ โˆˆ ๐‘ˆ ) ) โ†’ ๐‘‘ โˆˆ ๐‘‡ )
19 eqid โŠข ( Base โ€˜ ๐‘Š ) = ( Base โ€˜ ๐‘Š )
20 19 1 lssel โŠข ( ( ๐‘‡ โˆˆ ๐‘† โˆง ๐‘‘ โˆˆ ๐‘‡ ) โ†’ ๐‘‘ โˆˆ ( Base โ€˜ ๐‘Š ) )
21 17 18 20 syl2anc โŠข ( ( ( ( ๐‘Š โˆˆ LMod โˆง ๐‘‡ โˆˆ ๐‘† โˆง ๐‘ˆ โˆˆ ๐‘† ) โˆง ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) ) โˆง ( ๐‘‘ โˆˆ ๐‘‡ โˆง ๐‘’ โˆˆ ๐‘ˆ ) ) โ†’ ๐‘‘ โˆˆ ( Base โ€˜ ๐‘Š ) )
22 simpll3 โŠข ( ( ( ( ๐‘Š โˆˆ LMod โˆง ๐‘‡ โˆˆ ๐‘† โˆง ๐‘ˆ โˆˆ ๐‘† ) โˆง ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) ) โˆง ( ๐‘‘ โˆˆ ๐‘‡ โˆง ๐‘’ โˆˆ ๐‘ˆ ) ) โ†’ ๐‘ˆ โˆˆ ๐‘† )
23 simprr โŠข ( ( ( ( ๐‘Š โˆˆ LMod โˆง ๐‘‡ โˆˆ ๐‘† โˆง ๐‘ˆ โˆˆ ๐‘† ) โˆง ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) ) โˆง ( ๐‘‘ โˆˆ ๐‘‡ โˆง ๐‘’ โˆˆ ๐‘ˆ ) ) โ†’ ๐‘’ โˆˆ ๐‘ˆ )
24 19 1 lssel โŠข ( ( ๐‘ˆ โˆˆ ๐‘† โˆง ๐‘’ โˆˆ ๐‘ˆ ) โ†’ ๐‘’ โˆˆ ( Base โ€˜ ๐‘Š ) )
25 22 23 24 syl2anc โŠข ( ( ( ( ๐‘Š โˆˆ LMod โˆง ๐‘‡ โˆˆ ๐‘† โˆง ๐‘ˆ โˆˆ ๐‘† ) โˆง ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) ) โˆง ( ๐‘‘ โˆˆ ๐‘‡ โˆง ๐‘’ โˆˆ ๐‘ˆ ) ) โ†’ ๐‘’ โˆˆ ( Base โ€˜ ๐‘Š ) )
26 eqid โŠข ( Scalar โ€˜ ๐‘Š ) = ( Scalar โ€˜ ๐‘Š )
27 eqid โŠข ( ยท๐‘  โ€˜ ๐‘Š ) = ( ยท๐‘  โ€˜ ๐‘Š )
28 eqid โŠข ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) = ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) )
29 19 11 26 27 28 lmodvsdi โŠข ( ( ๐‘Š โˆˆ LMod โˆง ( ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) โˆง ๐‘‘ โˆˆ ( Base โ€˜ ๐‘Š ) โˆง ๐‘’ โˆˆ ( Base โ€˜ ๐‘Š ) ) ) โ†’ ( ๐‘Ž ( ยท๐‘  โ€˜ ๐‘Š ) ( ๐‘‘ ( +g โ€˜ ๐‘Š ) ๐‘’ ) ) = ( ( ๐‘Ž ( ยท๐‘  โ€˜ ๐‘Š ) ๐‘‘ ) ( +g โ€˜ ๐‘Š ) ( ๐‘Ž ( ยท๐‘  โ€˜ ๐‘Š ) ๐‘’ ) ) )
30 15 16 21 25 29 syl13anc โŠข ( ( ( ( ๐‘Š โˆˆ LMod โˆง ๐‘‡ โˆˆ ๐‘† โˆง ๐‘ˆ โˆˆ ๐‘† ) โˆง ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) ) โˆง ( ๐‘‘ โˆˆ ๐‘‡ โˆง ๐‘’ โˆˆ ๐‘ˆ ) ) โ†’ ( ๐‘Ž ( ยท๐‘  โ€˜ ๐‘Š ) ( ๐‘‘ ( +g โ€˜ ๐‘Š ) ๐‘’ ) ) = ( ( ๐‘Ž ( ยท๐‘  โ€˜ ๐‘Š ) ๐‘‘ ) ( +g โ€˜ ๐‘Š ) ( ๐‘Ž ( ยท๐‘  โ€˜ ๐‘Š ) ๐‘’ ) ) )
31 15 17 5 syl2anc โŠข ( ( ( ( ๐‘Š โˆˆ LMod โˆง ๐‘‡ โˆˆ ๐‘† โˆง ๐‘ˆ โˆˆ ๐‘† ) โˆง ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) ) โˆง ( ๐‘‘ โˆˆ ๐‘‡ โˆง ๐‘’ โˆˆ ๐‘ˆ ) ) โ†’ ๐‘‡ โˆˆ ( SubGrp โ€˜ ๐‘Š ) )
32 15 22 7 syl2anc โŠข ( ( ( ( ๐‘Š โˆˆ LMod โˆง ๐‘‡ โˆˆ ๐‘† โˆง ๐‘ˆ โˆˆ ๐‘† ) โˆง ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) ) โˆง ( ๐‘‘ โˆˆ ๐‘‡ โˆง ๐‘’ โˆˆ ๐‘ˆ ) ) โ†’ ๐‘ˆ โˆˆ ( SubGrp โ€˜ ๐‘Š ) )
33 26 27 28 1 lssvscl โŠข ( ( ( ๐‘Š โˆˆ LMod โˆง ๐‘‡ โˆˆ ๐‘† ) โˆง ( ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) โˆง ๐‘‘ โˆˆ ๐‘‡ ) ) โ†’ ( ๐‘Ž ( ยท๐‘  โ€˜ ๐‘Š ) ๐‘‘ ) โˆˆ ๐‘‡ )
34 15 17 16 18 33 syl22anc โŠข ( ( ( ( ๐‘Š โˆˆ LMod โˆง ๐‘‡ โˆˆ ๐‘† โˆง ๐‘ˆ โˆˆ ๐‘† ) โˆง ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) ) โˆง ( ๐‘‘ โˆˆ ๐‘‡ โˆง ๐‘’ โˆˆ ๐‘ˆ ) ) โ†’ ( ๐‘Ž ( ยท๐‘  โ€˜ ๐‘Š ) ๐‘‘ ) โˆˆ ๐‘‡ )
35 26 27 28 1 lssvscl โŠข ( ( ( ๐‘Š โˆˆ LMod โˆง ๐‘ˆ โˆˆ ๐‘† ) โˆง ( ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) โˆง ๐‘’ โˆˆ ๐‘ˆ ) ) โ†’ ( ๐‘Ž ( ยท๐‘  โ€˜ ๐‘Š ) ๐‘’ ) โˆˆ ๐‘ˆ )
36 15 22 16 23 35 syl22anc โŠข ( ( ( ( ๐‘Š โˆˆ LMod โˆง ๐‘‡ โˆˆ ๐‘† โˆง ๐‘ˆ โˆˆ ๐‘† ) โˆง ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) ) โˆง ( ๐‘‘ โˆˆ ๐‘‡ โˆง ๐‘’ โˆˆ ๐‘ˆ ) ) โ†’ ( ๐‘Ž ( ยท๐‘  โ€˜ ๐‘Š ) ๐‘’ ) โˆˆ ๐‘ˆ )
37 11 2 lsmelvali โŠข ( ( ( ๐‘‡ โˆˆ ( SubGrp โ€˜ ๐‘Š ) โˆง ๐‘ˆ โˆˆ ( SubGrp โ€˜ ๐‘Š ) ) โˆง ( ( ๐‘Ž ( ยท๐‘  โ€˜ ๐‘Š ) ๐‘‘ ) โˆˆ ๐‘‡ โˆง ( ๐‘Ž ( ยท๐‘  โ€˜ ๐‘Š ) ๐‘’ ) โˆˆ ๐‘ˆ ) ) โ†’ ( ( ๐‘Ž ( ยท๐‘  โ€˜ ๐‘Š ) ๐‘‘ ) ( +g โ€˜ ๐‘Š ) ( ๐‘Ž ( ยท๐‘  โ€˜ ๐‘Š ) ๐‘’ ) ) โˆˆ ( ๐‘‡ โŠ• ๐‘ˆ ) )
38 31 32 34 36 37 syl22anc โŠข ( ( ( ( ๐‘Š โˆˆ LMod โˆง ๐‘‡ โˆˆ ๐‘† โˆง ๐‘ˆ โˆˆ ๐‘† ) โˆง ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) ) โˆง ( ๐‘‘ โˆˆ ๐‘‡ โˆง ๐‘’ โˆˆ ๐‘ˆ ) ) โ†’ ( ( ๐‘Ž ( ยท๐‘  โ€˜ ๐‘Š ) ๐‘‘ ) ( +g โ€˜ ๐‘Š ) ( ๐‘Ž ( ยท๐‘  โ€˜ ๐‘Š ) ๐‘’ ) ) โˆˆ ( ๐‘‡ โŠ• ๐‘ˆ ) )
39 30 38 eqeltrd โŠข ( ( ( ( ๐‘Š โˆˆ LMod โˆง ๐‘‡ โˆˆ ๐‘† โˆง ๐‘ˆ โˆˆ ๐‘† ) โˆง ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) ) โˆง ( ๐‘‘ โˆˆ ๐‘‡ โˆง ๐‘’ โˆˆ ๐‘ˆ ) ) โ†’ ( ๐‘Ž ( ยท๐‘  โ€˜ ๐‘Š ) ( ๐‘‘ ( +g โ€˜ ๐‘Š ) ๐‘’ ) ) โˆˆ ( ๐‘‡ โŠ• ๐‘ˆ ) )
40 oveq2 โŠข ( ๐‘ข = ( ๐‘‘ ( +g โ€˜ ๐‘Š ) ๐‘’ ) โ†’ ( ๐‘Ž ( ยท๐‘  โ€˜ ๐‘Š ) ๐‘ข ) = ( ๐‘Ž ( ยท๐‘  โ€˜ ๐‘Š ) ( ๐‘‘ ( +g โ€˜ ๐‘Š ) ๐‘’ ) ) )
41 40 eleq1d โŠข ( ๐‘ข = ( ๐‘‘ ( +g โ€˜ ๐‘Š ) ๐‘’ ) โ†’ ( ( ๐‘Ž ( ยท๐‘  โ€˜ ๐‘Š ) ๐‘ข ) โˆˆ ( ๐‘‡ โŠ• ๐‘ˆ ) โ†” ( ๐‘Ž ( ยท๐‘  โ€˜ ๐‘Š ) ( ๐‘‘ ( +g โ€˜ ๐‘Š ) ๐‘’ ) ) โˆˆ ( ๐‘‡ โŠ• ๐‘ˆ ) ) )
42 39 41 syl5ibrcom โŠข ( ( ( ( ๐‘Š โˆˆ LMod โˆง ๐‘‡ โˆˆ ๐‘† โˆง ๐‘ˆ โˆˆ ๐‘† ) โˆง ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) ) โˆง ( ๐‘‘ โˆˆ ๐‘‡ โˆง ๐‘’ โˆˆ ๐‘ˆ ) ) โ†’ ( ๐‘ข = ( ๐‘‘ ( +g โ€˜ ๐‘Š ) ๐‘’ ) โ†’ ( ๐‘Ž ( ยท๐‘  โ€˜ ๐‘Š ) ๐‘ข ) โˆˆ ( ๐‘‡ โŠ• ๐‘ˆ ) ) )
43 42 rexlimdvva โŠข ( ( ( ๐‘Š โˆˆ LMod โˆง ๐‘‡ โˆˆ ๐‘† โˆง ๐‘ˆ โˆˆ ๐‘† ) โˆง ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) ) โ†’ ( โˆƒ ๐‘‘ โˆˆ ๐‘‡ โˆƒ ๐‘’ โˆˆ ๐‘ˆ ๐‘ข = ( ๐‘‘ ( +g โ€˜ ๐‘Š ) ๐‘’ ) โ†’ ( ๐‘Ž ( ยท๐‘  โ€˜ ๐‘Š ) ๐‘ข ) โˆˆ ( ๐‘‡ โŠ• ๐‘ˆ ) ) )
44 14 43 sylbid โŠข ( ( ( ๐‘Š โˆˆ LMod โˆง ๐‘‡ โˆˆ ๐‘† โˆง ๐‘ˆ โˆˆ ๐‘† ) โˆง ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) ) โ†’ ( ๐‘ข โˆˆ ( ๐‘‡ โŠ• ๐‘ˆ ) โ†’ ( ๐‘Ž ( ยท๐‘  โ€˜ ๐‘Š ) ๐‘ข ) โˆˆ ( ๐‘‡ โŠ• ๐‘ˆ ) ) )
45 44 impr โŠข ( ( ( ๐‘Š โˆˆ LMod โˆง ๐‘‡ โˆˆ ๐‘† โˆง ๐‘ˆ โˆˆ ๐‘† ) โˆง ( ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) โˆง ๐‘ข โˆˆ ( ๐‘‡ โŠ• ๐‘ˆ ) ) ) โ†’ ( ๐‘Ž ( ยท๐‘  โ€˜ ๐‘Š ) ๐‘ข ) โˆˆ ( ๐‘‡ โŠ• ๐‘ˆ ) )
46 45 ralrimivva โŠข ( ( ๐‘Š โˆˆ LMod โˆง ๐‘‡ โˆˆ ๐‘† โˆง ๐‘ˆ โˆˆ ๐‘† ) โ†’ โˆ€ ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) โˆ€ ๐‘ข โˆˆ ( ๐‘‡ โŠ• ๐‘ˆ ) ( ๐‘Ž ( ยท๐‘  โ€˜ ๐‘Š ) ๐‘ข ) โˆˆ ( ๐‘‡ โŠ• ๐‘ˆ ) )
47 26 28 19 27 1 islss4 โŠข ( ๐‘Š โˆˆ LMod โ†’ ( ( ๐‘‡ โŠ• ๐‘ˆ ) โˆˆ ๐‘† โ†” ( ( ๐‘‡ โŠ• ๐‘ˆ ) โˆˆ ( SubGrp โ€˜ ๐‘Š ) โˆง โˆ€ ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) โˆ€ ๐‘ข โˆˆ ( ๐‘‡ โŠ• ๐‘ˆ ) ( ๐‘Ž ( ยท๐‘  โ€˜ ๐‘Š ) ๐‘ข ) โˆˆ ( ๐‘‡ โŠ• ๐‘ˆ ) ) ) )
48 47 3ad2ant1 โŠข ( ( ๐‘Š โˆˆ LMod โˆง ๐‘‡ โˆˆ ๐‘† โˆง ๐‘ˆ โˆˆ ๐‘† ) โ†’ ( ( ๐‘‡ โŠ• ๐‘ˆ ) โˆˆ ๐‘† โ†” ( ( ๐‘‡ โŠ• ๐‘ˆ ) โˆˆ ( SubGrp โ€˜ ๐‘Š ) โˆง โˆ€ ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) โˆ€ ๐‘ข โˆˆ ( ๐‘‡ โŠ• ๐‘ˆ ) ( ๐‘Ž ( ยท๐‘  โ€˜ ๐‘Š ) ๐‘ข ) โˆˆ ( ๐‘‡ โŠ• ๐‘ˆ ) ) ) )
49 10 46 48 mpbir2and โŠข ( ( ๐‘Š โˆˆ LMod โˆง ๐‘‡ โˆˆ ๐‘† โˆง ๐‘ˆ โˆˆ ๐‘† ) โ†’ ( ๐‘‡ โŠ• ๐‘ˆ ) โˆˆ ๐‘† )