Description: The inner product is unaffected by restriction. (Contributed by Thierry Arnoux, 16-Jun-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | resssca.1 | |- H = ( G |`s A ) |
|
ressip.2 | |- ., = ( .i ` G ) |
||
Assertion | ressip | |- ( A e. V -> ., = ( .i ` H ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | resssca.1 | |- H = ( G |`s A ) |
|
2 | ressip.2 | |- ., = ( .i ` G ) |
|
3 | df-ip | |- .i = Slot 8 |
|
4 | 8nn | |- 8 e. NN |
|
5 | 1lt8 | |- 1 < 8 |
|
6 | 1 2 3 4 5 | resslem | |- ( A e. V -> ., = ( .i ` H ) ) |