Step |
Hyp |
Ref |
Expression |
1 |
|
lspprat.v |
|- V = ( Base ` W ) |
2 |
|
lspprat.s |
|- S = ( LSubSp ` W ) |
3 |
|
lspprat.n |
|- N = ( LSpan ` W ) |
4 |
|
lspprat.w |
|- ( ph -> W e. LVec ) |
5 |
|
lspprat.u |
|- ( ph -> U e. S ) |
6 |
|
lspprat.x |
|- ( ph -> X e. V ) |
7 |
|
lspprat.y |
|- ( ph -> Y e. V ) |
8 |
|
lspprat.p |
|- ( ph -> U C. ( N ` { X , Y } ) ) |
9 |
|
lsppratlem6.o |
|- .0. = ( 0g ` W ) |
10 |
8
|
adantr |
|- ( ( ph /\ x e. ( U \ { .0. } ) ) -> U C. ( N ` { X , Y } ) ) |
11 |
4
|
adantr |
|- ( ( ph /\ ( x e. ( U \ { .0. } ) /\ y e. ( U \ ( N ` { x } ) ) ) ) -> W e. LVec ) |
12 |
5
|
adantr |
|- ( ( ph /\ ( x e. ( U \ { .0. } ) /\ y e. ( U \ ( N ` { x } ) ) ) ) -> U e. S ) |
13 |
6
|
adantr |
|- ( ( ph /\ ( x e. ( U \ { .0. } ) /\ y e. ( U \ ( N ` { x } ) ) ) ) -> X e. V ) |
14 |
7
|
adantr |
|- ( ( ph /\ ( x e. ( U \ { .0. } ) /\ y e. ( U \ ( N ` { x } ) ) ) ) -> Y e. V ) |
15 |
8
|
adantr |
|- ( ( ph /\ ( x e. ( U \ { .0. } ) /\ y e. ( U \ ( N ` { x } ) ) ) ) -> U C. ( N ` { X , Y } ) ) |
16 |
|
simprl |
|- ( ( ph /\ ( x e. ( U \ { .0. } ) /\ y e. ( U \ ( N ` { x } ) ) ) ) -> x e. ( U \ { .0. } ) ) |
17 |
|
simprr |
|- ( ( ph /\ ( x e. ( U \ { .0. } ) /\ y e. ( U \ ( N ` { x } ) ) ) ) -> y e. ( U \ ( N ` { x } ) ) ) |
18 |
1 2 3 11 12 13 14 15 9 16 17
|
lsppratlem5 |
|- ( ( ph /\ ( x e. ( U \ { .0. } ) /\ y e. ( U \ ( N ` { x } ) ) ) ) -> ( N ` { X , Y } ) C_ U ) |
19 |
|
ssnpss |
|- ( ( N ` { X , Y } ) C_ U -> -. U C. ( N ` { X , Y } ) ) |
20 |
18 19
|
syl |
|- ( ( ph /\ ( x e. ( U \ { .0. } ) /\ y e. ( U \ ( N ` { x } ) ) ) ) -> -. U C. ( N ` { X , Y } ) ) |
21 |
20
|
expr |
|- ( ( ph /\ x e. ( U \ { .0. } ) ) -> ( y e. ( U \ ( N ` { x } ) ) -> -. U C. ( N ` { X , Y } ) ) ) |
22 |
10 21
|
mt2d |
|- ( ( ph /\ x e. ( U \ { .0. } ) ) -> -. y e. ( U \ ( N ` { x } ) ) ) |
23 |
22
|
eq0rdv |
|- ( ( ph /\ x e. ( U \ { .0. } ) ) -> ( U \ ( N ` { x } ) ) = (/) ) |
24 |
|
ssdif0 |
|- ( U C_ ( N ` { x } ) <-> ( U \ ( N ` { x } ) ) = (/) ) |
25 |
23 24
|
sylibr |
|- ( ( ph /\ x e. ( U \ { .0. } ) ) -> U C_ ( N ` { x } ) ) |
26 |
|
lveclmod |
|- ( W e. LVec -> W e. LMod ) |
27 |
4 26
|
syl |
|- ( ph -> W e. LMod ) |
28 |
27
|
adantr |
|- ( ( ph /\ x e. ( U \ { .0. } ) ) -> W e. LMod ) |
29 |
5
|
adantr |
|- ( ( ph /\ x e. ( U \ { .0. } ) ) -> U e. S ) |
30 |
|
eldifi |
|- ( x e. ( U \ { .0. } ) -> x e. U ) |
31 |
30
|
adantl |
|- ( ( ph /\ x e. ( U \ { .0. } ) ) -> x e. U ) |
32 |
2 3 28 29 31
|
lspsnel5a |
|- ( ( ph /\ x e. ( U \ { .0. } ) ) -> ( N ` { x } ) C_ U ) |
33 |
25 32
|
eqssd |
|- ( ( ph /\ x e. ( U \ { .0. } ) ) -> U = ( N ` { x } ) ) |
34 |
33
|
ex |
|- ( ph -> ( x e. ( U \ { .0. } ) -> U = ( N ` { x } ) ) ) |