Metamath Proof Explorer


Theorem islss3

Description: A linear subspace of a module is a subset which is a module in its own right. (Contributed by Stefan O'Rear, 6-Dec-2014) (Revised by Mario Carneiro, 30-Apr-2015)

Ref Expression
Hypotheses islss3.x โŠข ๐‘‹ = ( ๐‘Š โ†พs ๐‘ˆ )
islss3.v โŠข ๐‘‰ = ( Base โ€˜ ๐‘Š )
islss3.s โŠข ๐‘† = ( LSubSp โ€˜ ๐‘Š )
Assertion islss3 ( ๐‘Š โˆˆ LMod โ†’ ( ๐‘ˆ โˆˆ ๐‘† โ†” ( ๐‘ˆ โŠ† ๐‘‰ โˆง ๐‘‹ โˆˆ LMod ) ) )

Proof

Step Hyp Ref Expression
1 islss3.x โŠข ๐‘‹ = ( ๐‘Š โ†พs ๐‘ˆ )
2 islss3.v โŠข ๐‘‰ = ( Base โ€˜ ๐‘Š )
3 islss3.s โŠข ๐‘† = ( LSubSp โ€˜ ๐‘Š )
4 2 3 lssss โŠข ( ๐‘ˆ โˆˆ ๐‘† โ†’ ๐‘ˆ โŠ† ๐‘‰ )
5 4 adantl โŠข ( ( ๐‘Š โˆˆ LMod โˆง ๐‘ˆ โˆˆ ๐‘† ) โ†’ ๐‘ˆ โŠ† ๐‘‰ )
6 1 2 ressbas2 โŠข ( ๐‘ˆ โŠ† ๐‘‰ โ†’ ๐‘ˆ = ( Base โ€˜ ๐‘‹ ) )
7 6 adantl โŠข ( ( ๐‘Š โˆˆ LMod โˆง ๐‘ˆ โŠ† ๐‘‰ ) โ†’ ๐‘ˆ = ( Base โ€˜ ๐‘‹ ) )
8 4 7 sylan2 โŠข ( ( ๐‘Š โˆˆ LMod โˆง ๐‘ˆ โˆˆ ๐‘† ) โ†’ ๐‘ˆ = ( Base โ€˜ ๐‘‹ ) )
9 eqid โŠข ( +g โ€˜ ๐‘Š ) = ( +g โ€˜ ๐‘Š )
10 1 9 ressplusg โŠข ( ๐‘ˆ โˆˆ ๐‘† โ†’ ( +g โ€˜ ๐‘Š ) = ( +g โ€˜ ๐‘‹ ) )
11 10 adantl โŠข ( ( ๐‘Š โˆˆ LMod โˆง ๐‘ˆ โˆˆ ๐‘† ) โ†’ ( +g โ€˜ ๐‘Š ) = ( +g โ€˜ ๐‘‹ ) )
12 eqid โŠข ( Scalar โ€˜ ๐‘Š ) = ( Scalar โ€˜ ๐‘Š )
13 1 12 resssca โŠข ( ๐‘ˆ โˆˆ ๐‘† โ†’ ( Scalar โ€˜ ๐‘Š ) = ( Scalar โ€˜ ๐‘‹ ) )
14 13 adantl โŠข ( ( ๐‘Š โˆˆ LMod โˆง ๐‘ˆ โˆˆ ๐‘† ) โ†’ ( Scalar โ€˜ ๐‘Š ) = ( Scalar โ€˜ ๐‘‹ ) )
15 eqid โŠข ( ยท๐‘  โ€˜ ๐‘Š ) = ( ยท๐‘  โ€˜ ๐‘Š )
16 1 15 ressvsca โŠข ( ๐‘ˆ โˆˆ ๐‘† โ†’ ( ยท๐‘  โ€˜ ๐‘Š ) = ( ยท๐‘  โ€˜ ๐‘‹ ) )
17 16 adantl โŠข ( ( ๐‘Š โˆˆ LMod โˆง ๐‘ˆ โˆˆ ๐‘† ) โ†’ ( ยท๐‘  โ€˜ ๐‘Š ) = ( ยท๐‘  โ€˜ ๐‘‹ ) )
18 eqidd โŠข ( ( ๐‘Š โˆˆ LMod โˆง ๐‘ˆ โˆˆ ๐‘† ) โ†’ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) = ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) )
19 eqidd โŠข ( ( ๐‘Š โˆˆ LMod โˆง ๐‘ˆ โˆˆ ๐‘† ) โ†’ ( +g โ€˜ ( Scalar โ€˜ ๐‘Š ) ) = ( +g โ€˜ ( Scalar โ€˜ ๐‘Š ) ) )
20 eqidd โŠข ( ( ๐‘Š โˆˆ LMod โˆง ๐‘ˆ โˆˆ ๐‘† ) โ†’ ( .r โ€˜ ( Scalar โ€˜ ๐‘Š ) ) = ( .r โ€˜ ( Scalar โ€˜ ๐‘Š ) ) )
21 eqidd โŠข ( ( ๐‘Š โˆˆ LMod โˆง ๐‘ˆ โˆˆ ๐‘† ) โ†’ ( 1r โ€˜ ( Scalar โ€˜ ๐‘Š ) ) = ( 1r โ€˜ ( Scalar โ€˜ ๐‘Š ) ) )
22 12 lmodring โŠข ( ๐‘Š โˆˆ LMod โ†’ ( Scalar โ€˜ ๐‘Š ) โˆˆ Ring )
23 22 adantr โŠข ( ( ๐‘Š โˆˆ LMod โˆง ๐‘ˆ โˆˆ ๐‘† ) โ†’ ( Scalar โ€˜ ๐‘Š ) โˆˆ Ring )
24 3 lsssubg โŠข ( ( ๐‘Š โˆˆ LMod โˆง ๐‘ˆ โˆˆ ๐‘† ) โ†’ ๐‘ˆ โˆˆ ( SubGrp โ€˜ ๐‘Š ) )
25 1 subggrp โŠข ( ๐‘ˆ โˆˆ ( SubGrp โ€˜ ๐‘Š ) โ†’ ๐‘‹ โˆˆ Grp )
26 24 25 syl โŠข ( ( ๐‘Š โˆˆ LMod โˆง ๐‘ˆ โˆˆ ๐‘† ) โ†’ ๐‘‹ โˆˆ Grp )
27 eqid โŠข ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) = ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) )
28 12 15 27 3 lssvscl โŠข ( ( ( ๐‘Š โˆˆ LMod โˆง ๐‘ˆ โˆˆ ๐‘† ) โˆง ( ๐‘ฅ โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) โˆง ๐‘Ž โˆˆ ๐‘ˆ ) ) โ†’ ( ๐‘ฅ ( ยท๐‘  โ€˜ ๐‘Š ) ๐‘Ž ) โˆˆ ๐‘ˆ )
29 28 3impb โŠข ( ( ( ๐‘Š โˆˆ LMod โˆง ๐‘ˆ โˆˆ ๐‘† ) โˆง ๐‘ฅ โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) โˆง ๐‘Ž โˆˆ ๐‘ˆ ) โ†’ ( ๐‘ฅ ( ยท๐‘  โ€˜ ๐‘Š ) ๐‘Ž ) โˆˆ ๐‘ˆ )
30 simpll โŠข ( ( ( ๐‘Š โˆˆ LMod โˆง ๐‘ˆ โˆˆ ๐‘† ) โˆง ( ๐‘ฅ โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) โˆง ๐‘Ž โˆˆ ๐‘ˆ โˆง ๐‘ โˆˆ ๐‘ˆ ) ) โ†’ ๐‘Š โˆˆ LMod )
31 simpr1 โŠข ( ( ( ๐‘Š โˆˆ LMod โˆง ๐‘ˆ โˆˆ ๐‘† ) โˆง ( ๐‘ฅ โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) โˆง ๐‘Ž โˆˆ ๐‘ˆ โˆง ๐‘ โˆˆ ๐‘ˆ ) ) โ†’ ๐‘ฅ โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) )
32 4 ad2antlr โŠข ( ( ( ๐‘Š โˆˆ LMod โˆง ๐‘ˆ โˆˆ ๐‘† ) โˆง ( ๐‘ฅ โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) โˆง ๐‘Ž โˆˆ ๐‘ˆ โˆง ๐‘ โˆˆ ๐‘ˆ ) ) โ†’ ๐‘ˆ โŠ† ๐‘‰ )
33 simpr2 โŠข ( ( ( ๐‘Š โˆˆ LMod โˆง ๐‘ˆ โˆˆ ๐‘† ) โˆง ( ๐‘ฅ โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) โˆง ๐‘Ž โˆˆ ๐‘ˆ โˆง ๐‘ โˆˆ ๐‘ˆ ) ) โ†’ ๐‘Ž โˆˆ ๐‘ˆ )
34 32 33 sseldd โŠข ( ( ( ๐‘Š โˆˆ LMod โˆง ๐‘ˆ โˆˆ ๐‘† ) โˆง ( ๐‘ฅ โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) โˆง ๐‘Ž โˆˆ ๐‘ˆ โˆง ๐‘ โˆˆ ๐‘ˆ ) ) โ†’ ๐‘Ž โˆˆ ๐‘‰ )
35 simpr3 โŠข ( ( ( ๐‘Š โˆˆ LMod โˆง ๐‘ˆ โˆˆ ๐‘† ) โˆง ( ๐‘ฅ โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) โˆง ๐‘Ž โˆˆ ๐‘ˆ โˆง ๐‘ โˆˆ ๐‘ˆ ) ) โ†’ ๐‘ โˆˆ ๐‘ˆ )
36 32 35 sseldd โŠข ( ( ( ๐‘Š โˆˆ LMod โˆง ๐‘ˆ โˆˆ ๐‘† ) โˆง ( ๐‘ฅ โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) โˆง ๐‘Ž โˆˆ ๐‘ˆ โˆง ๐‘ โˆˆ ๐‘ˆ ) ) โ†’ ๐‘ โˆˆ ๐‘‰ )
37 2 9 12 15 27 lmodvsdi โŠข ( ( ๐‘Š โˆˆ LMod โˆง ( ๐‘ฅ โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) โˆง ๐‘Ž โˆˆ ๐‘‰ โˆง ๐‘ โˆˆ ๐‘‰ ) ) โ†’ ( ๐‘ฅ ( ยท๐‘  โ€˜ ๐‘Š ) ( ๐‘Ž ( +g โ€˜ ๐‘Š ) ๐‘ ) ) = ( ( ๐‘ฅ ( ยท๐‘  โ€˜ ๐‘Š ) ๐‘Ž ) ( +g โ€˜ ๐‘Š ) ( ๐‘ฅ ( ยท๐‘  โ€˜ ๐‘Š ) ๐‘ ) ) )
38 30 31 34 36 37 syl13anc โŠข ( ( ( ๐‘Š โˆˆ LMod โˆง ๐‘ˆ โˆˆ ๐‘† ) โˆง ( ๐‘ฅ โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) โˆง ๐‘Ž โˆˆ ๐‘ˆ โˆง ๐‘ โˆˆ ๐‘ˆ ) ) โ†’ ( ๐‘ฅ ( ยท๐‘  โ€˜ ๐‘Š ) ( ๐‘Ž ( +g โ€˜ ๐‘Š ) ๐‘ ) ) = ( ( ๐‘ฅ ( ยท๐‘  โ€˜ ๐‘Š ) ๐‘Ž ) ( +g โ€˜ ๐‘Š ) ( ๐‘ฅ ( ยท๐‘  โ€˜ ๐‘Š ) ๐‘ ) ) )
39 simpll โŠข ( ( ( ๐‘Š โˆˆ LMod โˆง ๐‘ˆ โˆˆ ๐‘† ) โˆง ( ๐‘ฅ โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) โˆง ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) โˆง ๐‘ โˆˆ ๐‘ˆ ) ) โ†’ ๐‘Š โˆˆ LMod )
40 simpr1 โŠข ( ( ( ๐‘Š โˆˆ LMod โˆง ๐‘ˆ โˆˆ ๐‘† ) โˆง ( ๐‘ฅ โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) โˆง ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) โˆง ๐‘ โˆˆ ๐‘ˆ ) ) โ†’ ๐‘ฅ โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) )
41 simpr2 โŠข ( ( ( ๐‘Š โˆˆ LMod โˆง ๐‘ˆ โˆˆ ๐‘† ) โˆง ( ๐‘ฅ โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) โˆง ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) โˆง ๐‘ โˆˆ ๐‘ˆ ) ) โ†’ ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) )
42 4 ad2antlr โŠข ( ( ( ๐‘Š โˆˆ LMod โˆง ๐‘ˆ โˆˆ ๐‘† ) โˆง ( ๐‘ฅ โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) โˆง ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) โˆง ๐‘ โˆˆ ๐‘ˆ ) ) โ†’ ๐‘ˆ โŠ† ๐‘‰ )
43 simpr3 โŠข ( ( ( ๐‘Š โˆˆ LMod โˆง ๐‘ˆ โˆˆ ๐‘† ) โˆง ( ๐‘ฅ โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) โˆง ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) โˆง ๐‘ โˆˆ ๐‘ˆ ) ) โ†’ ๐‘ โˆˆ ๐‘ˆ )
44 42 43 sseldd โŠข ( ( ( ๐‘Š โˆˆ LMod โˆง ๐‘ˆ โˆˆ ๐‘† ) โˆง ( ๐‘ฅ โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) โˆง ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) โˆง ๐‘ โˆˆ ๐‘ˆ ) ) โ†’ ๐‘ โˆˆ ๐‘‰ )
45 eqid โŠข ( +g โ€˜ ( Scalar โ€˜ ๐‘Š ) ) = ( +g โ€˜ ( Scalar โ€˜ ๐‘Š ) )
46 2 9 12 15 27 45 lmodvsdir โŠข ( ( ๐‘Š โˆˆ LMod โˆง ( ๐‘ฅ โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) โˆง ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) โˆง ๐‘ โˆˆ ๐‘‰ ) ) โ†’ ( ( ๐‘ฅ ( +g โ€˜ ( Scalar โ€˜ ๐‘Š ) ) ๐‘Ž ) ( ยท๐‘  โ€˜ ๐‘Š ) ๐‘ ) = ( ( ๐‘ฅ ( ยท๐‘  โ€˜ ๐‘Š ) ๐‘ ) ( +g โ€˜ ๐‘Š ) ( ๐‘Ž ( ยท๐‘  โ€˜ ๐‘Š ) ๐‘ ) ) )
47 39 40 41 44 46 syl13anc โŠข ( ( ( ๐‘Š โˆˆ LMod โˆง ๐‘ˆ โˆˆ ๐‘† ) โˆง ( ๐‘ฅ โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) โˆง ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) โˆง ๐‘ โˆˆ ๐‘ˆ ) ) โ†’ ( ( ๐‘ฅ ( +g โ€˜ ( Scalar โ€˜ ๐‘Š ) ) ๐‘Ž ) ( ยท๐‘  โ€˜ ๐‘Š ) ๐‘ ) = ( ( ๐‘ฅ ( ยท๐‘  โ€˜ ๐‘Š ) ๐‘ ) ( +g โ€˜ ๐‘Š ) ( ๐‘Ž ( ยท๐‘  โ€˜ ๐‘Š ) ๐‘ ) ) )
48 eqid โŠข ( .r โ€˜ ( Scalar โ€˜ ๐‘Š ) ) = ( .r โ€˜ ( Scalar โ€˜ ๐‘Š ) )
49 2 12 15 27 48 lmodvsass โŠข ( ( ๐‘Š โˆˆ LMod โˆง ( ๐‘ฅ โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) โˆง ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) โˆง ๐‘ โˆˆ ๐‘‰ ) ) โ†’ ( ( ๐‘ฅ ( .r โ€˜ ( Scalar โ€˜ ๐‘Š ) ) ๐‘Ž ) ( ยท๐‘  โ€˜ ๐‘Š ) ๐‘ ) = ( ๐‘ฅ ( ยท๐‘  โ€˜ ๐‘Š ) ( ๐‘Ž ( ยท๐‘  โ€˜ ๐‘Š ) ๐‘ ) ) )
50 39 40 41 44 49 syl13anc โŠข ( ( ( ๐‘Š โˆˆ LMod โˆง ๐‘ˆ โˆˆ ๐‘† ) โˆง ( ๐‘ฅ โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) โˆง ๐‘Ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) โˆง ๐‘ โˆˆ ๐‘ˆ ) ) โ†’ ( ( ๐‘ฅ ( .r โ€˜ ( Scalar โ€˜ ๐‘Š ) ) ๐‘Ž ) ( ยท๐‘  โ€˜ ๐‘Š ) ๐‘ ) = ( ๐‘ฅ ( ยท๐‘  โ€˜ ๐‘Š ) ( ๐‘Ž ( ยท๐‘  โ€˜ ๐‘Š ) ๐‘ ) ) )
51 5 sselda โŠข ( ( ( ๐‘Š โˆˆ LMod โˆง ๐‘ˆ โˆˆ ๐‘† ) โˆง ๐‘ฅ โˆˆ ๐‘ˆ ) โ†’ ๐‘ฅ โˆˆ ๐‘‰ )
52 eqid โŠข ( 1r โ€˜ ( Scalar โ€˜ ๐‘Š ) ) = ( 1r โ€˜ ( Scalar โ€˜ ๐‘Š ) )
53 2 12 15 52 lmodvs1 โŠข ( ( ๐‘Š โˆˆ LMod โˆง ๐‘ฅ โˆˆ ๐‘‰ ) โ†’ ( ( 1r โ€˜ ( Scalar โ€˜ ๐‘Š ) ) ( ยท๐‘  โ€˜ ๐‘Š ) ๐‘ฅ ) = ๐‘ฅ )
54 53 adantlr โŠข ( ( ( ๐‘Š โˆˆ LMod โˆง ๐‘ˆ โˆˆ ๐‘† ) โˆง ๐‘ฅ โˆˆ ๐‘‰ ) โ†’ ( ( 1r โ€˜ ( Scalar โ€˜ ๐‘Š ) ) ( ยท๐‘  โ€˜ ๐‘Š ) ๐‘ฅ ) = ๐‘ฅ )
55 51 54 syldan โŠข ( ( ( ๐‘Š โˆˆ LMod โˆง ๐‘ˆ โˆˆ ๐‘† ) โˆง ๐‘ฅ โˆˆ ๐‘ˆ ) โ†’ ( ( 1r โ€˜ ( Scalar โ€˜ ๐‘Š ) ) ( ยท๐‘  โ€˜ ๐‘Š ) ๐‘ฅ ) = ๐‘ฅ )
56 8 11 14 17 18 19 20 21 23 26 29 38 47 50 55 islmodd โŠข ( ( ๐‘Š โˆˆ LMod โˆง ๐‘ˆ โˆˆ ๐‘† ) โ†’ ๐‘‹ โˆˆ LMod )
57 5 56 jca โŠข ( ( ๐‘Š โˆˆ LMod โˆง ๐‘ˆ โˆˆ ๐‘† ) โ†’ ( ๐‘ˆ โŠ† ๐‘‰ โˆง ๐‘‹ โˆˆ LMod ) )
58 simprl โŠข ( ( ๐‘Š โˆˆ LMod โˆง ( ๐‘ˆ โŠ† ๐‘‰ โˆง ๐‘‹ โˆˆ LMod ) ) โ†’ ๐‘ˆ โŠ† ๐‘‰ )
59 58 6 syl โŠข ( ( ๐‘Š โˆˆ LMod โˆง ( ๐‘ˆ โŠ† ๐‘‰ โˆง ๐‘‹ โˆˆ LMod ) ) โ†’ ๐‘ˆ = ( Base โ€˜ ๐‘‹ ) )
60 fvex โŠข ( Base โ€˜ ๐‘‹ ) โˆˆ V
61 59 60 eqeltrdi โŠข ( ( ๐‘Š โˆˆ LMod โˆง ( ๐‘ˆ โŠ† ๐‘‰ โˆง ๐‘‹ โˆˆ LMod ) ) โ†’ ๐‘ˆ โˆˆ V )
62 1 12 resssca โŠข ( ๐‘ˆ โˆˆ V โ†’ ( Scalar โ€˜ ๐‘Š ) = ( Scalar โ€˜ ๐‘‹ ) )
63 61 62 syl โŠข ( ( ๐‘Š โˆˆ LMod โˆง ( ๐‘ˆ โŠ† ๐‘‰ โˆง ๐‘‹ โˆˆ LMod ) ) โ†’ ( Scalar โ€˜ ๐‘Š ) = ( Scalar โ€˜ ๐‘‹ ) )
64 63 eqcomd โŠข ( ( ๐‘Š โˆˆ LMod โˆง ( ๐‘ˆ โŠ† ๐‘‰ โˆง ๐‘‹ โˆˆ LMod ) ) โ†’ ( Scalar โ€˜ ๐‘‹ ) = ( Scalar โ€˜ ๐‘Š ) )
65 eqidd โŠข ( ( ๐‘Š โˆˆ LMod โˆง ( ๐‘ˆ โŠ† ๐‘‰ โˆง ๐‘‹ โˆˆ LMod ) ) โ†’ ( Base โ€˜ ( Scalar โ€˜ ๐‘‹ ) ) = ( Base โ€˜ ( Scalar โ€˜ ๐‘‹ ) ) )
66 2 a1i โŠข ( ( ๐‘Š โˆˆ LMod โˆง ( ๐‘ˆ โŠ† ๐‘‰ โˆง ๐‘‹ โˆˆ LMod ) ) โ†’ ๐‘‰ = ( Base โ€˜ ๐‘Š ) )
67 1 9 ressplusg โŠข ( ๐‘ˆ โˆˆ V โ†’ ( +g โ€˜ ๐‘Š ) = ( +g โ€˜ ๐‘‹ ) )
68 61 67 syl โŠข ( ( ๐‘Š โˆˆ LMod โˆง ( ๐‘ˆ โŠ† ๐‘‰ โˆง ๐‘‹ โˆˆ LMod ) ) โ†’ ( +g โ€˜ ๐‘Š ) = ( +g โ€˜ ๐‘‹ ) )
69 68 eqcomd โŠข ( ( ๐‘Š โˆˆ LMod โˆง ( ๐‘ˆ โŠ† ๐‘‰ โˆง ๐‘‹ โˆˆ LMod ) ) โ†’ ( +g โ€˜ ๐‘‹ ) = ( +g โ€˜ ๐‘Š ) )
70 1 15 ressvsca โŠข ( ๐‘ˆ โˆˆ V โ†’ ( ยท๐‘  โ€˜ ๐‘Š ) = ( ยท๐‘  โ€˜ ๐‘‹ ) )
71 61 70 syl โŠข ( ( ๐‘Š โˆˆ LMod โˆง ( ๐‘ˆ โŠ† ๐‘‰ โˆง ๐‘‹ โˆˆ LMod ) ) โ†’ ( ยท๐‘  โ€˜ ๐‘Š ) = ( ยท๐‘  โ€˜ ๐‘‹ ) )
72 71 eqcomd โŠข ( ( ๐‘Š โˆˆ LMod โˆง ( ๐‘ˆ โŠ† ๐‘‰ โˆง ๐‘‹ โˆˆ LMod ) ) โ†’ ( ยท๐‘  โ€˜ ๐‘‹ ) = ( ยท๐‘  โ€˜ ๐‘Š ) )
73 3 a1i โŠข ( ( ๐‘Š โˆˆ LMod โˆง ( ๐‘ˆ โŠ† ๐‘‰ โˆง ๐‘‹ โˆˆ LMod ) ) โ†’ ๐‘† = ( LSubSp โ€˜ ๐‘Š ) )
74 59 58 eqsstrrd โŠข ( ( ๐‘Š โˆˆ LMod โˆง ( ๐‘ˆ โŠ† ๐‘‰ โˆง ๐‘‹ โˆˆ LMod ) ) โ†’ ( Base โ€˜ ๐‘‹ ) โŠ† ๐‘‰ )
75 lmodgrp โŠข ( ๐‘‹ โˆˆ LMod โ†’ ๐‘‹ โˆˆ Grp )
76 75 ad2antll โŠข ( ( ๐‘Š โˆˆ LMod โˆง ( ๐‘ˆ โŠ† ๐‘‰ โˆง ๐‘‹ โˆˆ LMod ) ) โ†’ ๐‘‹ โˆˆ Grp )
77 eqid โŠข ( Base โ€˜ ๐‘‹ ) = ( Base โ€˜ ๐‘‹ )
78 77 grpbn0 โŠข ( ๐‘‹ โˆˆ Grp โ†’ ( Base โ€˜ ๐‘‹ ) โ‰  โˆ… )
79 76 78 syl โŠข ( ( ๐‘Š โˆˆ LMod โˆง ( ๐‘ˆ โŠ† ๐‘‰ โˆง ๐‘‹ โˆˆ LMod ) ) โ†’ ( Base โ€˜ ๐‘‹ ) โ‰  โˆ… )
80 eqid โŠข ( LSubSp โ€˜ ๐‘‹ ) = ( LSubSp โ€˜ ๐‘‹ )
81 77 80 lss1 โŠข ( ๐‘‹ โˆˆ LMod โ†’ ( Base โ€˜ ๐‘‹ ) โˆˆ ( LSubSp โ€˜ ๐‘‹ ) )
82 81 ad2antll โŠข ( ( ๐‘Š โˆˆ LMod โˆง ( ๐‘ˆ โŠ† ๐‘‰ โˆง ๐‘‹ โˆˆ LMod ) ) โ†’ ( Base โ€˜ ๐‘‹ ) โˆˆ ( LSubSp โ€˜ ๐‘‹ ) )
83 eqid โŠข ( Scalar โ€˜ ๐‘‹ ) = ( Scalar โ€˜ ๐‘‹ )
84 eqid โŠข ( Base โ€˜ ( Scalar โ€˜ ๐‘‹ ) ) = ( Base โ€˜ ( Scalar โ€˜ ๐‘‹ ) )
85 eqid โŠข ( +g โ€˜ ๐‘‹ ) = ( +g โ€˜ ๐‘‹ )
86 eqid โŠข ( ยท๐‘  โ€˜ ๐‘‹ ) = ( ยท๐‘  โ€˜ ๐‘‹ )
87 83 84 85 86 80 lsscl โŠข ( ( ( Base โ€˜ ๐‘‹ ) โˆˆ ( LSubSp โ€˜ ๐‘‹ ) โˆง ( ๐‘ฅ โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘‹ ) ) โˆง ๐‘Ž โˆˆ ( Base โ€˜ ๐‘‹ ) โˆง ๐‘ โˆˆ ( Base โ€˜ ๐‘‹ ) ) ) โ†’ ( ( ๐‘ฅ ( ยท๐‘  โ€˜ ๐‘‹ ) ๐‘Ž ) ( +g โ€˜ ๐‘‹ ) ๐‘ ) โˆˆ ( Base โ€˜ ๐‘‹ ) )
88 82 87 sylan โŠข ( ( ( ๐‘Š โˆˆ LMod โˆง ( ๐‘ˆ โŠ† ๐‘‰ โˆง ๐‘‹ โˆˆ LMod ) ) โˆง ( ๐‘ฅ โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘‹ ) ) โˆง ๐‘Ž โˆˆ ( Base โ€˜ ๐‘‹ ) โˆง ๐‘ โˆˆ ( Base โ€˜ ๐‘‹ ) ) ) โ†’ ( ( ๐‘ฅ ( ยท๐‘  โ€˜ ๐‘‹ ) ๐‘Ž ) ( +g โ€˜ ๐‘‹ ) ๐‘ ) โˆˆ ( Base โ€˜ ๐‘‹ ) )
89 64 65 66 69 72 73 74 79 88 islssd โŠข ( ( ๐‘Š โˆˆ LMod โˆง ( ๐‘ˆ โŠ† ๐‘‰ โˆง ๐‘‹ โˆˆ LMod ) ) โ†’ ( Base โ€˜ ๐‘‹ ) โˆˆ ๐‘† )
90 59 89 eqeltrd โŠข ( ( ๐‘Š โˆˆ LMod โˆง ( ๐‘ˆ โŠ† ๐‘‰ โˆง ๐‘‹ โˆˆ LMod ) ) โ†’ ๐‘ˆ โˆˆ ๐‘† )
91 57 90 impbida โŠข ( ๐‘Š โˆˆ LMod โ†’ ( ๐‘ˆ โˆˆ ๐‘† โ†” ( ๐‘ˆ โŠ† ๐‘‰ โˆง ๐‘‹ โˆˆ LMod ) ) )