Step |
Hyp |
Ref |
Expression |
1 |
|
lsmcv2.v |
|- V = ( Base ` W ) |
2 |
|
lsmcv2.s |
|- S = ( LSubSp ` W ) |
3 |
|
lsmcv2.n |
|- N = ( LSpan ` W ) |
4 |
|
lsmcv2.p |
|- .(+) = ( LSSum ` W ) |
5 |
|
lsmcv2.c |
|- C = (
|
6 |
|
lsmcv2.w |
|- ( ph -> W e. LVec ) |
7 |
|
lsmcv2.u |
|- ( ph -> U e. S ) |
8 |
|
lsmcv2.x |
|- ( ph -> X e. V ) |
9 |
|
lsmcv2.l |
|- ( ph -> -. ( N ` { X } ) C_ U ) |
10 |
|
lveclmod |
|- ( W e. LVec -> W e. LMod ) |
11 |
6 10
|
syl |
|- ( ph -> W e. LMod ) |
12 |
2
|
lsssssubg |
|- ( W e. LMod -> S C_ ( SubGrp ` W ) ) |
13 |
11 12
|
syl |
|- ( ph -> S C_ ( SubGrp ` W ) ) |
14 |
13 7
|
sseldd |
|- ( ph -> U e. ( SubGrp ` W ) ) |
15 |
1 2 3
|
lspsncl |
|- ( ( W e. LMod /\ X e. V ) -> ( N ` { X } ) e. S ) |
16 |
11 8 15
|
syl2anc |
|- ( ph -> ( N ` { X } ) e. S ) |
17 |
13 16
|
sseldd |
|- ( ph -> ( N ` { X } ) e. ( SubGrp ` W ) ) |
18 |
4 14 17
|
lssnle |
|- ( ph -> ( -. ( N ` { X } ) C_ U <-> U C. ( U .(+) ( N ` { X } ) ) ) ) |
19 |
9 18
|
mpbid |
|- ( ph -> U C. ( U .(+) ( N ` { X } ) ) ) |
20 |
|
3simpa |
|- ( ( ph /\ x e. S /\ ( U C. x /\ x C_ ( U .(+) ( N ` { X } ) ) ) ) -> ( ph /\ x e. S ) ) |
21 |
|
simp3l |
|- ( ( ph /\ x e. S /\ ( U C. x /\ x C_ ( U .(+) ( N ` { X } ) ) ) ) -> U C. x ) |
22 |
|
simp3r |
|- ( ( ph /\ x e. S /\ ( U C. x /\ x C_ ( U .(+) ( N ` { X } ) ) ) ) -> x C_ ( U .(+) ( N ` { X } ) ) ) |
23 |
6
|
adantr |
|- ( ( ph /\ x e. S ) -> W e. LVec ) |
24 |
7
|
adantr |
|- ( ( ph /\ x e. S ) -> U e. S ) |
25 |
|
simpr |
|- ( ( ph /\ x e. S ) -> x e. S ) |
26 |
8
|
adantr |
|- ( ( ph /\ x e. S ) -> X e. V ) |
27 |
1 2 3 4 23 24 25 26
|
lsmcv |
|- ( ( ( ph /\ x e. S ) /\ U C. x /\ x C_ ( U .(+) ( N ` { X } ) ) ) -> x = ( U .(+) ( N ` { X } ) ) ) |
28 |
20 21 22 27
|
syl3anc |
|- ( ( ph /\ x e. S /\ ( U C. x /\ x C_ ( U .(+) ( N ` { X } ) ) ) ) -> x = ( U .(+) ( N ` { X } ) ) ) |
29 |
28
|
3exp |
|- ( ph -> ( x e. S -> ( ( U C. x /\ x C_ ( U .(+) ( N ` { X } ) ) ) -> x = ( U .(+) ( N ` { X } ) ) ) ) ) |
30 |
29
|
ralrimiv |
|- ( ph -> A. x e. S ( ( U C. x /\ x C_ ( U .(+) ( N ` { X } ) ) ) -> x = ( U .(+) ( N ` { X } ) ) ) ) |
31 |
2 4
|
lsmcl |
|- ( ( W e. LMod /\ U e. S /\ ( N ` { X } ) e. S ) -> ( U .(+) ( N ` { X } ) ) e. S ) |
32 |
11 7 16 31
|
syl3anc |
|- ( ph -> ( U .(+) ( N ` { X } ) ) e. S ) |
33 |
2 5 6 7 32
|
lcvbr2 |
|- ( ph -> ( U C ( U .(+) ( N ` { X } ) ) <-> ( U C. ( U .(+) ( N ` { X } ) ) /\ A. x e. S ( ( U C. x /\ x C_ ( U .(+) ( N ` { X } ) ) ) -> x = ( U .(+) ( N ` { X } ) ) ) ) ) ) |
34 |
19 30 33
|
mpbir2and |
|- ( ph -> U C ( U .(+) ( N ` { X } ) ) ) |