Step |
Hyp |
Ref |
Expression |
1 |
|
lsatexch.s |
|- S = ( LSubSp ` W ) |
2 |
|
lsatexch.p |
|- .(+) = ( LSSum ` W ) |
3 |
|
lsatexch.o |
|- .0. = ( 0g ` W ) |
4 |
|
lsatexch.a |
|- A = ( LSAtoms ` W ) |
5 |
|
lsatexch.w |
|- ( ph -> W e. LVec ) |
6 |
|
lsatexch.u |
|- ( ph -> U e. S ) |
7 |
|
lsatexch.q |
|- ( ph -> Q e. A ) |
8 |
|
lsatexch.r |
|- ( ph -> R e. A ) |
9 |
|
lsatexch.l |
|- ( ph -> Q C_ ( U .(+) R ) ) |
10 |
|
lsatexch.z |
|- ( ph -> ( U i^i Q ) = { .0. } ) |
11 |
|
lveclmod |
|- ( W e. LVec -> W e. LMod ) |
12 |
5 11
|
syl |
|- ( ph -> W e. LMod ) |
13 |
1
|
lsssssubg |
|- ( W e. LMod -> S C_ ( SubGrp ` W ) ) |
14 |
12 13
|
syl |
|- ( ph -> S C_ ( SubGrp ` W ) ) |
15 |
14 6
|
sseldd |
|- ( ph -> U e. ( SubGrp ` W ) ) |
16 |
1 4 12 8
|
lsatlssel |
|- ( ph -> R e. S ) |
17 |
14 16
|
sseldd |
|- ( ph -> R e. ( SubGrp ` W ) ) |
18 |
2
|
lsmub2 |
|- ( ( U e. ( SubGrp ` W ) /\ R e. ( SubGrp ` W ) ) -> R C_ ( U .(+) R ) ) |
19 |
15 17 18
|
syl2anc |
|- ( ph -> R C_ ( U .(+) R ) ) |
20 |
|
eqid |
|- (
|
21 |
1 2
|
lsmcl |
|- ( ( W e. LMod /\ U e. S /\ R e. S ) -> ( U .(+) R ) e. S ) |
22 |
12 6 16 21
|
syl3anc |
|- ( ph -> ( U .(+) R ) e. S ) |
23 |
1 4 12 7
|
lsatlssel |
|- ( ph -> Q e. S ) |
24 |
1 2
|
lsmcl |
|- ( ( W e. LMod /\ U e. S /\ Q e. S ) -> ( U .(+) Q ) e. S ) |
25 |
12 6 23 24
|
syl3anc |
|- ( ph -> ( U .(+) Q ) e. S ) |
26 |
1 2 3 4 20 5 6 7
|
lcvp |
|- ( ph -> ( ( U i^i Q ) = { .0. } <-> U (
|
27 |
10 26
|
mpbid |
|- ( ph -> U (
|
28 |
1 20 5 6 25 27
|
lcvpss |
|- ( ph -> U C. ( U .(+) Q ) ) |
29 |
2
|
lsmub1 |
|- ( ( U e. ( SubGrp ` W ) /\ R e. ( SubGrp ` W ) ) -> U C_ ( U .(+) R ) ) |
30 |
15 17 29
|
syl2anc |
|- ( ph -> U C_ ( U .(+) R ) ) |
31 |
14 23
|
sseldd |
|- ( ph -> Q e. ( SubGrp ` W ) ) |
32 |
14 22
|
sseldd |
|- ( ph -> ( U .(+) R ) e. ( SubGrp ` W ) ) |
33 |
2
|
lsmlub |
|- ( ( U e. ( SubGrp ` W ) /\ Q e. ( SubGrp ` W ) /\ ( U .(+) R ) e. ( SubGrp ` W ) ) -> ( ( U C_ ( U .(+) R ) /\ Q C_ ( U .(+) R ) ) <-> ( U .(+) Q ) C_ ( U .(+) R ) ) ) |
34 |
15 31 32 33
|
syl3anc |
|- ( ph -> ( ( U C_ ( U .(+) R ) /\ Q C_ ( U .(+) R ) ) <-> ( U .(+) Q ) C_ ( U .(+) R ) ) ) |
35 |
30 9 34
|
mpbi2and |
|- ( ph -> ( U .(+) Q ) C_ ( U .(+) R ) ) |
36 |
28 35
|
psssstrd |
|- ( ph -> U C. ( U .(+) R ) ) |
37 |
1 2 4 20 5 6 8
|
lcv2 |
|- ( ph -> ( U C. ( U .(+) R ) <-> U (
|
38 |
36 37
|
mpbid |
|- ( ph -> U (
|
39 |
1 20 5 6 22 25 38 28 35
|
lcvnbtwn2 |
|- ( ph -> ( U .(+) Q ) = ( U .(+) R ) ) |
40 |
19 39
|
sseqtrrd |
|- ( ph -> R C_ ( U .(+) Q ) ) |