| 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.q |
|- ( ph -> R e. S ) |
| 8 |
|
lcvexch.d |
|- ( ph -> T C_ R ) |
| 9 |
|
lcvexch.e |
|- ( ph -> R C_ ( T .(+) 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 6
|
sseldd |
|- ( ph -> U e. ( SubGrp ` W ) ) |
| 14 |
11 5
|
sseldd |
|- ( ph -> T e. ( SubGrp ` W ) ) |
| 15 |
2
|
lsmmod2 |
|- ( ( ( R e. ( SubGrp ` W ) /\ U e. ( SubGrp ` W ) /\ T e. ( SubGrp ` W ) ) /\ T C_ R ) -> ( R i^i ( U .(+) T ) ) = ( ( R i^i U ) .(+) T ) ) |
| 16 |
12 13 14 8 15
|
syl31anc |
|- ( ph -> ( R i^i ( U .(+) T ) ) = ( ( R i^i U ) .(+) T ) ) |
| 17 |
|
lmodabl |
|- ( W e. LMod -> W e. Abel ) |
| 18 |
4 17
|
syl |
|- ( ph -> W e. Abel ) |
| 19 |
2
|
lsmcom |
|- ( ( W e. Abel /\ T e. ( SubGrp ` W ) /\ U e. ( SubGrp ` W ) ) -> ( T .(+) U ) = ( U .(+) T ) ) |
| 20 |
18 14 13 19
|
syl3anc |
|- ( ph -> ( T .(+) U ) = ( U .(+) T ) ) |
| 21 |
9 20
|
sseqtrd |
|- ( ph -> R C_ ( U .(+) T ) ) |
| 22 |
|
dfss2 |
|- ( R C_ ( U .(+) T ) <-> ( R i^i ( U .(+) T ) ) = R ) |
| 23 |
21 22
|
sylib |
|- ( ph -> ( R i^i ( U .(+) T ) ) = R ) |
| 24 |
16 23
|
eqtr3d |
|- ( ph -> ( ( R i^i U ) .(+) T ) = R ) |