Description: Scalar is unaffected by restriction. (Contributed by Mario Carneiro, 7-Dec-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | resssca.1 | |- H = ( G |`s A ) |
|
resssca.2 | |- F = ( Scalar ` G ) |
||
Assertion | resssca | |- ( A e. V -> F = ( Scalar ` H ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | resssca.1 | |- H = ( G |`s A ) |
|
2 | resssca.2 | |- F = ( Scalar ` G ) |
|
3 | df-sca | |- Scalar = Slot 5 |
|
4 | 5nn | |- 5 e. NN |
|
5 | 1lt5 | |- 1 < 5 |
|
6 | 1 2 3 4 5 | resslem | |- ( A e. V -> F = ( Scalar ` H ) ) |