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 โง ๐ โ ๐ โง ๐ โ ๐ ) โ ( ๐ โ ๐ ) โ ๐ ) |