Description: 0g is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018)
Ref | Expression | ||
---|---|---|---|
Hypotheses | resvbas.1 | ||
resv0g.2 | |||
Assertion | resv0g |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | resvbas.1 | ||
2 | resv0g.2 | ||
3 | eqidd | ||
4 | eqid | ||
5 | 1 4 | resvbas | |
6 | eqid | ||
7 | 1 6 | resvplusg | |
8 | 7 | oveqdr | |
9 | 3 5 8 | grpidpropd | |
10 | 2 9 | syl5eq |