Theorem affineid

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

	Ref	Expression
Hypotheses	affineid.f	$$⊢\phi \to A\in ℂ$$
	affineid.x	$$⊢\phi \to T\in ℂ$$
Assertion	affineid	$$⊢\phi \to \left(1-T\right)A+TA=A$$

Proof

Step	Hyp	Ref	Expression
1		affineid.f	$$⊢\phi \to A\in ℂ$$
2		affineid.x	$$⊢\phi \to T\in ℂ$$
3		1cnd	$$⊢\phi \to 1\in ℂ$$
4	3 2 1	subdird	$$⊢\phi \to \left(1-T\right)A=1A-TA$$
5	1	mulid2d	$$⊢\phi \to 1A=A$$
6	5	oveq1d	$$⊢\phi \to 1A-TA=A-TA$$
7	4 6	eqtrd	$$⊢\phi \to \left(1-T\right)A=A-TA$$
8	7	oveq1d	$$⊢\phi \to \left(1-T\right)A+TA=A-TA+TA$$
9	2 1	mulcld	$$⊢\phi \to TA\in ℂ$$
10	1 9	npcand	$$⊢\phi \to A-TA+TA=A$$
11	8 10	eqtrd	$$⊢\phi \to \left(1-T\right)A+TA=A$$