Theorem affineequivne

Description: Equivalence between two ways of expressing A as an affine combination of B and C if B and C are not equal. (Contributed by AV, 22-Jan-2023)

	Ref	Expression
Hypotheses	affineequiv.a	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
	affineequiv.b	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
	affineequiv.c	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
	affineequiv.d	⊢ ( 𝜑 → 𝐷 ∈ ℂ )
	affineequivne.d	⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
Assertion	affineequivne	⊢ ( 𝜑 → ( 𝐴 = ( ( ( 1 − 𝐷 ) · 𝐵 ) + ( 𝐷 · 𝐶 ) ) ↔ 𝐷 = ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		affineequiv.a	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2		affineequiv.b	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
3		affineequiv.c	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
4		affineequiv.d	⊢ ( 𝜑 → 𝐷 ∈ ℂ )
5		affineequivne.d	⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
6	1 2 3 4	affineequiv3	⊢ ( 𝜑 → ( 𝐴 = ( ( ( 1 − 𝐷 ) · 𝐵 ) + ( 𝐷 · 𝐶 ) ) ↔ ( 𝐴 − 𝐵 ) = ( 𝐷 · ( 𝐶 − 𝐵 ) ) ) )
7	1 2	subcld	⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) ∈ ℂ )
8	3 2	subcld	⊢ ( 𝜑 → ( 𝐶 − 𝐵 ) ∈ ℂ )
9	5	necomd	⊢ ( 𝜑 → 𝐶 ≠ 𝐵 )
10	3 2 9	subne0d	⊢ ( 𝜑 → ( 𝐶 − 𝐵 ) ≠ 0 )
11	7 4 8 10	divmul3d	⊢ ( 𝜑 → ( ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) = 𝐷 ↔ ( 𝐴 − 𝐵 ) = ( 𝐷 · ( 𝐶 − 𝐵 ) ) ) )
12		eqcom	⊢ ( ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) = 𝐷 ↔ 𝐷 = ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) )
13	11 12	bitr3di	⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) = ( 𝐷 · ( 𝐶 − 𝐵 ) ) ↔ 𝐷 = ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) ) )
14	6 13	bitrd	⊢ ( 𝜑 → ( 𝐴 = ( ( ( 1 − 𝐷 ) · 𝐵 ) + ( 𝐷 · 𝐶 ) ) ↔ 𝐷 = ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐵 ) ) ) )