| Step |
Hyp |
Ref |
Expression |
| 1 |
|
lcvexch.s |
|- S = ( LSubSp ` W ) |
| 2 |
|
lcvexch.p |
|- .(+) = ( LSSum ` W ) |
| 3 |
|
lcvexch.c |
|- C = (
|
| 4 |
|
lcvexch.w |
|- ( ph -> W e. LMod ) |
| 5 |
|
lcvexch.t |
|- ( ph -> T e. S ) |
| 6 |
|
lcvexch.u |
|- ( ph -> U e. S ) |
| 7 |
|
lcvexch.r |
|- ( ph -> R e. S ) |
| 8 |
|
lcvexch.a |
|- ( ph -> ( T i^i U ) C_ R ) |
| 9 |
|
lcvexch.b |
|- ( ph -> R C_ U ) |
| 10 |
1
|
lsssssubg |
|- ( W e. LMod -> S C_ ( SubGrp ` W ) ) |
| 11 |
4 10
|
syl |
|- ( ph -> S C_ ( SubGrp ` W ) ) |
| 12 |
11 7
|
sseldd |
|- ( ph -> R e. ( SubGrp ` W ) ) |
| 13 |
11 5
|
sseldd |
|- ( ph -> T e. ( SubGrp ` W ) ) |
| 14 |
11 6
|
sseldd |
|- ( ph -> U e. ( SubGrp ` W ) ) |
| 15 |
2
|
lsmmod |
|- ( ( ( R e. ( SubGrp ` W ) /\ T e. ( SubGrp ` W ) /\ U e. ( SubGrp ` W ) ) /\ R C_ U ) -> ( R .(+) ( T i^i U ) ) = ( ( R .(+) T ) i^i U ) ) |
| 16 |
12 13 14 9 15
|
syl31anc |
|- ( ph -> ( R .(+) ( T i^i U ) ) = ( ( R .(+) T ) i^i U ) ) |
| 17 |
1
|
lssincl |
|- ( ( W e. LMod /\ T e. S /\ U e. S ) -> ( T i^i U ) e. S ) |
| 18 |
4 5 6 17
|
syl3anc |
|- ( ph -> ( T i^i U ) e. S ) |
| 19 |
11 18
|
sseldd |
|- ( ph -> ( T i^i U ) e. ( SubGrp ` W ) ) |
| 20 |
2
|
lsmss2 |
|- ( ( R e. ( SubGrp ` W ) /\ ( T i^i U ) e. ( SubGrp ` W ) /\ ( T i^i U ) C_ R ) -> ( R .(+) ( T i^i U ) ) = R ) |
| 21 |
12 19 8 20
|
syl3anc |
|- ( ph -> ( R .(+) ( T i^i U ) ) = R ) |
| 22 |
16 21
|
eqtr3d |
|- ( ph -> ( ( R .(+) T ) i^i U ) = R ) |