Step |
Hyp |
Ref |
Expression |
1 |
|
lspindp1.v |
|- V = ( Base ` W ) |
2 |
|
lspindp1.o |
|- .0. = ( 0g ` W ) |
3 |
|
lspindp1.n |
|- N = ( LSpan ` W ) |
4 |
|
lspindp1.w |
|- ( ph -> W e. LVec ) |
5 |
|
lspindp1.y |
|- ( ph -> X e. ( V \ { .0. } ) ) |
6 |
|
lspindp1.z |
|- ( ph -> Y e. V ) |
7 |
|
lspindp1.x |
|- ( ph -> Z e. V ) |
8 |
|
lspindp1.q |
|- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) ) |
9 |
|
lspindp1.e |
|- ( ph -> -. Z e. ( N ` { X , Y } ) ) |
10 |
1 2 3 4 5 6 7 8 9
|
lspindp1 |
|- ( ph -> ( ( N ` { Z } ) =/= ( N ` { Y } ) /\ -. X e. ( N ` { Z , Y } ) ) ) |
11 |
10
|
simpld |
|- ( ph -> ( N ` { Z } ) =/= ( N ` { Y } ) ) |
12 |
11
|
necomd |
|- ( ph -> ( N ` { Y } ) =/= ( N ` { Z } ) ) |
13 |
10
|
simprd |
|- ( ph -> -. X e. ( N ` { Z , Y } ) ) |
14 |
|
prcom |
|- { Z , Y } = { Y , Z } |
15 |
14
|
fveq2i |
|- ( N ` { Z , Y } ) = ( N ` { Y , Z } ) |
16 |
15
|
eleq2i |
|- ( X e. ( N ` { Z , Y } ) <-> X e. ( N ` { Y , Z } ) ) |
17 |
13 16
|
sylnib |
|- ( ph -> -. X e. ( N ` { Y , Z } ) ) |
18 |
12 17
|
jca |
|- ( ph -> ( ( N ` { Y } ) =/= ( N ` { Z } ) /\ -. X e. ( N ` { Y , Z } ) ) ) |