Step |
Hyp |
Ref |
Expression |
1 |
|
lsmelval2.v |
|- V = ( Base ` W ) |
2 |
|
lsmelval2.s |
|- S = ( LSubSp ` W ) |
3 |
|
lsmelval2.p |
|- .(+) = ( LSSum ` W ) |
4 |
|
lsmelval2.n |
|- N = ( LSpan ` W ) |
5 |
|
lsmelval2.w |
|- ( ph -> W e. LMod ) |
6 |
|
lsmelval2.t |
|- ( ph -> T e. S ) |
7 |
|
lsmelval2.u |
|- ( ph -> U e. S ) |
8 |
2
|
lsssubg |
|- ( ( W e. LMod /\ T e. S ) -> T e. ( SubGrp ` W ) ) |
9 |
5 6 8
|
syl2anc |
|- ( ph -> T e. ( SubGrp ` W ) ) |
10 |
2
|
lsssubg |
|- ( ( W e. LMod /\ U e. S ) -> U e. ( SubGrp ` W ) ) |
11 |
5 7 10
|
syl2anc |
|- ( ph -> U e. ( SubGrp ` W ) ) |
12 |
|
eqid |
|- ( +g ` W ) = ( +g ` W ) |
13 |
12 3
|
lsmelval |
|- ( ( T e. ( SubGrp ` W ) /\ U e. ( SubGrp ` W ) ) -> ( X e. ( T .(+) U ) <-> E. y e. T E. z e. U X = ( y ( +g ` W ) z ) ) ) |
14 |
9 11 13
|
syl2anc |
|- ( ph -> ( X e. ( T .(+) U ) <-> E. y e. T E. z e. U X = ( y ( +g ` W ) z ) ) ) |
15 |
5
|
adantr |
|- ( ( ph /\ ( y e. T /\ z e. U ) ) -> W e. LMod ) |
16 |
6
|
adantr |
|- ( ( ph /\ ( y e. T /\ z e. U ) ) -> T e. S ) |
17 |
|
simprl |
|- ( ( ph /\ ( y e. T /\ z e. U ) ) -> y e. T ) |
18 |
1 2
|
lssel |
|- ( ( T e. S /\ y e. T ) -> y e. V ) |
19 |
16 17 18
|
syl2anc |
|- ( ( ph /\ ( y e. T /\ z e. U ) ) -> y e. V ) |
20 |
1 2 4
|
lspsncl |
|- ( ( W e. LMod /\ y e. V ) -> ( N ` { y } ) e. S ) |
21 |
15 19 20
|
syl2anc |
|- ( ( ph /\ ( y e. T /\ z e. U ) ) -> ( N ` { y } ) e. S ) |
22 |
2
|
lsssubg |
|- ( ( W e. LMod /\ ( N ` { y } ) e. S ) -> ( N ` { y } ) e. ( SubGrp ` W ) ) |
23 |
15 21 22
|
syl2anc |
|- ( ( ph /\ ( y e. T /\ z e. U ) ) -> ( N ` { y } ) e. ( SubGrp ` W ) ) |
24 |
7
|
adantr |
|- ( ( ph /\ ( y e. T /\ z e. U ) ) -> U e. S ) |
25 |
|
simprr |
|- ( ( ph /\ ( y e. T /\ z e. U ) ) -> z e. U ) |
26 |
1 2
|
lssel |
|- ( ( U e. S /\ z e. U ) -> z e. V ) |
27 |
24 25 26
|
syl2anc |
|- ( ( ph /\ ( y e. T /\ z e. U ) ) -> z e. V ) |
28 |
1 2 4
|
lspsncl |
|- ( ( W e. LMod /\ z e. V ) -> ( N ` { z } ) e. S ) |
29 |
15 27 28
|
syl2anc |
|- ( ( ph /\ ( y e. T /\ z e. U ) ) -> ( N ` { z } ) e. S ) |
30 |
2
|
lsssubg |
|- ( ( W e. LMod /\ ( N ` { z } ) e. S ) -> ( N ` { z } ) e. ( SubGrp ` W ) ) |
31 |
15 29 30
|
syl2anc |
|- ( ( ph /\ ( y e. T /\ z e. U ) ) -> ( N ` { z } ) e. ( SubGrp ` W ) ) |
32 |
1 4
|
lspsnid |
|- ( ( W e. LMod /\ y e. V ) -> y e. ( N ` { y } ) ) |
33 |
15 19 32
|
syl2anc |
|- ( ( ph /\ ( y e. T /\ z e. U ) ) -> y e. ( N ` { y } ) ) |
34 |
1 4
|
lspsnid |
|- ( ( W e. LMod /\ z e. V ) -> z e. ( N ` { z } ) ) |
35 |
15 27 34
|
syl2anc |
|- ( ( ph /\ ( y e. T /\ z e. U ) ) -> z e. ( N ` { z } ) ) |
36 |
12 3
|
lsmelvali |
|- ( ( ( ( N ` { y } ) e. ( SubGrp ` W ) /\ ( N ` { z } ) e. ( SubGrp ` W ) ) /\ ( y e. ( N ` { y } ) /\ z e. ( N ` { z } ) ) ) -> ( y ( +g ` W ) z ) e. ( ( N ` { y } ) .(+) ( N ` { z } ) ) ) |
37 |
23 31 33 35 36
|
syl22anc |
|- ( ( ph /\ ( y e. T /\ z e. U ) ) -> ( y ( +g ` W ) z ) e. ( ( N ` { y } ) .(+) ( N ` { z } ) ) ) |
38 |
|
eleq1a |
|- ( ( y ( +g ` W ) z ) e. ( ( N ` { y } ) .(+) ( N ` { z } ) ) -> ( X = ( y ( +g ` W ) z ) -> X e. ( ( N ` { y } ) .(+) ( N ` { z } ) ) ) ) |
39 |
37 38
|
syl |
|- ( ( ph /\ ( y e. T /\ z e. U ) ) -> ( X = ( y ( +g ` W ) z ) -> X e. ( ( N ` { y } ) .(+) ( N ` { z } ) ) ) ) |
40 |
2 3
|
lsmcl |
|- ( ( W e. LMod /\ ( N ` { y } ) e. S /\ ( N ` { z } ) e. S ) -> ( ( N ` { y } ) .(+) ( N ` { z } ) ) e. S ) |
41 |
15 21 29 40
|
syl3anc |
|- ( ( ph /\ ( y e. T /\ z e. U ) ) -> ( ( N ` { y } ) .(+) ( N ` { z } ) ) e. S ) |
42 |
1 2 4 15 41
|
lspsnel6 |
|- ( ( ph /\ ( y e. T /\ z e. U ) ) -> ( X e. ( ( N ` { y } ) .(+) ( N ` { z } ) ) <-> ( X e. V /\ ( N ` { X } ) C_ ( ( N ` { y } ) .(+) ( N ` { z } ) ) ) ) ) |
43 |
39 42
|
sylibd |
|- ( ( ph /\ ( y e. T /\ z e. U ) ) -> ( X = ( y ( +g ` W ) z ) -> ( X e. V /\ ( N ` { X } ) C_ ( ( N ` { y } ) .(+) ( N ` { z } ) ) ) ) ) |
44 |
43
|
reximdvva |
|- ( ph -> ( E. y e. T E. z e. U X = ( y ( +g ` W ) z ) -> E. y e. T E. z e. U ( X e. V /\ ( N ` { X } ) C_ ( ( N ` { y } ) .(+) ( N ` { z } ) ) ) ) ) |
45 |
14 44
|
sylbid |
|- ( ph -> ( X e. ( T .(+) U ) -> E. y e. T E. z e. U ( X e. V /\ ( N ` { X } ) C_ ( ( N ` { y } ) .(+) ( N ` { z } ) ) ) ) ) |
46 |
9
|
adantr |
|- ( ( ph /\ ( y e. T /\ z e. U ) ) -> T e. ( SubGrp ` W ) ) |
47 |
2 4 15 16 17
|
lspsnel5a |
|- ( ( ph /\ ( y e. T /\ z e. U ) ) -> ( N ` { y } ) C_ T ) |
48 |
3
|
lsmless1 |
|- ( ( T e. ( SubGrp ` W ) /\ ( N ` { z } ) e. ( SubGrp ` W ) /\ ( N ` { y } ) C_ T ) -> ( ( N ` { y } ) .(+) ( N ` { z } ) ) C_ ( T .(+) ( N ` { z } ) ) ) |
49 |
46 31 47 48
|
syl3anc |
|- ( ( ph /\ ( y e. T /\ z e. U ) ) -> ( ( N ` { y } ) .(+) ( N ` { z } ) ) C_ ( T .(+) ( N ` { z } ) ) ) |
50 |
11
|
adantr |
|- ( ( ph /\ ( y e. T /\ z e. U ) ) -> U e. ( SubGrp ` W ) ) |
51 |
2 4 15 24 25
|
lspsnel5a |
|- ( ( ph /\ ( y e. T /\ z e. U ) ) -> ( N ` { z } ) C_ U ) |
52 |
3
|
lsmless2 |
|- ( ( T e. ( SubGrp ` W ) /\ U e. ( SubGrp ` W ) /\ ( N ` { z } ) C_ U ) -> ( T .(+) ( N ` { z } ) ) C_ ( T .(+) U ) ) |
53 |
46 50 51 52
|
syl3anc |
|- ( ( ph /\ ( y e. T /\ z e. U ) ) -> ( T .(+) ( N ` { z } ) ) C_ ( T .(+) U ) ) |
54 |
49 53
|
sstrd |
|- ( ( ph /\ ( y e. T /\ z e. U ) ) -> ( ( N ` { y } ) .(+) ( N ` { z } ) ) C_ ( T .(+) U ) ) |
55 |
54
|
sseld |
|- ( ( ph /\ ( y e. T /\ z e. U ) ) -> ( X e. ( ( N ` { y } ) .(+) ( N ` { z } ) ) -> X e. ( T .(+) U ) ) ) |
56 |
42 55
|
sylbird |
|- ( ( ph /\ ( y e. T /\ z e. U ) ) -> ( ( X e. V /\ ( N ` { X } ) C_ ( ( N ` { y } ) .(+) ( N ` { z } ) ) ) -> X e. ( T .(+) U ) ) ) |
57 |
56
|
rexlimdvva |
|- ( ph -> ( E. y e. T E. z e. U ( X e. V /\ ( N ` { X } ) C_ ( ( N ` { y } ) .(+) ( N ` { z } ) ) ) -> X e. ( T .(+) U ) ) ) |
58 |
45 57
|
impbid |
|- ( ph -> ( X e. ( T .(+) U ) <-> E. y e. T E. z e. U ( X e. V /\ ( N ` { X } ) C_ ( ( N ` { y } ) .(+) ( N ` { z } ) ) ) ) ) |
59 |
|
r19.42v |
|- ( E. z e. U ( X e. V /\ ( N ` { X } ) C_ ( ( N ` { y } ) .(+) ( N ` { z } ) ) ) <-> ( X e. V /\ E. z e. U ( N ` { X } ) C_ ( ( N ` { y } ) .(+) ( N ` { z } ) ) ) ) |
60 |
59
|
rexbii |
|- ( E. y e. T E. z e. U ( X e. V /\ ( N ` { X } ) C_ ( ( N ` { y } ) .(+) ( N ` { z } ) ) ) <-> E. y e. T ( X e. V /\ E. z e. U ( N ` { X } ) C_ ( ( N ` { y } ) .(+) ( N ` { z } ) ) ) ) |
61 |
|
r19.42v |
|- ( E. y e. T ( X e. V /\ E. z e. U ( N ` { X } ) C_ ( ( N ` { y } ) .(+) ( N ` { z } ) ) ) <-> ( X e. V /\ E. y e. T E. z e. U ( N ` { X } ) C_ ( ( N ` { y } ) .(+) ( N ` { z } ) ) ) ) |
62 |
60 61
|
bitri |
|- ( E. y e. T E. z e. U ( X e. V /\ ( N ` { X } ) C_ ( ( N ` { y } ) .(+) ( N ` { z } ) ) ) <-> ( X e. V /\ E. y e. T E. z e. U ( N ` { X } ) C_ ( ( N ` { y } ) .(+) ( N ` { z } ) ) ) ) |
63 |
58 62
|
bitrdi |
|- ( ph -> ( X e. ( T .(+) U ) <-> ( X e. V /\ E. y e. T E. z e. U ( N ` { X } ) C_ ( ( N ` { y } ) .(+) ( N ` { z } ) ) ) ) ) |