| 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 |
1
|
lsssssubg |
|- ( W e. LMod -> S C_ ( SubGrp ` W ) ) |
| 8 |
4 7
|
syl |
|- ( ph -> S C_ ( SubGrp ` W ) ) |
| 9 |
8 5
|
sseldd |
|- ( ph -> T e. ( SubGrp ` W ) ) |
| 10 |
8 6
|
sseldd |
|- ( ph -> U e. ( SubGrp ` W ) ) |
| 11 |
2
|
lsmub1 |
|- ( ( T e. ( SubGrp ` W ) /\ U e. ( SubGrp ` W ) ) -> T C_ ( T .(+) U ) ) |
| 12 |
9 10 11
|
syl2anc |
|- ( ph -> T C_ ( T .(+) U ) ) |
| 13 |
|
inss2 |
|- ( T i^i U ) C_ U |
| 14 |
13
|
a1i |
|- ( ph -> ( T i^i U ) C_ U ) |
| 15 |
12 14
|
2thd |
|- ( ph -> ( T C_ ( T .(+) U ) <-> ( T i^i U ) C_ U ) ) |
| 16 |
2
|
lsmss2b |
|- ( ( T e. ( SubGrp ` W ) /\ U e. ( SubGrp ` W ) ) -> ( U C_ T <-> ( T .(+) U ) = T ) ) |
| 17 |
9 10 16
|
syl2anc |
|- ( ph -> ( U C_ T <-> ( T .(+) U ) = T ) ) |
| 18 |
|
eqcom |
|- ( ( T .(+) U ) = T <-> T = ( T .(+) U ) ) |
| 19 |
17 18
|
bitrdi |
|- ( ph -> ( U C_ T <-> T = ( T .(+) U ) ) ) |
| 20 |
|
sseqin2 |
|- ( U C_ T <-> ( T i^i U ) = U ) |
| 21 |
19 20
|
bitr3di |
|- ( ph -> ( T = ( T .(+) U ) <-> ( T i^i U ) = U ) ) |
| 22 |
21
|
necon3bid |
|- ( ph -> ( T =/= ( T .(+) U ) <-> ( T i^i U ) =/= U ) ) |
| 23 |
15 22
|
anbi12d |
|- ( ph -> ( ( T C_ ( T .(+) U ) /\ T =/= ( T .(+) U ) ) <-> ( ( T i^i U ) C_ U /\ ( T i^i U ) =/= U ) ) ) |
| 24 |
|
df-pss |
|- ( T C. ( T .(+) U ) <-> ( T C_ ( T .(+) U ) /\ T =/= ( T .(+) U ) ) ) |
| 25 |
|
df-pss |
|- ( ( T i^i U ) C. U <-> ( ( T i^i U ) C_ U /\ ( T i^i U ) =/= U ) ) |
| 26 |
23 24 25
|
3bitr4g |
|- ( ph -> ( T C. ( T .(+) U ) <-> ( T i^i U ) C. U ) ) |