Metamath Proof Explorer


Theorem affineid

Description: Identity of an affine combination. (Contributed by AV, 2-Feb-2023)

Ref Expression
Hypotheses affineid.f φA
affineid.x φT
Assertion affineid φ1TA+TA=A

Proof

Step Hyp Ref Expression
1 affineid.f φA
2 affineid.x φT
3 1cnd φ1
4 3 2 1 subdird φ1TA=1ATA
5 1 mullidd φ1A=A
6 5 oveq1d φ1ATA=ATA
7 4 6 eqtrd φ1TA=ATA
8 7 oveq1d φ1TA+TA=A-TA+TA
9 2 1 mulcld φTA
10 1 9 npcand φA-TA+TA=A
11 8 10 eqtrd φ1TA+TA=A