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 |
|
df-ss |
|- ( 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 ) |