Theorem affineid

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

	Ref	Expression
Hypotheses	affineid.f	|- ( ph -> A e. CC )
	affineid.x	|- ( ph -> T e. CC )
Assertion	affineid	|- ( ph -> ( ( ( 1 - T ) x. A ) + ( T x. A ) ) = A )

Proof

Step	Hyp	Ref	Expression
1		affineid.f	|- ( ph -> A e. CC )
2		affineid.x	|- ( ph -> T e. CC )
3		1cnd	|- ( ph -> 1 e. CC )
4	3 2 1	subdird	|- ( ph -> ( ( 1 - T ) x. A ) = ( ( 1 x. A ) - ( T x. A ) ) )
5	1	mulid2d	|- ( ph -> ( 1 x. A ) = A )
6	5	oveq1d	|- ( ph -> ( ( 1 x. A ) - ( T x. A ) ) = ( A - ( T x. A ) ) )
7	4 6	eqtrd	|- ( ph -> ( ( 1 - T ) x. A ) = ( A - ( T x. A ) ) )
8	7	oveq1d	|- ( ph -> ( ( ( 1 - T ) x. A ) + ( T x. A ) ) = ( ( A - ( T x. A ) ) + ( T x. A ) ) )
9	2 1	mulcld	|- ( ph -> ( T x. A ) e. CC )
10	1 9	npcand	|- ( ph -> ( ( A - ( T x. A ) ) + ( T x. A ) ) = A )
11	8 10	eqtrd	|- ( ph -> ( ( ( 1 - T ) x. A ) + ( T x. A ) ) = A )