Theorem affineid

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

	Ref	Expression
Hypotheses	affineid.f	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
	affineid.x	⊢ ( 𝜑 → 𝑇 ∈ ℂ )
Assertion	affineid	⊢ ( 𝜑 → ( ( ( 1 − 𝑇 ) · 𝐴 ) + ( 𝑇 · 𝐴 ) ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		affineid.f	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2		affineid.x	⊢ ( 𝜑 → 𝑇 ∈ ℂ )
3		1cnd	⊢ ( 𝜑 → 1 ∈ ℂ )
4	3 2 1	subdird	⊢ ( 𝜑 → ( ( 1 − 𝑇 ) · 𝐴 ) = ( ( 1 · 𝐴 ) − ( 𝑇 · 𝐴 ) ) )
5	1	mulid2d	⊢ ( 𝜑 → ( 1 · 𝐴 ) = 𝐴 )
6	5	oveq1d	⊢ ( 𝜑 → ( ( 1 · 𝐴 ) − ( 𝑇 · 𝐴 ) ) = ( 𝐴 − ( 𝑇 · 𝐴 ) ) )
7	4 6	eqtrd	⊢ ( 𝜑 → ( ( 1 − 𝑇 ) · 𝐴 ) = ( 𝐴 − ( 𝑇 · 𝐴 ) ) )
8	7	oveq1d	⊢ ( 𝜑 → ( ( ( 1 − 𝑇 ) · 𝐴 ) + ( 𝑇 · 𝐴 ) ) = ( ( 𝐴 − ( 𝑇 · 𝐴 ) ) + ( 𝑇 · 𝐴 ) ) )
9	2 1	mulcld	⊢ ( 𝜑 → ( 𝑇 · 𝐴 ) ∈ ℂ )
10	1 9	npcand	⊢ ( 𝜑 → ( ( 𝐴 − ( 𝑇 · 𝐴 ) ) + ( 𝑇 · 𝐴 ) ) = 𝐴 )
11	8 10	eqtrd	⊢ ( 𝜑 → ( ( ( 1 − 𝑇 ) · 𝐴 ) + ( 𝑇 · 𝐴 ) ) = 𝐴 )