Step |
Hyp |
Ref |
Expression |
1 |
|
lsmelpr.v |
|- V = ( Base ` W ) |
2 |
|
lsmelpr.n |
|- N = ( LSpan ` W ) |
3 |
|
lsmelpr.p |
|- .(+) = ( LSSum ` W ) |
4 |
|
lsmelpr.w |
|- ( ph -> W e. LMod ) |
5 |
|
lsmelpr.x |
|- ( ph -> X e. V ) |
6 |
|
lsmelpr.y |
|- ( ph -> Y e. V ) |
7 |
|
lsmelpr.z |
|- ( ph -> Z e. V ) |
8 |
|
eqid |
|- ( LSubSp ` W ) = ( LSubSp ` W ) |
9 |
1 8 2 4 6 7
|
lspprcl |
|- ( ph -> ( N ` { Y , Z } ) e. ( LSubSp ` W ) ) |
10 |
1 8 2 4 9 5
|
lspsnel5 |
|- ( ph -> ( X e. ( N ` { Y , Z } ) <-> ( N ` { X } ) C_ ( N ` { Y , Z } ) ) ) |
11 |
1 2 3 4 6 7
|
lsmpr |
|- ( ph -> ( N ` { Y , Z } ) = ( ( N ` { Y } ) .(+) ( N ` { Z } ) ) ) |
12 |
11
|
sseq2d |
|- ( ph -> ( ( N ` { X } ) C_ ( N ` { Y , Z } ) <-> ( N ` { X } ) C_ ( ( N ` { Y } ) .(+) ( N ` { Z } ) ) ) ) |
13 |
10 12
|
bitrd |
|- ( ph -> ( X e. ( N ` { Y , Z } ) <-> ( N ` { X } ) C_ ( ( N ` { Y } ) .(+) ( N ` { Z } ) ) ) ) |