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