Theorem affineequiv3

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

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

Proof

Step	Hyp	Ref	Expression
1		affineequiv.a	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2		affineequiv.b	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
3		affineequiv.c	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
4		affineequiv.d	⊢ ( 𝜑 → 𝐷 ∈ ℂ )
5		1cnd	⊢ ( 𝜑 → 1 ∈ ℂ )
6	5 4	subcld	⊢ ( 𝜑 → ( 1 − 𝐷 ) ∈ ℂ )
7	6 2	mulcld	⊢ ( 𝜑 → ( ( 1 − 𝐷 ) · 𝐵 ) ∈ ℂ )
8	4 3	mulcld	⊢ ( 𝜑 → ( 𝐷 · 𝐶 ) ∈ ℂ )
9	7 8	addcomd	⊢ ( 𝜑 → ( ( ( 1 − 𝐷 ) · 𝐵 ) + ( 𝐷 · 𝐶 ) ) = ( ( 𝐷 · 𝐶 ) + ( ( 1 − 𝐷 ) · 𝐵 ) ) )
10	9	eqeq2d	⊢ ( 𝜑 → ( 𝐴 = ( ( ( 1 − 𝐷 ) · 𝐵 ) + ( 𝐷 · 𝐶 ) ) ↔ 𝐴 = ( ( 𝐷 · 𝐶 ) + ( ( 1 − 𝐷 ) · 𝐵 ) ) ) )
11	3 1 2 4	affineequiv	⊢ ( 𝜑 → ( 𝐴 = ( ( 𝐷 · 𝐶 ) + ( ( 1 − 𝐷 ) · 𝐵 ) ) ↔ ( 𝐵 − 𝐴 ) = ( 𝐷 · ( 𝐵 − 𝐶 ) ) ) )
12	1 2	negsubdi2d	⊢ ( 𝜑 → - ( 𝐴 − 𝐵 ) = ( 𝐵 − 𝐴 ) )
13	12	eqcomd	⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) = - ( 𝐴 − 𝐵 ) )
14	13	eqeq1d	⊢ ( 𝜑 → ( ( 𝐵 − 𝐴 ) = ( 𝐷 · ( 𝐵 − 𝐶 ) ) ↔ - ( 𝐴 − 𝐵 ) = ( 𝐷 · ( 𝐵 − 𝐶 ) ) ) )
15	3 2	negsubdi2d	⊢ ( 𝜑 → - ( 𝐶 − 𝐵 ) = ( 𝐵 − 𝐶 ) )
16	15	eqcomd	⊢ ( 𝜑 → ( 𝐵 − 𝐶 ) = - ( 𝐶 − 𝐵 ) )
17	16	oveq2d	⊢ ( 𝜑 → ( 𝐷 · ( 𝐵 − 𝐶 ) ) = ( 𝐷 · - ( 𝐶 − 𝐵 ) ) )
18	3 2	subcld	⊢ ( 𝜑 → ( 𝐶 − 𝐵 ) ∈ ℂ )
19	4 18	mulneg2d	⊢ ( 𝜑 → ( 𝐷 · - ( 𝐶 − 𝐵 ) ) = - ( 𝐷 · ( 𝐶 − 𝐵 ) ) )
20	17 19	eqtrd	⊢ ( 𝜑 → ( 𝐷 · ( 𝐵 − 𝐶 ) ) = - ( 𝐷 · ( 𝐶 − 𝐵 ) ) )
21	20	eqeq2d	⊢ ( 𝜑 → ( - ( 𝐴 − 𝐵 ) = ( 𝐷 · ( 𝐵 − 𝐶 ) ) ↔ - ( 𝐴 − 𝐵 ) = - ( 𝐷 · ( 𝐶 − 𝐵 ) ) ) )
22	1 2	subcld	⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) ∈ ℂ )
23	4 18	mulcld	⊢ ( 𝜑 → ( 𝐷 · ( 𝐶 − 𝐵 ) ) ∈ ℂ )
24	22 23	neg11ad	⊢ ( 𝜑 → ( - ( 𝐴 − 𝐵 ) = - ( 𝐷 · ( 𝐶 − 𝐵 ) ) ↔ ( 𝐴 − 𝐵 ) = ( 𝐷 · ( 𝐶 − 𝐵 ) ) ) )
25	14 21 24	3bitrd	⊢ ( 𝜑 → ( ( 𝐵 − 𝐴 ) = ( 𝐷 · ( 𝐵 − 𝐶 ) ) ↔ ( 𝐴 − 𝐵 ) = ( 𝐷 · ( 𝐶 − 𝐵 ) ) ) )
26	10 11 25	3bitrd	⊢ ( 𝜑 → ( 𝐴 = ( ( ( 1 − 𝐷 ) · 𝐵 ) + ( 𝐷 · 𝐶 ) ) ↔ ( 𝐴 − 𝐵 ) = ( 𝐷 · ( 𝐶 − 𝐵 ) ) ) )