Description: Identity of an affine combination. (Contributed by AV, 2-Feb-2023)
Ref | Expression | ||
---|---|---|---|
Hypotheses | affineid.f | |
|
affineid.x | |
||
Assertion | affineid | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | affineid.f | |
|
2 | affineid.x | |
|
3 | 1cnd | |
|
4 | 3 2 1 | subdird | |
5 | 1 | mullidd | |
6 | 5 | oveq1d | |
7 | 4 6 | eqtrd | |
8 | 7 | oveq1d | |
9 | 2 1 | mulcld | |
10 | 1 9 | npcand | |
11 | 8 10 | eqtrd | |