Description: A vector plus itself is two times the vector. (Contributed by NM, 9-Feb-2008) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | nvdi.1 | |- X = ( BaseSet ` U ) |
|
nvdi.2 | |- G = ( +v ` U ) |
||
nvdi.4 | |- S = ( .sOLD ` U ) |
||
Assertion | nv2 | |- ( ( U e. NrmCVec /\ A e. X ) -> ( A G A ) = ( 2 S A ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nvdi.1 | |- X = ( BaseSet ` U ) |
|
2 | nvdi.2 | |- G = ( +v ` U ) |
|
3 | nvdi.4 | |- S = ( .sOLD ` U ) |
|
4 | eqid | |- ( 1st ` U ) = ( 1st ` U ) |
|
5 | 4 | nvvc | |- ( U e. NrmCVec -> ( 1st ` U ) e. CVecOLD ) |
6 | 2 | vafval | |- G = ( 1st ` ( 1st ` U ) ) |
7 | 3 | smfval | |- S = ( 2nd ` ( 1st ` U ) ) |
8 | 1 2 | bafval | |- X = ran G |
9 | 6 7 8 | vc2OLD | |- ( ( ( 1st ` U ) e. CVecOLD /\ A e. X ) -> ( A G A ) = ( 2 S A ) ) |
10 | 5 9 | sylan | |- ( ( U e. NrmCVec /\ A e. X ) -> ( A G A ) = ( 2 S A ) ) |